def Chapter1.map₁ {a : Type u_1} {b : Type u_2} (f : a → b) (xs : List a) : List b

Equations

• Chapter1.map₁ f [] = []
• Chapter1.map₁ f (x :: xs_2) = f x :: Chapter1.map₁ f xs_2

def Chapter1.map {a : Type u_1} {b : Type u_2} (f : a → b) : List a → List b

Equations

• Chapter1.map f [] = []
• Chapter1.map f (x :: xs_1) = f x :: Chapter1.map f xs_1

theorem Chapter1.map_equal {α : Type u_1} {β : Type u_2} (a : List α) (f : α → β) : map f a = List.map f a

def Chapter1.makeInc (n : ℕ) : ℕ → ℕ

Equations

• Chapter1.makeInc n x = x + n

def Chapter1.filter {a : Type} (p : a → Bool) : List a → List a

Equations

• Chapter1.filter p [] = []
• Chapter1.filter p (x_1 :: xs) = if p x_1 = true then x_1 :: Chapter1.filter p xs else Chapter1.filter p xs

def Chapter1.foldr {a b : Type} (f : a → b → b) (e : b) : List a → b

Equations

• Chapter1.foldr f e [] = e
• Chapter1.foldr f e (x_1 :: xs) = f x_1 (Chapter1.foldr f e xs)

def Chapter1.label {α : Type} (xs : List α) : List (ℕ × α)

Equations

• Chapter1.label xs = (List.range xs.length).zip xs

def Chapter1.length₁ {a : Type} (xs : List a) : ℕ

Equations

• Chapter1.length₁ xs = Chapter1.foldr (fun (x : a) (y : ℕ) => y + 1) 0 xs

def Chapter1.length₂ {α : Type} : List α → ℕ

Equations

• Chapter1.length₂ = Chapter1.foldr (fun (x : α) (n : ℕ) => n + 1) 0

def Chapter1.sum (as : List ℕ) : ℕ

Equations

• Chapter1.sum as = Chapter1.foldr Nat.add 0 as

def Chapter1.sum₁ : List ℕ → ℕ

Equations

• Chapter1.sum₁ = Chapter1.foldr Nat.add 0

def Chapter1.foldl {a b : Type} (f : b → a → b) (e : b) : List a → b

Equations

• Chapter1.foldl f e [] = e
• Chapter1.foldl f e (x_1 :: xs) = Chapter1.foldl f (f e x_1) xs

def Chapter1.foldl₀ {a b : Type} (f : b → a → b) (e : b) : List a → b

Equations

• Chapter1.foldl₀ f e = Chapter1.foldr (flip f) e ∘ List.reverse

def Chapter1.foldl₁ {a b : Type} (f : b → a → b) (e : b) (xs : List a) : b

Equations

• Chapter1.foldl₁ f e xs = Chapter1.foldr (flip f) e xs.reverse

structure Chapter1.Point : Type

• x : Float
• y : Float

@[implicit_reducible]

instance Chapter1.instReprPoint : Repr Point

Equations

• Chapter1.instReprPoint = { reprPrec := Chapter1.instReprPoint.repr }

def Chapter1.instReprPoint.repr : Point → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Chapter1.instInhabitedPoint : Inhabited Point

Equations

• Chapter1.instInhabitedPoint = { default := { x := 0, y := 0 } }

def Chapter1.head {α : Type} [Inhabited α] : List α → α

Equations

• Chapter1.head = List.foldr (fun (x x_1 : α) => x) default

def Chapter1.head₁ {α : Type} : List α → Option α

Equations

• Chapter1.head₁ = List.foldr (fun (x : α) (x_1 : Option α) => some x) none

def Chapter1.concat₁ {a : Type} : List (List a) → List a

Equations

• Chapter1.concat₁ = List.foldr List.append []

def Chapter1.concat₂ {a : Type} : List (List a) → List a

Equations

• Chapter1.concat₂ = List.foldl List.append []

def Chapter1.scanl {b : Type u_1} {a : Type u_2} (f : b → a → b) : b → List a → List b

Equations

• Chapter1.scanl f x✝ [] = [x✝]
• Chapter1.scanl f x✝ (x_2 :: xs) = x✝ :: Chapter1.scanl f (f x✝ x_2) xs

def Chapter1.scanr₀ {a b : Type} (f : a → b → b) (q₀ : b) (as : List a) : List b

Equations

• Chapter1.scanr₀ f q₀ as = ↑(Chapter1.scanr₀.aux f q₀ as)

def Chapter1.scanr₀.aux {a b : Type} (f : a → b → b) (q₀ : b) : List a → { l : List b // l ≠ [] }

Equations

• Chapter1.scanr₀.aux f q₀ [] = ⟨[q₀], ⋯⟩
• Chapter1.scanr₀.aux f q₀ (x_1 :: xs) = ⟨f x_1 ((↑(Chapter1.scanr₀.aux f q₀ xs)).head ⋯) :: ↑(Chapter1.scanr₀.aux f q₀ xs), ⋯⟩

def Chapter1.scanr {a : Type u_1} {b : Type u_2} (f : a → b → b) : b → List a → List b

Equations

• Chapter1.scanr f x✝ [] = [x✝]
• Chapter1.scanr f x✝ (x_2 :: xs) = match Chapter1.scanr f x✝ xs with | [] => [] | qs@h:(q :: tail) => f x_2 q :: qs

def Chapter1.inserts {a : Type u_1} (x : a) : List a → List (List a)

Equations

• Chapter1.inserts x [] = [[x]]
• Chapter1.inserts x (x_1 :: xs_1) = (x :: x_1 :: xs_1) :: Chapter1.map (fun (x : List a) => x_1 :: x) (Chapter1.inserts x xs_1)

def Chapter1.concatMap {a : Type u_1} {b : Type} (f : a → List b) : List a → List b

Equations

• Chapter1.concatMap f = Chapter1.concat₁ ∘ List.map f

def Chapter1.perms1₁ {a : Type} : List a → List (List a)

Equations

• Chapter1.perms1₁ [] = [[]]
• Chapter1.perms1₁ (x_1 :: xs) = Chapter1.concat₁ (List.map (fun (x : List a) => Chapter1.inserts x_1 x) (Chapter1.perms1₁ xs))

def Chapter1.perms1₂ {a : Type u_1} : List a → List (List a)

Equations

• Chapter1.perms1₂ [] = [[]]
• Chapter1.perms1₂ (x :: xs_1) = List.flatMap (fun (x_1 : List a) => Chapter1.inserts x x_1) (Chapter1.perms1₂ xs_1)

def Chapter1.perms1₃ {a : Type} : List a → List (List a)

Equations

• Chapter1.perms1₃ = Chapter1.foldr Chapter1.perms1₃.step [[]]

def Chapter1.perms1₃.step {a : Type} (x : a) (as : List (List a)) : List (List a)

Equations

• Chapter1.perms1₃.step x = List.flatMap (Chapter1.inserts x)

def Chapter1.perms1₄ {a : Type} : List a → List (List a)

Equations

• Chapter1.perms1₄ = Chapter1.foldr (List.flatMap ∘ Chapter1.inserts) [[]]

def Chapter1.picks {a : Type u_1} : List a → List (a × List a)

Equations

• Chapter1.picks [] = []
• Chapter1.picks (x :: xs_1) = (x, xs_1) :: List.map (fun (p : a × List a) => (p.1, x :: p.2)) (Chapter1.picks xs_1)

partial def Chapter1.perms2₁ {a : Type} : List a → List (List a)

partial because Lean cannot verify termination: p comes from concatMap with no proof that p ∈ picks xs, so p.2.length < xs.length is unknown.

theorem Chapter1.picks_decreases {a : Type} (xs : List a) (p : a × List a) : p ∈ picks xs → p.2.length < xs.length

@[irreducible]

def Chapter1.perms2₂ {a : Type} : List a → List (List a)

Uses List.attach to pair each element with its membership proof, then pattern-matches on ⟨p, hp⟩ to obtain hp : p ∈ picks xs inline.

Equations

• One or more equations did not get rendered due to their size.
• Chapter1.perms2₂ [] = [[]]

def Chapter1.picks₁ {a : Type u_1} (xs : List a) : List { r : a × List a // r.2.length < xs.length }

Equations

• Chapter1.picks₁ [] = []
• Chapter1.picks₁ (x :: xs_1) = ⟨(x, xs_1), ⋯⟩ :: List.map (fun (r : { r : a × List a // r.2.length < xs_1.length }) => ⟨((↑r).1, x :: (↑r).2), ⋯⟩) (Chapter1.picks₁ xs_1)

@[irreducible]

def Chapter1.perms2₄ {a : Type} : List a → List (List a)

Equations

• One or more equations did not get rendered due to their size.
• Chapter1.perms2₄ [] = [[]]

@[irreducible]

def Chapter1.perms2₅ {a : Type} : List a → List (List a)

Avoids attach by using an explicit helper go that threads the membership proof ∀ p, p ∈ ps → p.2.length < xs.length through the recursion. Requires a lexicographic termination measure (xs.length, ps.length).

Equations

• Chapter1.perms2₅ [] = [[]]
• Chapter1.perms2₅ x✝ = Chapter1.perms2₅.go x✝ (Chapter1.picks x✝) ⋯

@[irreducible]

def Chapter1.perms2₅.go {a : Type} (xs : List a) (ps : List (a × List a)) : (∀ p ∈ ps, p.2.length < xs.length) → List (List a)

Equations

• Chapter1.perms2₅.go xs [] x_2 = []
• Chapter1.perms2₅.go xs (p :: ps_1) h = List.map (fun (x : List a) => p.1 :: x) (Chapter1.perms2₅ p.2) ++ Chapter1.perms2₅.go xs ps_1 ⋯

partial def Chapter1.until' {a : Sort u_1} (p : a → Bool) (f : a → a) (x : a) : a

def Chapter1.while' {a : Sort u_1} (p : a → Bool) (f : a → a) (x : a) : a

Equations

• Chapter1.while' p = Chapter1.until' (not ∘ p)

theorem Chapter1.map_map {α β γ : Type} (f : β → γ) (g : α → β) : List.map f ∘ List.map g = List.map (f ∘ g)

theorem Chapter1.concatMap_map {α β : Type} (f : α → List β) (g : β → α) : concatMap f ∘ List.map g = concatMap (f ∘ g)

theorem Chapter1.foldr_map {α β : Type} (f : α → β → β) (e : β) (g : β → α) : List.foldr f e ∘ List.map g = List.foldr (f ∘ g) e

theorem Chapter1.foldr_fusion {a b c : Type} (f : a → c → c) (e : c) (xs : List a) (g : a → b → b) (h : c → b) (h₁ : ∀ (x : a) (y : c), h (f x y) = g x (h y)) : h (List.foldr f e xs) = List.foldr g (h e) xs

theorem Chapter1.foldl_comp {α β : Type} (y : α) (e : β) (f : β → α → β) : (List.foldl f e ∘ fun (x : List α) => y :: x) = List.foldl f (f e y)

def Chapter1.collapse₀ (xss : List (List ℤ)) : List ℤ

Equations

• Chapter1.collapse₀ xss = Chapter1.collapse₀.help [] xss

@[irreducible]

def Chapter1.collapse₀.help (xs : List ℤ) (xss : List (List ℤ)) : List ℤ

Equations

• Chapter1.collapse₀.help xs xss = if h : xs.sum > 0 ∨ xss.isEmpty = true then xs else have h₁ := ⋯; Chapter1.collapse₀.help (xs.append (xss.head h₁)) xss.tail

def Chapter1.collapse₁ (xss : List (List ℤ)) : List ℤ

Equations

• Chapter1.collapse₁ xss = Chapter1.collapse₁.help [] xss

def Chapter1.collapse₁.help : List ℤ → List (List ℤ) → List ℤ

Equations

• Chapter1.collapse₁.help a✝ [] = a✝
• Chapter1.collapse₁.help a✝ (as :: bss) = if a✝.sum > 0 then a✝ else Chapter1.collapse₁.help (a✝.append as) bss

def Chapter1.collapse₂ (xss : List (List ℤ)) : List ℤ

Equations

• Chapter1.collapse₂ xss = Chapter1.collapse₂.help (0, []) (Chapter1.collapse₂.labelsum xss)

def Chapter1.collapse₂.labelsum (xss : List (List ℤ)) : List (ℤ × List ℤ)

Equations

• Chapter1.collapse₂.labelsum xss = (Chapter1.map List.sum xss).zip xss

def Chapter1.collapse₂.help : ℤ × List ℤ → List (ℤ × List ℤ) → List ℤ

Equations

• Chapter1.collapse₂.help (fst, xs) [] = xs
• Chapter1.collapse₂.help (s, xs) (as :: bss) = if s > 0 then xs else Chapter1.collapse₂.help (Chapter1.collapse₂.cat (s, xs) as) bss

def Chapter1.collapse₂.cat (a b : ℤ × List ℤ) : ℤ × List ℤ

Equations

• Chapter1.collapse₂.cat a b = (a.1 + b.1, a.2 ++ b.2)

def Chapter1.collapse₃ (xss : List (List ℤ)) : List ℤ

Equations

• Chapter1.collapse₃ xss = Chapter1.collapse₃.help (0, id) ((fun (xss : List (List ℤ)) => (Chapter1.map List.sum xss).zip xss) xss) []

def Chapter1.collapse₃.help : ℤ × (List ℤ → List ℤ) → List (ℤ × List ℤ) → have tf := List ℤ → List ℤ; tf

Equations

• Chapter1.collapse₃.help (fst, f) [] = f
• Chapter1.collapse₃.help (s, f) (as :: bs) = if s > 0 then f else Chapter1.collapse₃.help (s + as.1, f ∘ fun (x : List ℤ) => as.2 ++ x) bs