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} : (a → b) → List a → List b

Equations

• Chapter1.map₂ x✝ [] = []
• Chapter1.map₂ x✝ (x_2 :: xs) = x✝ x_2 :: Chapter1.map₂ x✝ xs

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 : Nat) : Nat → Nat

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 (Nat × α)

Equations

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

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

Equations

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

def Chapter1.length₂ {a : Type} : List a → Nat

Equations

• Chapter1.length₂ = Chapter1.foldr Chapter1.length₂.succ 0

def Chapter1.length₂.succ {a : Type} : a → (n : Nat) → Nat

Equations

• Chapter1.length₂.succ x✝ n = n + 1

def Chapter1.length₃ {α : Type} : List α → Nat

Equations

• Chapter1.length₃ = Chapter1.foldr (fun (x : α) (n : Nat) => n + 1) 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

instance Chapter1.instReprPoint : Repr Point

Equations

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

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

Equations

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

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.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} : (b → a → b) → b → List a → List b

Equations

• Chapter1.scanl x✝¹ x✝ [] = [x✝]
• Chapter1.scanl x✝¹ x✝ (x_3 :: xs) = x✝ :: Chapter1.scanl x✝¹ (x✝¹ x✝ x_3) 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).val

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).val.head ⋯) :: (Chapter1.scanr₀.aux f q₀ xs).val, ⋯⟩

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

Equations

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

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

Equations

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

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.perm₁ {a : Type} : List a → List (List a)

Equations

• Chapter1.perm₁ [] = [[]]
• Chapter1.perm₁ (x_1 :: xs) = Chapter1.concatMap (fun (x : List a) => Chapter1.inserts x_1 x) (Chapter1.perm₁ xs)

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

Equations

• Chapter1.perm₁' = Chapter1.foldr Chapter1.perm₁'.step [[]]

def Chapter1.perm₁'.step {a : Type} (x : a) (xss : List (List a)) : List (List a)

Equations

• Chapter1.perm₁'.step x xss = Chapter1.concatMap (Chapter1.inserts x) xss

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

Equations

• Chapter1.perm₁'' = Chapter1.foldr (Chapter1.concatMap ∘ Chapter1.inserts) [[]]

def Chapter1.perm₁''' {a : Type} (xs : List a) : List (List a)

Equations

• Chapter1.perm₁''' xs = Chapter1.foldr Chapter1.perm₁'''.step [[]] xs

def Chapter1.perm₁'''.step {a : Type} : a → (b : List (List a)) → List (List a)

Equations

• Chapter1.perm₁'''.step a b = Chapter1.concatMap (Chapter1.inserts a) b

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

Equations

• Chapter1.picks [] = []
• Chapter1.picks (x_1 :: xs) = (x_1, xs) :: List.map (fun (p : a × List a) => (p.fst, x_1 :: p.snd)) (Chapter1.picks xs)

theorem Chapter1.picks_length {a : Type} (xs : List a) (ps : List (a × List a)) : ps = picks xs → (ps.all fun (p : a × List a) => decide (p.snd.length < xs.length)) = true

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

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

@[irreducible]

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

Equations

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

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

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

Equations

• Chapter1.inits [] = [[]]
• Chapter1.inits (x_1 :: xs) = [] :: List.map (fun (ys : List a) => x_1 :: ys) (Chapter1.inits xs)

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

Equations

• Chapter1.tails [] = [[]]
• Chapter1.tails (x_1 :: xs) = (x_1 :: xs) :: Chapter1.tails 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 Int)) : List Int

Equations

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

@[irreducible]

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

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 : Int × List Int) : Int × List Int

Equations

• Chapter1.collapse₂.cat a b = (a.fst + b.fst, a.snd ++ b.snd)

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

Equations

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

def Chapter1.collapse₃.help : Int × (List Int → List Int) → List (Int × List Int) → have tf := List Int → List Int; 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.fst, f ∘ fun (x : List Int) => as.snd ++ x) bs