Binary Tree

inductive ABTree (α β : Type) : Type

• leaf {α β : Type} (v : α) : ABTree α β
• node {α β : Type} (i : β) (bL bR : ABTree α β) : ABTree α β

def ABTree.sizeI {α β : Type} (sa : α → ℕ) (sb : β → ℕ) : ABTree α β → ℕ

Equations

• ABTree.sizeI sa sb (ABTree.leaf a) = sa a
• ABTree.sizeI sa sb (ABTree.node b bl br) = sb b + ABTree.sizeI sa sb bl + ABTree.sizeI sa sb br

def ABTree.size {α β : Type} : ABTree α β → ℕ

Equations

• ABTree.size = ABTree.sizeI (fun (x : α) => 1) fun (x : β) => 1

def ABTree.height {α β : Type} : ABTree α β → ℕ

Equations

• ABTree.height = ABTree.sizeI (fun (x : α) => 0) fun (x : β) => 1

def ABTree.getI' {α β γ : Type} (p : α → γ) (q : β → γ) : ABTree α β → γ

Equations

• ABTree.getI' p q (ABTree.leaf a) = p a
• ABTree.getI' p q (ABTree.node b bl br) = q b

def ABTree.hget {α : Type} : ABTree α α → α

Equations

• ABTree.hget = ABTree.getI' id id

def ABTree.getI {α β : Type} : ABTree (α × β) β → β

Equations

• ABTree.getI = ABTree.getI' (fun (p : α × β) => p.snd) id

def ABTree.fold {α β γ : Type} (l : α → γ) (n : β → γ → γ → γ) : ABTree α β → γ

Equations

• ABTree.fold l n (ABTree.leaf a) = l a
• ABTree.fold l n (ABTree.node b bl br) = n b (ABTree.fold l n bl) (ABTree.fold l n br)

theorem ABTree.fold_node {α β γ : Type} {l : α → γ} {n : β → γ → γ → γ} (bl br : ABTree α β) (b : β) : fold l n (node b bl br) = n b (fold l n bl) (fold l n br)

def ABTree.map {α₁ α₂ β₁ β₂ : Type} (f : α₁ → α₂) (g : β₁ → β₂) : ABTree α₁ β₁ → ABTree α₂ β₂

Equations

• ABTree.map f g (ABTree.leaf a) = ABTree.leaf (f a)
• ABTree.map f g (ABTree.node b bl br) = ABTree.node (g b) (ABTree.map f g bl) (ABTree.map f g br)

theorem abtree_map_compose {α₁ α₂ α₃ β₁ β₂ β₃ : Type} (f : α₁ → α₂) (f' : α₂ → α₃) (g : β₁ → β₂) (g' : β₂ → β₃) (t : ABTree α₁ β₁) : ABTree.map f' g' (ABTree.map f g t) = ABTree.map (f' ∘ f) (g' ∘ g) t

instance instBifunctorABTree : Bifunctor ABTree

Equations

• instBifunctorABTree = { bimap := fun {α α' β β' : Type} => ABTree.map }

theorem getMapLaw {α β δ γ σ : Type} (f : α → δ) (g : β → γ) (f' : δ → σ) (g' : γ → σ) (t : ABTree α β) : ABTree.getI' f' g' (ABTree.map f g t) = ABTree.getI' (f' ∘ f) (g' ∘ g) t

def abtree_zip_with {α β δ ε ρ η : Type} (f : α → δ → ρ) (g : β → ε → η) (l : ABTree α β) (r : ABTree δ ε) : Option (ABTree ρ η)

Equations

• abtree_zip_with f g (ABTree.leaf a) (ABTree.leaf d) = some (ABTree.leaf (f a d))
• abtree_zip_with f g (ABTree.node b bl br) (ABTree.node e el er) = ABTree.node (g b e) <$> abtree_zip_with f g bl el <*> abtree_zip_with f g br er
• abtree_zip_with f g l r = none

def ABTree.forget {α β : Type} : ABTree α β → ABTree Unit Unit

Equations

• ABTree.forget = ABTree.map (fun (x : α) => ()) fun (x : β) => ()

@[reducible, inline]

abbrev BTree (α : Type) : Type

Equations

• BTree α = ABTree α Unit

def BTree.toAB {α : Type} : BTree α → ABTree α Unit

Equations

• BTree.toAB = id

def BTree.leaf {α : Type} : α → BTree α

Equations

• BTree.leaf = ABTree.leaf

def BTree.node {α : Type} : BTree α → BTree α → BTree α

Equations

• BTree.node = ABTree.node ()

def BTree.map {α β : Type} (f : α → β) : BTree α → BTree β

Equations

• BTree.map f = ABTree.map f id

def BTree.fold {α γ : Type} (l : α → γ) (n : γ → γ → γ) : BTree α → γ

Equations

• BTree.fold l n = ABTree.fold l fun (x : Unit) => n

def BTree.toList {α : Type} : BTree α → List α

Equations

• BTree.toList = BTree.fold List.singleton List.append

theorem abfold_bfold {α γ : Type} (l : α → γ) (n : γ → γ → γ) (t : BTree α) : BTree.fold l n t = ABTree.fold l (fun (_x : Unit) => n) t

instance instFunctorBTree : Functor BTree

Equations

• instFunctorBTree = { map := fun {α β : Type} => BTree.map, mapConst := fun {α β : Type} => BTree.map ∘ Function.const β }

inductive Mem {α : Type} (a : α) : BTree α → Prop

• here {α : Type} {a : α} : Mem a (BTree.leaf a)
• inL {α : Type} {a : α} (br : BTree α) {bl : BTree α} : Mem a bl → Mem a (bl.node br)
• inR {α : Type} {a : α} (bl : BTree α) {br : BTree α} : Mem a br → Mem a (bl.node br)

instance instMembershipBTree {α : Type} : Membership α (BTree α)

Equations

• instMembershipBTree = { mem := fun (t : BTree α) (a : α) => Mem a t }

def pairUp' {α : Type} (acc : Option (BTree α)) (ls : List (BTree α)) : List (BTree α)

Equations

• pairUp' none [] = []
• pairUp' (some a) [] = [a]
• pairUp' none (p :: ps) = pairUp' (some p) ps
• pairUp' (some a) (p :: ps) = a.node p :: pairUp' none ps

theorem pairSize' {α : Type} (ls : List (BTree α)) (p : Option (BTree α)) : (pairUp' p ls).length ≤ ls.length.succ

theorem pairSizeNone {α : Type} (ls : List (BTree α)) : (pairUp' none ls).length ≤ ls.length

def pairUp {α : Type} (ls : List (BTree α)) : List (BTree α)

Equations

• pairUp ls = pairUp' none ls

theorem pairSize {α : Type} (ls : List (BTree α)) : (pairUp ls).length ≤ ls.length

@[irreducible]

def List.fromList' {α : Type} (ls : List (BTree α)) : Option (BTree α)

Equations

• [].fromList' = none
• [x].fromList' = some x
• (x :: y :: rs).fromList' = (pairUp (x :: y :: rs)).fromList'

def List.fromList {α : Type} (ls : List α) : Option (BTree α)

Equations

• ls.fromList = (List.map BTree.leaf ls).fromList'

@[reducible, inline]

abbrev TreePath (α : Type) : Type

Equations

• TreePath α = List (BTree α ⊕ BTree α)

Value Contention

Value Contention Definition

def valueIn {α : Type} [BEq α] (v : α) (bt : BTree α) : Bool

Equations

• valueIn v (ABTree.leaf vb) = (v == vb)
• valueIn v (ABTree.node PUnit.unit l r) = decide (valueIn v l = true ∨ valueIn v r = true)

def valueInProof {α : Type} [BEq α] (v : α) (bt : BTree α) : Option (TreePath α)

Equations

• One or more equations did not get rendered due to their size.
• valueInProof v (ABTree.leaf vb) = if (v == vb) = true then some [] else none

theorem notValue {α : Type} [BEq α] (v : α) (bt : BTree α) : valueIn v bt = false → valueInProof v bt = none

theorem valueInToProof {α : Type} [BEq α] (v : α) (bt : BTree α) : valueIn v bt = true → ∃ (p : TreePath α), valueInProof v bt = some p

theorem valueInProofToValueIn {α : Type} [BEq α] (v : α) (bt : BTree α) (tpath : TreePath α) : valueInProof v bt = some tpath → valueIn v bt = true

theorem ValueInIFFPath {α : Type} [BEq α] (v : α) (bt : BTree α) : valueIn v bt = true ↔ ∃ (p : TreePath α), valueInProof v bt = some p

Utils

def length {α : Type} (bt : BTree α) : ℕ

Equations

• length (ABTree.leaf vb) = 1
• length (ABTree.node PUnit.unit l r) = length l + length r

def toList {α : Type} (bt : BTree α) : List α

Equations

• toList (ABTree.leaf vb) = [vb]
• toList (ABTree.node PUnit.unit l r) = toList l ++ toList r

axiom lengthConcat {α : Type} (l r : List α) : (l ++ r).length = l.length + r.length

theorem sameLength {α : Type} (bt : BTree α) : length bt = (toList bt).length

Tree Building from Paths

def buildTreeN {α : Type} (accumTree : BTree α) (path : TreePath α) : BTree α

Equations

• buildTreeN accumTree [] = accumTree
• buildTreeN accumTree (Sum.inl pl :: ps) = buildTreeN (pl.node accumTree) ps
• buildTreeN accumTree (Sum.inr pr :: ps) = buildTreeN (accumTree.node pr) ps

def buildTree {α : Type} (v : α) (path : TreePath α) : BTree α

Equations

• buildTree v path = buildTreeN (BTree.leaf v) path

@[reducible, inline]

abbrev ABTreeSkeleton : Type

Equations

• ABTreeSkeleton = ABTree Unit Unit

def complete_tree_skeleton (lvl : ℕ) : ABTreeSkeleton

Equations

• complete_tree_skeleton Nat.zero = ABTree.leaf ()
• complete_tree_skeleton plvl.succ = ABTree.node () (complete_tree_skeleton plvl) (complete_tree_skeleton plvl)