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 v
Tree
(
β: 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 v
Tree
β: Type v
β
) (
key: Nat
key
:
Nat: Type
Nat
) (
value: β
value
:
β: Type v
β
) (
right: Tree β
right
:
Tree: Type v → Type v
Tree
β: Type v
β
) deriving
Repr: Type u → Type u
Repr

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

def 
Tree.contains: {β : Type u_1} → Tree β → Nat → Bool
Tree.contains
(
t: Tree β
t
:
Tree: Type u_1 → Type u_1
Tree
β: Type u_1
β
) (
k: Nat
k
:
Nat: Type
Nat
) :
Bool: Type
Bool
:= match
t: Tree β
t
with |
leaf: {β : Type ?u.1676} → Tree β
leaf
=>
false: Bool
false
|
node: {β : Type ?u.1685} → Tree β → Nat → β → Tree β → Tree β
node
left: Tree β
left
key: Nat
key
Warning: unused variable `value` [linter.unusedVariables]
right: Tree β
right
=> if
k: Nat
k
<
key: Nat
key
then
left: Tree β
left
.
contains: {β : Type u_1} → Tree β → Nat → Bool
contains
k: Nat
k
else if
key: Nat
key
<
k: Nat
k
then
right: Tree β
right
.
contains: {β : Type u_1} → Tree β → Nat → Bool
contains
k: Nat
k
else
true: Bool
true

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_1
Tree
β: Type u_1
β
) (
k: Nat
k
:
Nat: Type
Nat
) :
Option: Type u_1 → Type u_1
Option
β: Type u_1
β
:= match
t: Tree β
t
with |
leaf: {β : Type ?u.2132} → Tree β
leaf
=>
none: {α : Type u_1} → Option α
none
|
node: {β : Type ?u.2144} → Tree β → Nat → β → Tree β → Tree β
node
left: Tree β
left
key: Nat
key
value: β
value
right: Tree β
right
=> if
k: Nat
k
<
key: Nat
key
then
left: Tree β
left
.
find?: {β : Type u_1} → Tree β → Nat → Option β
find?
k: Nat
k
else if
key: Nat
key
<
k: Nat
k
then
right: Tree β
right
.
find?: {β : Type u_1} → Tree β → Nat → Option β
find?
k: Nat
k
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_1
Tree
β: Type u_1
β
) (
k: Nat
k
:
Nat: Type
Nat
) (
v: β
v
:
β: Type u_1
β
) :
Tree: Type u_1 → Type u_1
Tree
β: Type u_1
β
:= match
t: Tree β
t
with |
leaf: {β : Type ?u.2597} → Tree β
leaf
=>
node: {β : Type u_1} → Tree β → Nat → β → Tree β → Tree β
node
leaf: {β : Type u_1} → Tree β
leaf
k: Nat
k
v: β
v
leaf: {β : Type u_1} → Tree β
leaf
|
node: {β : Type ?u.2612} → Tree β → Nat → β → Tree β → Tree β
node
left: Tree β
left
key: Nat
key
value: β
value
right: Tree β
right
=> if
k: Nat
k
<
key: Nat
key
then
node: {β : Type u_1} → Tree β → Nat → β → Tree β → Tree β
node
(
left: Tree β
left
.
insert: {β : Type u_1} → Tree β → Nat → β → Tree β
insert
k: Nat
k
v: β
v
)
key: Nat
key
value: β
value
right: Tree β
right
else if
key: Nat
key
<
k: Nat
k
then
node: {β : Type u_1} → Tree β → Nat → β → Tree β → Tree β
node
left: Tree β
left
key: Nat
key
value: β
value
(
right: Tree β
right
.
insert: {β : Type u_1} → Tree β → Nat → β → Tree β
insert
k: Nat
k
v: β
v
) else
node: {β : Type u_1} → Tree β → Nat → β → Tree β → Tree β
node
left: Tree β
left
k: Nat
k
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_1
Tree
β: Type u_1
β
) :
List: Type u_1 → Type u_1
List
(
Nat: Type
Nat
×
β: Type u_1
β
) := match
t: Tree β
t
with |
leaf: {β : Type ?u.3098} → Tree β
leaf
=>
[]: List (Nat × β)
[]
|
node: {β : Type ?u.3110} → Tree β → Nat → β → Tree β → Tree β
node
l: Tree β
l
k: Nat
k
v: β
v
r: Tree β
r
=>
l: Tree β
l
.
toList: {β : Type u_1} → Tree β → List (Nat × β)
toList
++ [(
k: Nat
k
,
v: β
v
)] ++
r: Tree β
r
.
toList: {β : Type u_1} → Tree β → List (Nat × β)
toList
Tree.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: Nat
2
"two": String
"two"
|>.
insert: {β : Type} → Tree β → Nat → β → Tree β
insert
3: Nat
3
"three": String
"three"
|>.
insert: {β : Type} → Tree β → Nat → β → Tree β
insert
1: Nat
1
"one": String
"one"
[(1, "one"), (2, "two"), (3, "three")]
Tree.leaf: {β : Type} → Tree β
Tree.leaf
.
insert: {β : Type} → Tree β → Nat → β → Tree β
insert
2: Nat
2
"two": String
"two"
|>.
insert: {β : Type} → Tree β → Nat → β → Tree β
insert
3: Nat
3
"three": String
"three"
|>.
insert: {β : Type} → Tree β → Nat → β → Tree β
insert
1: Nat
1
"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_1
Tree
β: Type u_1
β
) :
List: Type u_1 → Type u_1
List
(
Nat: Type
Nat
×
β: Type u_1
β
) :=
go: Tree β → List (Nat × β) → List (Nat × β)
go
t: Tree β
t
[]: List (Nat × β)
[]
where
go: {β : Type u_1} → Tree β → List (Nat × β) → List (Nat × β)
go
(
t: Tree β
t
:
Tree: Type u_1 → Type u_1
Tree
β: Type u_1
β
) (
acc: List (Nat × β)
acc
:
List: Type u_1 → Type u_1
List
(
Nat: Type
Nat
×
β: Type u_1
β
)) :
List: Type u_1 → Type u_1
List
(
Nat: Type
Nat
×
β: Type u_1
β
) := match
t: Tree β
t
with |
leaf: {β : Type ?u.9397} → Tree β
leaf
=>
acc: List (Nat × β)
acc
|
node: {β : Type ?u.9407} → Tree β → Nat → β → Tree β → Tree β
node
l: Tree β
l
k: Nat
k
v: β
v
r: Tree β
r
=>
go: Tree β → List (Nat × β) → List (Nat × β)
go
l: Tree β
l
((
k: Nat
k
,
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 Trees, 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 t
Tree.toList_eq_toListTR
(
t: Tree β
t
:
Tree: Type u_1 → Type u_1
Tree
β: 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
:=
β: Type u_1
t: Tree β

toList t = toListTR t

Goals accomplished! 🐙
where
go: ∀ {β : Type u_1} (t : Tree β) (acc : List (Nat × β)), toListTR.go t acc = toList t ++ acc
go
(
t: Tree β
t
:
Tree: Type u_1 → Type u_1
Tree
β: Type u_1
β
) (
acc: List (Nat × β)
acc
:
List: Type u_1 → Type u_1
List
(
Nat: Type
Nat
×
β: 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
:=
β: Type u_1
t✝, t: Tree β
acc: List (Nat × β)

toListTR.go t acc = toList t ++ acc
β: Type u_1
t: Tree β
acc: List (Nat × β)

leaf
toListTR.go leaf acc = toList leaf ++ acc
β: Type u_1
t, left✝: Tree β
key✝: Nat
value✝: β
right✝: Tree β
left_ih✝: (acc : List (Nat × β)), toListTR.go left acc = toList left ++ acc
right_ih✝: (acc : List (Nat × β)), toListTR.go right acc = toList right ++ acc
acc: List (Nat × β)
toListTR.go (node left key value right) acc = toList (node left key value right) ++ acc
β: Type u_1
t: Tree β
acc: List (Nat × β)

leaf
toListTR.go leaf acc = toList leaf ++ acc
β: Type u_1
t, left✝: Tree β
key✝: Nat
value✝: β
right✝: Tree β
left_ih✝: (acc : List (Nat × β)), toListTR.go left acc = toList left ++ acc
right_ih✝: (acc : List (Nat × β)), toListTR.go right acc = toList right ++ acc
acc: List (Nat × β)
toListTR.go (node left key value right) acc = toList (node left key value right) ++ acc

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 = @toListTR
Tree.toList_eq_toListTR_csimp
: @
Tree.toList: {β : Type u_1} → Tree β → List (Nat × β)
Tree.toList
= @
Tree.toListTR: {β : Type u_1} → Tree β → List (Nat × β)
Tree.toListTR
:=

@toList = @toListTR
β: Type u_1
t: Tree β

h.h
toList t = toListTR t

Goals 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 β → Prop
ForallTree
(
p: Nat → β → Prop
p
:
Nat: Type
Nat
β: Type u_1
β
Prop: Type
Prop
) :
Tree: Type u_1 → Type u_1
Tree
β: Type u_1
β
Prop: Type
Prop
|
leaf: ∀ {β : Type u_1} {p : Nat → β → Prop}, ForallTree p Tree.leaf
leaf
:
ForallTree: {β : Type u_1} → (Nat → β → Prop) → Tree β → Prop
ForallTree
p: Nat → β → Prop
p
.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 β → Prop
ForallTree
p: Nat → β → Prop
p
left: Tree β
left
p: Nat → β → Prop
p
key: Nat
key
value: β
value
ForallTree: {β : Type u_1} → (Nat → β → Prop) → Tree β → Prop
ForallTree
p: Nat → β → Prop
p
right: Tree β
right
ForallTree: {β : Type u_1} → (Nat → β → Prop) → Tree β → Prop
ForallTree
p: Nat → β → Prop
p
(
.node: {β : Type u_1} → Tree β → Nat → β → Tree β → Tree β
.node
left: Tree β
left
key: Nat
key
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 β → Prop
BST
:
Tree: Type u_1 → Type u_1
Tree
β: Type u_1
β
Prop: Type
Prop
|
leaf: ∀ {β : Type u_1}, BST Tree.leaf
leaf
:
BST: {β : Type u_1} → Tree β → Prop
BST
.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 β → Prop
ForallTree
(fun
k: Nat
k
Warning: unused variable `v` [linter.unusedVariables]
=>
k: Nat
k
<
key: Nat
key
)
left: Tree ?m.11563
left
ForallTree: {β : Type u_1} → (Nat → β → Prop) → Tree β → Prop
ForallTree
(fun
k: Nat
k
Warning: unused variable `v` [linter.unusedVariables]
=>
key: Nat
key
<
k: Nat
k
)
right: Tree ?m.11563
right
BST: {β : Type u_1} → Tree β → Prop
BST
left: Tree ?m.11563
left
BST: {β : Type u_1} → Tree β → Prop
BST
right: Tree ?m.11563
right
BST: {β : Type u_1} → Tree β → Prop
BST
(
.node: {β : Type u_1} → Tree β → Nat → β → Tree β → Tree β
.node
left: Tree ?m.11563
left
key: Nat
key
value: ?m.11563
value
right: Tree ?m.11563
right
)

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 `term
lhs
:
term: Lean.Parser.Category
term
:max
rhs: Lean.TSyntax `term
rhs
:
term: Lean.Parser.Category
term
:max :
tactic: Lean.Parser.Category
tactic
=> `(tactic| (have h : $
lhs: Lean.TSyntax `term
lhs
= $
rhs: Lean.TSyntax `term
rhs
:= -- TODO: replace with linarith by simp_arith at *; apply Nat.le_antisymm <;> assumption try subst $
lhs: Lean.TSyntax `term
lhs
))

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 `term
e
:
term: Lean.Parser.Category
term
:
tactic: Lean.Parser.Category
tactic
=> `(tactic| by_cases $
e: Lean.TSyntax `term
e
<;> 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 t
h₁
:
ForallTree: {β : Type u_1} → (Nat → β → Prop) → Tree β → Prop
ForallTree
p: Nat → ?m.18602 → Prop
p
t: Tree ?m.18602
t
) (
h₂: p key value
h₂
:
p: Nat → ?m.18602 → Prop
p
key: Nat
key
value: ?m.18602
value
) :
ForallTree: {β : Type u_1} → (Nat → β → Prop) → Tree β → Prop
ForallTree
p: Nat → ?m.18602 → Prop
p
(
t: Tree ?m.18602
t
.
insert: {β : Type u_1} → Tree β → Nat → β → Tree β
insert
key: Nat
key
value: ?m.18602
value
) :=
β✝: Type u_1
p: Nat β Prop
t: Tree β
key: Nat
value: β
h₁: ForallTree p t
h₂: p key value

ForallTree p (insert t key value)
β✝: Type u_1
p: Nat β Prop
t: Tree β
key: Nat
value: β
h₁: ForallTree p t
h₂: p key value

ForallTree p (insert t key value)
β✝: Type u_1
p: Nat β Prop
t: Tree β
key: Nat
value: β
h₂: p key value

leaf
ForallTree p (insert leaf key value)

Goals accomplished! 🐙
β✝: Type u_1
p: Nat β Prop
t: Tree β
key: Nat
value: β
h₂: p key value
left✝: Tree β
key✝: Nat
value✝: β
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)

node
ForallTree p (insert (node left key value right) key value)
β✝: Type u_1
p: Nat β Prop
t: Tree β
key: Nat
value: β
h₂: p key value
left✝: Tree β
k: Nat
value✝: β
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)

node
ForallTree p (insert (node left k value right) key value)
β✝: Type u_1
p: Nat β Prop
t: Tree β
key: Nat
value: β
h₂: p key value
left✝: Tree β
k: Nat
value✝: β
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 < k

node.inl
ForallTree p (node (insert left key value) k value right)
β✝: Type u_1
p: Nat β Prop
t: Tree β
key: Nat
value: β
h₂: p key value
left✝: Tree β
k: Nat
value✝: β
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 < k
ForallTree p (if k < key then node left k value (insert right key value) else node left key value right)
β✝: Type u_1
p: Nat β Prop
t: Tree β
key: Nat
value: β
h₂: p key value
left✝: Tree β
k: Nat
value✝: β
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 < k

node.inl
ForallTree p (node (insert left key value) k value right)
β✝: Type u_1
p: Nat β Prop
t: Tree β
key: Nat
value: β
h₂: p key value
left✝: Tree β
k: Nat
value✝: β
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 < k
ForallTree p (if k < key then node left k value (insert right key value) else node left key value right)

Goals accomplished! 🐙
β✝: Type u_1
p: Nat β Prop
t: Tree β
key: Nat
value: β
h₂: p key value
left✝: Tree β
k: Nat
value✝: β
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 < k

node.inr
ForallTree p (if k < key then node left k value (insert right key value) else node left key value right)
β✝: Type u_1
p: Nat β Prop
t: Tree β
key: Nat
value: β
h₂: p key value
left✝: Tree β
k: Nat
value✝: β
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 < k
h✝: k < key

node.inr.inl
ForallTree p (node left k value (insert right key value))
β✝: Type u_1
p: Nat β Prop
t: Tree β
key: Nat
value: β
h₂: p key value
left✝: Tree β
k: Nat
value✝: β
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 < k
h✝: ¬k < key
ForallTree p (node left key value right)
β✝: Type u_1
p: Nat β Prop
t: Tree β
key: Nat
value: β
h₂: p key value
left✝: Tree β
k: Nat
value✝: β
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 < k
h✝: k < key

node.inr.inl
ForallTree p (node left k value (insert right key value))
β✝: Type u_1
p: Nat β Prop
t: Tree β
key: Nat
value: β
h₂: p key value
left✝: Tree β
k: Nat
value✝: β
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 < k
h✝: ¬k < key
ForallTree p (node left key value right)

Goals accomplished! 🐙
β✝: Type u_1
p: Nat β Prop
t: Tree β
key: Nat
value: β
h₂: p key value
left✝: Tree β
k: Nat
value✝: β
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 < k
h✝: ¬k < key

node.inr.inr
ForallTree p (node left key value right)
β✝: Type u_1
p: Nat β Prop
t: Tree β
value: β
left✝: Tree β
k: Nat
value✝: β
right✝: Tree β
hl: ForallTree p left
hp: p k value
hr: ForallTree p right
h₂: p k value
ihl: ForallTree p (insert left k value)
ihr: ForallTree p (insert right k value)
h✝¹, h✝: ¬k < k

node.inr.inr
ForallTree p (node left k value right)

Goals 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_1
Tree
β: Type u_1
β
} (
h: BST t
h
:
BST: {β : Type u_1} → Tree β → Prop
BST
t: Tree β
t
) (
key: Nat
key
:
Nat: Type
Nat
) (
value: β
value
:
β: Type u_1
β
) :
BST: {β : Type u_1} → Tree β → Prop
BST
(
t: Tree β
t
.
insert: {β : Type u_1} → Tree β → Nat → β → Tree β
insert
key: Nat
key
value: β
value
) :=
β: Type u_1
t: Tree β
h: BST t
key: Nat
value: β

BST (insert t key value)
β: Type u_1
t: Tree β
h: BST t
key: Nat
value: β

BST (insert t key value)
β: Type u_1
t: Tree β
key: Nat
value: β

leaf
BST (insert leaf key value)

Goals accomplished! 🐙
β: Type u_1
t: Tree β
key: Nat
value: β
key✝: Nat
left✝, 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)

node
BST (insert (node left key value right) key value)
β: Type u_1
t: Tree β
key: Nat
value: β
k: Nat
left✝, 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)

node
BST (insert (node left k value right) key value)
β: Type u_1
t: Tree β
key: Nat
value: β
k: Nat
left✝, 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)

node
BST (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)
β: Type u_1
t: Tree β
key: Nat
value: β
k: Nat
left✝, 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 < k

node.inl
BST (node (insert left key value) k value right)
β: Type u_1
t: Tree β
key: Nat
value: β
k: Nat
left✝, 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 < k
BST (if k < key then node left k value (insert right key value) else node left key value right)
β: Type u_1
t: Tree β
key: Nat
value: β
k: Nat
left✝, 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 < k

node.inl
BST (node (insert left key value) k value right)
β: Type u_1
t: Tree β
key: Nat
value: β
k: Nat
left✝, 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 < k
BST (if k < key then node left k value (insert right key value) else node left key value right)

Goals accomplished! 🐙
β: Type u_1
t: Tree β
key: Nat
value: β
k: Nat
left✝, 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 < k

node.inr
BST (if k < key then node left k value (insert right key value) else node left key value right)
β: Type u_1
t: Tree β
key: Nat
value: β
k: Nat
left✝, 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 < k
h✝: k < key

node.inr.inl
BST (node left k value (insert right key value))
β: Type u_1
t: Tree β
key: Nat
value: β
k: Nat
left✝, 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 < k
h✝: ¬k < key
BST (node left key value right)
β: Type u_1
t: Tree β
key: Nat
value: β
k: Nat
left✝, 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 < k
h✝: k < key

node.inr.inl
BST (node left k value (insert right key value))
β: Type u_1
t: Tree β
key: Nat
value: β
k: Nat
left✝, 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 < k
h✝: ¬k < key
BST (node left key value right)

Goals accomplished! 🐙
β: Type u_1
t: Tree β
key: Nat
value: β
k: Nat
left✝, 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 < k
h✝: ¬k < key

node.inr.inr
BST (node left key value right)
β: Type u_1
t: Tree β
value: β
k: Nat
left✝, 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 < k

node.inr.inr
BST (node left k value right)

Goals accomplished! 🐙

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

def 
BinTree: Type u → Type u
BinTree
(
β: Type u
β
:
Type u: Type (u + 1)
Type u
) := {
t: Tree β
t
:
Tree: Type u → Type u
Tree
β: Type u
β
//
BST: {β : Type u} → Tree β → Prop
BST
t: Tree β
t
} def
BinTree.mk: {β : Type u_1} → BinTree β
BinTree.mk
:
BinTree: Type u_1 → Type u_1
BinTree
β: 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 → Bool
BinTree.contains
(
b: BinTree β
b
:
BinTree: Type u_1 → Type u_1
BinTree
β: Type u_1
β
) (
k: Nat
k
:
Nat: Type
Nat
) :
Bool: Type
Bool
:=
b: BinTree β
b
.
val: {α : Type u_1} → {p : α → Prop} → Subtype p → α
val
.
contains: {β : Type u_1} → Tree β → Nat → Bool
contains
k: Nat
k
def
BinTree.find?: {β : Type u_1} → BinTree β → Nat → Option β
BinTree.find?
(
b: BinTree β
b
:
BinTree: Type u_1 → Type u_1
BinTree
β: Type u_1
β
) (
k: Nat
k
:
Nat: Type
Nat
) :
Option: Type u_1 → Type u_1
Option
β: Type u_1
β
:=
b: BinTree β
b
.
val: {α : Type u_1} → {p : α → Prop} → Subtype p → α
val
.
find?: {β : Type u_1} → Tree β → Nat → Option β
find?
k: Nat
k
def
BinTree.insert: {β : Type u_1} → BinTree β → Nat → β → BinTree β
BinTree.insert
(
b: BinTree β
b
:
BinTree: Type u_1 → Type u_1
BinTree
β: Type u_1
β
) (
k: Nat
k
:
Nat: Type
Nat
) (
v: β
v
:
β: Type u_1
β
) :
BinTree: Type u_1 → Type u_1
BinTree
β: Type u_1
β
:= ⟨
b: BinTree β
b
.
val: {α : Type u_1} → {p : α → Prop} → Subtype p → α
val
.
insert: {β : Type u_1} → Tree β → Nat → β → Tree β
insert
k: Nat
k
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.val
property
k: Nat
k
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 → Bool
BinTree.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 → Bool
Tree.contains
Tree.insert: {β : Type u_1} → Tree β → Nat → β → Tree β
Tree.insert
theorem
BinTree.find_mk: ∀ {β : Type u_1} (k : Nat), find? mk k = none
BinTree.find_mk
(
k: Nat
k
:
Nat: Type
Nat
) :
BinTree.mk: {β : Type u_1} → BinTree β
BinTree.mk
.
find?: {β : Type u_1} → BinTree β → Nat → Option β
find?
k: Nat
k
= (
none: {α : Type u_1} → Option α
none
:
Option: Type u_1 → Type u_1
Option
β: Type u_1
β
) :=
β: Type u_1
k: Nat

find? mk k = none

Goals accomplished! 🐙
theorem
BinTree.find_insert: ∀ {β : Type u_1} (b : BinTree β) (k : Nat) (v : β), find? (insert b k v) k = some v
BinTree.find_insert
(
b: BinTree β
b
:
BinTree: Type u_1 → Type u_1
BinTree
β: Type u_1
β
) (
k: Nat
k
:
Nat: Type
Nat
) (
v: β
v
:
β: Type u_1
β
) : (
b: BinTree β
b
.
insert: {β : Type u_1} → BinTree β → Nat → β → BinTree β
insert
k: Nat
k
v: β
v
).
find?: {β : Type u_1} → BinTree β → Nat → Option β
find?
k: Nat
k
=
some: {α : Type u_1} → α → Option α
some
v: β
v
:=
β: Type u_1
b: BinTree β
k: Nat
v: β

find? (insert b k v) k = some v
β: Type u_1
b: BinTree β
k: Nat
v: β
t: Tree β
h: BST t

find? (insert { val := t, property := h } k v) k = some v
;
β: Type u_1
b: BinTree β
k: Nat
v: β
t: Tree β
h: BST t

Tree.find? (Tree.insert t k v) k = some v
β: Type u_1
b: BinTree β
k: Nat
v: β
t: Tree β
h: BST t

Tree.find? (Tree.insert t k v) k = some v

Goals accomplished! 🐙
β: Type u_1
b: BinTree β
k: Nat
v: β
left: Tree β
key: Nat
value: β
right: Tree β
ihl: BST left Tree.find? (Tree.insert left k v) k = some v
ihr: BST right Tree.find? (Tree.insert right k v) k = some v
h: BST (Tree.node left key value right)

node
Tree.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
β: Type u_1
b: BinTree β
k: Nat
v: β
left: Tree β
key: Nat
value: β
right: Tree β
ihl: BST left Tree.find? (Tree.insert left k v) k = some v
ihr: BST right Tree.find? (Tree.insert right k v) k = some v
h: BST (Tree.node left key value right)
h✝: k < key

node.inl
Tree.find? (Tree.insert left k v) k = some v
β: Type u_1
b: BinTree β
k: Nat
v: β
left: Tree β
key: Nat
value: β
right: Tree β
ihl: BST left Tree.find? (Tree.insert left k v) k = some v
ihr: BST right Tree.find? (Tree.insert right k v) k = some v
h: BST (Tree.node left key value right)
h✝: ¬k < key
Tree.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_1
b: BinTree β
k: Nat
v: β
left: Tree β
key: Nat
value: β
right: Tree β
ihl: BST left Tree.find? (Tree.insert left k v) k = some v
ihr: BST right Tree.find? (Tree.insert right k v) k = some v
h: BST (Tree.node left key value right)
h✝: k < key

node.inl
Tree.find? (Tree.insert left k v) k = some v
β: Type u_1
b: BinTree β
k: Nat
v: β
left: Tree β
key: Nat
value: β
right: Tree β
ihl: BST left Tree.find? (Tree.insert left k v) k = some v
ihr: BST right Tree.find? (Tree.insert right k v) k = some v
h: BST (Tree.node left key value right)
h✝: ¬k < key
Tree.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_1
b: BinTree β
k: Nat
v: β
left: Tree β
key: Nat
value: β
right: Tree β
ihl: BST left Tree.find? (Tree.insert left k v) k = some v
ihr: BST right Tree.find? (Tree.insert right k v) k = some v
h✝: k < key
a✝³: BST left
a✝²: ForallTree (fun k v => k < key) left
a✝¹: BST right
a✝: ForallTree (fun k v => key < k) right

node.inl.node
Tree.find? (Tree.insert left k v) k = some v
;
β: Type u_1
b: BinTree β
k: Nat
v: β
left: Tree β
key: Nat
value: β
right: Tree β
ihl: BST left Tree.find? (Tree.insert left k v) k = some v
ihr: BST right Tree.find? (Tree.insert right k v) k = some v
h✝: k < key
a✝³: BST left
a✝²: ForallTree (fun k v => k < key) left
a✝¹: BST right
a✝: ForallTree (fun k v => key < k) right

node.inl.node
BST left
;

Goals accomplished! 🐙
β: Type u_1
b: BinTree β
k: Nat
v: β
left: Tree β
key: Nat
value: β
right: Tree β
ihl: BST left Tree.find? (Tree.insert left k v) k = some v
ihr: BST right Tree.find? (Tree.insert right k v) k = some v
h: BST (Tree.node left key value right)
h✝: ¬k < key

node.inr
Tree.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_1
b: BinTree β
k: Nat
v: β
left: Tree β
key: Nat
value: β
right: Tree β
ihl: BST left Tree.find? (Tree.insert left k v) k = some v
ihr: BST right Tree.find? (Tree.insert right k v) k = some v
h: BST (Tree.node left key value right)
h✝¹: ¬k < key
h✝: key < k

node.inr.inl
Tree.find? (Tree.insert right k v) k = some v
β: Type u_1
b: BinTree β
k: Nat
v: β
left: Tree β
key: Nat
value: β
right: Tree β
ihl: BST left Tree.find? (Tree.insert left k v) k = some v
ihr: BST right Tree.find? (Tree.insert right k v) k = some v
h✝¹: ¬k < key
h✝: key < k
a✝³: BST left
a✝²: ForallTree (fun k v => k < key) left
a✝¹: BST right
a✝: ForallTree (fun k v => key < k) right

node.inr.inl.node
Tree.find? (Tree.insert right k v) k = some v
;
β: Type u_1
b: BinTree β
k: Nat
v: β
left: Tree β
key: Nat
value: β
right: Tree β
ihl: BST left Tree.find? (Tree.insert left k v) k = some v
ihr: BST right Tree.find? (Tree.insert right k v) k = some v
h✝¹: ¬k < key
h✝: key < k
a✝³: BST left
a✝²: ForallTree (fun k v => k < key) left
a✝¹: BST right
a✝: ForallTree (fun k v => key < k) right

node.inr.inl.node
BST right
;

Goals 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_1
BinTree
β: Type u_1
β
) (
h: k ≠ k'
h
:
k: Nat
k
k': Nat
k'
) (
v: β
v
:
β: Type u_1
β
) : (
b: BinTree β
b
.
insert: {β : Type u_1} → BinTree β → Nat → β → BinTree β
insert
k: Nat
k
v: β
v
).
find?: {β : Type u_1} → BinTree β → Nat → Option β
find?
k': Nat
k'
=
b: BinTree β
b
.
find?: {β : Type u_1} → BinTree β → Nat → Option β
find?
k': Nat
k'
:=
β: Type u_1
k, k': Nat
b: BinTree β
h: k k'
v: β

find? (insert b k v) k' = find? b k'
β: Type u_1
k, k': Nat
b: BinTree β
h✝: k k'
v: β
t: Tree β
h: BST t

find? (insert { val := t, property := h } k v) k' = find? { val := t, property := h } k'
;
β: Type u_1
k, k': Nat
b: BinTree β
h✝: k k'
v: β
t: Tree β
h: BST t

Tree.find? (Tree.insert t k v) k' = Tree.find? t k'
β: Type u_1
k, k': Nat
b: BinTree β
h✝: k k'
v: β
t: Tree β
h: BST t

Tree.find? (Tree.insert t k v) k' = Tree.find? t k'
β: Type u_1
k, k': Nat
b: BinTree β
h✝: k k'
v: β
h: BST Tree.leaf

leaf
(if k' < k then none else if k < k' then none else some v) = none
β: Type u_1
k, k': Nat
b: BinTree β
h✝: k k'
v: β
h: BST Tree.leaf

leaf
(if k' < k then none else if k < k' then none else some v) = none
β: Type u_1
k, k': Nat
b: BinTree β
h✝¹: k k'
v: β
h: BST Tree.leaf
h✝: k' < k

leaf.inl
none = none
β: Type u_1
k, k': Nat
b: BinTree β
h✝¹: k k'
v: β
h: BST Tree.leaf
h✝: ¬k' < k
(if k < k' then none else some v) = none
β: Type u_1
k, k': Nat
b: BinTree β
h✝¹: k k'
v: β
h: BST Tree.leaf
h✝: k' < k

leaf.inl
none = none
β: Type u_1
k, k': Nat
b: BinTree β
h✝¹: k k'
v: β
h: BST Tree.leaf
h✝: ¬k' < k
(if k < k' then none else some v) = none

Goals accomplished! 🐙
β: Type u_1
k, k': Nat
b: BinTree β
h✝¹: k k'
v: β
h: BST Tree.leaf
h✝: ¬k' < k

leaf.inr
(if k < k' then none else some v) = none
β: Type u_1
k, k': Nat
b: BinTree β
h✝²: k k'
v: β
h: BST Tree.leaf
h✝¹: ¬k' < k
h✝: k < k'

leaf.inr.inl
none = none
β: Type u_1
k, k': Nat
b: BinTree β
h✝²: k k'
v: β
h: BST Tree.leaf
h✝¹: ¬k' < k
h✝: ¬k < k'
False
β: Type u_1
k, k': Nat
b: BinTree β
h✝²: k k'
v: β
h: BST Tree.leaf
h✝¹: ¬k' < k
h✝: k < k'

leaf.inr.inl
none = none
β: Type u_1
k, k': Nat
b: BinTree β
h✝²: k k'
v: β
h: BST Tree.leaf
h✝¹: ¬k' < k
h✝: ¬k < k'
False

Goals accomplished! 🐙
β: Type u_1
k': Nat
b: BinTree β
v: β
h✝²: BST Tree.leaf
h: k' k'
h✝¹, h✝: ¬k' < k'

leaf.inr.inr
False

Goals accomplished! 🐙
β: Type u_1
k, k': Nat
b: BinTree β
h✝: k k'
v: β
left: Tree β
key: Nat
value: β
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)

node
Tree.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
β: Type u_1
k, k': Nat
b: BinTree β
h✝: k k'
v: β
left: Tree β
key: Nat
value: β
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) left
hr: ForallTree (fun k v => key < k) right
bl: BST left
br: BST right

node
Tree.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
β: Type u_1
k, k': Nat
b: BinTree β
h✝: k k'
v: β
left: Tree β
key: Nat
value: β
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) left
hr: ForallTree (fun k v => key < k) right
bl: BST left
br: BST right
ihl: Tree.find? (Tree.insert left k v) k' = Tree.find? left k'

node
Tree.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
β: Type u_1
k, k': Nat
b: BinTree β
h✝: k k'
v: β
left: Tree β
key: Nat
value: β
right: Tree β
h: BST (Tree.node left key value right)
hl: ForallTree (fun k v => k < key) left
hr: ForallTree (fun k v => key < k) right
bl: BST left
br: BST right
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'

node
Tree.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
β: Type u_1
k, k': Nat
b: BinTree β
h✝¹: k k'
v: β
left: Tree β
key: Nat
value: β
right: Tree β
h: BST (Tree.node left key value right)
hl: ForallTree (fun k v => k < key) left
hr: ForallTree (fun k v => key < k) right
bl: BST left
br: BST right
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✝: ¬k < key

node.inr
Tree.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
;
β: Type u_1
k, k': Nat
b: BinTree β
h✝²: k k'
v: β
left: Tree β
key: Nat
value: β
right: Tree β
h: BST (Tree.node left key value right)
hl: ForallTree (fun k v => k < key) left
hr: ForallTree (fun k v => key < k) right
bl: BST left
br: BST right
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✝¹: ¬k < key
h✝: ¬key < k

node.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
β: Type u_1
k, k': Nat
b: BinTree β
h✝²: k k'
v: β
left: Tree β
value: β
right: Tree β
bl: BST left
br: BST right
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_1 v => k_1 < k) left
hr: ForallTree (fun k_1 v => k < k_1) right
h✝¹, h✝: ¬k < k

node.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
β: Type u_1
k, k': Nat
b: BinTree β
h✝³: k k'
v: β
left: Tree β
value: β
right: Tree β
bl: BST left
br: BST right
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_1 v => k_1 < k) left
hr: ForallTree (fun k_1 v => k < k_1) right
h✝², h✝¹: ¬k < k
h✝: ¬k' < k

node.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
;
β: Type u_1
k, k': Nat
b: BinTree β
h✝⁴: k k'
v: β
left: Tree β
value: β
right: Tree β
bl: BST left
br: BST right
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_1 v => k_1 < k) left
hr: ForallTree (fun k_1 v => k < k_1) right
h✝³, h✝²: ¬k < k
h✝¹: ¬k' < k
h✝: ¬k < k'

node.inr.inr.inr.inr
v = value
β: Type u_1
k': Nat
b: BinTree β
v: β
left: Tree β
value: β
right: Tree β
bl: BST left
br: BST right
h✝⁴: 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') left
hr: ForallTree (fun k v => k' < k) right
h✝³, h✝², h✝¹, h✝: ¬k' < k'

node.inr.inr.inr.inr
v = value

Goals accomplished! 🐙