blob: 6010d26933ff1b3b5aed3f1b06565901f997225a (
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
|
import «AvlVerification»
open Primitives
namespace Avl
-- synthesize inhabited?
-- synthesize type aliases
-- AVLTree T := Option<Box<AVLNode>> ~ AVLTree T := Option<AVLNode>
open avl_verification
variable {T: Type}
-- instance {H: avl_verification.Ord T}: LT T := {
-- lt := λ x y => H.cmp x y = Result.ret Ordering.Less
-- }
-- This is the binary search invariant.
def BSTree.searchInvariant {H: avl_verification.Ord T} (t: AVLTree T) := match t with
| none => True
| some (AVLNode.mk y u v) => ∀ x ∈ AVLTree.setOf (u : AVLTree T), H.cmp y x = Result.ret Ordering.Less ∧ ∀ x ∈ AVLTree.setOf (v : AVLTree T), H.cmp y x = Result.ret Ordering.Greater
-- Prove that:
-- searchInvariant t <-> searchInvariant t.left /\ searchInvariant t.right /\ something about t.val
-- searchInvariant t -> searchInvariant t.left /\ searchInvariant t.right by weakening.
def BSTree.nil_has_searchInvariant {H: avl_verification.Ord T}: @BSTree.searchInvariant _ H AVL.nil.root := by trivial
theorem BSTree.searchInvariant_children {H: avl_verification.Ord T} (t: AVLTree T): @searchInvariant _ H t -> @searchInvariant _ H t.left ∧ @searchInvariant _ H t.right := sorry
def AVLTree.height (t: AVLTree T) := AVL.height t
def AVLTree.balanceFactor (t: AVLTree T): Int := t.right.height - t.left.height
def AVLTree.balanceInvariant (t: AVLTree T) := t.balanceFactor = -1 ∨ t.balanceFactor = 0 ∨ t.balanceFactor = 1
def AVLTree.mem_eq_setOf (t: AVLTree T): AVLTree.mem t = t.setOf := rfl
end Avl
|
