def List.single {α : Type u_1} (xs : List α) : Bool

Equations

• xs.single = decide (xs.length = 1)

def Chapter3.snoc {a : Type} (x : a) (xs : List a) : List a

Equations

• Chapter3.snoc x xs = xs ++ [x]

@[reducible, inline]

abbrev Chapter3.DoesNotWork.SymList (α : Type u_1) : Type u_1

Equations

• Chapter3.DoesNotWork.SymList α = (List α × List α)

def Chapter3.DoesNotWork.nilSL {α : Type} : SymList α

Equations

• Chapter3.DoesNotWork.nilSL = ([], [])

def Chapter3.DoesNotWork.fromSL {α : Type} (sl : SymList α) : List α

Equations

• Chapter3.DoesNotWork.fromSL sl = sl.1 ++ sl.2.reverse

def Chapter3.DoesNotWork.snocSL {α : Type} : α → SymList α → SymList α

Equations

• Chapter3.DoesNotWork.snocSL x✝ ([], ys) = (ys, [x✝])
• Chapter3.DoesNotWork.snocSL x✝ (bs, ys) = (bs, x✝ :: ys)

def Chapter3.DoesNotWork.consSL {α : Type} : α → SymList α → SymList α

Equations

• Chapter3.DoesNotWork.consSL x✝ (xs, []) = ([x✝], xs)
• Chapter3.DoesNotWork.consSL x✝ (xs, ys) = (x✝ :: xs, ys)

structure Chapter3.SymList (a : Type) : Type

• lhs : List a
• rhs : List a
• ok : (self.lhs.isEmpty = true → self.rhs.isEmpty = true ∨ self.rhs.length = 1) ∧ (self.rhs.isEmpty = true → self.lhs.isEmpty = true ∨ self.lhs.length = 1)

@[implicit_reducible]

instance Chapter3.instReprSymList {a✝ : Type} [Repr a✝] : Repr (SymList a✝)

Equations

• Chapter3.instReprSymList = { reprPrec := Chapter3.instReprSymList.repr }

def Chapter3.instReprSymList.repr {a✝ : Type} [Repr a✝] : SymList a✝ → ℕ → Std.Format

Equations

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

def Chapter3.SymList.nil {a : Type} : SymList a

Equations

• Chapter3.SymList.nil = { lhs := [], rhs := [], ok := ⋯ }

@[implicit_reducible]

instance Chapter3.SymList.instInhabited {a : Type} : Inhabited (SymList a)

Equations

• Chapter3.SymList.instInhabited = { default := Chapter3.SymList.nil }

def Chapter3.SymList.fromSL {a : Type} (sl : SymList a) : List a

Equations

• sl.fromSL = sl.lhs ++ sl.rhs.reverse

def Chapter3.SymList.consSL {a : Type} : a → SymList a → SymList a

Equations

• Chapter3.SymList.consSL x✝ { lhs := xs, rhs := [], ok := h } = { lhs := [x✝], rhs := xs, ok := ⋯ }
• Chapter3.SymList.consSL x✝ { lhs := xs, rhs := y :: ys, ok := h } = { lhs := x✝ :: xs, rhs := y :: ys, ok := ⋯ }

def Chapter3.SymList.snocSL {a : Type} : a → SymList a → SymList a

Equations

• Chapter3.SymList.snocSL x✝ { lhs := [], rhs := bs, ok := ok } = { lhs := bs, rhs := [x✝], ok := ⋯ }
• Chapter3.SymList.snocSL x✝ { lhs := a_1 :: as, rhs := bs, ok := ok } = { lhs := a_1 :: as, rhs := x✝ :: bs, ok := ⋯ }

theorem Chapter3.SymList.cons_fromSL_eq_fromSL_consSL {a : Type} (x : a) : List.cons x ∘ fromSL = fromSL ∘ consSL x

theorem Chapter3.SymList.snoc_fromSL_eq_fromSL_snocSL {a : Type} (x : a) : snoc x ∘ fromSL = fromSL ∘ snocSL x

def Chapter3.SymList.isEmpty {a : Type} (sl : SymList a) : Bool

Equations

• sl.isEmpty = decide (sl.lhs.isEmpty = true ∧ sl.rhs.isEmpty = true)

theorem Chapter3.SymList.fromSL_isEmpty_iff_isEmpty {a : Type} (sl : SymList a) : sl.fromSL.isEmpty = true ↔ sl.isEmpty = true

theorem Chapter3.SymList.fromSL_ne_nil_of_not_isEmpty {a : Type} (sl : SymList a) (h : ¬sl.isEmpty = true) : sl.fromSL ≠ []

def Chapter3.SymList.getLast {a : Type} (sl : SymList a) (ne : ¬sl.isEmpty = true) : a

Equations

• { lhs := xs, rhs := ys, ok := ok }.getLast ne_2 = if h₁ : ys.isEmpty = true then xs.head ⋯ else ys.head ⋯

def Chapter3.SymList.getLast? {a : Type} : SymList a → Option a

Equations

• { lhs := [], rhs := [], ok := ok }.getLast? = none
• { lhs := x_1 :: tail, rhs := [], ok := ok }.getLast? = some x_1
• { lhs := lhs, rhs := y :: tail, ok := ok }.getLast? = some y

theorem Chapter3.SymList.fromSL_getLast_eq_getLast {a : Type} (sl : SymList a) (h : ¬sl.isEmpty = true) : sl.fromSL.getLast ⋯ = sl.getLast h

def List.toSL {a : Type} : List a → Chapter3.SymList a

Equations

• [].toSL = Chapter3.SymList.nil
• (x_1 :: xs).toSL = Chapter3.SymList.consSL x_1 xs.toSL

def Chapter3.SymList.headSL {a : Type} : SymList a → Option a

Equations

• { lhs := [], rhs := [], ok := ok }.headSL = none
• { lhs := [], rhs := y :: tail, ok := ok }.headSL = some y
• { lhs := x_1 :: tail, rhs := rhs, ok := ok }.headSL = some x_1

def Chapter3.SymList.headSL! {a : Type} [Inhabited a] : SymList a → a

Equations

• { lhs := [], rhs := [], ok := ok }.headSL! = panicWithPosWithDecl "Fad.Chapter3" "Chapter3.SymList.headSL!" 177 22 "empty list"
• { lhs := [], rhs := y :: tail, ok := ok }.headSL! = y
• { lhs := x_1 :: tail, rhs := rhs, ok := ok }.headSL! = x_1

def Chapter3.SymList.singleSL {a : Type} (sl : SymList a) : Bool

Equations

• { lhs := as, rhs := [], ok := ok }.singleSL = as.single
• { lhs := [], rhs := bs, ok := ok }.singleSL = bs.single
• { lhs := lhs, rhs := rhs, ok := ok }.singleSL = false

def Chapter3.SymList.lengthSL {a : Type} (sl : SymList a) : ℕ

Equations

• sl.lengthSL = sl.lhs.length + sl.rhs.length

def Chapter3.SymList.splitInTwoSL {a : Type} (xs : List a) : SymList a

Equations

• Chapter3.SymList.splitInTwoSL xs = { lhs := ↑(List.MergeSort.Internal.splitInTwo ⟨xs, ⋯⟩).1, rhs := (↑(List.MergeSort.Internal.splitInTwo ⟨xs, ⋯⟩).2).reverse, ok := ⋯ }

def Chapter3.SymList.tailSL {a : Type} (as : SymList a) : SymList a

Equations

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

theorem Chapter3.SymList.tailSL_eq_tail {a : Type} : fromSL ∘ tailSL = List.tail ∘ fromSL

theorem Chapter3.SymList.lengthSL_splitInTwoSL_eq_length {a : Type} (xs : List a) : (splitInTwoSL xs).lengthSL = xs.length

theorem Chapter3.SymList.length_tail_lt_length {a : Type} (sl : SymList a) (h : sl ≠ nil) : sl.lengthSL > sl.tailSL.lengthSL

theorem Chapter3.SymList.headSL_none_iff_nilSL {a : Type} {sl : SymList a} : sl.headSL = none ↔ sl = nil

theorem Chapter3.SymList.lengthSL_zero_iff_nilSL {a✝ : Type} {sl : SymList a✝} : sl.lengthSL = 0 ↔ sl = nil

@[irreducible]

def Chapter3.SymList.dropWhileSL {a : Type} (p : a → Bool) (sl : SymList a) : SymList a

Equations

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

theorem Chapter3.SymList.head?_fromSL_eq_headSL {a : Type} : List.head? ∘ fromSL = headSL

theorem Chapter3.SymList.fromSL_eq_cons_fromSL_tailSL {a : Type} (sl : SymList a) (x : a) (h : sl.headSL = some x) : sl.fromSL = x :: sl.tailSL.fromSL

theorem Chapter3.SymList.dropWhile_eq_dropWhileSL {a : Type} (p : a → Bool) : List.dropWhile p ∘ fromSL = fromSL ∘ dropWhileSL p

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

Equations

• Chapter3.inits₁ = List.map List.reverse ∘ List.reverse ∘ List.tails ∘ List.reverse

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

Equations

• Chapter3.inits₂ = List.map Chapter3.SymList.fromSL ∘ List.scanl (flip Chapter3.SymList.snocSL) Chapter3.SymList.nil

theorem Chapter3.tails_append_singleton {α : Type u_1} (xs : List α) (x : α) : (xs ++ [x]).tails = List.map (fun (ys : List α) => ys ++ [x]) xs.tails ++ [[]]

theorem Chapter3.map_reverse_tails_snoc {α : Type} (x : α) (xs : List α) : List.map List.reverse (snoc x xs).tails = List.map (fun (ys : List α) => x :: ys.reverse) xs.tails ++ [[]]

theorem Chapter3.map_reverse {α : Type u_1} {β : Type u_2} (f : α → β) (xs : List α) : List.map f xs.reverse = (List.map f xs).reverse

theorem Chapter3.fromSL_snoc {α : Type} (z : α) (sl : SymList α) : (SymList.snocSL z sl).fromSL = sl.fromSL ++ [z]

theorem Chapter3.fromSL_foldl_snocSL {α : Type} (zs : List α) (sl : SymList α) : (List.foldl (flip SymList.snocSL) sl zs).fromSL = sl.fromSL ++ zs

theorem Chapter3.inits_eq {a : Type} (xs : List a) : inits₁ xs = inits₂ xs

def Chapter3.RAList.fetch {a : Type} : ℕ → List a → Option a

Equations

• Chapter3.RAList.fetch x✝ [] = none
• Chapter3.RAList.fetch x✝ (x_2 :: xs) = if x✝ = 0 then some x_2 else Chapter3.RAList.fetch (x✝ - 1) xs

inductive Chapter3.RAList.Tree (α : Type) : Type

• leaf {α : Type} (n : α) : Tree α
• node {α : Type} (n : ℕ) (t₁ t₂ : Tree α) : Tree α

def Chapter3.RAList.instReprTree.repr {α✝ : Type} [Repr α✝] : Tree α✝ → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Chapter3.RAList.instReprTree {α✝ : Type} [Repr α✝] : Repr (Tree α✝)

Equations

• Chapter3.RAList.instReprTree = { reprPrec := Chapter3.RAList.instReprTree.repr }

def Chapter3.RAList.Tree.toString {α : Type} [ToString α] : Tree α → String

Equations

• (Chapter3.RAList.Tree.leaf a).toString = toString "leaf " ++ toString a
• (Chapter3.RAList.Tree.node a a_1 a_2).toString = toString "node " ++ toString a ++ toString " (" ++ toString a_1.toString ++ toString ") (" ++ toString a_2.toString ++ toString ")"

@[implicit_reducible]

instance Chapter3.RAList.instToStringTree {α : Type} [ToString α] : ToString (Tree α)

Equations

• Chapter3.RAList.instToStringTree = { toString := Chapter3.RAList.Tree.toString }

def Chapter3.RAList.Tree.size {a : Type} : Tree a → ℕ

Equations

• (Chapter3.RAList.Tree.leaf a_1).size = 1
• (Chapter3.RAList.Tree.node a_1 a_2 a_3).size = a_1

def Chapter3.RAList.Tree.height {α : Type} : Tree α → ℕ

Equations

• (Chapter3.RAList.Tree.leaf a).height = 1
• (Chapter3.RAList.Tree.node a a_1 a_2).height = 1 + max a_1.height a_2.height

def Chapter3.RAList.Tree.mk {a : Type} (t₁ t₂ : Tree a) : Tree a

Equations

• t₁.mk t₂ = Chapter3.RAList.Tree.node (t₁.size + t₂.size) t₁ t₂

inductive Chapter3.RAList.Digit (a : Type) : Type

• zero {a : Type} : Digit a
• one {a : Type} (t : Tree a) : Digit a

def Chapter3.RAList.instReprDigit.repr {a✝ : Type} [Repr a✝] : Digit a✝ → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Chapter3.RAList.instReprDigit {a✝ : Type} [Repr a✝] : Repr (Digit a✝)

Equations

• Chapter3.RAList.instReprDigit = { reprPrec := Chapter3.RAList.instReprDigit.repr }

def Chapter3.RAList.Digit.toString {α : Type} [ToString α] : Digit α → String

Equations

• Chapter3.RAList.Digit.zero.toString = "zero"
• (Chapter3.RAList.Digit.one a).toString = toString "one (" ++ toString a.toString ++ toString ")"

@[implicit_reducible]

instance Chapter3.RAList.instToStringDigit {α : Type} [ToString α] : ToString (Digit α)

Equations

• Chapter3.RAList.instToStringDigit = { toString := Chapter3.RAList.Digit.toString }

@[reducible, inline]

abbrev Chapter3.RAList (a : Type) : Type

Equations

• Chapter3.RAList a = List (Chapter3.RAList.Digit a)

def Chapter3.concat1 {a : Type} : List (List a) → List a

Equations

• Chapter3.concat1 = List.foldr List.append []

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

Equations

• Chapter3.concatMap f = Chapter3.concat1 ∘ List.map f

def Chapter3.RAList.fromT {a : Type} : Tree a → List a

Equations

• Chapter3.RAList.fromT (Chapter3.RAList.Tree.leaf a_1) = [a_1]
• Chapter3.RAList.fromT (Chapter3.RAList.Tree.node a_1 a_2 a_3) = Chapter3.RAList.fromT a_2 ++ Chapter3.RAList.fromT a_3

def Chapter3.RAList.fromRA {a : Type} : RAList a → List a

Equations

• Chapter3.RAList.fromRA = Chapter3.concatMap Chapter3.RAList.fromRA.frm

def Chapter3.RAList.fromRA.frm {a : Type} : Digit a → List a

Equations

• Chapter3.RAList.fromRA.frm Chapter3.RAList.Digit.zero = []
• Chapter3.RAList.fromRA.frm (Chapter3.RAList.Digit.one a_1) = Chapter3.RAList.fromT a_1

def Chapter3.RAList.fetchT {a : Type} [ToString a] (n : ℕ) (t : Tree a) : Option a

Equations

• Chapter3.RAList.fetchT 0 (Chapter3.RAList.Tree.leaf x) = some x
• Chapter3.RAList.fetchT n (Chapter3.RAList.Tree.node n_2 t₁ t₂) = if n < n_2 / 2 then Chapter3.RAList.fetchT n t₁ else Chapter3.RAList.fetchT (n - n_2 / 2) t₂
• Chapter3.RAList.fetchT n (Chapter3.RAList.Tree.leaf n_2) = none

def Chapter3.RAList.fetchRA {a : Type} [ToString a] (n : ℕ) (ra : RAList a) : Option a

Equations

• Chapter3.RAList.fetchRA n [] = none
• Chapter3.RAList.fetchRA n (Chapter3.RAList.Digit.zero :: xs) = Chapter3.RAList.fetchRA n xs
• Chapter3.RAList.fetchRA n (Chapter3.RAList.Digit.one t :: xs) = if n < t.size then Chapter3.RAList.fetchT n t else Chapter3.RAList.fetchRA (n - t.size) xs

def Chapter3.RAList.nilRA {a : Type} : RAList a

Equations

• Chapter3.RAList.nilRA = []

def Chapter3.RAList.consRA {a : Type} (x : a) (xs : RAList a) : RAList a

Equations

• Chapter3.RAList.consRA x xs = Chapter3.RAList.consRA.consT (Chapter3.RAList.Tree.leaf x) xs

def Chapter3.RAList.consRA.consT {a : Type} : Tree a → RAList a → RAList a

Equations

• Chapter3.RAList.consRA.consT a✝ [] = [Chapter3.RAList.Digit.one a✝]
• Chapter3.RAList.consRA.consT a✝ (Chapter3.RAList.Digit.zero :: xs) = Chapter3.RAList.Digit.one a✝ :: xs
• Chapter3.RAList.consRA.consT a✝ (Chapter3.RAList.Digit.one t2 :: xs) = Chapter3.RAList.Digit.zero :: Chapter3.RAList.consRA.consT (a✝.mk t2) xs

class Chapter3.Ix (α : Type) extends Ord α : Type

• compare : α → α → Ordering
• inRange : α × α → α → Bool
• range : α × α → List α
• index : α × α → α → ℕ
• rangeSize : α × α → ℕ

@[implicit_reducible]

instance Chapter3.instIxNat : Ix ℕ

Equations

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

@[implicit_reducible]

instance Chapter3.instIxChar : Ix Char

Equations

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

def Chapter3.listArray {i e : Type} [Ix i] (bnds : i × i) (xs : List e) : Lean.AssocList i e

Equations

• Chapter3.listArray bnds xs = ((Chapter3.Ix.range bnds).zip xs).toAssocList'

def Chapter3.accumArray₀ {i : Type} {e : Type u_1} {v : Type u_2} [Ix i] [BEq i] (fcmb : e → v → e) (init : e) (bounds : i × i) (pairs : List (i × v)) : Lean.AssocList i e

Equations

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

def Chapter3.accumArray {i e v : Type} [Ix i] [BEq i] (cmb : e → v → e) (init : e) (bounds : i × i) (as : List (i × v)) : Lean.AssocList i e

Equations

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

def Chapter3.assocs {i e : Type} [Ix i] [BEq i] (bounds : i × i) (default : e) (arr : Lean.AssocList i e) : List (i × e)

Equations

• Chapter3.assocs bounds default arr = List.map (fun (i_1 : i) => (i_1, (Lean.AssocList.find? i_1 arr).getD default)) (Chapter3.Ix.range bounds)

def Chapter3.elems {i e : Type} [Ix i] [BEq i] (bnds : i × i) (default : e) (arr : Lean.AssocList i e) : List e

Equations

• Chapter3.elems bnds default arr = List.map Prod.snd (Chapter3.assocs bnds default arr)

def Chapter3.indices {i e : Type} [Ix i] [BEq i] (bnds : i × i) (default : e) (arr : Lean.AssocList i e) : List i

Equations

• Chapter3.indices bnds default arr = List.map Prod.fst (Chapter3.assocs bnds default arr)

def Chapter3.sort (m : ℕ) (xs : List ℕ) : List ℕ

Equations

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