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.SL1.SymList (α : Type u) : Type u

Equations

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

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

Equations

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

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

Equations

• Chapter3.SL1.fromSL sl = sl.fst ++ sl.snd.reverse

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

Equations

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

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

Equations

• Chapter3.SL1.consSL x✝ (xs, []) = ([x✝], xs)
• Chapter3.SL1.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)

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

Equations

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

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

Equations

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

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

Equations

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

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 := ok } = { lhs := [x✝], rhs := xs, ok := ⋯ }
• Chapter3.SymList.consSL x✝ { lhs := xs, rhs := y :: ys, ok := ok } = { 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 := ⋯ }

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.sl_empty_l_empty {a : Type} (sl : SymList a) : sl.isEmpty = true → sl.fromSL.isEmpty = true

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

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

Equations

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

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

Equations

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

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!" 225 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

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

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

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, ⋯⟩).fst.val, rhs := (List.MergeSort.Internal.splitInTwo ⟨xs, ⋯⟩).snd.val.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.length_sl_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.

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.scanl_cons {α : Type u_1} {β : Type u_2} (f : β → α → β) (b : β) (a : α) (as : List α) : List.scanl f b (a :: as) = b :: List.scanl f (f b a) as

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

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

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

Equations

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

inductive Chapter3.Tree (α : Type) : Type

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

def Chapter3.Tree.size {a : Type} : Tree a → Nat

Equations

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

def Chapter3.Tree.height {α : Type} : Tree α → Nat

Equations

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

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

Equations

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

inductive Chapter3.Digit (a : Type) : Type

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

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

Equations

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

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

Equations

• One or more equations did not get rendered due to their size.
• Chapter3.instReprDigit.repr Chapter3.Digit.zero prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Chapter3.Digit.zero")).group prec✝

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

Equations

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

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

Equations

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

@[reducible, inline]

abbrev Chapter3.RAList (a : Type) : Type

Equations

• Chapter3.RAList a = List (Chapter3.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.fromT {a : Type} : Tree a → List a

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

• Chapter3.nilRA = []

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

Equations

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

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

Equations

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

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

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

instance Chapter3.instIxNat : Ix Nat

Equations

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

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 : Nat) (xs : List Nat) : List Nat

Equations

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