def Chapter4.D1.search₀ (f : Nat → Nat) (t : Nat) : List Nat

Equations

• Chapter4.D1.search₀ f t = List.filter (fun (x : Nat) => decide (t = f x)) (List.range (t + 1))

def Chapter4.D1.search₁ (f : Nat → Nat) (t : Nat) : List Nat

Equations

• Chapter4.D1.search₁ f t = Chapter4.D1.search₁.seek f t (0, t)

def Chapter4.D1.search₁.seek (f : Nat → Nat) (t : Nat) : Nat × Nat → List Nat

Equations

• Chapter4.D1.search₁.seek f t (a, b) = List.filter (fun (x : Nat) => decide (t = f x)) (List.range' a (b - a + 1))

def Chapter4.D1.search₂ (f : Nat → Nat) (t : Nat) : List Nat

Equations

• Chapter4.D1.search₂ f t = Chapter4.D1.search₂.seek f t 0 t

@[irreducible]

def Chapter4.D1.search₂.seek (f : Nat → Nat) (t a b : Nat) : List Nat

Equations

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

def Chapter4.D1.bound (f : Nat → Nat) (t : Nat) : Nat × Nat

Equations

• Chapter4.D1.bound f t = if t ≤ f 0 then (0, 0) else (Chapter4.D1.bound.b f t / 2, Chapter4.D1.bound.b f t)

def Chapter4.D1.bound.b (f : Nat → Nat) (t : Nat) : Nat

Equations

• Chapter4.D1.bound.b f t = Chapter1.until' (Chapter4.D1.bound.done f t) (fun (x : Nat) => x * 2) 1

def Chapter4.D1.bound.done (f : Nat → Nat) (t b : Nat) : Bool

Equations

• Chapter4.D1.bound.done f t b = decide (t ≤ f b)

@[irreducible]

def Chapter4.D1.smallest (f : Nat → Nat) (t : Nat) (p : Nat × Nat) : Nat

Equations

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

def Chapter4.D1.search₃ (f : Nat → Nat) (t : Nat) : List Nat

Equations

• Chapter4.D1.search₃ f t = if f (Chapter4.D1.search₃.x f t) = t then [Chapter4.D1.search₃.x f t] else []

def Chapter4.D1.search₃.x (f : Nat → Nat) (t : Nat) : Nat

Equations

• Chapter4.D1.search₃.x f t = Chapter4.D1.smallest f t (Chapter4.D1.bound f t)

def Chapter4.D2.search₀ (f : Nat × Nat → Nat) (t : Nat) : List (Nat × Nat)

Equations

• Chapter4.D2.search₀ f t = List.filter (fun (p : Nat × Nat) => decide (t = f p)) (Chapter4.D2.search₀.ps t)

def Chapter4.D2.search₀.as (t : Nat) : List Nat

Equations

• Chapter4.D2.search₀.as t = List.range (t + 1)

def Chapter4.D2.search₀.ps (t : Nat) : List (Nat × Nat)

Equations

• Chapter4.D2.search₀.ps t = Chapter1.concatMap (fun (x : Nat) => List.map (fun (y : Nat) => (x, y)) (Chapter4.D2.search₀.as t)) (Chapter4.D2.search₀.as t)

def Chapter4.D2.search₁ (f : Nat × Nat → Nat) (t : Nat) : List (Nat × Nat)

Equations

• Chapter4.D2.search₁ f t = Chapter4.D2.search₁.searchIn f t 0 t []

@[irreducible]

def Chapter4.D2.search₁.searchIn (f : Nat × Nat → Nat) (t x y : Nat) (sofar : List (Nat × Nat)) : List (Nat × Nat)

Equations

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

partial def Chapter4.D2.helper (t : Nat) (f : Nat × Nat → Nat) : Nat × Nat → Nat × Nat → List (Nat × Nat)

def Chapter4.D2.search₂ (f : Nat × Nat → Nat) (t : Nat) : List (Nat × Nat)

Equations

• Chapter4.D2.search₂ f t = Chapter4.D2.helper t f (0, Chapter4.D1.smallest (fun (y : Nat) => f (0, y)) t (0, t)) (Chapter4.D1.smallest (fun (x : Nat) => f (x, 0)) t (0, t), 0)

def Chapter4.D2.scale (a : Array Int) (c : Int) : Array Int

Equations

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

def Chapter4.D2.myhead₁ {a : Type u_1} (xs : List a) (h : xs.length ≠ 0) : a

Equations

• Chapter4.D2.myhead₁ [] h_2 = absurd ⋯ h_2
• Chapter4.D2.myhead₁ (x :: tail) h_2 = x

def Chapter4.D2.myhead₂ {a : Type u_1} (xs : List a) (h : xs.length ≠ 0) : a

Equations

• Chapter4.D2.myhead₂ (x :: tail) x_1 = x

inductive Chapter4.BST1.Tree (α : Type) : Type

• null {α : Type} : Tree α
• node {α : Type} : Tree α → α → Tree α → Tree α

instance Chapter4.BST1.instInhabitedTree {a✝ : Type} : Inhabited (Tree a✝)

Equations

• Chapter4.BST1.instInhabitedTree = { default := Chapter4.BST1.instInhabitedTree.default }

def Chapter4.BST1.instInhabitedTree.default {a✝ : Type} : Tree a✝

Equations

• Chapter4.BST1.instInhabitedTree.default = Chapter4.BST1.Tree.null

def Chapter4.BST1.Tree.toFormat {α : Type} [ToString α] (t : Tree α) : Std.Format

Equations

• Chapter4.BST1.Tree.null.toFormat = Std.Format.text "."
• (t₁.node x_1 t₂).toFormat = Std.Format.bracket "(" (Std.format x_1 ++ Std.Format.line ++ Std.Format.nest 2 t₁.toFormat ++ Std.Format.line ++ Std.Format.nest 2 t₂.toFormat) ")"

instance Chapter4.BST1.instReprTreeOfToString {α : Type} [ToString α] : Repr (Tree α)

Equations

• Chapter4.BST1.instReprTreeOfToString = { reprPrec := fun (e : Chapter4.BST1.Tree α) (x : Nat) => e.toFormat }

def Chapter4.BST1.Tree.size {α : Type} : Tree α → Nat

Equations

• Chapter4.BST1.Tree.null.size = 0
• (t₁.node x_1 t₂).size = 1 + t₁.size + t₂.size

def Chapter4.BST1.Tree.flatten {α : Type} : Tree α → List α

Equations

• Chapter4.BST1.Tree.null.flatten = []
• (t₁.node x_1 t₂).flatten = t₁.flatten ++ [x_1] ++ t₂.flatten

def Chapter4.BST1.search (f : Nat → Nat) : Nat → Tree Nat → Option Nat

Equations

• Chapter4.BST1.search f x✝ Chapter4.BST1.Tree.null = none
• Chapter4.BST1.search f x✝ (l.node x_2 r) = if f x_2 < x✝ then Chapter4.BST1.search f x✝ r else if f x_2 = x✝ then some x_2 else Chapter4.BST1.search f x✝ l

def Chapter4.BST1.Tree.height {α : Type} : Tree α → Nat

Equations

• Chapter4.BST1.Tree.null.height = 0
• (t₁.node x_1 t₂).height = 1 + max t₁.height t₂.height

@[irreducible]

def Chapter4.BST1.mkTree {α : Type} [LT α] [DecidableRel fun (x1 x2 : α) => x1 < x2] : List α → Tree α

Equations

• One or more equations did not get rendered due to their size.
• Chapter4.BST1.mkTree [] = Chapter4.BST1.Tree.null

inductive Chapter4.BST2.Tree (a : Type) : Type

• null {a : Type} : Tree a
• node {a : Type} : Nat → Tree a → a → Tree a → Tree a

instance Chapter4.BST2.instNonemptyTree {a✝ : Type} : Nonempty (Tree a✝)

def Chapter4.BST2.instInhabitedTree.default {a✝ : Type} : Tree a✝

Equations

• Chapter4.BST2.instInhabitedTree.default = Chapter4.BST2.Tree.null

instance Chapter4.BST2.instInhabitedTree {a✝ : Type} : Inhabited (Tree a✝)

Equations

• Chapter4.BST2.instInhabitedTree = { default := Chapter4.BST2.instInhabitedTree.default }

def Chapter4.BST2.Tree.toFormat {a : Type} [ToString a] (t : Tree a) : Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Chapter4.BST2.Tree.null.toFormat = Std.Format.text "."

instance Chapter4.BST2.instReprTreeOfToString {a : Type} [ToString a] : Repr (Tree a)

Equations

• Chapter4.BST2.instReprTreeOfToString = { reprPrec := fun (e : Chapter4.BST2.Tree a) (x : Nat) => e.toFormat }

def Chapter4.BST2.Tree.height {a : Type} : Tree a → Nat

Equations

• Chapter4.BST2.Tree.null.height = 0
• (Chapter4.BST2.Tree.node a_1 t₁ x_1 t₂).height = a_1

def Chapter4.BST2.Tree.flatten {a : Type} : Tree a → List a

Equations

• Chapter4.BST2.Tree.null.flatten = []
• (Chapter4.BST2.Tree.node a_1 t₁ x_1 t₂).flatten = t₁.flatten ++ [x_1] ++ t₂.flatten

def Chapter4.BST2.node {a : Type} (l : Tree a) (x : a) (r : Tree a) : Tree a

Equations

• Chapter4.BST2.node l x r = Chapter4.BST2.Tree.node (Chapter4.BST2.node.h l r) l x r

def Chapter4.BST2.node.h {a : Type} (l r : Tree a) : Nat

Equations

• Chapter4.BST2.node.h l r = 1 + max l.height r.height

def Chapter4.BST2.bias {a : Type} : Tree a → Int

Equations

• Chapter4.BST2.bias Chapter4.BST2.Tree.null = 0
• Chapter4.BST2.bias (Chapter4.BST2.Tree.node a_1 t₁ x_1 t₂) = ↑t₁.height - ↑t₂.height

def Chapter4.BST2.rotr {a : Type} : Tree a → Tree a

Equations

• Chapter4.BST2.rotr Chapter4.BST2.Tree.null = Chapter4.BST2.Tree.null
• Chapter4.BST2.rotr (Chapter4.BST2.Tree.node a_1 (Chapter4.BST2.Tree.node a_2 ll y rl) x_1 r) = Chapter4.BST2.node ll y (Chapter4.BST2.node rl x_1 r)
• Chapter4.BST2.rotr (Chapter4.BST2.Tree.node a_1 Chapter4.BST2.Tree.null a_2 a_3) = Chapter4.BST2.Tree.null

def Chapter4.BST2.rotl {a : Type} : Tree a → Tree a

Equations

• Chapter4.BST2.rotl Chapter4.BST2.Tree.null = Chapter4.BST2.Tree.null
• Chapter4.BST2.rotl (Chapter4.BST2.Tree.node a_1 ll y (Chapter4.BST2.Tree.node a_2 lrl z rrl)) = Chapter4.BST2.node (Chapter4.BST2.node ll y lrl) z rrl
• Chapter4.BST2.rotl (Chapter4.BST2.Tree.node a_1 a_2 a_3 Chapter4.BST2.Tree.null) = Chapter4.BST2.Tree.null

def Chapter4.BST2.balance {a : Type} (t1 : Tree a) (x : a) (t2 : Tree a) : Tree a

Equations

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

def Chapter4.BST2.balance.h1 {a : Type} (t1 : Tree a) : Nat

Equations

• Chapter4.BST2.balance.h1 t1 = t1.height

def Chapter4.BST2.balance.h2 {a : Type} (t2 : Tree a) : Nat

Equations

• Chapter4.BST2.balance.h2 t2 = t2.height

def Chapter4.BST2.balance.rotateR {a : Type} (t1 : Tree a) (x : a) (t2 : Tree a) : Tree a

Equations

• Chapter4.BST2.balance.rotateR t1 x t2 = if 0 ≤ Chapter4.BST2.bias t1 then Chapter4.BST2.rotr (Chapter4.BST2.node t1 x t2) else Chapter4.BST2.rotr (Chapter4.BST2.node (Chapter4.BST2.rotl t1) x t2)

def Chapter4.BST2.balance.rotateL {a : Type} (t1 : Tree a) (x : a) (t2 : Tree a) : Tree a

Equations

• Chapter4.BST2.balance.rotateL t1 x t2 = if Chapter4.BST2.bias t2 ≤ 0 then Chapter4.BST2.rotl (Chapter4.BST2.node t1 x t2) else Chapter4.BST2.rotl (Chapter4.BST2.node t1 x (Chapter4.BST2.rotr t2))

def Chapter4.BST2.insert {a : Type} [LT a] [DecidableRel fun (x1 x2 : a) => x1 < x2] (x : a) : Tree a → Tree a

Equations

• One or more equations did not get rendered due to their size.
• Chapter4.BST2.insert x✝ Chapter4.BST2.Tree.null = Chapter4.BST2.node Chapter4.BST2.Tree.null x✝ Chapter4.BST2.Tree.null

def Chapter4.BST2.mkTree {a : Type} [LT a] [DecidableRel fun (x1 x2 : a) => x1 < x2] (xs : List a) : Tree a

Equations

• Chapter4.BST2.mkTree = List.foldr Chapter4.BST2.insert Chapter4.BST2.Tree.null

def Chapter4.BST2.balanceR {a : Type} (t₁ : Tree a) (x : a) (t₂ : Tree a) : Tree a

Equations

• One or more equations did not get rendered due to their size.
• Chapter4.BST2.balanceR Chapter4.BST2.Tree.null x t₂ = Chapter4.BST2.Tree.null

def Chapter4.BST2.balanceL {a : Type} (t₁ : Tree a) (x : a) (t₂ : Tree a) : Tree a

Equations

• One or more equations did not get rendered due to their size.
• Chapter4.BST2.balanceL t₁ x Chapter4.BST2.Tree.null = Chapter4.BST2.Tree.null

def Chapter4.BST2.gbalance {a : Type} (t₁ : Tree a) (x : a) (t₂ : Tree a) : Tree a

Equations

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

def Chapter4.BST2.insert₁ {a : Type} [LT a] [DecidableRel fun (x1 x2 : a) => x1 < x2] (x : a) : Tree a → Tree a

Equations

• One or more equations did not get rendered due to their size.
• Chapter4.BST2.insert₁ x✝ Chapter4.BST2.Tree.null = Chapter4.BST2.node Chapter4.BST2.Tree.null x✝ Chapter4.BST2.Tree.null

def Chapter4.BST2.mkTree₁ {a : Type} [LT a] [DecidableRel fun (x1 x2 : a) => x1 < x2] : List a → Tree a

Equations

• Chapter4.BST2.mkTree₁ = List.foldr Chapter4.BST2.insert₁ Chapter4.BST2.Tree.null

def Chapter4.BST2.insert₂ {a b : Type} [Ord b] (key : a → b) (x : a) : Tree a → Tree a

Equations

• One or more equations did not get rendered due to their size.
• Chapter4.BST2.insert₂ key x✝ Chapter4.BST2.Tree.null = Chapter4.BST2.node Chapter4.BST2.Tree.null x✝ Chapter4.BST2.Tree.null

def Chapter4.BST2.mkTree₂ {a b : Type} [Ord b] (key : a → b) : List a → Tree a

Equations

• Chapter4.BST2.mkTree₂ key = List.foldr (Chapter4.BST2.insert₂ key) Chapter4.BST2.Tree.null

instance Chapter4.BST2.instOrdProdNat_fad : Ord (Nat × Nat)

Equations

• Chapter4.BST2.instOrdProdNat_fad = { compare := fun (a b : Nat × Nat) => match compare a.fst b.fst with | Ordering.eq => compare a.snd b.snd | x => x }

def Chapter4.BST2.sort {a : Type} [LT a] [DecidableRel fun (x1 x2 : a) => x1 < x2] : List a → List a

Equations

• Chapter4.BST2.sort = Chapter4.BST2.Tree.flatten ∘ Chapter4.BST2.mkTree₁

def Chapter4.BST2.search {a b : Type} [Ord b] (key : a → b) (k : b) : Tree a → Option a

Equations

• One or more equations did not get rendered due to their size.
• Chapter4.BST2.search key k Chapter4.BST2.Tree.null = none

@[reducible, inline]

abbrev Chapter4.DSet.Set (a : Type) : Type

Equations

• Chapter4.DSet.Set a = Chapter4.BST2.Tree a

def Chapter4.DSet.member {a : Type} [LT a] [DecidableRel fun (x1 x2 : a) => x1 < x2] (x : a) : Set a → Bool

Equations

• Chapter4.DSet.member x Chapter4.BST2.Tree.null = false
• Chapter4.DSet.member x (Chapter4.BST2.Tree.node a_1 l y r) = if x < y then Chapter4.DSet.member x l else if x > y then Chapter4.DSet.member x r else true

inductive Chapter4.DSet.Piece (α : Type) : Type

• lp {α : Type} : Set α → α → Piece α
• rp {α : Type} : α → Set α → Piece α

@[simp]

theorem Chapter4.DSet.flatten_left_lt {α : Type} {t : BST2.Tree α} {h : Nat} {l r : BST2.Tree α} {x : α} (ht : t = BST2.Tree.node h l x r) : t.flatten.length > l.flatten.length

@[irreducible]

def Chapter4.DSet.deleteMin {α : Type} (t : Set α) (ht : t ≠ BST2.Tree.null) : α × Set α

Equations

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

def Chapter4.DSet.combine {a : Type} [LT a] [DecidableRel fun (x1 x2 : a) => x1 < x2] : Set a → Set a → Set a

Equations

• Chapter4.DSet.combine Chapter4.BST2.Tree.null x✝ = x✝
• Chapter4.DSet.combine x✝ Chapter4.BST2.Tree.null = x✝
• Chapter4.DSet.combine x Chapter4.BST2.Tree.null = x
• Chapter4.DSet.combine x✝ (Chapter4.BST2.Tree.node a_1 b c d) = match Chapter4.DSet.deleteMin (Chapter4.BST2.Tree.node a_1 b c d) ⋯ with | (x, t) => Chapter4.BST2.balance x✝ x t

def Chapter4.DSet.delete {a : Type} [LT a] [DecidableRel fun (x1 x2 : a) => x1 < x2] [DecidableEq a] : a → Set a → Set a

Equations

• One or more equations did not get rendered due to their size.
• Chapter4.DSet.delete x✝ Chapter4.BST2.Tree.null = Chapter4.BST2.Tree.null

def Chapter4.DSet.pieces {α : Type} [LT α] [DecidableRel fun (x1 x2 : α) => x1 < x2] : α → Set α → List (Piece α)

Equations

• Chapter4.DSet.pieces x✝¹ x✝ = Chapter4.DSet.pieces.addPiece x✝¹ x✝ []

def Chapter4.DSet.pieces.addPiece {α : Type} [LT α] [DecidableRel fun (x1 x2 : α) => x1 < x2] (x : α) : Set α → List (Piece α) → List (Piece α)

Equations

• One or more equations did not get rendered due to their size.
• Chapter4.DSet.pieces.addPiece x Chapter4.BST2.Tree.null x✝ = x✝

def Chapter4.DSet.sew {α : Type} : List (Piece α) → Set α × Set α

Equations

• Chapter4.DSet.sew = List.foldl Chapter4.DSet.sew.step (Chapter4.BST2.Tree.null, Chapter4.BST2.Tree.null)

def Chapter4.DSet.sew.step {α : Type} : Set α × Set α → Piece α → Set α × Set α

Equations

• Chapter4.DSet.sew.step (t1, t2) (Chapter4.DSet.Piece.lp t x_2) = (Chapter4.BST2.gbalance t x_2 t1, t2)
• Chapter4.DSet.sew.step (t1, t2) (Chapter4.DSet.Piece.rp x_2 t) = (t1, Chapter4.BST2.gbalance t2 x_2 t)

def Chapter4.DSet.split {α : Type} [LT α] [DecidableRel fun (x1 x2 : α) => x1 < x2] : α → Set α → Set α × Set α

Equations

• Chapter4.DSet.split x t = Chapter4.DSet.sew (Chapter4.DSet.pieces x t)