def Chapter2.fib : ℕ → ℕ

Equations

• Chapter2.fib 0 = 1
• Chapter2.fib 1 = 1
• Chapter2.fib n.succ.succ = Chapter2.fib (n + 1) + Chapter2.fib n

def Chapter2.fibFast (n : ℕ) : ℕ

Equations

• Chapter2.fibFast n = (Chapter2.fibFast.loop n).2

def Chapter2.fibFast.loop : ℕ → ℕ × ℕ

Equations

• Chapter2.fibFast.loop 0 = (0, 1)
• Chapter2.fibFast.loop n.succ = ((Chapter2.fibFast.loop n).2, (Chapter2.fibFast.loop n).1 + (Chapter2.fibFast.loop n).2)

def Chapter2.append' {a : Type u_1} : List a → List a → Cslib.Algorithms.Lean.TimeM ℕ (List a)

Equations

• Chapter2.append' [] x✝ = pure x✝
• Chapter2.append' (x_2 :: xs) x✝ = do Cslib.Algorithms.Lean.TimeM.tick 1 let __do_lift ← Chapter2.append' xs x✝ pure (x_2 :: __do_lift)

def Chapter2.concat₁' {a : Type u_1} : List (List a) → Cslib.Algorithms.Lean.TimeM ℕ (List a)

Equations

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

def Chapter2.concat₁'' {a : Type u_1} : List (List a) → Cslib.Algorithms.Lean.TimeM ℕ (List a)

Equations

• Chapter2.concat₁'' [] = pure []
• Chapter2.concat₁'' (xs :: xss) = do let res ← Chapter2.concat₁'' xss Cslib.Algorithms.Lean.TimeM.tick xs.length pure (xs ++ res)

theorem Chapter2.concat₁'_time {a : Type u_1} (xss : List (List a)) (n : ℕ) (h : ∀ xs ∈ xss, xs.length = n) : (concat₁' xss).time = xss.length * n

theorem Chapter2.concat₁''_time {a : Type u_1} (xss : List (List a)) (n : ℕ) (h : ∀ xs ∈ xss, xs.length = n) : (concat₁'' xss).time = xss.length * n

def Chapter2.concat₂' {a : Type u_1} : List (List a) → Cslib.Algorithms.Lean.TimeM ℕ (List a)

Equations

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

def Chapter2.concat₂'' {a : Type u_1} : List (List a) → Cslib.Algorithms.Lean.TimeM ℕ (List a) → Cslib.Algorithms.Lean.TimeM ℕ (List a)

Equations

• Chapter2.concat₂'' [] x✝ = x✝
• Chapter2.concat₂'' (xs :: xss) x✝ = do let res ← x✝ Chapter2.concat₂'' xss do Cslib.Algorithms.Lean.TimeM.tick res.length pure (res ++ xs)

theorem Chapter2.concat₂'_time {a : Type u_1} (xss : List (List a)) (n : ℕ) (h : ∀ xs ∈ xss, xs.length = n) : 2 * ↑(concat₂' xss).time = ↑n * ↑xss.length * (↑xss.length - 1)

def Chapter2.build {a : Type u_1} (p : a → a → Bool) : List a → List a

Equations

• Chapter2.build p = List.foldr (Chapter2.build.insert p) []

def Chapter2.build.insert {a : Type u_1} (p : a → a → Bool) (x : a) (xs : List a) : List a

Equations

• Chapter2.build.insert p x xs = x :: Chapter1.dropWhile (p x) xs

def Chapter2.iterate {a : Type u_1} : ℕ → (a → a) → a → List a

Equations

• Chapter2.iterate 0 x✝¹ x✝ = [x✝]
• Chapter2.iterate n.succ x✝¹ x✝ = x✝ :: Chapter2.iterate n x✝¹ (x✝¹ x✝)

def Chapter2.bits (n : ℕ) : List (List Bool)

Equations

• Chapter2.bits n = Chapter2.iterate n Chapter2.bits.inc []

def Chapter2.bits.inc : List Bool → List Bool

Equations

• Chapter2.bits.inc [] = [true]
• Chapter2.bits.inc (false :: bs) = true :: bs
• Chapter2.bits.inc (true :: bs) = false :: Chapter2.bits.inc bs

def Chapter2.init₀ {α : Type u_1} : List α → List α

Equations

• Chapter2.init₀ [] = panicWithPosWithDecl "Fad.Chapter2" "Chapter2.init₀" 176 13 "no elements"
• Chapter2.init₀ [head] = []
• Chapter2.init₀ (x_1 :: xs) = x_1 :: Chapter2.init₀ xs

def Chapter2.init₁ {α : Type u_1} : List α → Option (List α)

Equations

• Chapter2.init₁ [] = none
• Chapter2.init₁ [head] = some []
• Chapter2.init₁ (x_1 :: xs) = match Chapter2.init₁ xs with | none => none | some ys => some (x_1 :: ys)

def Chapter2.init₂ {α : Type u_1} : List α → Option (List α)

Equations

• Chapter2.init₂ [] = none
• Chapter2.init₂ [head] = some []
• Chapter2.init₂ (x_1 :: xs) = do let ys ← Chapter2.init₂ xs pure (x_1 :: ys)

def Chapter2.prune {a : Type u_1} (p : List a → Bool) (xs : List a) : List a

Equations

• Chapter2.prune p xs = List.foldr (Chapter2.prune.cut p) [] xs

def Chapter2.prune.cut {a : Type u_1} (p : List a → Bool) (x : a) (xs : List a) : List a

Equations

• Chapter2.prune.cut p x xs = Chapter1.until' (Chapter2.prune.done p) Chapter2.init₀ (x :: xs)

def Chapter2.prune.done {a : Type u_1} (p : List a → Bool) (xs : List a) : Bool

Equations

• Chapter2.prune.done p xs = decide (xs.isEmpty = true ∨ p xs = true)

def Chapter2.ordered : List ℕ → Bool

Equations

• Chapter2.ordered [] = true
• Chapter2.ordered [head] = true
• Chapter2.ordered (x_1 :: y :: xs) = decide (x_1 ≤ y ∧ Chapter2.ordered (y :: xs) = true)