blob: 3316e9e79c8795cf0c1aa2a01102289ffed22bb1 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
|
import «AvlVerification»
namespace Tree
variable {T: Type}
open avl_verification
-- Otherwise, Lean cannot prove termination by itself.
@[reducible]
def AVLTree (U: Type) := Option (AVLNode U)
def AVLTree.nil: AVLTree T := none
def AVLTree.val (t: AVLTree T): Option T := match t with
| none => none
| some (AVLNode.mk x _ _) => some x
def AVLTree.left (t: AVLTree T): AVLTree T := match t with
| none => none
| some (AVLNode.mk _ left _) => left
def AVLTree.right (t: AVLTree T): AVLTree T := match t with
| none => none
| some (AVLNode.mk _ _ right) => right
def AVLNode.left (t: AVLNode T): AVLTree T := match t with
| AVLNode.mk _ left _ => left
def AVLNode.right (t: AVLNode T): AVLTree T := match t with
| AVLNode.mk _ _ right => right
def AVLNode.val (t: AVLNode T): T := match t with
| AVLNode.mk x _ _ => x
mutual
def AVLTree.height_node (tree: AVLNode T): Nat := match tree with
| AVLNode.mk y left right => 1 + AVLTree.height left + AVLTree.height right
def AVLTree.height (tree: AVLTree T): Nat := match tree with
| none => 0
| some n => 1 + AVLTree.height_node n
end
def AVLTreeSet.nil: AVLTreeSet T := { root := AVLTree.nil }
-- Automatic synthesization of this seems possible at the Lean level?
instance: Inhabited (AVLTree T) where
default := AVLTree.nil
instance: Inhabited (AVLTreeSet T) where
default := AVLTreeSet.nil
instance: Coe (Option (AVLNode T)) (AVLTree T) where
coe x := x
-- TODO: ideally, it would be nice if we could generalize
-- this to any `BinaryTree` typeclass.
def AVLTree.mem (tree: AVLTree T) (x: T) :=
match tree with
| none => False
| some (AVLNode.mk y left right) => x = y ∨ AVLTree.mem left x ∨ AVLTree.mem right x
@[simp]
def AVLTree.mem_none: AVLTree.mem none = ({}: Set T) := rfl
@[simp]
def AVLTree.mem_some {x: T} {left right: AVLTree T}: AVLTree.mem (some (AVLNode.mk x left right)) = (({x}: Set T) ∪ AVLTree.mem left ∪ AVLTree.mem right) := by
ext y
rw [AVLTree.mem]
simp [Set.insert_union]
simp [Set.insert_def, Set.setOf_set, Set.mem_def, Set.union_def]
-- TODO(reinforcement): ∪ is actually disjoint if we prove this is a binary search tree.
def AVLTree.set (t: AVLTree T): Set T := _root_.setOf (AVLTree.mem t)
def AVLTree.setOf_left_incl (t: AVLTree T): t.left.set ⊂ t.set := sorry
def AVLTree.setOf_right_incl (t: AVLTree T): t.right.set ⊂ t.set := sorry
end Tree
|
