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 "Software 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.1354} → Tree β
leaf => false: Bool
false
  | node: {β : Type ?u.1363} → Tree β → Nat → β → Tree β → Tree β
node left: Tree β
left key: Nat
key value: β
valueWarning: unused variable `value`
note: this linter can be disabled with `set_option linter.unusedVariables false` 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.1655} → Tree β
leaf => none: {α : Type u_1} → Option α
none
  | node: {β : Type ?u.1667} → 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.1964} → 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.1979} → 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.2298} → Tree β
leaf => []: List (Nat × β)
[]
  | node: {β : Type ?u.2310} → 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

#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: 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"

#eval[(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 implementation 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 concatenations 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.3168} → Tree β
leaf => acc: List (Nat × β)
acc
    | node: {β : Type ?u.3178} → 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 * instructs 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 instructs the simplifier to use the List.append_assoc theorem as a rewriting rule.

theorem Tree.toList_eq_toListTR: ∀ {β : Type u_1} (t : Tree β), t.toList = t.toListTR
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 := byGoals accomplished! 🐙
  simp [toListTR: {β : Type ?u.4147} → Tree β → List (Nat × β)
toListTR, go: ∀ (t : Tree β) (acc : List (Nat × β)), toListTR.go t acc = t.toList ++ acc
go t: Tree β
t []: List (Nat × β)
[]]Goals accomplished! 🐙
where
  go: ∀ {β : Type u_1} (t : Tree β) (acc : List (Nat × β)), toListTR.go t acc = t.toList ++ 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 := byGoals accomplished! 🐙
    induction t: Tree β
t generalizing acc: List (Nat × β)
accβ: Type u_1
t: Tree β
acc: List (Nat × β)
leaftoListTR.go leaf acc = leaf.toList ++ acc
β: Type u_1
t, left✝: Tree β
key✝: Nat
value✝: β
right✝: Tree β
left_ih✝: ∀ (acc : List (Nat × β)), toListTR.go left✝ acc = left✝.toList ++ acc
right_ih✝: ∀ (acc : List (Nat × β)), toListTR.go right✝ acc = right✝.toList ++ acc
acc: List (Nat × β)
nodetoListTR.go (left✝.node key✝ value✝ right✝) acc = (left✝.node key✝ value✝ right✝).toList ++ acc <;>β: Type u_1
t: Tree β
acc: List (Nat × β)
leaftoListTR.go leaf acc = leaf.toList ++ acc
β: Type u_1
t, left✝: Tree β
key✝: Nat
value✝: β
right✝: Tree β
left_ih✝: ∀ (acc : List (Nat × β)), toListTR.go left✝ acc = left✝.toList ++ acc
right_ih✝: ∀ (acc : List (Nat × β)), toListTR.go right✝ acc = right✝.toList ++ acc
acc: List (Nat × β)
nodetoListTR.go (left✝.node key✝ value✝ right✝) acc = (left✝.node key✝ value✝ right✝).toList ++ acc
      simp [toListTR.go: {β : Type ?u.4003} → Tree β → List (Nat × β) → List (Nat × β)
toListTR.go, toList: {β : Type ?u.4021} → Tree β → List (Nat × β)
toList, *, List.append_assoc: ∀ {α : Type ?u.4035} (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 = @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 := byGoals accomplished! 🐙
  funext β: Type u_1
β t: Tree β
tβ: Type u_1
t: Tree β
h.ht.toList = t.toListTR
  apply toList_eq_toListTR: ∀ {β : Type u_1} (t : Tree β), t.toList = t.toListTR
toList_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 β → 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 (left.node 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 (left.node key value right)
node :
     ForallTree: {β : Type u_1} → (Nat → β → Prop) → Tree β → Prop
ForallTree (fun k: Nat
k v: ?m.4990
vWarning: unused variable `v`
note: this linter can be disabled with `set_option linter.unusedVariables false` => k: Nat
k < key: Nat
key) left: Tree ?m.4990
left →
     ForallTree: {β : Type u_1} → (Nat → β → Prop) → Tree β → Prop
ForallTree (fun k: Nat
k v: ?m.4990
vWarning: unused variable `v`
note: this linter can be disabled with `set_option linter.unusedVariables false` => key: Nat
key < k: Nat
k) right: Tree ?m.4990
right →
     BST: {β : Type u_1} → Tree β → Prop
BST left: Tree ?m.4990
left → BST: {β : Type u_1} → Tree β → Prop
BST right: Tree ?m.4990
right →
     BST: {β : Type u_1} → Tree β → Prop
BST (.node: {β : Type u_1} → Tree β → Nat → β → Tree β → Tree β
.node left: Tree ?m.4990
left key: Nat
key value: ?m.4990
value right: Tree ?m.4990
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 simplifier 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 (t.insert key value)
Tree.forall_insert_of_forall
        (h₁: ForallTree p t
h₁ : ForallTree: {β : Type u_1} → (Nat → β → Prop) → Tree β → Prop
ForallTree p: Nat → ?m.6770 → Prop
p t: Tree ?m.6770
t) (h₂: p key value
h₂ : p: Nat → ?m.6770 → Prop
p key: Nat
key value: ?m.6770
value)
        : ForallTree: {β : Type u_1} → (Nat → β → Prop) → Tree β → Prop
ForallTree p: Nat → ?m.6770 → Prop
p (t: Tree ?m.6770
t.insert: {β : Type u_1} → Tree β → Nat → β → Tree β
insert key: Nat
key value: ?m.6770
value) := byGoals accomplished! 🐙
  induction h₁: ForallTree p t
h₁ withβ✝: Type u_1
p: Nat → β✝ → Prop
t: Tree β✝
key: Nat
value: β✝
h₁: ForallTree p t
h₂: p key value
ForallTree p (t.insert key value)
  | leaf: ∀ {β : Type u_1} {p : Nat → β → Prop}, ForallTree p leaf
leaf =>Goals accomplished! 🐙 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 (left.node key value right)
.node .leaf: ∀ {β : Type u_1} {p : Nat → β → Prop}, ForallTree p leaf
.leaf h₂: p key value
h₂ .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 (left.node key value right)
node hl: ForallTree p left✝
hl hp: p key✝ value✝
hp hr: ForallTree p right✝
hr ihl: ForallTree p (left✝.insert key value)
ihl ihr: ForallTree p (right✝.insert key value)
ihr =>Goals accomplished! 🐙
    rename Nat: Type
Nat => kβ✝: 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 (left✝.insert key value)
ihr: ForallTree p (right✝.insert key value)
nodeForallTree p ((left✝.node k value✝ right✝).insert key value)
    by_cases' key: Nat
key < k: Nat
kβ✝: 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 (left✝.insert key value)
ihr: ForallTree p (right✝.insert key value)
h✝: key < k
posForallTree p ((left✝.insert key value).node 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 (left✝.insert key value)
ihr: ForallTree p (right✝.insert key value)
h✝: ¬key < k
negForallTree p (if k < key then left✝.node k value✝ (right✝.insert key value) else left✝.node 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 (left✝.insert key value)
ihr: ForallTree p (right✝.insert key value)
h✝: key < k
posForallTree p ((left✝.insert key value).node 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 (left.node key value right)
.node ihl: ForallTree p (left✝.insert key value)
ihl hp: p k value✝
hp hr: ForallTree p right✝
hrGoals 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 (left✝.insert key value)
ihr: ForallTree p (right✝.insert key value)
h✝: ¬key < k
negForallTree p (if k < key then left✝.node k value✝ (right✝.insert key value) else left✝.node key value right✝) by_cases' k: Nat
k < key: Nat
keyβ✝: 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 (left✝.insert key value)
ihr: ForallTree p (right✝.insert key value)
h✝¹: ¬key < k
h✝: k < key
posForallTree p (left✝.node k value✝ (right✝.insert 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 (left✝.insert key value)
ihr: ForallTree p (right✝.insert key value)
h✝¹: ¬key < k
h✝: ¬k < key
negForallTree p (left✝.node 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 (left✝.insert key value)
ihr: ForallTree p (right✝.insert key value)
h✝¹: ¬key < k
h✝: k < key
posForallTree p (left✝.node k value✝ (right✝.insert 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 (left.node key value right)
.node hl: ForallTree p left✝
hl hp: p k value✝
hp ihr: ForallTree p (right✝.insert key value)
ihrGoals 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 (left✝.insert key value)
ihr: ForallTree p (right✝.insert key value)
h✝¹: ¬key < k
h✝: ¬k < key
negForallTree p (left✝.node key value right✝) have_eq key: Nat
key k: Nat
kβ✝: 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 (left✝.insert k value)
ihr: ForallTree p (right✝.insert k value)
h✝¹, h✝: ¬k < k
negForallTree p (left✝.node 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 (left.node key value right)
.node hl: ForallTree p left✝
hl h₂: p k value
h₂ hr: ForallTree p right✝
hrGoals accomplished! 🐙

theorem Tree.bst_insert_of_bst: ∀ {β : Type u_1} {t : Tree β}, BST t → ∀ (key : Nat) (value : β), BST (t.insert 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) := byGoals accomplished! 🐙
  induction h: BST t
h withβ: Type u_1
t: Tree β
h: BST t
key: Nat
value: β
BST (t.insert key value)
  | leaf: ∀ {β : Type u_1}, BST leaf
leaf =>Goals accomplished! 🐙 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 (left.node 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 (left.node 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 (left✝.insert key value)
ih₁ ih₂: BST (right✝.insert key value)
ih₂ =>Goals accomplished! 🐙
    rename Nat: Type
Nat => kβ: 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 (left✝.insert key value)
ih₂: BST (right✝.insert key value)
nodeBST ((left✝.node k value✝ right✝).insert key value)
    simpβ: 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 (left✝.insert key value)
ih₂: BST (right✝.insert key value)
nodeBST
  (if key < k then (left✝.insert key value).node k value✝ right✝
  else if k < key then left✝.node k value✝ (right✝.insert key value) else left✝.node key value right✝)
    by_cases' key: Nat
key < k: Nat
kβ: 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 (left✝.insert key value)
ih₂: BST (right✝.insert key value)
h✝: key < k
posBST ((left✝.insert key value).node 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 (left✝.insert key value)
ih₂: BST (right✝.insert key value)
h✝: ¬key < k
negBST (if k < key then left✝.node k value✝ (right✝.insert key value) else left✝.node 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 (left✝.insert key value)
ih₂: BST (right✝.insert key value)
h✝: key < k
posBST ((left✝.insert key value).node 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 (left.node 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 (t.insert 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 (left✝.insert key value)
ih₁ b₂: BST right✝
b₂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 (left✝.insert key value)
ih₂: BST (right✝.insert key value)
h✝: ¬key < k
negBST (if k < key then left✝.node k value✝ (right✝.insert key value) else left✝.node key value right✝) by_cases' k: Nat
k < key: Nat
keyβ: 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 (left✝.insert key value)
ih₂: BST (right✝.insert key value)
h✝¹: ¬key < k
h✝: k < key
posBST (left✝.node k value✝ (right✝.insert 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 (left✝.insert key value)
ih₂: BST (right✝.insert key value)
h✝¹: ¬key < k
h✝: ¬k < key
negBST (left✝.node 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 (left✝.insert key value)
ih₂: BST (right✝.insert key value)
h✝¹: ¬key < k
h✝: k < key
posBST (left✝.node k value✝ (right✝.insert 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 (left.node 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 (t.insert 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 (right✝.insert key value)
ih₂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 (left✝.insert key value)
ih₂: BST (right✝.insert key value)
h✝¹: ¬key < k
h✝: ¬k < key
negBST (left✝.node key value right✝) have_eq key: Nat
key k: Nat
kβ: 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 (left✝.insert k value)
ih₂: BST (right✝.insert k value)
h✝¹, h✝: ¬k < k
negBST (left✝.node 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 (left.node 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 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 (t.insert 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), mk.find? 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
β) := byGoals accomplished! 🐙
  simpGoals accomplished! 🐙

theorem BinTree.find_insert: ∀ {β : Type u_1} (b : BinTree β) (k : Nat) (v : β), (b.insert k v).find? 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 := byGoals accomplished! 🐙
  let ⟨t: Tree β
t, h: BST t
h⟩ := b: BinTree β
bβ: Type u_1
b: BinTree β
k: Nat
v: β
t: Tree β
h: BST t
(insert ⟨t, h⟩ k v).find? k = some v; simpβ: Type u_1
b: BinTree β
k: Nat
v: β
t: Tree β
h: BST t
(t.insert k v).find? k = some v
  induction t: Tree β
t withβ: Type u_1
b: BinTree β
k: Nat
v: β
t: Tree β
h: BST t
(t.insert k v).find? k = some v simpβ: Type u_1
b: BinTree β
k: Nat
v: β
left: Tree β
key: Nat
value: β
right: Tree β
ihl: BST left → (left.insert k v).find? k = some v
ihr: BST right → (right.insert k v).find? k = some v
h: BST (left.node key value right)
node(if k < key then (left.insert k v).node key value right
      else if key < k then left.node key value (right.insert k v) else left.node k v right).find?
    k =
  some v
  | node: {β : Type v} → Tree β → Nat → β → Tree β → Tree β
node left: Tree β
left key: Nat
key value: β
value right: Tree β
right ihl: BST left → (left.insert k v).find? k = some v
ihl ihr: BST right → (right.insert k v).find? k = some v
ihr =>Goals accomplished! 🐙
    by_cases' k: Nat
k < key: Nat
keyβ: Type u_1
b: BinTree β
k: Nat
v: β
left: Tree β
key: Nat
value: β
right: Tree β
ihl: BST left → (left.insert k v).find? k = some v
ihr: BST right → (right.insert k v).find? k = some v
h: BST (left.node key value right)
h✝: k < key
pos(left.insert k v).find? k = some v
β: Type u_1
b: BinTree β
k: Nat
v: β
left: Tree β
key: Nat
value: β
right: Tree β
ihl: BST left → (left.insert k v).find? k = some v
ihr: BST right → (right.insert k v).find? k = some v
h: BST (left.node key value right)
h✝: ¬k < key
neg(if key < k then left.node key value (right.insert k v) else left.node k v right).find? k = some v
    .β: Type u_1
b: BinTree β
k: Nat
v: β
left: Tree β
key: Nat
value: β
right: Tree β
ihl: BST left → (left.insert k v).find? k = some v
ihr: BST right → (right.insert k v).find? k = some v
h: BST (left.node key value right)
h✝: k < key
pos(left.insert k v).find? k = some v cases h: BST (left.node key value right)
hβ: Type u_1
b: BinTree β
k: Nat
v: β
left: Tree β
key: Nat
value: β
right: Tree β
ihl: BST left → (left.insert k v).find? k = some v
ihr: BST right → (right.insert k v).find? 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
pos.node(left.insert k v).find? k = some v; apply ihl: BST left → (left.insert k v).find? k = some v
ihlβ: Type u_1
b: BinTree β
k: Nat
v: β
left: Tree β
key: Nat
value: β
right: Tree β
ihl: BST left → (left.insert k v).find? k = some v
ihr: BST right → (right.insert k v).find? 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
pos.nodeBST left; assumptionGoals accomplished! 🐙
    .β: Type u_1
b: BinTree β
k: Nat
v: β
left: Tree β
key: Nat
value: β
right: Tree β
ihl: BST left → (left.insert k v).find? k = some v
ihr: BST right → (right.insert k v).find? k = some v
h: BST (left.node key value right)
h✝: ¬k < key
neg(if key < k then left.node key value (right.insert k v) else left.node k v right).find? k = some v by_cases' key: Nat
key < k: Nat
kβ: Type u_1
b: BinTree β
k: Nat
v: β
left: Tree β
key: Nat
value: β
right: Tree β
ihl: BST left → (left.insert k v).find? k = some v
ihr: BST right → (right.insert k v).find? k = some v
h: BST (left.node key value right)
h✝¹: ¬k < key
h✝: key < k
pos(right.insert k v).find? k = some v
      cases h: BST (left.node key value right)
hβ: Type u_1
b: BinTree β
k: Nat
v: β
left: Tree β
key: Nat
value: β
right: Tree β
ihl: BST left → (left.insert k v).find? k = some v
ihr: BST right → (right.insert k v).find? 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
pos.node(right.insert k v).find? k = some v; apply ihr: BST right → (right.insert k v).find? k = some v
ihrβ: Type u_1
b: BinTree β
k: Nat
v: β
left: Tree β
key: Nat
value: β
right: Tree β
ihl: BST left → (left.insert k v).find? k = some v
ihr: BST right → (right.insert k v).find? 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
pos.nodeBST right; assumptionGoals accomplished! 🐙

theorem BinTree.find_insert_of_ne: ∀ {β : Type u_1} {k k' : Nat} (b : BinTree β), k ≠ k' → ∀ (v : β), (b.insert k v).find? k' = b.find? k'
BinTree.find_insert_of_ne (b: BinTree β
b : BinTree: Type u_1 → Type u_1
BinTree β: Type u_1
β) (ne: k ≠ k'
ne : 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' := byGoals accomplished! 🐙
  let ⟨t: Tree β
t, h: BST t
h⟩ := b: BinTree β
bβ: Type u_1
k, k': Nat
b: BinTree β
ne: k ≠ k'
v: β
t: Tree β
h: BST t
(insert ⟨t, h⟩ k v).find? k' = find? ⟨t, h⟩ k'; simpβ: Type u_1
k, k': Nat
b: BinTree β
ne: k ≠ k'
v: β
t: Tree β
h: BST t
(t.insert k v).find? k' = t.find? k'
  induction t: Tree β
t withβ: Type u_1
k, k': Nat
b: BinTree β
ne: k ≠ k'
v: β
t: Tree β
h: BST t
(t.insert k v).find? k' = t.find? k' simpβ: Type u_1
k, k': Nat
b: BinTree β
ne: k ≠ k'
v: β
left: Tree β
key: Nat
value: β
right: Tree β
ihl: BST left → (left.insert k v).find? k' = left.find? k'
ihr: BST right → (right.insert k v).find? k' = right.find? k'
h: BST (left.node key value right)
node(if k < key then (left.insert k v).node key value right
      else if key < k then left.node key value (right.insert k v) else left.node k v right).find?
    k' =
  if k' < key then left.find? k' else if key < k' then right.find? k' else some value
  | leaf: {β : Type v} → Tree β
leaf =>Goals accomplished! 🐙
    intros le: k ≤ k'
leβ: Type u_1
k, k': Nat
b: BinTree β
ne: k ≠ k'
v: β
h: BST Tree.leaf
le: k ≤ k'
leafk < k'
    exact Nat.lt_of_le_of_ne: ∀ {n m : Nat}, n ≤ m → ¬n = m → n < m
Nat.lt_of_le_of_ne le: k ≤ k'
le ne: k ≠ k'
neGoals accomplished! 🐙
  | node: {β : Type v} → Tree β → Nat → β → Tree β → Tree β
node left: Tree β
left key: Nat
key value: β
value right: Tree β
right ihl: BST left → (left.insert k v).find? k' = left.find? k'
ihl ihr: BST right → (right.insert k v).find? k' = right.find? k'
ihr =>Goals accomplished! 🐙
    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 (left.node key value right)
.node hl: ForallTree (fun k v => k < key) left
hl hr: ForallTree (fun k v => key < k) right
hr bl: BST left
bl br: BST right
br := h: BST (left.node key value right)
hβ: Type u_1
k, k': Nat
b: BinTree β
ne: k ≠ k'
v: β
left: Tree β
key: Nat
value: β
right: Tree β
ihl: BST left → (left.insert k v).find? k' = left.find? k'
ihr: BST right → (right.insert k v).find? k' = right.find? k'
h: BST (left.node 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(if k < key then (left.insert k v).node key value right
      else if key < k then left.node key value (right.insert k v) else left.node k v right).find?
    k' =
  if k' < key then left.find? k' else if key < k' then right.find? k' else some value
    specialize ihl: BST left → (left.insert k v).find? k' = left.find? k'
ihl bl: BST left
blβ: Type u_1
k, k': Nat
b: BinTree β
ne: k ≠ k'
v: β
left: Tree β
key: Nat
value: β
right: Tree β
ihr: BST right → (right.insert k v).find? k' = right.find? k'
h: BST (left.node 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: (left.insert k v).find? k' = left.find? k'
node(if k < key then (left.insert k v).node key value right
      else if key < k then left.node key value (right.insert k v) else left.node k v right).find?
    k' =
  if k' < key then left.find? k' else if key < k' then right.find? k' else some value
    specialize ihr: BST right → (right.insert k v).find? k' = right.find? k'
ihr br: BST right
brβ: Type u_1
k, k': Nat
b: BinTree β
ne: k ≠ k'
v: β
left: Tree β
key: Nat
value: β
right: Tree β
h: BST (left.node 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: (left.insert k v).find? k' = left.find? k'
ihr: (right.insert k v).find? k' = right.find? k'
node(if k < key then (left.insert k v).node key value right
      else if key < k then left.node key value (right.insert k v) else left.node k v right).find?
    k' =
  if k' < key then left.find? k' else if key < k' then right.find? k' else some value
    by_cases' k: Nat
k < key: Nat
keyβ: Type u_1
k, k': Nat
b: BinTree β
ne: k ≠ k'
v: β
left: Tree β
key: Nat
value: β
right: Tree β
h: BST (left.node 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: (left.insert k v).find? k' = left.find? k'
ihr: (right.insert k v).find? k' = right.find? k'
h✝: ¬k < key
neg(if key < k then left.node key value (right.insert k v) else left.node k v right).find? k' =
  if k' < key then left.find? k' else if key < k' then right.find? k' else some value; by_cases' key: Nat
key < k: Nat
kβ: Type u_1
k, k': Nat
b: BinTree β
ne: k ≠ k'
v: β
left: Tree β
key: Nat
value: β
right: Tree β
h: BST (left.node 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: (left.insert k v).find? k' = left.find? k'
ihr: (right.insert k v).find? k' = right.find? k'
h✝¹: ¬k < key
h✝: ¬key < k
neg(if k' < k then left.find? k' else if k < k' then right.find? k' else some v) =
  if k' < key then left.find? k' else if key < k' then right.find? k' else some value
    have_eq key: Nat
key k: Nat
kβ: Type u_1
k, k': Nat
b: BinTree β
ne: k ≠ k'
v: β
left: Tree β
value: β
right: Tree β
bl: BST left
br: BST right
ihl: (left.insert k v).find? k' = left.find? k'
ihr: (right.insert k v).find? k' = right.find? k'
h: BST (left.node 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
neg(if k' < k then left.find? k' else if k < k' then right.find? k' else some v) =
  if k' < k then left.find? k' else if k < k' then right.find? k' else some value
    by_cases' k': Nat
k' < k: Nat
kβ: Type u_1
k, k': Nat
b: BinTree β
ne: k ≠ k'
v: β
left: Tree β
value: β
right: Tree β
bl: BST left
br: BST right
ihl: (left.insert k v).find? k' = left.find? k'
ihr: (right.insert k v).find? k' = right.find? k'
h: BST (left.node 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
neg(if k < k' then right.find? k' else some v) = if k < k' then right.find? k' else some value; by_cases' k: Nat
k  < k': Nat
k'β: Type u_1
k, k': Nat
b: BinTree β
ne: k ≠ k'
v: β
left: Tree β
value: β
right: Tree β
bl: BST left
br: BST right
ihl: (left.insert k v).find? k' = left.find? k'
ihr: (right.insert k v).find? k' = right.find? k'
h: BST (left.node 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'
negv = value
    have_eq k: Nat
k k': Nat
k'β: Type u_1
k': Nat
b: BinTree β
v: β
left: Tree β
value: β
right: Tree β
bl: BST left
br: BST right
ne: k' ≠ k'
ihl: (left.insert k' v).find? k' = left.find? k'
ihr: (right.insert k' v).find? k' = right.find? k'
h: BST (left.node 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'
negv = value
    contradictionGoals accomplished! 🐙

Lean Manual

Binary Search Trees