@[irreducible]

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

partial def Chapter5.Quicksort.qsort₃ {α : Type u_1} [LE α] [DecidableRel fun (x1 x2 : α) => x1 ≤ x2] (y : List α) : List α

partial def Chapter5.Quicksort.qsort₃.help {α : Type u_1} [LE α] [DecidableRel fun (x1 x2 : α) => x1 ≤ x2] (x : α) (ys us vs : List α) : List α

partial def Chapter5.Quicksort.help₄ {α : Type u_1} [LE α] [DecidableRel fun (x1 x2 : α) => x1 ≤ x2] (x : α) (ys us vs : List α) : List α

partial def Chapter5.Quicksort.qsort₄ {α : Type u_1} [LE α] [DecidableRel fun (x1 x2 : α) => x1 ≤ x2] : List α → List α

@[irreducible]

def Chapter5.Quicksort.help₅ {α : Type u_1} [LE α] [DecidableEq α] [DecidableRel LE.le] (t : ℕ) (x : α) (ys us vs : List α) : List α

Equations

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

@[irreducible]

def Chapter5.Quicksort.qsort₅ {α : Type u_1} [LE α] [DecidableEq α] [DecidableRel fun (x1 x2 : α) => x1 ≤ x2] (n : ℕ) (ys : List α) : List α

Equations

• Chapter5.Quicksort.qsort₅ n ys = if n = 0 then ys else if x : ys.length = 0 then [] else match ys, x with | x :: xs, x_1 => Chapter5.Quicksort.help₅ n x xs [] []

@[irreducible]

def Chapter5.T (m n : ℕ) : ℕ

Equations

• Chapter5.T 0 n = 0
• Chapter5.T m 0 = 0
• Chapter5.T m_2.succ n_2.succ = 1 + max (Chapter5.T m_2 (n_2 + 1)) (Chapter5.T (m_2 + 1) n_2)

def Chapter5.expression₁ {α : Type} : List α → List α

Equations

• Chapter5.expression₁ = flip (List.foldl (fun (f : List α → List α) (x : α) => (fun (x_1 : List α) => x :: x_1) ∘ f) id) []

def Chapter5.expression₂ {α : Type} : List α → List α

Equations

• Chapter5.expression₂ = flip (List.foldr (fun (x : α) (f : List α → List α) => f ∘ fun (x_1 : List α) => x :: x_1) id) []

def Chapter5.reverse {α : Type} : List α → List α

Equations

• Chapter5.reverse = List.foldl (flip List.cons) []

structure Chapter5.Card : Type

Exercise 5.11

• suit : Char
• rank : Char

instance Chapter5.instReprCard : Repr Card

Equations

• Chapter5.instReprCard = { reprPrec := Chapter5.instReprCard.repr }

def Chapter5.instReprCard.repr : Card → ℕ → Std.Format

Equations

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

instance Chapter5.instOrdCard : Ord Card

Equations

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

@[irreducible]

def Chapter5.merge₁ {a : Type u_1} (f : a → a → Ordering) : List a → List a → List a

Exercise 5.12

sortBy é uma função de ordenação de listas parametrizada pela função de comparação. Precisamos adaptar merge para então basicamente renomear S52.msort₃ para sortBy parametrizando pela função de comparação.

Como em Haskell, compare é definida para todo tipo instância de Ord. A função compareOn é equivalente a comparing do livro.

Equations

• Chapter5.merge₁ f [] x✝ = x✝
• Chapter5.merge₁ f x✝ [] = x✝
• Chapter5.merge₁ f (x_2 :: xs) (y :: ys) = if f x_2 y = Ordering.lt then x_2 :: Chapter5.merge₁ f xs (y :: ys) else y :: Chapter5.merge₁ f (x_2 :: xs) ys

def Chapter5.sortBy {a : Type} (f : a → a → Ordering) : List a → List a

Equations

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

def Chapter5.sortOn₁ {b : Type u_1} {a : Type} [Ord b] (f : a → b) : List a → List a

Equations

• Chapter5.sortOn₁ f = Chapter5.sortBy (compareOn f)

def Chapter5.sortOn₂ {b a : Type} [Ord b] (f : a → b) (xs : List a) : List a

Equations

• Chapter5.sortOn₂ f xs = List.map Prod.snd (Chapter5.sortBy (compareOn Prod.fst) ((List.map f xs).zip xs))

def Chapter5.sortOn₃ {b a : Type} [Ord b] (f : a → b) : List a → List a

Equations

• Chapter5.sortOn₃ f = List.map Prod.snd ∘ Chapter5.sortBy (compareOn Prod.fst) ∘ List.map fun (x : a) => (f x, x)

def Chapter5.Heapsort.split {a : Type u_1} [Inhabited a] [LE a] [DecidableRel fun (x1 x2 : a) => x1 ≤ x2] : List a → a × List a × List a

Equations

• One or more equations did not get rendered due to their size.
• Chapter5.Heapsort.split [] = (default, [], [])

def Chapter5.Heapsort.split₁ {a : Type u_1} [Inhabited a] [LE a] [DecidableRel fun (x1 x2 : a) => x1 ≤ x2] : List a → a × List a × List a

Nn split₁ the where makes op visible from outside. In split, let is defined only in the second equation of the pattern match. let rec would make op also visible.

If op is not visible, in the split_left_le we would need lift_lets ; intro op

Equations

• Chapter5.Heapsort.split₁ [] = (default, [], [])
• Chapter5.Heapsort.split₁ (y :: xs) = List.foldr Chapter5.Heapsort.split₁.op (y, [], []) xs

def Chapter5.Heapsort.split₁.op {a : Type u_1} [LE a] [DecidableRel fun (x1 x2 : a) => x1 ≤ x2] (x : a) (acc : a × List a × List a) : a × List a × List a

Equations

• Chapter5.Heapsort.split₁.op x acc = if x ≤ acc.1 then (x, acc.1 :: acc.2.2, acc.2.1) else (acc.1, x :: acc.2.2, acc.2.1)

theorem Chapter5.Heapsort.split_left_le {a : Type u_1} [Inhabited a] [LE a] [DecidableRel fun (x1 x2 : a) => x1 ≤ x2] (xs : List a) : (split₁ xs).2.1.length ≤ xs.length

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

@[irreducible]

def Chapter5.Heapsort.mkPair₀ {a : Type} : ℕ → List a → Tree a × List a

Equations

• One or more equations did not get rendered due to their size.
• Chapter5.Heapsort.mkPair₀ x✝ [] = (Chapter5.Heapsort.Tree.null, [])

@[irreducible]

def Chapter5.Heapsort.mkPair {a : Type} : ℕ → List a → Tree a × List a

this is not necessary. Keeping only to preserve the proofs.

Equations

• One or more equations did not get rendered due to their size.
• Chapter5.Heapsort.mkPair x✝ [] = (Chapter5.Heapsort.Tree.null, [])

def Chapter5.Heapsort.mkTree {a : Type} (xs : List a) : Tree a

Equations

• Chapter5.Heapsort.mkTree xs = (Chapter5.Heapsort.mkPair₀ xs.length xs).1

def Chapter5.csort (m : ℕ) (xs : List ℕ) : List ℕ

Equations

• Chapter5.csort m xs = List.flatMap (Function.uncurry List.replicate) (Chapter3.accumArray Nat.add 0 (0, m) (List.map (fun (x : ℕ) => (x, 1)) xs)).toList

def Chapter5.filter {α : Type u_1} : (α → Bool) → List α → List α

Equations

• Chapter5.filter x✝ [] = []
• Chapter5.filter x✝ (x_2 :: xs) = if x✝ x_2 = true then x_2 :: Chapter5.filter x✝ xs else Chapter5.filter x✝ xs

def Chapter5.remove_empty {α : Type u_1} : List (List α) → List (List α)

Equations

• Chapter5.remove_empty [] = []
• Chapter5.remove_empty ([] :: xs) = Chapter5.remove_empty xs
• Chapter5.remove_empty (x_1 :: xs) = x_1 :: Chapter5.remove_empty xs

def Chapter5.string_ptn : (String → Char) → List String → List (List String)

Equations

• One or more equations did not get rendered due to their size.
• Chapter5.string_ptn x✝ [] = []

def Chapter5.lists_concat {α : Type u_1} : List (List α) → List α

Equations

• Chapter5.lists_concat [] = []
• Chapter5.lists_concat (x_1 :: xs) = x_1 ++ Chapter5.lists_concat xs

def Chapter5.string_rsort : List (String → Char) → List String → List String

Equations

• Chapter5.string_rsort x✝ [] = []
• Chapter5.string_rsort [] x✝ = x✝
• Chapter5.string_rsort (f :: fs) x✝ = Chapter5.lists_concat (Chapter5.string_ptn f (Chapter5.string_rsort fs x✝))

def Chapter5.string_incresing_order : ℕ → List (String → Char)

Equations

• Chapter5.string_incresing_order x✝ = List.map (fun (x : ℕ) => flip String.get { byteIdx := x }) (List.range x✝)