-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathbst_holes.v
155 lines (144 loc) · 4.12 KB
/
bst_holes.v
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
Require Import VST.floyd.proofauto.
(* Require Import Coq.Program.Equality. *)
Require Import my_tactics.
Require Import bst_spec.
(* bin_tree with *exactly* one hole *)
Inductive bin_tree_hole (A: Type) : Type :=
| hole : bin_tree_hole A
| node_hole_l : A -> bin_tree_hole A -> bin_tree A -> bin_tree_hole A
| node_hole_r : A -> bin_tree A -> bin_tree_hole A -> bin_tree_hole A.
Arguments bin_tree_hole _%type_scope.
Arguments hole {A}%type_scope.
Arguments node_hole_l {A}%type_scope.
Arguments node_hole_r {A}%type_scope.
Fixpoint fill_hole {A} (outer: bin_tree_hole A) (inner: bin_tree A) : bin_tree A :=
match outer with
| hole => inner
| node_hole_l a l r => node a (fill_hole l inner) r
| node_hole_r a l r => node a l (fill_hole r inner)
end.
Fixpoint extend_hole {A} (outer inner: bin_tree_hole A) : bin_tree_hole A :=
match outer with
| hole => inner
| node_hole_l a l r => node_hole_l a (extend_hole l inner) r
| node_hole_r a l r => node_hole_r a l (extend_hole r inner)
end.
Definition bst_hole A := bin_tree_hole (Z * A).
(* This acts as a complement to search - where search returns the subtree, this returns the original tree,
but with a hole where the subtree used to be. *)
Fixpoint search_make_hole {A} (k: Z) (b: bst A) : bst_hole A :=
match b with
| leaf => hole
| node (k', v) l r =>
match k ?= k' with
| Eq => hole
| Lt => node_hole_l (k', v) (search_make_hole k l) r
| Gt => node_hole_r (k', v) l (search_make_hole k r)
end
end.
Theorem fill_search_hole {A} : forall k (b: bst A),
fill_hole (search_make_hole k b) (search k b) = b.
Proof.
intros k b.
induction b.
- reflexivity.
- simpl.
destruct_pair.
find_Z_compare_destruct; simpl.
+ reflexivity.
+ f_equal. assumption.
+ f_equal. assumption.
Qed.
(* This does search and search_make_hole together *)
Fixpoint split_bst_at {A} (k: Z) (b: bst A) : bst_hole A * bst A :=
match b with
| leaf => (hole, leaf)
| node (k', v) l r =>
match k ?= k' with
| Eq => (hole, b)
| Lt => let (outer, inner) := split_bst_at k l
in (node_hole_l (k', v) outer r, inner)
| Gt => let (outer, inner) := split_bst_at k r
in (node_hole_r (k', v) l outer, inner)
end
end.
(* Intended for when `search_path k outer inner` *)
Definition bst_subtract_path k (outer inner: bst Z) : bst_hole Z :=
match inner with
| leaf => search_make_hole k outer
| node (k',v) l r => search_make_hole k' outer
end.
Lemma bst_subtract_path_b_b : forall k b, bst_subtract_path k b b = hole.
Proof.
intros.
destruct b.
- reflexivity.
- simpl.
destruct_pair.
rewrite Z.compare_refl.
reflexivity.
Qed.
Theorem fill_hole_bst_subtract_path: forall k b sub,
well_ordered b ->
search_path k b sub ->
fill_hole (bst_subtract_path k b sub) sub = b.
Proof.
intros k b sub H_wo H_path.
induction H_path.
- destruct b.
+ reflexivity.
+ simpl.
destruct_pair.
rewrite Z.compare_refl.
reflexivity.
- inv H_wo.
simplify_assumps.
destruct b.
+ simpl.
rewrite Zaux.Zcompare_Lt by assumption.
simpl.
f_equal.
simpl in *.
assumption.
+ simpl.
destruct_pair.
simpl in *.
apply search_path_is_subtree in H_path.
find_Z_compare_destruct.
* eapply subtree_forall in H_path; [|eassumption].
inv H_path.
simpl in *.
lia.
* simpl.
f_equal.
assumption.
* eapply subtree_forall in H_path; [|eapply H4].
inv H_path.
simpl in *.
lia.
- inv H_wo.
simplify_assumps.
destruct b.
+ simpl.
rewrite Zaux.Zcompare_Gt by lia.
simpl.
f_equal.
simpl in *.
assumption.
+ simpl.
destruct_pair.
simpl in *.
apply search_path_is_subtree in H_path.
find_Z_compare_destruct.
* eapply subtree_forall in H_path; [|eassumption].
inv H_path.
simpl in *.
lia.
* eapply subtree_forall in H_path; [|eapply H5].
inv H_path.
simpl in *.
lia.
* simpl.
f_equal.
assumption.
Qed.