aboutsummaryrefslogtreecommitdiffstats
path: root/theories/utils.v
diff options
context:
space:
mode:
Diffstat (limited to 'theories/utils.v')
-rw-r--r--theories/utils.v275
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++ *)
2From stdpp Require Export gmap stringmap ssreflect.
3From stdpp Require Import sorting.
4From stdpp Require Import options.
5Set Default Proof Using "Type*".
6
7(* Succeeds if [t] is syntactically a constructor applied to some arguments.
8Note that Coq's [is_constructor] succeeds on [S], but fails on [S n]. *)
9Ltac is_app_constructor t :=
10 lazymatch t with
11 | ?t _ => is_app_constructor t
12 | _ => is_constructor t
13 end.
14
15Lemma xorb_True b1 b2 : xorb b1 b2 ↔ ¬(b1 ↔ b2).
16Proof. destruct b1, b2; naive_solver. Qed.
17
18Definition 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]. *)
25Lemma option_to_eq_Some_Some `{!EqDecision A} (mx : option A) x (H : mx = Some x) :
26 option_to_eq_Some mx = Some (x ↾ H).
27Proof.
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 _).
31Qed.
32
33Definition 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
36Global Instance maybe_String : Maybe2 String := λ s,
37 if s is String a s then Some (a,s) else None.
38
39Global Instance String_inj a : Inj (=) (=) (String a).
40Proof. by injection 1. Qed.
41
42Global Instance full_relation_dec {A} : RelDecision (λ _ _ : A, True).
43Proof. unfold RelDecision. apply _. Defined.
44
45Global Instance prod_relation_dec `{RA : relation A, RB : relation B} :
46 RelDecision RA → RelDecision RB → RelDecision (prod_relation RA RB).
47Proof. unfold RelDecision. apply _. Defined.
48
49Global Hint Extern 0 (from_option _ _ _) => progress simpl : core.
50
51Definition map_sum_with `{MapFold K A M} (f : A → nat) : M → nat :=
52 map_fold (λ _, plus ∘ f) 0.
53Lemma 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.
55Proof.
56 intros. rewrite /map_sum_with (map_fold_delete_L _ _ i x m) /=; auto with lia.
57Qed.
58
59Lemma 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.
62Proof.
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 //.
67Qed.
68Lemma 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.
71Proof. unfold_leibniz. apply map_Forall2_dom. Qed.
72
73Definition 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
78Section 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.
132End fin_map.
133
134Definition 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
142Section 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.
215End map_sorted.
216
217Definition 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
223Definition 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
230Section 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.
275End fin_map.