Commit 8396f122 by Dan Frumin

### Better naming

parent 6058134f
 ... ... @@ -1326,23 +1326,24 @@ Section map_filter_ext. Context {A} (P Q : K * A → Prop) `{!∀ x, Decision (P x), !∀ x, Decision (Q x)}. Lemma map_filter_strong_ext (m1 m2 : M A) : (∀ i x, (P (i, x) ∧ m1 !! i = Some x) ↔ (Q (i, x) ∧ m2 !! i = Some x)) → filter P m1 = filter Q m2. filter P m1 = filter Q m2 ↔ (∀ i x, (P (i, x) ∧ m1 !! i = Some x) ↔ (Q (i, x) ∧ m2 !! i = Some x)). Proof. intros HPiff. apply map_eq. intros i. apply option_eq; intros x. rewrite !map_filter_lookup_Some. naive_solver. intros. rewrite map_eq_iff. setoid_rewrite option_eq. setoid_rewrite map_filter_lookup_Some. naive_solver. Qed. Lemma map_filter_strong_ext_1 (m1 m2 : M A) : (∀ i x, (P (i, x) ∧ m1 !! i = Some x) ↔ (Q (i, x) ∧ m2 !! i = Some x)) → filter P m1 = filter Q m2. Proof. by rewrite map_filter_strong_ext. Qed. Lemma map_filter_strong_ext_2 (m1 m2 : M A) i x : filter P m1 = filter Q m2 → (P (i, x) ∧ m1 !! i = Some x) ↔ (Q (i, x) ∧ m2 !! i = Some x). Proof. intros Hfilt. rewrite (comm _ (P (i, x))), (comm _ (Q (i, x))). rewrite <- !map_filter_lookup_Some. by repeat f_equiv. Qed. Proof. by rewrite map_filter_strong_ext. Qed. Lemma map_filter_ext (m : M A) : (∀ i x, m !! i = Some x → P (i, x) ↔ Q (i, x)) → (∀ i x, m !! i = Some x → P (i, x) ↔ Q (i, x)) ↔ filter P m = filter Q m. Proof. intro. apply map_filter_strong_ext. naive_solver. Qed. Proof. rewrite map_filter_strong_ext. naive_solver. Qed. End map_filter_ext. Section map_filter_insert_and_delete. ... ...
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!