# Binary Search Trees

If the type of keys can be totally ordered -- that is, it supports a well-behaved `≤` comparison -- then maps can be implemented with binary search trees (BSTs). Insert and lookup operations on BSTs take time proportional to the height of the tree. If the tree is balanced, the operations therefore take logarithmic time.

This example is based on a similar example found in the "Sofware Foundations" book (volume 3).

We use `Nat` as the key type in our implementation of BSTs, since it has a convenient total order with lots of theorems and automation available. We leave as an exercise to the reader the generalization to arbitrary types.

```inductive Tree: Type v → Type vTree (β: Type vβ : Type v: Type (v + 1)Type v) where
| leaf: {β : Type v} → Tree βleaf
| node: {β : Type v} → Tree β → Nat → β → Tree β → Tree βnode (left: Tree βleft : Tree: Type v → Type vTree β: Type vβ) (key: Natkey : Nat: TypeNat) (value: βvalue : β: Type vβ) (right: Tree βright : Tree: Type v → Type vTree β: Type vβ)
deriving Repr: Type u → Type uRepr```

The function `contains` returns `true` iff the given tree contains the key `k`.

```def Tree.contains: {β : Type u_1} → Tree β → Nat → BoolTree.contains (t: Tree βt : Tree: Type u_1 → Type u_1Tree β: Type u_1β) (k: Natk : Nat: TypeNat) : Bool: TypeBool :=
match t: Tree βt with
| leaf: {β : Type ?u.1670} → Tree βleaf => false: Boolfalse
| node: {β : Type ?u.1679} → Tree β → Nat → β → Tree β → Tree βnode left: Tree βleft key: Natkey value: βvalueWarning: unused variable `value` [linter.unusedVariables] right: Tree βright =>
if k: Natk < key: Natkey then
left: Tree βleft.contains: {β : Type u_1} → Tree β → Nat → Boolcontains k: Natk
else if key: Natkey < k: Natk then
right: Tree βright.contains: {β : Type u_1} → Tree β → Nat → Boolcontains k: Natk
else
true: Booltrue```

`t.find? k` returns `some v` if `v` is the value bound to key `k` in the tree `t`. It returns `none` otherwise.

```def Tree.find?: {β : Type u_1} → Tree β → Nat → Option βTree.find? (t: Tree βt : Tree: Type u_1 → Type u_1Tree β: Type u_1β) (k: Natk : Nat: TypeNat) : Option: Type u_1 → Type u_1Option β: Type u_1β :=
match t: Tree βt with
| leaf: {β : Type ?u.2126} → Tree βleaf => none: {α : Type u_1} → Option αnone
| node: {β : Type ?u.2138} → Tree β → Nat → β → Tree β → Tree βnode left: Tree βleft key: Natkey value: βvalue right: Tree βright =>
if k: Natk < key: Natkey then
left: Tree βleft.find?: {β : Type u_1} → Tree β → Nat → Option βfind? k: Natk
else if key: Natkey < k: Natk then
right: Tree βright.find?: {β : Type u_1} → Tree β → Nat → Option βfind? k: Natk
else
some: {α : Type u_1} → α → Option αsome value: βvalue```

`t.insert k v` is the map containing all the bindings of `t` along with a binding of `k` to `v`.

```def Tree.insert: {β : Type u_1} → Tree β → Nat → β → Tree βTree.insert (t: Tree βt : Tree: Type u_1 → Type u_1Tree β: Type u_1β) (k: Natk : Nat: TypeNat) (v: βv : β: Type u_1β) : Tree: Type u_1 → Type u_1Tree β: Type u_1β :=
match t: Tree βt with
| leaf: {β : Type ?u.2591} → Tree βleaf => node: {β : Type u_1} → Tree β → Nat → β → Tree β → Tree βnode leaf: {β : Type u_1} → Tree βleaf k: Natk v: βv leaf: {β : Type u_1} → Tree βleaf
| node: {β : Type ?u.2606} → Tree β → Nat → β → Tree β → Tree βnode left: Tree βleft key: Natkey value: βvalue right: Tree βright =>
if k: Natk < key: Natkey then
node: {β : Type u_1} → Tree β → Nat → β → Tree β → Tree βnode (left: Tree βleft.insert: {β : Type u_1} → Tree β → Nat → β → Tree βinsert k: Natk v: βv) key: Natkey value: βvalue right: Tree βright
else if key: Natkey < k: Natk then
node: {β : Type u_1} → Tree β → Nat → β → Tree β → Tree βnode left: Tree βleft key: Natkey value: βvalue (right: Tree βright.insert: {β : Type u_1} → Tree β → Nat → β → Tree βinsert k: Natk v: βv)
else
node: {β : Type u_1} → Tree β → Nat → β → Tree β → Tree βnode left: Tree βleft k: Natk v: βv right: Tree βright```

Let's add a new operation to our tree: converting it to an association list that contains the key--value bindings from the tree stored as pairs. If that list is sorted by the keys, then any two trees that represent the same map would be converted to the same list. Here's a function that does so with an in-order traversal of the tree.

```def Tree.toList: {β : Type u_1} → Tree β → List (Nat × β)Tree.toList (t: Tree βt : Tree: Type u_1 → Type u_1Tree β: Type u_1β) : List: Type u_1 → Type u_1List (Nat: TypeNat × β: Type u_1β) :=
match t: Tree βt with
| leaf: {β : Type ?u.3092} → Tree βleaf => []: List (Nat × β)[]
| node: {β : Type ?u.3104} → Tree β → Nat → β → Tree β → Tree βnode l: Tree βl k: Natk v: βv r: Tree βr => l: Tree βl.toList: {β : Type u_1} → Tree β → List (Nat × β)toList ++ [(k: Natk, v: βv)] ++ r: Tree βr.toList: {β : Type u_1} → Tree β → List (Nat × β)toList

#evalTree.node (Tree.node (Tree.leaf) 1 "one" (Tree.leaf)) 2 "two" (Tree.node (Tree.leaf) 3 "three" (Tree.leaf))
Tree.leaf: {β : Type} → Tree βTree.leaf.insert: {β : Type} → Tree β → Nat → β → Tree βinsert 2: Nat2 "two": String"two"
|>.insert: {β : Type} → Tree β → Nat → β → Tree βinsert 3: Nat3 "three": String"three"
|>.insert: {β : Type} → Tree β → Nat → β → Tree βinsert 1: Nat1 "one": String"one"

#eval[(1, "one"), (2, "two"), (3, "three")]
Tree.leaf: {β : Type} → Tree βTree.leaf.insert: {β : Type} → Tree β → Nat → β → Tree βinsert 2: Nat2 "two": String"two"
|>.insert: {β : Type} → Tree β → Nat → β → Tree βinsert 3: Nat3 "three": String"three"
|>.insert: {β : Type} → Tree β → Nat → β → Tree βinsert 1: Nat1 "one": String"one"
|>.toList: {β : Type} → Tree β → List (Nat × β)toList```

The implemention of `Tree.toList` is inefficient because of how it uses the `++` operator. On a balanced tree its running time is linearithmic, because it does a linear number of concatentations at each level of the tree. On an unbalanced tree it's quadratic time. Here's a tail-recursive implementation than runs in linear time, regardless of whether the tree is balanced:

```def Tree.toListTR: {β : Type u_1} → Tree β → List (Nat × β)Tree.toListTR (t: Tree βt : Tree: Type u_1 → Type u_1Tree β: Type u_1β) : List: Type u_1 → Type u_1List (Nat: TypeNat × β: Type u_1β) :=
go: Tree β → List (Nat × β) → List (Nat × β)go t: Tree βt []: List (Nat × β)[]
where
go: Tree β → List (Nat × β) → List (Nat × β)go (t: Tree βt : Tree: Type u_1 → Type u_1Tree β: Type u_1β) (acc: List (Nat × β)acc : List: Type u_1 → Type u_1List (Nat: TypeNat × β: Type u_1β)) : List: Type u_1 → Type u_1List (Nat: TypeNat × β: Type u_1β) :=
match t: Tree βt with
| leaf: {β : Type ?u.9384} → Tree βleaf => acc: List (Nat × β)acc
| node: {β : Type ?u.9394} → Tree β → Nat → β → Tree β → Tree βnode l: Tree βl k: Natk v: βv r: Tree βr => go: Tree β → List (Nat × β) → List (Nat × β)go l: Tree βl ((k: Natk, v: βv) :: go: Tree β → List (Nat × β) → List (Nat × β)go r: Tree βr acc: List (Nat × β)acc)```

We now prove that `t.toList` and `t.toListTR` return the same list. The proof is on induction, and as we used the auxiliary function `go` to define `Tree.toListTR`, we use the auxiliary theorem `go` to prove the theorem.

The proof of the auxiliary theorem is by induction on `t`. The `generalizing acc` modifier instructs Lean to revert `acc`, apply the induction theorem for `Tree`s, and then reintroduce `acc` in each case. By using `generalizing`, we obtain the more general induction hypotheses

• `left_ih : ∀ acc, toListTR.go left acc = toList left ++ acc`

• `right_ih : ∀ acc, toListTR.go right acc = toList right ++ acc`

Recall that the combinator `tac <;> tac'` runs `tac` on the main goal and `tac'` on each produced goal, concatenating all goals produced by `tac'`. In this theorem, we use it to apply `simp` and close each subgoal produced by the `induction` tactic.

The `simp` parameters `toListTR.go` and `toList` instruct the simplifier to try to reduce and/or apply auto generated equation theorems for these two functions. The parameter `*` intructs the simplifier to use any equation in a goal as rewriting rules. In this particular case, `simp` uses the induction hypotheses as rewriting rules. Finally, the parameter `List.append_assoc` intructs the simplifier to use the `List.append_assoc` theorem as a rewriting rule.

```theorem Tree.toList_eq_toListTR: ∀ {β : Type u_1} (t : Tree β), toList t = toListTR tTree.toList_eq_toListTR (t: Tree βt : Tree: Type u_1 → Type u_1Tree β: Type u_1β)
: t: Tree βt.toList: {β : Type u_1} → Tree β → List (Nat × β)toList = t: Tree βt.toListTR: {β : Type u_1} → Tree β → List (Nat × β)toListTR := byGoals accomplished! 🐙
simp [toListTR: {β : Type ?u.10768} → Tree β → List (Nat × β)toListTR, go: ∀ (t : Tree β) (acc : List (Nat × β)), toListTR.go t acc = toList t ++ accgo t: Tree βt []: List (Nat × β)[]]Goals accomplished! 🐙
where
go: ∀ {β : Type u_1} (t : Tree β) (acc : List (Nat × β)), toListTR.go t acc = toList t ++ accgo (t: Tree βt : Tree: Type u_1 → Type u_1Tree β: Type u_1β) (acc: List (Nat × β)acc : List: Type u_1 → Type u_1List (Nat: TypeNat × β: Type u_1β))
: toListTR.go: {β : Type u_1} → Tree β → List (Nat × β) → List (Nat × β)toListTR.go t: Tree βt acc: List (Nat × β)acc = t: Tree βt.toList: {β : Type u_1} → Tree β → List (Nat × β)toList ++ acc: List (Nat × β)acc := byGoals accomplished! 🐙
induction t: Tree βt generalizing acc: List (Nat × β)accβ: Type u_1t: Tree βacc: List (Nat × β)leaftoListTR.go leaf acc = toList leaf ++ accβ: Type u_1t, left✝: Tree βkey✝: Natvalue✝: βright✝: Tree βleft_ih✝: ∀ (acc : List (Nat × β)), toListTR.go left✝ acc = toList left✝ ++ accright_ih✝: ∀ (acc : List (Nat × β)), toListTR.go right✝ acc = toList right✝ ++ accacc: List (Nat × β)nodetoListTR.go (node left✝ key✝ value✝ right✝) acc = toList (node left✝ key✝ value✝ right✝) ++ acc <;>β: Type u_1t: Tree βacc: List (Nat × β)leaftoListTR.go leaf acc = toList leaf ++ accβ: Type u_1t, left✝: Tree βkey✝: Natvalue✝: βright✝: Tree βleft_ih✝: ∀ (acc : List (Nat × β)), toListTR.go left✝ acc = toList left✝ ++ accright_ih✝: ∀ (acc : List (Nat × β)), toListTR.go right✝ acc = toList right✝ ++ accacc: List (Nat × β)nodetoListTR.go (node left✝ key✝ value✝ right✝) acc = toList (node left✝ key✝ value✝ right✝) ++ acc
simp [toListTR.go: {β : Type ?u.10598} → Tree β → List (Nat × β) → List (Nat × β)toListTR.go, toList: {β : Type ?u.10619} → Tree β → List (Nat × β)toList, *, List.append_assoc: ∀ {α : Type ?u.10510} (as bs cs : List α), as ++ bs ++ cs = as ++ (bs ++ cs)List.append_assoc]Goals accomplished! 🐙```

The `[csimp]` annotation instructs the Lean code generator to replace any `Tree.toList` with `Tree.toListTR` when generating code.

```@[csimp] theorem Tree.toList_eq_toListTR_csimp: @toList = @toListTRTree.toList_eq_toListTR_csimp
: @Tree.toList: {β : Type u_1} → Tree β → List (Nat × β)Tree.toList = @Tree.toListTR: {β : Type u_1} → Tree β → List (Nat × β)Tree.toListTR := byGoals accomplished! 🐙
funext β: Type u_1β t: Tree βtβ: Type u_1t: Tree βh.htoList t = toListTR t
apply toList_eq_toListTR: ∀ {β : Type u_1} (t : Tree β), toList t = toListTR ttoList_eq_toListTRGoals accomplished! 🐙```

The implementations of `Tree.find?` and `Tree.insert` assume that values of type tree obey the BST invariant: for any non-empty node with key `k`, all the values of the `left` subtree are less than `k` and all the values of the right subtree are greater than `k`. But that invariant is not part of the definition of tree.

So, let's formalize the BST invariant. Here's one way to do so. First, we define a helper `ForallTree` to express that idea that a predicate holds at every node of a tree:

```inductive ForallTree: {β : Type u_1} → (Nat → β → Prop) → Tree β → PropForallTree (p: Nat → β → Propp : Nat: TypeNat → β: Type u_1β → Prop: TypeProp) : Tree: Type u_1 → Type u_1Tree β: Type u_1β → Prop: TypeProp
| leaf: ∀ {β : Type u_1} {p : Nat → β → Prop}, ForallTree p Tree.leafleaf : ForallTree: {β : Type u_1} → (Nat → β → Prop) → Tree β → PropForallTree p: Nat → β → Propp .leaf: {β : Type u_1} → Tree β.leaf
| node: ∀ {β : Type u_1} {p : Nat → β → Prop} {left : Tree β} {key : Nat} {value : β} {right : Tree β},
ForallTree p left → p key value → ForallTree p right → ForallTree p (Tree.node left key value right)node :
ForallTree: {β : Type u_1} → (Nat → β → Prop) → Tree β → PropForallTree p: Nat → β → Propp left: Tree βleft →
p: Nat → β → Propp key: Natkey value: βvalue →
ForallTree: {β : Type u_1} → (Nat → β → Prop) → Tree β → PropForallTree p: Nat → β → Propp right: Tree βright →
ForallTree: {β : Type u_1} → (Nat → β → Prop) → Tree β → PropForallTree p: Nat → β → Propp (.node: {β : Type u_1} → Tree β → Nat → β → Tree β → Tree β.node left: Tree βleft key: Natkey value: βvalue right: Tree βright)```

Second, we define the BST invariant: An empty tree is a BST. A non-empty tree is a BST if all its left nodes have a lesser key, its right nodes have a greater key, and the left and right subtrees are themselves BSTs.

```inductive BST: {β : Type u_1} → Tree β → PropBST : Tree: Type u_1 → Type u_1Tree β: Type u_1β → Prop: TypeProp
| leaf: ∀ {β : Type u_1}, BST Tree.leafleaf : BST: {β : Type u_1} → Tree β → PropBST .leaf: {β : Type u_1} → Tree β.leaf
| node: ∀ {β : Type u_1} {key : Nat} {left right : Tree β} {value : β},
ForallTree (fun k v => k < key) left →
ForallTree (fun k v => key < k) right → BST left → BST right → BST (Tree.node left key value right)node :
ForallTree: {β : Type u_1} → (Nat → β → Prop) → Tree β → PropForallTree (fun k: Natk v: ?m.11584vWarning: unused variable `v` [linter.unusedVariables] => k: Natk < key: Natkey) left: Tree ?m.11584left →
ForallTree: {β : Type u_1} → (Nat → β → Prop) → Tree β → PropForallTree (fun k: Natk v: ?m.11584vWarning: unused variable `v` [linter.unusedVariables] => key: Natkey < k: Natk) right: Tree ?m.11584right →
BST: {β : Type u_1} → Tree β → PropBST left: Tree ?m.11584left → BST: {β : Type u_1} → Tree β → PropBST right: Tree ?m.11584right →
BST: {β : Type u_1} → Tree β → PropBST (.node: {β : Type u_1} → Tree β → Nat → β → Tree β → Tree β.node left: Tree ?m.11584left key: Natkey value: ?m.11584value right: Tree ?m.11584right)```

We can use the `macro` command to create helper tactics for organizing our proofs. The macro `have_eq x y` tries to prove `x = y` using linear arithmetic, and then immediately uses the new equality to substitute `x` with `y` everywhere in the goal.

The modifier `local` specifies the scope of the macro.

```/-- The `have_eq lhs rhs` tactic (tries to) prove that `lhs = rhs`,
and then replaces `lhs` with `rhs`. -/
local macro "have_eq " lhs: Lean.TSyntax `termlhs:term: Lean.Parser.Categoryterm:max rhs: Lean.TSyntax `termrhs:term: Lean.Parser.Categoryterm:max : tactic: Lean.Parser.Categorytactic =>
`(tactic|
(have h : \$lhs: Lean.TSyntax `termlhs = \$rhs: Lean.TSyntax `termrhs :=
-- TODO: replace with linarith
by simp_arith at *; apply Nat.le_antisymm <;> assumption
try subst \$lhs: Lean.TSyntax `termlhs))```

The `by_cases' e` is just the regular `by_cases` followed by `simp` using all hypotheses in the current goal as rewriting rules. Recall that the `by_cases` tactic creates two goals. One where we have `h : e` and another one containing `h : ¬ e`. The simplier uses the `h` to rewrite `e` to `True` in the first subgoal, and `e` to `False` in the second. This is particularly useful if `e` is the condition of an `if`-statement.

```/-- `by_cases' e` is a shorthand form `by_cases e <;> simp[*]` -/
local macro "by_cases' " e: Lean.TSyntax `terme:term: Lean.Parser.Categoryterm :  tactic: Lean.Parser.Categorytactic =>
`(tactic| by_cases \$e: Lean.TSyntax `terme <;> simp [*])```

We can use the attribute `[simp]` to instruct the simplifier to reduce given definitions or apply rewrite theorems. The `local` modifier limits the scope of this modification to this file.

`attribute [local simp] Tree.insert: {β : Type u_1} → Tree β → Nat → β → Tree βTree.insert`

We now prove that `Tree.insert` preserves the BST invariant using induction and case analysis. Recall that the tactic `. tac` focuses on the main goal and tries to solve it using `tac`, or else fails. It is used to structure proofs in Lean. The notation `‹e›` is just syntax sugar for `(by assumption : e)`. That is, it tries to find a hypothesis `h : e`. It is useful to access hypothesis that have auto generated names (aka "inaccessible") names.

```theorem Tree.forall_insert_of_forall: ∀ {β : Type u_1} {p : Nat → β → Prop} {t : Tree β} {key : Nat} {value : β},
ForallTree p t → p key value → ForallTree p (insert t key value)Tree.forall_insert_of_forall
(h₁: ForallTree p th₁ : ForallTree: {β : Type u_1} → (Nat → β → Prop) → Tree β → PropForallTree p: Nat → ?m.18615 → Propp t: Tree ?m.18615t) (h₂: p key valueh₂ : p: Nat → ?m.18615 → Propp key: Natkey value: ?m.18615value)
: ForallTree: {β : Type u_1} → (Nat → β → Prop) → Tree β → PropForallTree p: Nat → ?m.18615 → Propp (t: Tree ?m.18615t.insert: {β : Type u_1} → Tree β → Nat → β → Tree βinsert key: Natkey value: ?m.18615value) := byGoals accomplished! 🐙
induction h₁: ForallTree p th₁ withβ✝: Type u_1p: Nat → β✝ → Propt: Tree β✝key: Natvalue: β✝h₁: ForallTree p th₂: p key valueForallTree p (insert t key value)
| leaf: ∀ {β : Type u_1} {p : Nat → β → Prop}, ForallTree p leafleaf =>β✝: Type u_1p: Nat → β✝ → Propt: Tree β✝key: Natvalue: β✝h₂: p key valueleafForallTree p (insert leaf key value) exact .node: ∀ {β : Type u_1} {p : Nat → β → Prop} {left : Tree β} {key : Nat} {value : β} {right : Tree β},
ForallTree p left → p key value → ForallTree p right → ForallTree p (node left key value right).node .leaf: ∀ {β : Type u_1} {p : Nat → β → Prop}, ForallTree p leaf.leaf h₂: p key valueh₂ .leaf: ∀ {β : Type u_1} {p : Nat → β → Prop}, ForallTree p leaf.leafGoals accomplished! 🐙
| node: ∀ {β : Type u_1} {p : Nat → β → Prop} {left : Tree β} {key : Nat} {value : β} {right : Tree β},
ForallTree p left → p key value → ForallTree p right → ForallTree p (node left key value right)node hl: ForallTree p left✝hl hp: p key✝ value✝hp hr: ForallTree p right✝hr ihl: ForallTree p (insert left✝ key value)ihl ihr: ForallTree p (insert right✝ key value)ihr =>β✝: Type u_1p: Nat → β✝ → Propt: Tree β✝key: Natvalue: β✝h₂: p key valueleft✝: Tree β✝key✝: Natvalue✝: β✝right✝: Tree β✝hl: ForallTree p left✝hp: p key✝ value✝hr: ForallTree p right✝ihl: ForallTree p (insert left✝ key value)ihr: ForallTree p (insert right✝ key value)nodeForallTree p (insert (node left✝ key✝ value✝ right✝) key value)
rename Nat: TypeNat => kβ✝: Type u_1p: Nat → β✝ → Propt: Tree β✝key: Natvalue: β✝h₂: p key valueleft✝: Tree β✝k: Natvalue✝: β✝right✝: Tree β✝hl: ForallTree p left✝hp: p k value✝hr: ForallTree p right✝ihl: ForallTree p (insert left✝ key value)ihr: ForallTree p (insert right✝ key value)nodeForallTree p (insert (node left✝ k value✝ right✝) key value)
by_cases' key: Natkey < k: Natkβ✝: Type u_1p: Nat → β✝ → Propt: Tree β✝key: Natvalue: β✝h₂: p key valueleft✝: Tree β✝k: Natvalue✝: β✝right✝: Tree β✝hl: ForallTree p left✝hp: p k value✝hr: ForallTree p right✝ihl: ForallTree p (insert left✝ key value)ihr: ForallTree p (insert right✝ key value)h✝: key < knode.inlForallTree p (node (insert left✝ key value) k value✝ right✝)β✝: Type u_1p: Nat → β✝ → Propt: Tree β✝key: Natvalue: β✝h₂: p key valueleft✝: Tree β✝k: Natvalue✝: β✝right✝: Tree β✝hl: ForallTree p left✝hp: p k value✝hr: ForallTree p right✝ihl: ForallTree p (insert left✝ key value)ihr: ForallTree p (insert right✝ key value)h✝: ¬key < knode.inrForallTree p (if k < key then node left✝ k value✝ (insert right✝ key value) else node left✝ key value right✝)
.β✝: Type u_1p: Nat → β✝ → Propt: Tree β✝key: Natvalue: β✝h₂: p key valueleft✝: Tree β✝k: Natvalue✝: β✝right✝: Tree β✝hl: ForallTree p left✝hp: p k value✝hr: ForallTree p right✝ihl: ForallTree p (insert left✝ key value)ihr: ForallTree p (insert right✝ key value)h✝: key < knode.inlForallTree p (node (insert left✝ key value) k value✝ right✝) exact .node: ∀ {β : Type u_1} {p : Nat → β → Prop} {left : Tree β} {key : Nat} {value : β} {right : Tree β},
ForallTree p left → p key value → ForallTree p right → ForallTree p (node left key value right).node ihl: ForallTree p (insert left✝ key value)ihl hp: p k value✝hp hr: ForallTree p right✝hrGoals accomplished! 🐙
.β✝: Type u_1p: Nat → β✝ → Propt: Tree β✝key: Natvalue: β✝h₂: p key valueleft✝: Tree β✝k: Natvalue✝: β✝right✝: Tree β✝hl: ForallTree p left✝hp: p k value✝hr: ForallTree p right✝ihl: ForallTree p (insert left✝ key value)ihr: ForallTree p (insert right✝ key value)h✝: ¬key < knode.inrForallTree p (if k < key then node left✝ k value✝ (insert right✝ key value) else node left✝ key value right✝) by_cases' k: Natk < key: Natkeyβ✝: Type u_1p: Nat → β✝ → Propt: Tree β✝key: Natvalue: β✝h₂: p key valueleft✝: Tree β✝k: Natvalue✝: β✝right✝: Tree β✝hl: ForallTree p left✝hp: p k value✝hr: ForallTree p right✝ihl: ForallTree p (insert left✝ key value)ihr: ForallTree p (insert right✝ key value)h✝¹: ¬key < kh✝: k < keynode.inr.inlForallTree p (node left✝ k value✝ (insert right✝ key value))β✝: Type u_1p: Nat → β✝ → Propt: Tree β✝key: Natvalue: β✝h₂: p key valueleft✝: Tree β✝k: Natvalue✝: β✝right✝: Tree β✝hl: ForallTree p left✝hp: p k value✝hr: ForallTree p right✝ihl: ForallTree p (insert left✝ key value)ihr: ForallTree p (insert right✝ key value)h✝¹: ¬key < kh✝: ¬k < keynode.inr.inrForallTree p (node left✝ key value right✝)
.β✝: Type u_1p: Nat → β✝ → Propt: Tree β✝key: Natvalue: β✝h₂: p key valueleft✝: Tree β✝k: Natvalue✝: β✝right✝: Tree β✝hl: ForallTree p left✝hp: p k value✝hr: ForallTree p right✝ihl: ForallTree p (insert left✝ key value)ihr: ForallTree p (insert right✝ key value)h✝¹: ¬key < kh✝: k < keynode.inr.inlForallTree p (node left✝ k value✝ (insert right✝ key value)) exact .node: ∀ {β : Type u_1} {p : Nat → β → Prop} {left : Tree β} {key : Nat} {value : β} {right : Tree β},
ForallTree p left → p key value → ForallTree p right → ForallTree p (node left key value right).node hl: ForallTree p left✝hl hp: p k value✝hp ihr: ForallTree p (insert right✝ key value)ihrGoals accomplished! 🐙
.β✝: Type u_1p: Nat → β✝ → Propt: Tree β✝key: Natvalue: β✝h₂: p key valueleft✝: Tree β✝k: Natvalue✝: β✝right✝: Tree β✝hl: ForallTree p left✝hp: p k value✝hr: ForallTree p right✝ihl: ForallTree p (insert left✝ key value)ihr: ForallTree p (insert right✝ key value)h✝¹: ¬key < kh✝: ¬k < keynode.inr.inrForallTree p (node left✝ key value right✝) have_eq key: Natkey k: Natkβ✝: Type u_1p: Nat → β✝ → Propt: Tree β✝value: β✝left✝: Tree β✝k: Natvalue✝: β✝right✝: Tree β✝hl: ForallTree p left✝hp: p k value✝hr: ForallTree p right✝h₂: p k valueihl: ForallTree p (insert left✝ k value)ihr: ForallTree p (insert right✝ k value)h✝¹, h✝: ¬k < knode.inr.inrForallTree p (node left✝ k value right✝)
exact .node: ∀ {β : Type u_1} {p : Nat → β → Prop} {left : Tree β} {key : Nat} {value : β} {right : Tree β},
ForallTree p left → p key value → ForallTree p right → ForallTree p (node left key value right).node hl: ForallTree p left✝hl h₂: p k valueh₂ hr: ForallTree p right✝hrGoals accomplished! 🐙

theorem Tree.bst_insert_of_bst: ∀ {β : Type u_1} {t : Tree β}, BST t → ∀ (key : Nat) (value : β), BST (insert t key value)Tree.bst_insert_of_bst
{t: Tree βt : Tree: Type u_1 → Type u_1Tree β: Type u_1β} (h: BST th : BST: {β : Type u_1} → Tree β → PropBST t: Tree βt) (key: Natkey : Nat: TypeNat) (value: βvalue : β: Type u_1β)
: BST: {β : Type u_1} → Tree β → PropBST (t: Tree βt.insert: {β : Type u_1} → Tree β → Nat → β → Tree βinsert key: Natkey value: βvalue) := byGoals accomplished! 🐙
induction h: BST th withβ: Type u_1t: Tree βh: BST tkey: Natvalue: βBST (insert t key value)
| leaf: ∀ {β : Type u_1}, BST leafleaf =>β: Type u_1t: Tree βkey: Natvalue: βleafBST (insert leaf key value) exact .node: ∀ {β : Type u_1} {key : Nat} {left right : Tree β} {value : β},
ForallTree (fun k v => k < key) left →
ForallTree (fun k v => key < k) right → BST left → BST right → BST (node left key value right).node .leaf: ∀ {β : Type u_1} {p : Nat → β → Prop}, ForallTree p leaf.leaf .leaf: ∀ {β : Type u_1} {p : Nat → β → Prop}, ForallTree p leaf.leaf .leaf: ∀ {β : Type u_1}, BST leaf.leaf .leaf: ∀ {β : Type u_1}, BST leaf.leafGoals accomplished! 🐙
| node: ∀ {β : Type u_1} {key : Nat} {left right : Tree β} {value : β},
ForallTree (fun k v => k < key) left →
ForallTree (fun k v => key < k) right → BST left → BST right → BST (node left key value right)node h₁: ForallTree (fun k v => k < key✝) left✝h₁ h₂: ForallTree (fun k v => key✝ < k) right✝h₂ b₁: BST left✝b₁ b₂: BST right✝b₂ ih₁: BST (insert left✝ key value)ih₁ ih₂: BST (insert right✝ key value)ih₂ =>β: Type u_1t: Tree βkey: Natvalue: βkey✝: Natleft✝, right✝: Tree βvalue✝: βh₁: ForallTree (fun k v => k < key✝) left✝h₂: ForallTree (fun k v => key✝ < k) right✝b₁: BST left✝b₂: BST right✝ih₁: BST (insert left✝ key value)ih₂: BST (insert right✝ key value)nodeBST (insert (node left✝ key✝ value✝ right✝) key value)
rename Nat: TypeNat => kβ: Type u_1t: Tree βkey: Natvalue: βk: Natleft✝, right✝: Tree βvalue✝: βh₁: ForallTree (fun k_1 v => k_1 < k) left✝h₂: ForallTree (fun k_1 v => k < k_1) right✝b₁: BST left✝b₂: BST right✝ih₁: BST (insert left✝ key value)ih₂: BST (insert right✝ key value)nodeBST (insert (node left✝ k value✝ right✝) key value)
simpβ: Type u_1t: Tree βkey: Natvalue: βk: Natleft✝, right✝: Tree βvalue✝: βh₁: ForallTree (fun k_1 v => k_1 < k) left✝h₂: ForallTree (fun k_1 v => k < k_1) right✝b₁: BST left✝b₂: BST right✝ih₁: BST (insert left✝ key value)ih₂: BST (insert right✝ key value)nodeBST
(if key < k then node (insert left✝ key value) k value✝ right✝
else if k < key then node left✝ k value✝ (insert right✝ key value) else node left✝ key value right✝)
by_cases' key: Natkey < k: Natkβ: Type u_1t: Tree βkey: Natvalue: βk: Natleft✝, right✝: Tree βvalue✝: βh₁: ForallTree (fun k_1 v => k_1 < k) left✝h₂: ForallTree (fun k_1 v => k < k_1) right✝b₁: BST left✝b₂: BST right✝ih₁: BST (insert left✝ key value)ih₂: BST (insert right✝ key value)h✝: key < knode.inlBST (node (insert left✝ key value) k value✝ right✝)β: Type u_1t: Tree βkey: Natvalue: βk: Natleft✝, right✝: Tree βvalue✝: βh₁: ForallTree (fun k_1 v => k_1 < k) left✝h₂: ForallTree (fun k_1 v => k < k_1) right✝b₁: BST left✝b₂: BST right✝ih₁: BST (insert left✝ key value)ih₂: BST (insert right✝ key value)h✝: ¬key < knode.inrBST (if k < key then node left✝ k value✝ (insert right✝ key value) else node left✝ key value right✝)
.β: Type u_1t: Tree βkey: Natvalue: βk: Natleft✝, right✝: Tree βvalue✝: βh₁: ForallTree (fun k_1 v => k_1 < k) left✝h₂: ForallTree (fun k_1 v => k < k_1) right✝b₁: BST left✝b₂: BST right✝ih₁: BST (insert left✝ key value)ih₂: BST (insert right✝ key value)h✝: key < knode.inlBST (node (insert left✝ key value) k value✝ right✝) exact .node: ∀ {β : Type u_1} {key : Nat} {left right : Tree β} {value : β},
ForallTree (fun k v => k < key) left →
ForallTree (fun k v => key < k) right → BST left → BST right → BST (node left key value right).node (forall_insert_of_forall: ∀ {β : Type u_1} {p : Nat → β → Prop} {t : Tree β} {key : Nat} {value : β},
ForallTree p t → p key value → ForallTree p (insert t key value)forall_insert_of_forall h₁: ForallTree (fun k_1 v => k_1 < k) left✝h₁ ‹key < k›) h₂: ForallTree (fun k_1 v => k < k_1) right✝h₂ ih₁: BST (insert left✝ key value)ih₁ b₂: BST right✝b₂Goals accomplished! 🐙
.β: Type u_1t: Tree βkey: Natvalue: βk: Natleft✝, right✝: Tree βvalue✝: βh₁: ForallTree (fun k_1 v => k_1 < k) left✝h₂: ForallTree (fun k_1 v => k < k_1) right✝b₁: BST left✝b₂: BST right✝ih₁: BST (insert left✝ key value)ih₂: BST (insert right✝ key value)h✝: ¬key < knode.inrBST (if k < key then node left✝ k value✝ (insert right✝ key value) else node left✝ key value right✝) by_cases' k: Natk < key: Natkeyβ: Type u_1t: Tree βkey: Natvalue: βk: Natleft✝, right✝: Tree βvalue✝: βh₁: ForallTree (fun k_1 v => k_1 < k) left✝h₂: ForallTree (fun k_1 v => k < k_1) right✝b₁: BST left✝b₂: BST right✝ih₁: BST (insert left✝ key value)ih₂: BST (insert right✝ key value)h✝¹: ¬key < kh✝: k < keynode.inr.inlBST (node left✝ k value✝ (insert right✝ key value))β: Type u_1t: Tree βkey: Natvalue: βk: Natleft✝, right✝: Tree βvalue✝: βh₁: ForallTree (fun k_1 v => k_1 < k) left✝h₂: ForallTree (fun k_1 v => k < k_1) right✝b₁: BST left✝b₂: BST right✝ih₁: BST (insert left✝ key value)ih₂: BST (insert right✝ key value)h✝¹: ¬key < kh✝: ¬k < keynode.inr.inrBST (node left✝ key value right✝)
.β: Type u_1t: Tree βkey: Natvalue: βk: Natleft✝, right✝: Tree βvalue✝: βh₁: ForallTree (fun k_1 v => k_1 < k) left✝h₂: ForallTree (fun k_1 v => k < k_1) right✝b₁: BST left✝b₂: BST right✝ih₁: BST (insert left✝ key value)ih₂: BST (insert right✝ key value)h✝¹: ¬key < kh✝: k < keynode.inr.inlBST (node left✝ k value✝ (insert right✝ key value)) exact .node: ∀ {β : Type u_1} {key : Nat} {left right : Tree β} {value : β},
ForallTree (fun k v => k < key) left →
ForallTree (fun k v => key < k) right → BST left → BST right → BST (node left key value right).node h₁: ForallTree (fun k_1 v => k_1 < k) left✝h₁ (forall_insert_of_forall: ∀ {β : Type u_1} {p : Nat → β → Prop} {t : Tree β} {key : Nat} {value : β},
ForallTree p t → p key value → ForallTree p (insert t key value)forall_insert_of_forall h₂: ForallTree (fun k_1 v => k < k_1) right✝h₂ ‹k < key›) b₁: BST left✝b₁ ih₂: BST (insert right✝ key value)ih₂Goals accomplished! 🐙
.β: Type u_1t: Tree βkey: Natvalue: βk: Natleft✝, right✝: Tree βvalue✝: βh₁: ForallTree (fun k_1 v => k_1 < k) left✝h₂: ForallTree (fun k_1 v => k < k_1) right✝b₁: BST left✝b₂: BST right✝ih₁: BST (insert left✝ key value)ih₂: BST (insert right✝ key value)h✝¹: ¬key < kh✝: ¬k < keynode.inr.inrBST (node left✝ key value right✝) have_eq key: Natkey k: Natkβ: Type u_1t: Tree βvalue: βk: Natleft✝, right✝: Tree βvalue✝: βh₁: ForallTree (fun k_1 v => k_1 < k) left✝h₂: ForallTree (fun k_1 v => k < k_1) right✝b₁: BST left✝b₂: BST right✝ih₁: BST (insert left✝ k value)ih₂: BST (insert right✝ k value)h✝¹, h✝: ¬k < knode.inr.inrBST (node left✝ k value right✝)
exact .node: ∀ {β : Type u_1} {key : Nat} {left right : Tree β} {value : β},
ForallTree (fun k v => k < key) left →
ForallTree (fun k v => key < k) right → BST left → BST right → BST (node left key value right).node h₁: ForallTree (fun k_1 v => k_1 < k) left✝h₁ h₂: ForallTree (fun k_1 v => k < k_1) right✝h₂ b₁: BST left✝b₁ b₂: BST right✝b₂Goals accomplished! 🐙```

Now, we define the type `BinTree` using a `Subtype` that states that only trees satisfying the BST invariant are `BinTree`s.

```def BinTree: Type u → Type uBinTree (β: Type uβ : Type u: Type (u + 1)Type u) := { t: Tree βt : Tree: Type u → Type uTree β: Type uβ // BST: {β : Type u} → Tree β → PropBST t: Tree βt }

def BinTree.mk: {β : Type u_1} → BinTree βBinTree.mk : BinTree: Type u_1 → Type u_1BinTree β: Type u_1β :=
⟨.leaf: {β : Type u_1} → Tree β.leaf, .leaf: ∀ {β : Type u_1}, BST Tree.leaf.leaf⟩

def BinTree.contains: {β : Type u_1} → BinTree β → Nat → BoolBinTree.contains (b: BinTree βb : BinTree: Type u_1 → Type u_1BinTree β: Type u_1β) (k: Natk : Nat: TypeNat) : Bool: TypeBool :=
b: BinTree βb.val: {α : Type u_1} → {p : α → Prop} → Subtype p → αval.contains: {β : Type u_1} → Tree β → Nat → Boolcontains k: Natk

def BinTree.find?: {β : Type u_1} → BinTree β → Nat → Option βBinTree.find? (b: BinTree βb : BinTree: Type u_1 → Type u_1BinTree β: Type u_1β) (k: Natk : Nat: TypeNat) : Option: Type u_1 → Type u_1Option β: Type u_1β :=
b: BinTree βb.val: {α : Type u_1} → {p : α → Prop} → Subtype p → αval.find?: {β : Type u_1} → Tree β → Nat → Option βfind? k: Natk

def BinTree.insert: {β : Type u_1} → BinTree β → Nat → β → BinTree βBinTree.insert (b: BinTree βb : BinTree: Type u_1 → Type u_1BinTree β: Type u_1β) (k: Natk : Nat: TypeNat) (v: βv : β: Type u_1β) : BinTree: Type u_1 → Type u_1BinTree β: Type u_1β :=
⟨b: BinTree βb.val: {α : Type u_1} → {p : α → Prop} → Subtype p → αval.insert: {β : Type u_1} → Tree β → Nat → β → Tree βinsert k: Natk v: βv, b: BinTree βb.val: {α : Type u_1} → {p : α → Prop} → Subtype p → αval.bst_insert_of_bst: ∀ {β : Type u_1} {t : Tree β}, BST t → ∀ (key : Nat) (value : β), BST (Tree.insert t key value)bst_insert_of_bst b: BinTree βb.property: ∀ {α : Type u_1} {p : α → Prop} (self : Subtype p), p self.valproperty k: Natk v: βv⟩```

Finally, we prove that `BinTree.find?` and `BinTree.insert` satisfy the map properties.

```attribute [local simp]
BinTree.mk: {β : Type u_1} → BinTree βBinTree.mk BinTree.contains: {β : Type u_1} → BinTree β → Nat → BoolBinTree.contains BinTree.find?: {β : Type u_1} → BinTree β → Nat → Option βBinTree.find?
BinTree.insert: {β : Type u_1} → BinTree β → Nat → β → BinTree βBinTree.insert Tree.find?: {β : Type u_1} → Tree β → Nat → Option βTree.find? Tree.contains: {β : Type u_1} → Tree β → Nat → BoolTree.contains Tree.insert: {β : Type u_1} → Tree β → Nat → β → Tree βTree.insert

theorem BinTree.find_mk: ∀ {β : Type u_1} (k : Nat), find? mk k = noneBinTree.find_mk (k: Natk : Nat: TypeNat)
: BinTree.mk: {β : Type u_1} → BinTree βBinTree.mk.find?: {β : Type u_1} → BinTree β → Nat → Option βfind? k: Natk = (none: {α : Type u_1} → Option αnone : Option: Type u_1 → Type u_1Option β: Type u_1β) := byGoals accomplished! 🐙
simpGoals accomplished! 🐙

theorem BinTree.find_insert: ∀ {β : Type u_1} (b : BinTree β) (k : Nat) (v : β), find? (insert b k v) k = some vBinTree.find_insert (b: BinTree βb : BinTree: Type u_1 → Type u_1BinTree β: Type u_1β) (k: Natk : Nat: TypeNat) (v: βv : β: Type u_1β)
: (b: BinTree βb.insert: {β : Type u_1} → BinTree β → Nat → β → BinTree βinsert k: Natk v: βv).find?: {β : Type u_1} → BinTree β → Nat → Option βfind? k: Natk = some: {α : Type u_1} → α → Option αsome v: βv := byGoals accomplished! 🐙
let ⟨t: Tree βt, h: BST th⟩ := b: BinTree βbβ: Type u_1b: BinTree βk: Natv: βt: Tree βh: BST tfind? (insert { val := t, property := h } k v) k = some v; simpβ: Type u_1b: BinTree βk: Natv: βt: Tree βh: BST tTree.find? (Tree.insert t k v) k = some v
induction t: Tree βt withβ: Type u_1b: BinTree βk: Natv: βt: Tree βh: BST tTree.find? (Tree.insert t k v) k = some v simpGoals accomplished! 🐙
| node: {β : Type v} → Tree β → Nat → β → Tree β → Tree βnode left: Tree βleft key: Natkey value: βvalue right: Tree βright ihl: BST left → Tree.find? (Tree.insert left k v) k = some vihl ihr: BST right → Tree.find? (Tree.insert right k v) k = some vihr =>β: Type u_1b: BinTree βk: Natv: βleft: Tree βkey: Natvalue: βright: Tree βihl: BST left → Tree.find? (Tree.insert left k v) k = some vihr: BST right → Tree.find? (Tree.insert right k v) k = some vh: BST (Tree.node left key value right)nodeTree.find?
(if k < key then Tree.node (Tree.insert left k v) key value right
else if key < k then Tree.node left key value (Tree.insert right k v) else Tree.node left k v right)
k =
some v
by_cases' k: Natk < key: Natkeyβ: Type u_1b: BinTree βk: Natv: βleft: Tree βkey: Natvalue: βright: Tree βihl: BST left → Tree.find? (Tree.insert left k v) k = some vihr: BST right → Tree.find? (Tree.insert right k v) k = some vh: BST (Tree.node left key value right)h✝: k < keynode.inlTree.find? (Tree.insert left k v) k = some vβ: Type u_1b: BinTree βk: Natv: βleft: Tree βkey: Natvalue: βright: Tree βihl: BST left → Tree.find? (Tree.insert left k v) k = some vihr: BST right → Tree.find? (Tree.insert right k v) k = some vh: BST (Tree.node left key value right)h✝: ¬k < keynode.inrTree.find? (if key < k then Tree.node left key value (Tree.insert right k v) else Tree.node left k v right) k = some v
.β: Type u_1b: BinTree βk: Natv: βleft: Tree βkey: Natvalue: βright: Tree βihl: BST left → Tree.find? (Tree.insert left k v) k = some vihr: BST right → Tree.find? (Tree.insert right k v) k = some vh: BST (Tree.node left key value right)h✝: k < keynode.inlTree.find? (Tree.insert left k v) k = some v cases h: BST (Tree.node left key value right)hβ: Type u_1b: BinTree βk: Natv: βleft: Tree βkey: Natvalue: βright: Tree βihl: BST left → Tree.find? (Tree.insert left k v) k = some vihr: BST right → Tree.find? (Tree.insert right k v) k = some vh✝: k < keya✝³: BST lefta✝²: ForallTree (fun k v => k < key) lefta✝¹: BST righta✝: ForallTree (fun k v => key < k) rightnode.inl.nodeTree.find? (Tree.insert left k v) k = some v; apply ihl: BST left → Tree.find? (Tree.insert left k v) k = some vihlβ: Type u_1b: BinTree βk: Natv: βleft: Tree βkey: Natvalue: βright: Tree βihl: BST left → Tree.find? (Tree.insert left k v) k = some vihr: BST right → Tree.find? (Tree.insert right k v) k = some vh✝: k < keya✝³: BST lefta✝²: ForallTree (fun k v => k < key) lefta✝¹: BST righta✝: ForallTree (fun k v => key < k) rightnode.inl.nodeBST left; assumptionGoals accomplished! 🐙
.β: Type u_1b: BinTree βk: Natv: βleft: Tree βkey: Natvalue: βright: Tree βihl: BST left → Tree.find? (Tree.insert left k v) k = some vihr: BST right → Tree.find? (Tree.insert right k v) k = some vh: BST (Tree.node left key value right)h✝: ¬k < keynode.inrTree.find? (if key < k then Tree.node left key value (Tree.insert right k v) else Tree.node left k v right) k = some v by_cases' key: Natkey < k: Natkβ: Type u_1b: BinTree βk: Natv: βleft: Tree βkey: Natvalue: βright: Tree βihl: BST left → Tree.find? (Tree.insert left k v) k = some vihr: BST right → Tree.find? (Tree.insert right k v) k = some vh: BST (Tree.node left key value right)h✝¹: ¬k < keyh✝: key < knode.inr.inlTree.find? (Tree.insert right k v) k = some v
cases h: BST (Tree.node left key value right)hβ: Type u_1b: BinTree βk: Natv: βleft: Tree βkey: Natvalue: βright: Tree βihl: BST left → Tree.find? (Tree.insert left k v) k = some vihr: BST right → Tree.find? (Tree.insert right k v) k = some vh✝¹: ¬k < keyh✝: key < ka✝³: BST lefta✝²: ForallTree (fun k v => k < key) lefta✝¹: BST righta✝: ForallTree (fun k v => key < k) rightnode.inr.inl.nodeTree.find? (Tree.insert right k v) k = some v; apply ihr: BST right → Tree.find? (Tree.insert right k v) k = some vihrβ: Type u_1b: BinTree βk: Natv: βleft: Tree βkey: Natvalue: βright: Tree βihl: BST left → Tree.find? (Tree.insert left k v) k = some vihr: BST right → Tree.find? (Tree.insert right k v) k = some vh✝¹: ¬k < keyh✝: key < ka✝³: BST lefta✝²: ForallTree (fun k v => k < key) lefta✝¹: BST righta✝: ForallTree (fun k v => key < k) rightnode.inr.inl.nodeBST right; assumptionGoals accomplished! 🐙

theorem BinTree.find_insert_of_ne: ∀ {β : Type u_1} {k k' : Nat} (b : BinTree β), k ≠ k' → ∀ (v : β), find? (insert b k v) k' = find? b k'BinTree.find_insert_of_ne (b: BinTree βb : BinTree: Type u_1 → Type u_1BinTree β: Type u_1β) (h: k ≠ k'h : k: Natk ≠ k': Natk') (v: βv : β: Type u_1β)
: (b: BinTree βb.insert: {β : Type u_1} → BinTree β → Nat → β → BinTree βinsert k: Natk v: βv).find?: {β : Type u_1} → BinTree β → Nat → Option βfind? k': Natk' = b: BinTree βb.find?: {β : Type u_1} → BinTree β → Nat → Option βfind? k': Natk' := byGoals accomplished! 🐙
let ⟨t: Tree βt, h: BST th⟩ := b: BinTree βbβ: Type u_1k, k': Natb: BinTree βh✝: k ≠ k'v: βt: Tree βh: BST tfind? (insert { val := t, property := h } k v) k' = find? { val := t, property := h } k'; simpβ: Type u_1k, k': Natb: BinTree βh✝: k ≠ k'v: βt: Tree βh: BST tTree.find? (Tree.insert t k v) k' = Tree.find? t k'
induction t: Tree βt withβ: Type u_1k, k': Natb: BinTree βh✝: k ≠ k'v: βt: Tree βh: BST tTree.find? (Tree.insert t k v) k' = Tree.find? t k' simpβ: Type u_1k, k': Natb: BinTree βh✝: k ≠ k'v: βh: BST Tree.leafleaf(if k' < k then none else if k < k' then none else some v) = none
| leaf: {β : Type v} → Tree βleaf =>β: Type u_1k, k': Natb: BinTree βh✝: k ≠ k'v: βh: BST Tree.leafleaf(if k' < k then none else if k < k' then none else some v) = none
splitβ: Type u_1k, k': Natb: BinTree βh✝¹: k ≠ k'v: βh: BST Tree.leafh✝: k' < kleaf.inlnone = noneβ: Type u_1k, k': Natb: BinTree βh✝¹: k ≠ k'v: βh: BST Tree.leafh✝: ¬k' < kleaf.inr(if k < k' then none else some v) = none <;>β: Type u_1k, k': Natb: BinTree βh✝¹: k ≠ k'v: βh: BST Tree.leafh✝: k' < kleaf.inlnone = noneβ: Type u_1k, k': Natb: BinTree βh✝¹: k ≠ k'v: βh: BST Tree.leafh✝: ¬k' < kleaf.inr(if k < k' then none else some v) = none simpβ: Type u_1k, k': Natb: BinTree βh✝¹: k ≠ k'v: βh: BST Tree.leafh✝: ¬k' < kleaf.inr(if k < k' then none else some v) = none <;>β: Type u_1k, k': Natb: BinTree βh✝¹: k ≠ k'v: βh: BST Tree.leafh✝: ¬k' < kleaf.inr(if k < k' then none else some v) = none splitβ: Type u_1k, k': Natb: BinTree βh✝²: k ≠ k'v: βh: BST Tree.leafh✝¹: ¬k' < kh✝: k < k'leaf.inr.inlnone = noneβ: Type u_1k, k': Natb: BinTree βh✝²: k ≠ k'v: βh: BST Tree.leafh✝¹: ¬k' < kh✝: ¬k < k'leaf.inr.inrFalse <;>β: Type u_1k, k': Natb: BinTree βh✝²: k ≠ k'v: βh: BST Tree.leafh✝¹: ¬k' < kh✝: k < k'leaf.inr.inlnone = noneβ: Type u_1k, k': Natb: BinTree βh✝²: k ≠ k'v: βh: BST Tree.leafh✝¹: ¬k' < kh✝: ¬k < k'leaf.inr.inrFalse simpβ: Type u_1k, k': Natb: BinTree βh✝²: k ≠ k'v: βh: BST Tree.leafh✝¹: ¬k' < kh✝: ¬k < k'leaf.inr.inrFalse
have_eq k: Natk k': Natk'β: Type u_1k': Natb: BinTree βv: βh✝²: BST Tree.leafh: k' ≠ k'h✝¹, h✝: ¬k' < k'leaf.inr.inrFalse
| node: {β : Type v} → Tree β → Nat → β → Tree β → Tree βnode left: Tree βleft key: Natkey value: βvalue right: Tree βright ihl: BST left → Tree.find? (Tree.insert left k v) k' = Tree.find? left k'ihl ihr: BST right → Tree.find? (Tree.insert right k v) k' = Tree.find? right k'ihr =>β: Type u_1k, k': Natb: BinTree βh✝: k ≠ k'v: βleft: Tree βkey: Natvalue: βright: Tree βihl: BST left → Tree.find? (Tree.insert left k v) k' = Tree.find? left k'ihr: BST right → Tree.find? (Tree.insert right k v) k' = Tree.find? right k'h: BST (Tree.node left key value right)nodeTree.find?
(if k < key then Tree.node (Tree.insert left k v) key value right
else if key < k then Tree.node left key value (Tree.insert right k v) else Tree.node left k v right)
k' =
if k' < key then Tree.find? left k' else if key < k' then Tree.find? right k' else some value
let .node: ∀ {β : Type u_1} {key : Nat} {left right : Tree β} {value : β},
ForallTree (fun k v => k < key) left →
ForallTree (fun k v => key < k) right → BST left → BST right → BST (Tree.node left key value right).node hl: ForallTree (fun k v => k < key) lefthl hr: ForallTree (fun k v => key < k) righthr bl: BST leftbl br: BST rightbr := h: BST (Tree.node left key value right)hβ: Type u_1k, k': Natb: BinTree βh✝: k ≠ k'v: βleft: Tree βkey: Natvalue: βright: Tree βihl: BST left → Tree.find? (Tree.insert left k v) k' = Tree.find? left k'ihr: BST right → Tree.find? (Tree.insert right k v) k' = Tree.find? right k'h: BST (Tree.node left key value right)hl: ForallTree (fun k v => k < key) lefthr: ForallTree (fun k v => key < k) rightbl: BST leftbr: BST rightnodeTree.find?
(if k < key then Tree.node (Tree.insert left k v) key value right
else if key < k then Tree.node left key value (Tree.insert right k v) else Tree.node left k v right)
k' =
if k' < key then Tree.find? left k' else if key < k' then Tree.find? right k' else some value
specialize ihl: BST left → Tree.find? (Tree.insert left k v) k' = Tree.find? left k'ihl bl: BST leftblβ: Type u_1k, k': Natb: BinTree βh✝: k ≠ k'v: βleft: Tree βkey: Natvalue: βright: Tree βihr: BST right → Tree.find? (Tree.insert right k v) k' = Tree.find? right k'h: BST (Tree.node left key value right)hl: ForallTree (fun k v => k < key) lefthr: ForallTree (fun k v => key < k) rightbl: BST leftbr: BST rightihl: Tree.find? (Tree.insert left k v) k' = Tree.find? left k'nodeTree.find?
(if k < key then Tree.node (Tree.insert left k v) key value right
else if key < k then Tree.node left key value (Tree.insert right k v) else Tree.node left k v right)
k' =
if k' < key then Tree.find? left k' else if key < k' then Tree.find? right k' else some value
specialize ihr: BST right → Tree.find? (Tree.insert right k v) k' = Tree.find? right k'ihr br: BST rightbrβ: Type u_1k, k': Natb: BinTree βh✝: k ≠ k'v: βleft: Tree βkey: Natvalue: βright: Tree βh: BST (Tree.node left key value right)hl: ForallTree (fun k v => k < key) lefthr: ForallTree (fun k v => key < k) rightbl: BST leftbr: BST rightihl: Tree.find? (Tree.insert left k v) k' = Tree.find? left k'ihr: Tree.find? (Tree.insert right k v) k' = Tree.find? right k'nodeTree.find?
(if k < key then Tree.node (Tree.insert left k v) key value right
else if key < k then Tree.node left key value (Tree.insert right k v) else Tree.node left k v right)
k' =
if k' < key then Tree.find? left k' else if key < k' then Tree.find? right k' else some value
by_cases' k: Natk < key: Natkeyβ: Type u_1k, k': Natb: BinTree βh✝¹: k ≠ k'v: βleft: Tree βkey: Natvalue: βright: Tree βh: BST (Tree.node left key value right)hl: ForallTree (fun k v => k < key) lefthr: ForallTree (fun k v => key < k) rightbl: BST leftbr: BST rightihl: Tree.find? (Tree.insert left k v) k' = Tree.find? left k'ihr: Tree.find? (Tree.insert right k v) k' = Tree.find? right k'h✝: ¬k < keynode.inrTree.find? (if key < k then Tree.node left key value (Tree.insert right k v) else Tree.node left k v right) k' =
if k' < key then Tree.find? left k' else if key < k' then Tree.find? right k' else some value; by_cases' key: Natkey < k: Natkβ: Type u_1k, k': Natb: BinTree βh✝²: k ≠ k'v: βleft: Tree βkey: Natvalue: βright: Tree βh: BST (Tree.node left key value right)hl: ForallTree (fun k v => k < key) lefthr: ForallTree (fun k v => key < k) rightbl: BST leftbr: BST rightihl: Tree.find? (Tree.insert left k v) k' = Tree.find? left k'ihr: Tree.find? (Tree.insert right k v) k' = Tree.find? right k'h✝¹: ¬k < keyh✝: ¬key < knode.inr.inr(if k' < k then Tree.find? left k' else if k < k' then Tree.find? right k' else some v) =
if k' < key then Tree.find? left k' else if key < k' then Tree.find? right k' else some value
have_eq key: Natkey k: Natkβ: Type u_1k, k': Natb: BinTree βh✝²: k ≠ k'v: βleft: Tree βvalue: βright: Tree βbl: BST leftbr: BST rightihl: Tree.find? (Tree.insert left k v) k' = Tree.find? left k'ihr: Tree.find? (Tree.insert right k v) k' = Tree.find? right k'h: BST (Tree.node left k value right)hl: ForallTree (fun k_1 v => k_1 < k) lefthr: ForallTree (fun k_1 v => k < k_1) righth✝¹, h✝: ¬k < knode.inr.inr(if k' < k then Tree.find? left k' else if k < k' then Tree.find? right k' else some v) =
if k' < k then Tree.find? left k' else if k < k' then Tree.find? right k' else some value
by_cases' k': Natk' < k: Natkβ: Type u_1k, k': Natb: BinTree βh✝³: k ≠ k'v: βleft: Tree βvalue: βright: Tree βbl: BST leftbr: BST rightihl: Tree.find? (Tree.insert left k v) k' = Tree.find? left k'ihr: Tree.find? (Tree.insert right k v) k' = Tree.find? right k'h: BST (Tree.node left k value right)hl: ForallTree (fun k_1 v => k_1 < k) lefthr: ForallTree (fun k_1 v => k < k_1) righth✝², h✝¹: ¬k < kh✝: ¬k' < knode.inr.inr.inr(if k < k' then Tree.find? right k' else some v) = if k < k' then Tree.find? right k' else some value; by_cases' k: Natk  < k': Natk'β: Type u_1k, k': Natb: BinTree βh✝⁴: k ≠ k'v: βleft: Tree βvalue: βright: Tree βbl: BST leftbr: BST rightihl: Tree.find? (Tree.insert left k v) k' = Tree.find? left k'ihr: Tree.find? (Tree.insert right k v) k' = Tree.find? right k'h: BST (Tree.node left k value right)hl: ForallTree (fun k_1 v => k_1 < k) lefthr: ForallTree (fun k_1 v => k < k_1) righth✝³, h✝²: ¬k < kh✝¹: ¬k' < kh✝: ¬k < k'node.inr.inr.inr.inrv = value
have_eq k: Natk k': Natk'β: Type u_1k': Natb: BinTree βv: βleft: Tree βvalue: βright: Tree βbl: BST leftbr: BST righth✝⁴: k' ≠ k'ihl: Tree.find? (Tree.insert left k' v) k' = Tree.find? left k'ihr: Tree.find? (Tree.insert right k' v) k' = Tree.find? right k'h: BST (Tree.node left k' value right)hl: ForallTree (fun k v => k < k') lefthr: ForallTree (fun k v => k' < k) righth✝³, h✝², h✝¹, h✝: ¬k' < k'node.inr.inr.inr.inrv = value