blob: a49be5e27a8127e48bc6361566444d49f4ea3eb5 (
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
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
|
import Verification.Tree
import AvlVerification
namespace BST
open Primitives (Result)
open avl_verification (AVLNode Ordering)
open Tree (AVLTree AVLNode.left AVLNode.right AVLNode.val)
inductive ForallNode (p: T -> Prop): AVLTree T -> Prop
| none : ForallNode p none
| some (a: T) (left: AVLTree T) (right: AVLTree T) : ForallNode p left -> p a -> ForallNode p right -> ForallNode p (some (AVLNode.mk a left right))
theorem ForallNode.left {p: T -> Prop} {t: AVLTree T}: ForallNode p t -> ForallNode p t.left := by
intro Hpt
cases Hpt with
| none => simp [AVLTree.left, ForallNode.none]
| some a left right f_pleft f_pa f_pright => simp [AVLTree.left, f_pleft]
theorem ForallNode.right {p: T -> Prop} {t: AVLTree T}: ForallNode p t -> ForallNode p t.right := by
intro Hpt
cases Hpt with
| none => simp [AVLTree.right, ForallNode.none]
| some a left right f_pleft f_pa f_pright => simp [AVLTree.right, f_pright]
theorem ForallNode.label {a: T} {p: T -> Prop} {left right: AVLTree T}: ForallNode p (AVLNode.mk a left right) -> p a := by
intro Hpt
cases Hpt with
| some a left right f_pleft f_pa f_pright => exact f_pa
theorem ForallNode.not_mem {a: T} (p: T -> Prop) (t: Option (AVLNode T)): ¬ p a -> ForallNode p t -> a ∉ AVLTree.set t := fun Hnpa Hpt => by
cases t with
| none => simp [AVLTree.set]; tauto
| some t =>
cases Hpt with
| some b left right f_pbleft f_pb f_pbright =>
simp [AVLTree.set_some]
push_neg
split_conjs
. by_contra hab; rw [hab] at Hnpa; exact Hnpa f_pb
. exact ForallNode.not_mem p left Hnpa f_pbleft
. exact ForallNode.not_mem p right Hnpa f_pbright
theorem ForallNode.not_mem' {a: T} (p: T -> Prop) (t: Option (AVLNode T)): p a -> ForallNode (fun x => ¬p x) t -> a ∉ AVLTree.set t := fun Hpa Hnpt => by
refine' ForallNode.not_mem (fun x => ¬ p x) t _ _
simp [Hpa]
exact Hnpt
theorem ForallNode.imp {p q: T -> Prop} {t: AVLTree T}: (∀ x, p x -> q x) -> ForallNode p t -> ForallNode q t := fun Himp Hpt => by
induction Hpt
. simp [ForallNode.none]
. constructor
. assumption
. apply Himp; assumption
. assumption
-- This is the binary search invariant.
variable [LinearOrder T]
inductive Invariant: AVLTree T -> Prop
| none : Invariant none
| some (a: T) (left: AVLTree T) (right: AVLTree T) :
ForallNode (fun v => v < a) left -> ForallNode (fun v => a < v) right
-> Invariant left -> Invariant right -> Invariant (some (AVLNode.mk a left right))
@[simp]
theorem singleton_bst {a: T}: Invariant (some (AVLNode.mk a none none)) := by
apply Invariant.some
all_goals simp [ForallNode.none, Invariant.none]
theorem left {t: AVLTree T}: Invariant t -> Invariant t.left := by
intro H
induction H with
| none => exact Invariant.none
| some _ _ _ _ _ _ _ _ _ => simp [AVLTree.left]; assumption
theorem right {t: AVLTree T}: Invariant t -> Invariant t.right := by
intro H
induction H with
| none => exact Invariant.none
| some _ _ _ _ _ _ _ _ _ => simp [AVLTree.right]; assumption
-- TODO: ask at most for LT + Irreflexive (lt_irrefl) + Trichotomy (le_of_not_lt)?
theorem left_pos {left right: Option (AVLNode T)} {a x: T}: BST.Invariant (some (AVLNode.mk a left right)) -> x ∈ AVLTree.set (AVLNode.mk a left right) -> x < a -> x ∈ AVLTree.set left := fun Hbst Hmem Hxa => by
simp [AVLTree.set_some] at Hmem
rcases Hmem with (Heq | Hleft) | Hright
. rewrite [Heq] at Hxa; exact absurd Hxa (lt_irrefl _)
. assumption
. exfalso
-- Hbst -> x ∈ right -> ForallNode (fun v => ¬ v < a)
refine' ForallNode.not_mem' (fun v => v < a) right Hxa _ _
simp [le_of_not_lt]
cases Hbst with
| some _ _ _ _ Hforall _ =>
refine' ForallNode.imp _ Hforall
exact fun x => le_of_lt
assumption
theorem right_pos {left right: Option (AVLNode T)} {a x: T}: BST.Invariant (some (AVLNode.mk a left right)) -> x ∈ AVLTree.set (AVLNode.mk a left right) -> a < x -> x ∈ AVLTree.set right := fun Hbst Hmem Hax => by
simp [AVLTree.set_some] at Hmem
rcases Hmem with (Heq | Hleft) | Hright
. rewrite [Heq] at Hax; exact absurd Hax (lt_irrefl _)
. exfalso
refine' ForallNode.not_mem' (fun v => a < v) left Hax _ _
simp [le_of_not_lt]
cases Hbst with
| some _ _ _ Hforall _ _ =>
refine' ForallNode.imp _ Hforall
exact fun x => le_of_lt
assumption
. assumption
end BST
|
