inductive Chapter5.Quicksort.Tree (a : Sort u_1) : Sort (max 1 u_1)

• null {a : Sort u_1} : Tree a
• node {a : Sort u_1} : Tree a → a → Tree a → Tree a

@[irreducible]

def Chapter5.Quicksort.mkTree {a : Type} [h₁ : LT a] [h₂ : DecidableRel fun (x1 x2 : a) => x1 < x2] : List a → Tree a

Equations

• One or more equations did not get rendered due to their size.
• Chapter5.Quicksort.mkTree [] = Chapter5.Quicksort.Tree.null

def Chapter5.Quicksort.Tree.flatten {a : Type} : Tree a → List a

Equations

• Chapter5.Quicksort.Tree.null.flatten = []
• (l.node x_1 r).flatten = l.flatten ++ [x_1] ++ r.flatten

def Chapter5.Quicksort.qsort₀ {a : Type} [h₁ : LT a] [h₂ : DecidableRel fun (x1 x2 : a) => x1 < x2] : List a → List a

Equations

• Chapter5.Quicksort.qsort₀ = Chapter5.Quicksort.Tree.flatten ∘ Chapter5.Quicksort.mkTree

@[irreducible]

def Chapter5.Quicksort.qsort₁ {a : Type} [h₁ : LT a] [h₂ : DecidableRel fun (x1 x2 : a) => x1 < x2] : List a → List a

Equations

• One or more equations did not get rendered due to their size.
• Chapter5.Quicksort.qsort₁ [] = []

@[irreducible]

def Chapter5.Quicksort.qsort₂ {a : Type} [Ord a] (f : a → a → Ordering) : List a → List a

Equations

• One or more equations did not get rendered due to their size.
• Chapter5.Quicksort.qsort₂ f [] = []

inductive Chapter5.Mergesort.Tree (a : Type) : Type

• null {a : Type} : Tree a
• leaf {a : Type} : a → Tree a
• node {a : Type} : Tree a → Tree a → Tree a

def Chapter5.Mergesort.instReprTree.repr {a✝ : Type} [Repr a✝] : Tree a✝ → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

instance Chapter5.Mergesort.instReprTree {a✝ : Type} [Repr a✝] : Repr (Tree a✝)

Equations

• Chapter5.Mergesort.instReprTree = { reprPrec := Chapter5.Mergesort.instReprTree.repr }

instance Chapter5.Mergesort.instInhabitedTree {a✝ : Type} : Inhabited (Tree a✝)

Equations

• Chapter5.Mergesort.instInhabitedTree = { default := Chapter5.Mergesort.instInhabitedTree.default }

def Chapter5.Mergesort.instInhabitedTree.default {a✝ : Type} : Tree a✝

Equations

• Chapter5.Mergesort.instInhabitedTree.default = Chapter5.Mergesort.Tree.null

@[irreducible]

def Chapter5.Mergesort.merge {a : Type} [LE a] [DecidableRel fun (x1 x2 : a) => x1 ≤ x2] : List a → List a → List a

Equations

• Chapter5.Mergesort.merge [] x✝ = x✝
• Chapter5.Mergesort.merge x✝ [] = x✝
• Chapter5.Mergesort.merge (x_2 :: xs) (y :: ys) = if x_2 ≤ y then x_2 :: Chapter5.Mergesort.merge xs (y :: ys) else y :: Chapter5.Mergesort.merge (x_2 :: xs) ys

def Chapter5.Mergesort.Tree.flatten {a : Type} [LE a] [DecidableRel fun (x1 x2 : a) => x1 ≤ x2] : Tree a → List a

Equations

• Chapter5.Mergesort.Tree.null.flatten = []
• (Chapter5.Mergesort.Tree.leaf a_1).flatten = [a_1]
• (a_1.node a_2).flatten = Chapter5.Mergesort.merge a_1.flatten a_2.flatten

def Chapter5.Mergesort.halve₀ {a : Type} (xs : List a) : List a × List a

Equations

• Chapter5.Mergesort.halve₀ xs = (List.take (xs.length / 2) xs, List.drop (xs.length / 2) xs)

def Chapter5.Mergesort.halve {a : Type} : List a → List a × List a

Equations

• Chapter5.Mergesort.halve = List.foldr (fun (x : a) (p : List a × List a) => (p.2, x :: p.1)) ([], [])

def Chapter5.Mergesort.twoStepInduction {a : Type} {P : List a → Prop} (empty : P []) (single : ∀ (as : List a), as.length = 1 → P as) (more : ∀ (a_1 b : a) (as : List a), P as → P (a_1 :: b :: as)) (as : List a) : P as

Equations

• ⋯ = ⋯

theorem Chapter5.Mergesort.length_halve_fst {α✝ : Type} {xs : List α✝} : (halve xs).1.length = xs.length / 2

theorem Chapter5.Mergesort.length_halve_snd {α✝ : Type} {xs : List α✝} : (halve xs).2.length = (xs.length + 1) / 2

@[irreducible]

def Chapter5.Mergesort.mkTree₀ {a : Type} (as : List a) : Tree a

Equations

• One or more equations did not get rendered due to their size.
• Chapter5.Mergesort.mkTree₀ [] = Chapter5.Mergesort.Tree.null

def Chapter5.Mergesort.msort₀ {a : Type} [LE a] [DecidableRel fun (x1 x2 : a) => x1 ≤ x2] (xs : List a) : List a

Equations

• Chapter5.Mergesort.msort₀ xs = (Chapter5.Mergesort.Tree.flatten ∘ Chapter5.Mergesort.mkTree₀) xs

@[irreducible]

def Chapter5.Mergesort.msort₁ {a : Type} [LE a] [DecidableRel fun (x1 x2 : a) => x1 ≤ x2] : List a → List a

Equations

• One or more equations did not get rendered due to their size.
• Chapter5.Mergesort.msort₁ [] = []

@[irreducible]

def Chapter5.Mergesort.mkPair {a : Type} [Inhabited a] (n : ℕ) (xs : List a) : Tree a × List a

Equations

• One or more equations did not get rendered due to their size.

def Chapter5.Mergesort.mkTree₁ {a : Type} [Inhabited a] (as : List a) : Tree a

Equations

• Chapter5.Mergesort.mkTree₁ as = (Chapter5.Mergesort.mkPair as.length as).1

def Chapter5.Mergesort.msort₂ {a : Type} [Inhabited a] [LE a] [DecidableRel fun (x1 x2 : a) => x1 ≤ x2] (xs : List a) : List a

Equations

• Chapter5.Mergesort.msort₂ xs = (Chapter5.Mergesort.Tree.flatten ∘ Chapter5.Mergesort.mkTree₁) xs

def Chapter5.Mergesort.pairWith {a : Type} (f : a → a → a) : List a → List a

Equations

• Chapter5.Mergesort.pairWith f [] = []
• Chapter5.Mergesort.pairWith f [x_1] = [x_1]
• Chapter5.Mergesort.pairWith f (x_1 :: y :: xs) = f x_1 y :: Chapter5.Mergesort.pairWith f xs

def Chapter5.Mergesort.mkTree₂ {a : Type} : List a → Tree a

Equations

• One or more equations did not get rendered due to their size.
• Chapter5.Mergesort.mkTree₂ [] = Chapter5.Mergesort.Tree.null

def Chapter5.Mergesort.msort₃ {a : Type} [LE a] [DecidableRel fun (x1 x2 : a) => x1 ≤ x2] (xs : List a) : List a

Equations

• Chapter5.Mergesort.msort₃ xs = (Chapter5.Mergesort.Tree.flatten ∘ Chapter5.Mergesort.mkTree₂) xs

def Chapter5.Mergesort.msort₄ {a : Type} [LE a] [DecidableRel fun (x1 x2 : a) => x1 ≤ x2] : List a → List a

Equations

• Chapter5.Mergesort.msort₄ [] = []
• Chapter5.Mergesort.msort₄ x✝ = (Chapter1.unwrap (Chapter1.until' Chapter1.single (Chapter5.Mergesort.pairWith Chapter5.Mergesort.merge) (List.map Chapter1.wrap x✝))).getD []

def Chapter5.Mergesort.msort₅ {a : Type} [LE a] [DecidableRel fun (x1 x2 : a) => x1 ≤ x2] : List a → List a

Equations

• One or more equations did not get rendered due to their size.
• Chapter5.Mergesort.msort₅ [] = []

inductive Chapter5.Heapsort.Tree (a : Type) : Type

• null {a : Type} : Tree a
• node {a : Type} : a → Tree a → Tree a → Tree a

def Chapter5.Heapsort.instInhabitedTree.default {a✝ : Type} : Tree a✝

Equations

• Chapter5.Heapsort.instInhabitedTree.default = Chapter5.Heapsort.Tree.null

instance Chapter5.Heapsort.instInhabitedTree {a✝ : Type} : Inhabited (Tree a✝)

Equations

• Chapter5.Heapsort.instInhabitedTree = { default := Chapter5.Heapsort.instInhabitedTree.default }

def Chapter5.Heapsort.flatten {a : Type} [LE a] [DecidableRel fun (x1 x2 : a) => x1 ≤ x2] : Tree a → List a

Equations

• Chapter5.Heapsort.flatten Chapter5.Heapsort.Tree.null = []
• Chapter5.Heapsort.flatten (Chapter5.Heapsort.Tree.node x_1 u v) = x_1 :: Chapter5.Mergesort.merge (Chapter5.Heapsort.flatten u) (Chapter5.Heapsort.flatten v)

def Chapter5.Heapsort.Tree.toFormat {a : Type} [ToString a] (t : Tree a) : Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Chapter5.Heapsort.Tree.null.toFormat = Std.Format.text "."

instance Chapter5.Heapsort.instReprTree {a : Type} [ToString a] : Repr (Tree a)

Equations

• Chapter5.Heapsort.instReprTree = { reprPrec := fun (e : Chapter5.Heapsort.Tree a) (x : ℕ) => e.toFormat }

def Chapter5.Bucketsort.ordered {α β : Type} [BEq β] [LT β] [DecidableRel fun (x1 x2 : β) => x1 < x2] : List (α → β) → α → α → Bool

Equations

• Chapter5.Bucketsort.ordered [] x✝¹ x✝ = true
• Chapter5.Bucketsort.ordered (d :: ds) x✝¹ x✝ = (decide (d x✝¹ < d x✝) || d x✝¹ == d x✝ && Chapter5.Bucketsort.ordered ds x✝¹ x✝)

inductive Chapter5.Bucketsort.Tree (α : Type) : Type

• leaf {α : Type} : α → Tree α
• node {α : Type} : List (Tree α) → Tree α

partial def Chapter5.Bucketsort.instReprTree.repr {α✝ : Type} [Repr α✝] : Tree α✝ → ℕ → Std.Format

instance Chapter5.Bucketsort.instReprTree {α✝ : Type} [Repr α✝] : Repr (Tree α✝)

Equations

• Chapter5.Bucketsort.instReprTree = { reprPrec := Chapter5.Bucketsort.instReprTree.repr }

@[irreducible]

def Chapter5.Bucketsort.Tree.flatten {α : Type} (r : Tree (List α)) : List α

Equations

• (Chapter5.Bucketsort.Tree.leaf v).flatten = v
• (Chapter5.Bucketsort.Tree.node ts).flatten = (List.map Chapter5.Bucketsort.Tree.flatten ts).flatten

def Chapter5.Bucketsort.ptn₀ {α β : Type} [BEq β] (rng : List β) (f : α → β) (xs : List α) : List (List α)

Equations

• Chapter5.Bucketsort.ptn₀ rng f xs = List.map (fun (m : β) => List.filter (fun (x : α) => f x == m) xs) rng

def Chapter5.Bucketsort.mkTree {α β : Type} [BEq β] (rng : List β) (ds : List (α → β)) (xs : List α) : Tree (List α)

Equations

• Chapter5.Bucketsort.mkTree rng [] xs = Chapter5.Bucketsort.Tree.leaf xs
• Chapter5.Bucketsort.mkTree rng (d :: ds') xs = Chapter5.Bucketsort.Tree.node (List.map (Chapter5.Bucketsort.mkTree rng ds') (Chapter5.Bucketsort.ptn₀ rng d xs))

def Chapter5.Bucketsort.bsort₀ {α β : Type} [BEq β] (rng : List β) (ds : List (α → β)) (xs : List α) : List α

Equations

• Chapter5.Bucketsort.bsort₀ rng ds xs = (Chapter5.Bucketsort.mkTree rng ds xs).flatten

def Chapter5.Bucketsort.bsort₁ {α β : Type} [BEq β] (rng : List β) : List (α → β) → List α → List α

Equations

• Chapter5.Bucketsort.bsort₁ rng [] x✝ = x✝
• Chapter5.Bucketsort.bsort₁ rng (d :: ds) x✝ = Chapter1.concatMap (Chapter5.Bucketsort.bsort₁ rng ds) (Chapter5.Bucketsort.ptn₀ rng d x✝)

def Chapter5.Bucketsort.rsort₀ {α β : Type} [BEq β] (rng : List β) : List (α → β) → List α → List α

Equations

• Chapter5.Bucketsort.rsort₀ rng [] x✝ = x✝
• Chapter5.Bucketsort.rsort₀ rng (d :: ds) x✝ = (Chapter5.Bucketsort.ptn₀ rng d (Chapter5.Bucketsort.rsort₀ rng ds x✝)).flatten

def Chapter5.Bucketsort.ptn₁ {a b : Type} (bnds : b × b) [Chapter3.Ix b] [BEq b] (d : a → b) (xs : List a) : List (List a)

Equations

• Chapter5.Bucketsort.ptn₁ bnds d xs = Chapter3.elems bnds default (Chapter3.accumArray (fun (xs : List a) (x : a) => xs ++ [x]) [] bnds ((List.map d xs).zip xs))

def Chapter5.SortingSums.sortsums₀ {a : Type} [Ord a] [Add a] (xs ys : List a) : List a

Equations

• Chapter5.SortingSums.sortsums₀ xs ys = Chapter5.Quicksort.qsort₂ compare (List.flatMap (fun (x : a) => List.map (fun (y : a) => x + y) ys) xs)

@[reducible, inline]

abbrev Chapter5.SortingSums.Label : Type

Equations

• Chapter5.SortingSums.Label = ℕ

@[reducible, inline]

abbrev Chapter5.SortingSums.Pair : Type

Equations

• Chapter5.SortingSums.Pair = (Chapter5.SortingSums.Label × Chapter5.SortingSums.Label)

def Chapter5.SortingSums.subs {a : Type} [Sub a] (xs ys : List (a × Label)) : List (a × Pair)

Equations

• One or more equations did not get rendered due to their size.

def Chapter5.SortingSums.switch {a : Type} [Neg a] : a × Pair → a × Pair

Equations

• Chapter5.SortingSums.switch (x_1, i, j) = (-x_1, j, i)

instance Chapter5.SortingSums.instOrdProdPair {a : Type} [Ord a] : Ord (a × Pair)

Equations

• Chapter5.SortingSums.instOrdProdPair = { compare := fun (p q : a × Chapter5.SortingSums.Pair) => compare p.1 q.1 }

def Chapter5.SortingSums.sortWith {a : Type} [Ord a] [Sub a] (abs : List (a × Pair)) (xis yis : List (a × Label)) : List (a × Pair)

Equations

• One or more equations did not get rendered due to their size.

def Chapter5.SortingSums.sortsubs₁ {a : Type} [Ord a] [Sub a] [Neg a] [OfNat a 0] [LE a] [DecidableRel fun (x1 x2 : a) => x1 ≤ x2] : List (a × Label) → ℕ → List (a × Pair)

Equations

• One or more equations did not get rendered due to their size.
• Chapter5.SortingSums.sortsubs₁ [] x✝ = []
• Chapter5.SortingSums.sortsubs₁ [(fst, i)] x✝ = [(0, i, i)]
• Chapter5.SortingSums.sortsubs₁ x✝ 0 = panicWithPosWithDecl "Fad.Chapter5" "Chapter5.SortingSums.sortsubs₁" 386 25 "never here"

def Chapter5.SortingSums.sortsubs {a : Type} [Ord a] [Sub a] [Neg a] [OfNat a 0] [LE a] [DecidableRel fun (x1 x2 : a) => x1 ≤ x2] (xs ys : List a) : List a

Equations

• One or more equations did not get rendered due to their size.

def Chapter5.SortingSums.sortsums₁ {a : Type} [Ord a] [Sub a] [Neg a] [OfNat a 0] [LE a] [DecidableRel fun (x1 x2 : a) => x1 ≤ x2] (xs ys : List a) : List a

Equations

• Chapter5.SortingSums.sortsums₁ xs ys = Chapter5.SortingSums.sortsubs xs (List.map Neg.neg ys)