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 :: xs_2) = some (x, xs_2)

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!" 34 10 "unwrap!: empty list"

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

Equations

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

theorem Chapter1.single_aux {x : Nat} {xs : List Nat} : single (x :: xs) = true ↔ xs = []

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 :: xs_1) res = Chapter1.reverse₀.helper xs_1 (x :: 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 Nat → Nat

Equations

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

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

Equations

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

def Chapter1.fraction : List Nat → Float

Equations

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

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

Equations

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

def Chapter1.apply {a : Type} : Nat → (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} : Nat → (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_1 :: xs_1) = if x = x_1 then xs_1 else x_1 :: Chapter1.remove x xs_1

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

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

Equations

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

def Chapter1.steep₁ : List Nat → Bool

Equations

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

def Chapter1.steep₁.faststeep : List Nat → Nat × 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 Nat → Bool

Equations

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

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

Equations

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

theorem Chapter1.faststeep_sum (xs : List Nat) : (steep₁.faststeep xs).fst = xs.sum

theorem Chapter1.faststeep_bool (xs : List Nat) : (steep₁.faststeep xs).snd = steep₀ xs

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