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
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
|
import AvlVerification.Tree
import AvlVerification.BinarySearchTree
import AvlVerification.Specifications
namespace Implementation
open Primitives
open avl_verification
open Tree (AVLTree AVLTree.set)
open Specifications (OrdSpecDualityEq ordOfOrdSpec ltOfRustOrder gtOfRustOrder)
-- example: OrdSpec OrdU32 := ordSpecOfTotalityAndDuality _
-- (by
-- -- Totality
-- intro a b
-- unfold Ord.cmp
-- unfold OrdU32
-- unfold OrdU32.cmp
-- if hlt : a < b then
-- use .Less
-- simp [hlt]
-- else
-- if heq: a = b
-- then
-- use .Equal
-- simp [hlt]
-- rw [heq]
-- -- TODO: simp [hlt, heq] breaks everything???
-- else
-- use .Greater
-- simp [hlt, heq]
-- ) (by
-- -- Duality
-- intro a b Hgt
-- if hlt : b < a then
-- unfold Ord.cmp
-- unfold OrdU32
-- unfold OrdU32.cmp
-- simp [hlt]
-- else
-- unfold Ord.cmp at Hgt
-- unfold OrdU32 at Hgt
-- unfold OrdU32.cmp at Hgt
-- have hnlt : ¬ (a < b) := sorry
-- have hneq : ¬ (a = b) := sorry
-- exfalso
-- apply hlt
-- -- I need a Preorder on U32 now.
-- sorry)
variable (T: Type) (H: avl_verification.Ord T) (Ospec: @OrdSpecDualityEq T H)
@[pspec]
theorem AVLTreeSet.insert_loop_spec_local (p: T -> Prop)
(Hcmp_spec: ∀ a b, ∃ o, H.cmp a b = Result.ok o)
(a: T) (t: Option (AVLNode T)):
∃ added t_new, AVLTreeSet.insert_loop T H a t = Result.ok ⟨ added, t_new ⟩
-- ∧ AVLTree.set t'.2 = insert a (AVLTree.set t)
∧ (BST.ForallNode p t -> p a -> BST.ForallNode p t_new)
:= by match t with
| none =>
simp [AVLTreeSet.insert_loop, AVLTree.set, setOf]
intros _ Hpa
constructor; all_goals try simp [BST.ForallNode.none]
exact Hpa
| some (AVLNode.mk b left right) =>
rw [AVLTreeSet.insert_loop]
simp only []
progress keep Hordering as ⟨ ordering ⟩
cases ordering
all_goals simp only []
{
progress keep Htree as ⟨ added₁, right₁, Hnode ⟩
refine' ⟨ added₁, ⟨ some (AVLNode.mk b left right₁), _ ⟩ ⟩
simp only [true_and]
intros Hptree Hpa
constructor
exact Hptree.left
exact Hptree.label
exact Hnode Hptree.right Hpa
}
{
simp; tauto
}
{
-- TODO: investigate wlog.
-- Symmetric case of left.
progress keep Htree as ⟨ added₁, left₁, Hnode ⟩
refine' ⟨ added₁, ⟨ some (AVLNode.mk b left₁ right), _ ⟩ ⟩
simp only [true_and]
intros Hptree Hpa
constructor
exact Hnode Hptree.left Hpa
exact Hptree.label
exact Hptree.right
}
@[pspec]
lemma AVLTreeSet.insert_loop_spec_global
(a: T) (t: Option (AVLNode T))
:
BST.Invariant t -> ∃ added t_new, AVLTreeSet.insert_loop T H a t = Result.ok ⟨ added, t_new ⟩
∧ BST.Invariant t_new ∧ AVLTree.set t_new = {a} ∪ AVLTree.set t := by
intro Hbst
match t with
| none => simp [AVLTreeSet.insert_loop, AVLTree.set, setOf]
| some (AVLNode.mk b left right) =>
rw [AVLTreeSet.insert_loop]
simp only []
have : ∀ a b, ∃ o, H.cmp a b = .ok o := Ospec.infallible
progress keep Hordering as ⟨ ordering ⟩
cases ordering
all_goals simp only []
{
have ⟨ added₂, right₂, ⟨ H_result, ⟨ H_bst, H_set ⟩ ⟩ ⟩ := AVLTreeSet.insert_loop_spec_global a right (BST.right Hbst)
progress keep Htree with AVLTreeSet.insert_loop_spec_local as ⟨ added₁, right₁, Hnode ⟩
exact (fun x => b < x)
rewrite [Htree] at H_result; simp at H_result
refine' ⟨ added₁, ⟨ some (AVLNode.mk b left right₁), _ ⟩ ⟩
simp only [true_and]
split_conjs
cases' Hbst with _ _ _ H_forall_left H_forall_right H_bst_left H_bst_right
constructor
exact H_forall_left
apply Hnode; exact H_forall_right
exact (ltOfRustOrder H b a Hordering)
exact H_bst_left
convert H_bst
exact H_result.2
simp [AVLTree.set_some]
rewrite [H_result.2, H_set]
simp
}
{
simp; split_conjs
. tauto
. simp [Ospec.equivalence _ _ Hordering]
}
{
have ⟨ added₂, left₂, ⟨ H_result, ⟨ H_bst, H_set ⟩ ⟩ ⟩ := AVLTreeSet.insert_loop_spec_global a left (BST.left Hbst)
progress keep Htree with AVLTreeSet.insert_loop_spec_local as ⟨ added₁, left₁, Hnode ⟩
exact (fun x => x < b)
rewrite [Htree] at H_result; simp at H_result
refine' ⟨ added₁, ⟨ some (AVLNode.mk b left₁ right), _ ⟩ ⟩
simp only [true_and]
split_conjs
cases' Hbst with _ _ _ H_forall_left H_forall_right H_bst_left H_bst_right
constructor
apply Hnode; exact H_forall_left
exact (gtOfRustOrder H b a Hordering)
exact H_forall_right
convert H_bst
exact H_result.2
exact H_bst_right
simp [AVLTree.set_some]
rewrite [H_result.2, H_set]
simp [Set.singleton_union, Set.insert_comm, Set.insert_union]
}
@[pspec]
def AVLTreeSet.insert_spec
(a: T) (t: AVLTreeSet T):
BST.Invariant t.root -> (∃ t' added,t.insert _ H a = Result.ok (added, t')
-- it's still a binary search tree.
∧ BST.Invariant t'.root
∧ AVLTree.set t'.root = {a} ∪ AVLTree.set t.root)
:= by
rw [AVLTreeSet.insert]; intro Hbst
progress keep h as ⟨ t', Hset ⟩;
simp; assumption
end Implementation
|
