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

Equations

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

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

Equations

• Chapter1.tails [] = [[]]
• Chapter1.tails (x_1 :: xs) = (x_1 :: xs) :: Chapter1.tails xs

def Chapter1.dropWhile {α : Type u_1} (p : α → Bool) (xs : List α) : List α

Equations

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

def Chapter1.uncons {α : Type} (xs : List α) : Option (α × List α)

Equations

• Chapter1.uncons [] = none
• Chapter1.uncons (x_1 :: xs) = some (x_1, xs)

def Chapter1.wrap {α : Type} (a : α) : List α

Equations

• Chapter1.wrap a = [a]

def Chapter1.unwrap {α : Type} (a : List α) : Option α

Equations

• Chapter1.unwrap [x] = some x
• Chapter1.unwrap a = none

def Chapter1.unwrap! {α : Type} [Inhabited α] (a : List α) : α

Equations

• Chapter1.unwrap! [x] = x
• Chapter1.unwrap! x✝ = panicWithPosWithDecl "Fad.«Chapter1-Ex»" "Chapter1.unwrap!" 42 10 "unwrap!: not single list"

def Chapter1.single {α : Type} (a : List α) : Bool

Equations

• Chapter1.single [x] = true
• Chapter1.single a = false

def Chapter1.reverse₀ {α : Type} (a : List α) : List α

Equations

• Chapter1.reverse₀ a = Chapter1.reverse₀.helper a []

def Chapter1.reverse₀.helper {α : Type} (a res : List α) : List α

Equations

• Chapter1.reverse₀.helper [] res = res
• Chapter1.reverse₀.helper (x_1 :: xs) res = Chapter1.reverse₀.helper xs (x_1 :: res)

def Chapter1.reverse₁ {a : Type} : List a → List a

Equations

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

theorem Chapter1.aux_rev_append {α : Type} (as bs : List α) : List.foldl (flip List.cons) as bs = List.foldl (flip List.cons) [] bs ++ as

theorem Chapter1.rev_cons {α✝ : Type} {x : α✝} {xs : List α✝} : reverse₁ (x :: xs) = reverse₁ xs ++ [x]

theorem Chapter1.rev_append {α : Type} (as bs : List α) : reverse₁ (as ++ bs) = reverse₁ bs ++ reverse₁ as

theorem Chapter1.reverse_reverse {α : Type} (xs : List α) : reverse₁ (reverse₁ xs) = xs

def Chapter1.map' {α β : Type} (f : α → β) (xs : List α) : List β

Equations

• Chapter1.map' f xs = List.foldr (fun (x : α) (xs : List β) => f x :: xs) [] xs

def Chapter1.filter' {α : Type} (p : α → Bool) (xs : List α) : List α

Equations

• Chapter1.filter' p xs = List.foldr (fun (x : α) (xs : List α) => if p x = true then x :: xs else xs) [] xs

theorem Chapter1.foldr_filter_aux {α✝ α✝¹ : Type} {f : α✝ → α✝¹ → α✝¹} {e : α✝¹} {p : α✝ → Bool} {ys : List α✝} : (foldr f e ∘ filter p) ys = foldr f e (filter p ys)

def Chapter1.takeWhile {α : Type} (p : α → Bool) : List α → List α

Equations

• Chapter1.takeWhile p = List.foldr (fun (x : α) (acc : List α) => if p x = true then x :: acc else []) []

def Chapter1.dropWhileEnd {α : Type} (p : α → Bool) (xs : List α) : List α

Equations

• Chapter1.dropWhileEnd p xs = List.foldr (fun (x : α) (xs : List α) => if p x = true ∧ xs.isEmpty = true then [] else x :: xs) [] xs

@[irreducible]

def Chapter1.foldr' {a b : Type} [Inhabited a] (f : a → b → b) (e : b) (xs : List a) : b

Equations

• Chapter1.foldr' f e xs = if h : xs.isEmpty = true then e else have this := ⋯; f (xs.head ⋯) (Chapter1.foldr' f e xs.tail)

def Chapter1.last₁ {a : Type} (as : List a) (ok : as ≠ []) : a

Equations

• Chapter1.last₁ as ok = as.reverse.head ⋯

def Chapter1.init₁ {a : Type} : List a → List a

Equations

• Chapter1.init₁ = List.reverse ∘ List.tail ∘ List.reverse

@[irreducible]

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

Equations

• Chapter1.foldl' f e xs = if h : xs.isEmpty = true then e else have this := ⋯; have h₂ := ⋯; f (Chapter1.foldl' f e (Chapter1.init₁ xs)) (Chapter1.last₁ xs h₂)

def Chapter1.integer : List ℕ → ℕ

Equations

• Chapter1.integer = List.foldl Chapter1.integer.shiftl 0

def Chapter1.integer.shiftl (n d : ℕ) : ℕ

Equations

• Chapter1.integer.shiftl n d = 10 * n + d

def Chapter1.fraction : List ℕ → Float

Equations

• Chapter1.fraction = List.foldr Chapter1.fraction.shiftr 0

def Chapter1.fraction.shiftr (d : ℕ) (n : Float) : Float

Equations

• Chapter1.fraction.shiftr d n = (d.toFloat + n) / 10

def Chapter1.apply {a : Type} : ℕ → (a → a) → a → a

Equations

• Chapter1.apply 0 x✝ = id
• Chapter1.apply n.succ x✝ = x✝ ∘ Chapter1.apply n x✝

def Chapter1.apply₁ {a : Type} : ℕ → (a → a) → a → a

Equations

• Chapter1.apply₁ 0 x✝ = id
• Chapter1.apply₁ n.succ x✝ = Chapter1.apply n x✝ ∘ x✝

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

Equations

• Chapter1.inserts₁ x ys = List.foldr (fun (y : a) (yss : List (List a)) => (x :: y :: yss.head!.tail) :: List.map (fun (x : List a) => y :: x) yss) [[x]] ys

def Chapter1.remove {α : Type} [DecidableEq α] (x : α) : List α → List α

Equations

• Chapter1.remove x [] = []
• Chapter1.remove x (x_2 :: xs) = if x = x_2 then xs else x_2 :: Chapter1.remove x xs

partial def Chapter1.perms₃ {α : Type} [DecidableEq α] : List α → List (List α)

def Chapter1.replace (x : ℤ) : ℤ

Equations

• Chapter1.replace x = if Even x then x else 0

def Chapter1.f (x y : ℤ) : ℤ

Equations

• Chapter1.f x y = 2 * x + y

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

theorem Chapter1.replace_of_even {x : ℤ} (h : Even x) : replace x = x

replace é a identidade em todo valor computado por foldr f 0, pois esses valores são sempre pares. -

theorem Chapter1.even_foldr_f (xs : List ℤ) : Even (List.foldr f 0 xs)

theorem Chapter1.replace_foldr_f_eq : replace ∘ List.foldr f 0 = List.foldr f 0

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

Fusion law for foldl.

The intuition mirrors the foldr fusion law: we want to push a post-processing function h inside a foldl, replacing an accumulator of type c by an already-transformed accumulator of type b.

The hypothesis h₁ : ∀ y x, h (f y x) = g (h y) x states that h turns one step of f (taken on the untransformed accumulator) into the corresponding step of g (taken on the transformed accumulator). In other words, h is a step-by-step homomorphism between the two accumulators: the diagram commutes for every element x of the list.

Consequently, applying h to the final result of xs.foldl f e is the same as running xs.foldl g starting from the transformed accumulator h e.

Note the contrast with foldr fusion: since in foldl the accumulator sits on the left, the condition relates h (f y x) to g (h y) x, keeping x on the same side. -

def Chapter1.concat {α : Type} (xss : List (List α)) : List α

Equations

• Chapter1.concat xss = List.foldl (fun (f : List α → List α) (xs ys : List α) => f (xs ++ ys)) id xss []

def Chapter1.steep₀ (xs : List ℕ) : Bool

Equations

• Chapter1.steep₀ [] = true
• Chapter1.steep₀ (x :: xs_2) = decide (x > xs_2.sum ∧ Chapter1.steep₀ xs_2 = true)

def Chapter1.steep₁ : List ℕ → Bool

Equations

• Chapter1.steep₁ = Prod.snd ∘ Chapter1.steep₁.faststeep

def Chapter1.steep₁.faststeep : List ℕ → ℕ × Bool

Equations

• Chapter1.steep₁.faststeep [] = (0, true)
• Chapter1.steep₁.faststeep (x :: xs_1) = match Chapter1.steep₁.faststeep xs_1 with | (s, b) => (x + s, decide (x > s ∧ b = true))

def Chapter1.steep₂ : List ℕ → Bool

Equations

• Chapter1.steep₂ = Prod.snd ∘ Chapter1.steep₂.faststeep

def Chapter1.steep₂.faststeep (xs : List ℕ) : ℕ × Bool

Equations

• Chapter1.steep₂.faststeep xs = List.foldr (fun (x : ℕ) (t : ℕ × Bool) => (x + t.1, decide (x > t.1 ∧ t.2 = true))) (0, true) xs

theorem Chapter1.faststeep_sum (xs : List ℕ) : (steep₁.faststeep xs).1 = xs.sum

theorem Chapter1.faststeep_bool (xs : List ℕ) : (steep₁.faststeep xs).2 = steep₀ xs

theorem Chapter1.steep₀_eq_steep₁ (xs : List ℕ) : steep₀ xs = steep₁ xs