diff options
Diffstat (limited to 'theories/utils.v')
-rw-r--r-- | theories/utils.v | 275 |
1 files changed, 275 insertions, 0 deletions
diff --git a/theories/utils.v b/theories/utils.v new file mode 100644 index 0000000..0cb1b33 --- /dev/null +++ b/theories/utils.v | |||
@@ -0,0 +1,275 @@ | |||
1 | (* Stuff that should be upstreamed to std++ *) | ||
2 | From stdpp Require Export gmap stringmap ssreflect. | ||
3 | From stdpp Require Import sorting. | ||
4 | From stdpp Require Import options. | ||
5 | Set Default Proof Using "Type*". | ||
6 | |||
7 | (* Succeeds if [t] is syntactically a constructor applied to some arguments. | ||
8 | Note that Coq's [is_constructor] succeeds on [S], but fails on [S n]. *) | ||
9 | Ltac is_app_constructor t := | ||
10 | lazymatch t with | ||
11 | | ?t _ => is_app_constructor t | ||
12 | | _ => is_constructor t | ||
13 | end. | ||
14 | |||
15 | Lemma xorb_True b1 b2 : xorb b1 b2 ↔ ¬(b1 ↔ b2). | ||
16 | Proof. destruct b1, b2; naive_solver. Qed. | ||
17 | |||
18 | Definition option_to_eq_Some {A} (mx : option A) : option { x | mx = Some x } := | ||
19 | match mx with | ||
20 | | Some x => Some (x ↾ eq_refl) | ||
21 | | None => None | ||
22 | end. | ||
23 | |||
24 | (* Premise can probably be weakened to something with [ProofIrrel]. *) | ||
25 | Lemma option_to_eq_Some_Some `{!EqDecision A} (mx : option A) x (H : mx = Some x) : | ||
26 | option_to_eq_Some mx = Some (x ↾ H). | ||
27 | Proof. | ||
28 | destruct mx as [x'|]; simplify_eq/=; f_equal/=. | ||
29 | assert (x' = x) as Hx by congruence. destruct Hx. | ||
30 | f_equal. apply (proof_irrel _). | ||
31 | Qed. | ||
32 | |||
33 | Definition from_sum {A B C} (f : A → C) (g : B → C) (xy : A + B) : C := | ||
34 | match xy with inl x => f x | inr y => g y end. | ||
35 | |||
36 | Global Instance maybe_String : Maybe2 String := λ s, | ||
37 | if s is String a s then Some (a,s) else None. | ||
38 | |||
39 | Global Instance String_inj a : Inj (=) (=) (String a). | ||
40 | Proof. by injection 1. Qed. | ||
41 | |||
42 | Global Instance full_relation_dec {A} : RelDecision (λ _ _ : A, True). | ||
43 | Proof. unfold RelDecision. apply _. Defined. | ||
44 | |||
45 | Global Instance prod_relation_dec `{RA : relation A, RB : relation B} : | ||
46 | RelDecision RA → RelDecision RB → RelDecision (prod_relation RA RB). | ||
47 | Proof. unfold RelDecision. apply _. Defined. | ||
48 | |||
49 | Global Hint Extern 0 (from_option _ _ _) => progress simpl : core. | ||
50 | |||
51 | Definition map_sum_with `{MapFold K A M} (f : A → nat) : M → nat := | ||
52 | map_fold (λ _, plus ∘ f) 0. | ||
53 | Lemma map_sum_with_lookup_le `{FinMap K M} {A} (f : A → nat) (m : M A) i x : | ||
54 | m !! i = Some x → f x ≤ map_sum_with f m. | ||
55 | Proof. | ||
56 | intros. rewrite /map_sum_with (map_fold_delete_L _ _ i x m) /=; auto with lia. | ||
57 | Qed. | ||
58 | |||
59 | Lemma map_Forall2_dom `{FinMapDom K M C} {A B} (P : K → A → B → Prop) | ||
60 | (m1 : M A) (m2 : M B) : | ||
61 | map_Forall2 P m1 m2 → dom m1 ≡ dom m2. | ||
62 | Proof. | ||
63 | revert m2. induction m1 as [|i x1 m1 ? IH] using map_ind; intros m2. | ||
64 | { intros ->%map_Forall2_empty_inv_l. by rewrite !dom_empty. } | ||
65 | intros (x2 & m2' & -> & ? & ? & ?)%map_Forall2_insert_inv_l; last done. | ||
66 | rewrite !dom_insert IH //. | ||
67 | Qed. | ||
68 | Lemma map_Forall2_dom_L `{FinMapDom K M C, !LeibnizEquiv C} {A B} | ||
69 | (P : K → A → B → Prop) (m1 : M A) (m2 : M B) : | ||
70 | map_Forall2 P m1 m2 → dom m1 = dom m2. | ||
71 | Proof. unfold_leibniz. apply map_Forall2_dom. Qed. | ||
72 | |||
73 | Definition map_mapM | ||
74 | `{!∀ A, MapFold K A (M A), !∀ A, Empty (M A), !∀ A, Insert K A (M A)} | ||
75 | `{MBind F, MRet F} {A B} (f : A → F B) (m : M A) : F (M B) := | ||
76 | map_fold (λ i x mm, y ← f x; m ← mm; mret $ <[i:=y]> m) (mret ∅) m. | ||
77 | |||
78 | Section fin_map. | ||
79 | Context `{FinMap K M}. | ||
80 | |||
81 | Lemma map_insert_inv_eq {A} {m1 m2 : M A} x v u : | ||
82 | m1 !! x = None → | ||
83 | m2 !! x = None → | ||
84 | <[x:=v]> m1 = <[x:=u]> m2 → | ||
85 | v = u ∧ m1 = m2. | ||
86 | Proof. | ||
87 | intros Hm1 Hm2 Heq. split. | ||
88 | - assert (Huv : <[x:=v]> m1 !! x = Some v). { apply lookup_insert. } | ||
89 | rewrite Heq lookup_insert in Huv. by injection Huv as ->. | ||
90 | - apply map_eq. intros i. | ||
91 | replace m1 with (delete x (<[x:=v]> m1)) by (apply delete_insert; done). | ||
92 | replace m2 with (delete x (<[x:=u]> m2)) by (apply delete_insert; done). | ||
93 | by rewrite Heq. | ||
94 | Qed. | ||
95 | |||
96 | Lemma map_insert_inv_ne {A} {m1 m2 : M A} x1 x2 v1 v2 : | ||
97 | x1 ≠ x2 → | ||
98 | m1 !! x1 = None → | ||
99 | m2 !! x2 = None → | ||
100 | <[x1:=v1]> m1 = <[x2:=v2]> m2 → | ||
101 | m1 !! x2 = Some v2 ∧ m2 !! x1 = Some v1 ∧ delete x2 m1 = delete x1 m2. | ||
102 | Proof. | ||
103 | intros Hx1x2 Hm1 Hm2 Hm1m2. rewrite map_eq_iff in Hm1m2. split_and!. | ||
104 | - rewrite -(lookup_insert_ne _ x1 _ v1) // Hm1m2 lookup_insert //. | ||
105 | - rewrite -(lookup_insert_ne _ x2 _ v2) // -Hm1m2 lookup_insert //. | ||
106 | - apply map_eq. intros y. destruct (decide (y = x1)) as [->|]; | ||
107 | first rewrite lookup_delete_ne // lookup_delete //. | ||
108 | destruct (decide (y = x2)) as [->|]; | ||
109 | first rewrite lookup_delete lookup_delete_ne //. | ||
110 | rewrite !lookup_delete_ne // | ||
111 | -(lookup_insert_ne m2 x2 _ v2) // | ||
112 | -(lookup_insert_ne m1 x1 _ v1) //. | ||
113 | Qed. | ||
114 | |||
115 | Lemma map_mapM_empty `{MBind F, MRet F} {A B} (f : A → F B) : | ||
116 | map_mapM f (∅ : M A) =@{F (M B)} mret ∅. | ||
117 | Proof. unfold map_mapM. by rewrite map_fold_empty. Qed. | ||
118 | |||
119 | Lemma map_mapM_insert `{MBind F, MRet F} {A B} (f : A → F B) (m : M A) i x : | ||
120 | m !! i = None → map_first_key (<[i:=x]> m) i → | ||
121 | map_mapM f (<[i:=x]> m) = y ← f x; m ← map_mapM f m; mret $ <[i:=y]> m. | ||
122 | Proof. intros. rewrite /map_mapM map_fold_insert_first_key //. Qed. | ||
123 | |||
124 | Lemma map_mapM_insert_option {A B} (f : A → option B) (m : M A) i x : | ||
125 | m !! i = None → | ||
126 | map_mapM f (<[i:=x]> m) = y ← f x; m ← map_mapM f m; mret $ <[i:=y]> m. | ||
127 | Proof. | ||
128 | intros. apply: map_fold_insert; [|done]. | ||
129 | intros ?? z1 z2 my ???. destruct (f z1), (f z2), my; f_equal/=. | ||
130 | by apply insert_commute. | ||
131 | Qed. | ||
132 | End fin_map. | ||
133 | |||
134 | Definition map_minimal_key `{MapFold K A M} (R : relation K) `{!RelDecision R} | ||
135 | (m : M) : option K := | ||
136 | map_fold (λ i _ mj, | ||
137 | match mj with | ||
138 | | Some j => if decide (R i j) then Some i else Some j | ||
139 | | None => Some i | ||
140 | end) None m. | ||
141 | |||
142 | Section map_sorted. | ||
143 | Context `{FinMap K M} (R : relation K) . | ||
144 | |||
145 | Lemma map_minimal_key_None {A} `{!RelDecision R} (m : M A) : | ||
146 | map_minimal_key R m = None ↔ m = ∅. | ||
147 | Proof. | ||
148 | split; [|intros ->; apply map_fold_empty]. | ||
149 | induction m as [|j x m ?? _] using map_first_key_ind; intros Hm; [done|]. | ||
150 | rewrite /map_minimal_key map_fold_insert_first_key // in Hm. | ||
151 | repeat case_match; simplify_option_eq. | ||
152 | Qed. | ||
153 | |||
154 | Lemma map_minimal_key_Some_1 {A} `{!RelDecision R, !PreOrder R, !Total R} | ||
155 | (m : M A) i : | ||
156 | map_minimal_key R m = Some i → | ||
157 | is_Some (m !! i) ∧ ∀ j, is_Some (m !! j) → R i j. | ||
158 | Proof. | ||
159 | revert i. induction m as [|j x m ?? IH] using map_first_key_ind; intros i Hm. | ||
160 | { by rewrite /map_minimal_key map_fold_empty in Hm. } | ||
161 | rewrite /map_minimal_key map_fold_insert_first_key // in Hm. | ||
162 | destruct (map_fold _ _ m) as [i'|] eqn:Hfold; simplify_eq. | ||
163 | - apply IH in Hfold as [??]. rewrite lookup_insert_is_Some. | ||
164 | case_decide as HR; simplify_eq/=. | ||
165 | + split; [by auto|]. intros j [->|[??]]%lookup_insert_is_Some; [done|]. | ||
166 | trans i'; eauto. | ||
167 | + split. | ||
168 | { right; split; [|done]. intros ->. by destruct HR. } | ||
169 | intros j' [->|[??]]%lookup_insert_is_Some; [|by eauto]. | ||
170 | by destruct (total R i j'). | ||
171 | - apply map_minimal_key_None in Hfold as ->. | ||
172 | split; [rewrite lookup_insert; by eauto|]. | ||
173 | intros j' [->|[? Hj']]%lookup_insert_is_Some; [done|]. | ||
174 | rewrite lookup_empty in Hj'. by destruct Hj'. | ||
175 | Qed. | ||
176 | |||
177 | Lemma map_minimal_key_Some {A} `{!RelDecision R, !PartialOrder R, !Total R} | ||
178 | (m : M A) i : | ||
179 | map_minimal_key R m = Some i ↔ | ||
180 | is_Some (m !! i) ∧ ∀ j, is_Some (m !! j) → R i j. | ||
181 | Proof. | ||
182 | split; [apply map_minimal_key_Some_1|]. | ||
183 | intros [Hi ?]. destruct (map_minimal_key R m) as [i'|] eqn:Hmin. | ||
184 | - f_equal. apply map_minimal_key_Some_1 in Hmin as [??]. | ||
185 | apply (anti_symm R); eauto. | ||
186 | - apply map_minimal_key_None in Hmin as ->. | ||
187 | rewrite lookup_empty in Hi. by destruct Hi. | ||
188 | Qed. | ||
189 | |||
190 | Lemma map_sorted_ind {A} `{!PreOrder R, !Total R} (P : M A → Prop) : | ||
191 | P ∅ → | ||
192 | (∀ i x m, | ||
193 | m !! i = None → | ||
194 | (∀ j, is_Some (m !! j) → R i j) → | ||
195 | P m → | ||
196 | P (<[i:=x]> m)) → | ||
197 | (∀ m, P m). | ||
198 | Proof. | ||
199 | intros Hemp Hins m. induction (Nat.lt_wf_0_projected size m) as [m _ IH]. | ||
200 | cut (m = ∅ ∨ map_Exists (λ i _, ∀ j, is_Some (m !! j) → R i j) m). | ||
201 | { intros [->|(i & x & Hi & ?)]; [done|]. rewrite -(insert_delete m i x) //. | ||
202 | apply Hins; [by rewrite lookup_delete|..]. | ||
203 | - intros j ?%lookup_delete_is_Some. naive_solver. | ||
204 | - apply IH. | ||
205 | rewrite -{2}(insert_delete m i x) // map_size_insert lookup_delete. lia. } | ||
206 | clear P Hemp Hins IH. induction m as [|i x m ? IH] using map_ind; [by auto|]. | ||
207 | right. destruct IH as [->|(i' & x' & ? & ?)]. | ||
208 | { rewrite insert_empty map_Exists_singleton. | ||
209 | by intros j [y [-> ->]%lookup_singleton_Some]. } | ||
210 | apply map_Exists_insert; first done. destruct (total R i i'). | ||
211 | - left. intros j [->|[??]]%lookup_insert_is_Some; [done|]. trans i'; eauto. | ||
212 | - right. exists i', x'. split; [done|]. | ||
213 | intros j [->|[??]]%lookup_insert_is_Some; eauto. | ||
214 | Qed. | ||
215 | End map_sorted. | ||
216 | |||
217 | Definition map_fold_sorted `{!MapFold K A M} {B} | ||
218 | (R : relation K) `{!RelDecision R} | ||
219 | (f : K → A → B → B) (b : B) | ||
220 | (m : M) : B := foldr (λ '(i,x), f i x) b $ | ||
221 | merge_sort (prod_relation R (λ _ _, True)) (map_to_list m). | ||
222 | |||
223 | Definition map_mapM_sorted | ||
224 | `{!∀ A, MapFold K A (M A), !∀ A, Empty (M A), !∀ A, Insert K A (M A)} | ||
225 | `{MBind F, MRet F} {A B} | ||
226 | (R : relation K) `{!RelDecision R} | ||
227 | (f : A → F B) (m : M A) : F (M B) := | ||
228 | map_fold_sorted R (λ i x mm, y ← f x; m ← mm; mret $ <[i:=y]> m) (mret ∅) m. | ||
229 | |||
230 | Section fin_map. | ||
231 | Context `{FinMap K M}. | ||
232 | Context (R : relation K) `{!RelDecision R, !PartialOrder R, !Total R}. | ||
233 | |||
234 | Lemma map_fold_sorted_empty {A B} (f : K → A → B → B) b : | ||
235 | map_fold_sorted R f b (∅ : M A) = b. | ||
236 | Proof. by rewrite /map_fold_sorted map_to_list_empty. Qed. | ||
237 | |||
238 | Lemma map_fold_sorted_insert {A B} (f : K → A → B → B) (m : M A) b i x : | ||
239 | m !! i = None → (∀ j, is_Some (m !! j) → R i j) → | ||
240 | map_fold_sorted R f b (<[i:=x]> m) = f i x (map_fold_sorted R f b m). | ||
241 | Proof. | ||
242 | intros Hi Hleast. unfold map_fold_sorted. | ||
243 | set (R' := prod_relation R _). | ||
244 | assert (PreOrder R'). | ||
245 | { split; [done|]. | ||
246 | intros [??] [??] [??] [??] [??]; split; [by etrans|done]. } | ||
247 | assert (Total R'). | ||
248 | { intros [i1 ?] [i2 ?]. destruct (total R i1 i2); [by left|by right]. } | ||
249 | assert (merge_sort R' (map_to_list (<[i:=x]> m)) | ||
250 | = (i,x) :: merge_sort R' (map_to_list m)) as ->; [|done]. | ||
251 | eapply (Sorted_unique_strong R'). | ||
252 | - intros [i1 y1] [i2 y2]. | ||
253 | rewrite !merge_sort_Permutation elem_of_cons !elem_of_map_to_list. | ||
254 | rewrite lookup_insert_Some. intros ?? [? _] [? _]. | ||
255 | assert (i1 = i2) as -> by (by apply (anti_symm R)); naive_solver. | ||
256 | - apply (Sorted_merge_sort _). | ||
257 | - apply Sorted_cons; [apply (Sorted_merge_sort _)|]. | ||
258 | destruct (merge_sort R' (map_to_list m)) | ||
259 | as [|[i' x'] ixs] eqn:Hixs; repeat constructor; simpl. | ||
260 | apply Hleast. exists x'. apply elem_of_map_to_list. | ||
261 | rewrite -(merge_sort_Permutation R' (map_to_list m)) Hixs. left. | ||
262 | - by rewrite !merge_sort_Permutation map_to_list_insert. | ||
263 | Qed. | ||
264 | |||
265 | Lemma map_mapM_sorted_empty `{MBind F, MRet F} {A B} (f : A → F B) : | ||
266 | map_mapM_sorted R f (∅ : M A) =@{F (M B)} mret ∅. | ||
267 | Proof. by rewrite /map_mapM_sorted map_fold_sorted_empty. Qed. | ||
268 | |||
269 | Lemma map_mapM_sorted_insert `{MBind F, MRet F} | ||
270 | {A B} (f : A → F B) (m : M A) i x : | ||
271 | m !! i = None → (∀ j, is_Some (m !! j) → R i j) → | ||
272 | map_mapM_sorted R f (<[i:=x]> m) | ||
273 | = y ← f x; m ← map_mapM_sorted R f m; mret $ <[i:=y]> m. | ||
274 | Proof. intros. by rewrite /map_mapM_sorted map_fold_sorted_insert. Qed. | ||
275 | End fin_map. | ||