From 5a9726ceb89ee54b9b15b1d992085505783c723b Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Paulo=20Em=C3=ADlio=20de=20Vilhena?= <pevilhena2@gmail.com>
Date: Mon, 15 Feb 2021 09:40:41 +0100
Subject: [PATCH] Add several simple lemmas (mostly about list and map filter).

---
 CHANGELOG.md        |   2 +
 theories/fin_maps.v | 101 +++++++++++++++++++++++++++++---------------
 theories/fin_sets.v |   5 +++
 theories/list.v     |  34 +++++++++++++++
 4 files changed, 107 insertions(+), 35 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index efb636f4..b596a311 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -59,6 +59,8 @@ Coq 8.8 and 8.9 are no longer supported.
   `set_equiv_spec_L` → `set_eq_subseteq`,
   `elem_of_equiv` → `set_equiv`,
   `set_equiv_spec` → `set_equiv_subseteq`.
+- Remove lemmas `map_filter_iff` and `map_filter_lookup_eq` in favor of the stronger
+  extensionality lemmas `map_filter_ext` and `map_filter_strong_ext`.
 
 The following `sed` script should perform most of the renaming
 (on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`):
diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index 95a4aa6c..4e7ae1fc 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -1248,12 +1248,12 @@ Proof.
 Qed.
 
 (** ** The filter operation *)
-Section map_filter.
+Section map_filter_lookup.
   Context {A} (P : K * A → Prop) `{!∀ x, Decision (P x)}.
   Implicit Types m : M A.
 
   Lemma map_filter_lookup_Some m i x :
-    filter P m !! i = Some x ↔ m !! i = Some x ∧ P (i,x).
+    filter P m !! i = Some x ↔ m !! i = Some x ∧ P (i, x).
   Proof.
     revert m i x. apply (map_fold_ind (λ m1 m2,
       ∀ i x, m1 !! i = Some x ↔ m2 !! i = Some x ∧ P _)); intros i x.
@@ -1268,7 +1268,7 @@ Section map_filter.
     filter P m !! i = Some x → m !! i = Some x.
   Proof. apply map_filter_lookup_Some. Qed.
   Lemma map_filter_lookup_Some_1_2 m i x :
-    filter P m !! i = Some x → P (i,x).
+    filter P m !! i = Some x → P (i, x).
   Proof. apply map_filter_lookup_Some. Qed.
   Lemma map_filter_lookup_Some_2 m i x :
     m !! i = Some x →
@@ -1277,46 +1277,57 @@ Section map_filter.
   Proof. intros. by apply map_filter_lookup_Some. Qed.
 
   Lemma map_filter_lookup_None m i :
-    filter P m !! i = None ↔ m !! i = None ∨ ∀ x, m !! i = Some x → ¬ P (i,x).
+    filter P m !! i = None ↔ m !! i = None ∨ ∀ x, m !! i = Some x → ¬ P (i, x).
   Proof.
     rewrite eq_None_not_Some. unfold is_Some.
     setoid_rewrite map_filter_lookup_Some. naive_solver.
   Qed.
   Lemma map_filter_lookup_None_1 m i :
     filter P m !! i = None →
-    m !! i = None ∨ ∀ x, m !! i = Some x → ¬ P (i,x).
+    m !! i = None ∨ ∀ x, m !! i = Some x → ¬ P (i, x).
   Proof. apply map_filter_lookup_None. Qed.
   Lemma map_filter_lookup_None_2 m i :
     m !! i = None ∨ (∀ x : A, m !! i = Some x → ¬ P (i, x)) →
     filter P m !! i = None.
   Proof. apply map_filter_lookup_None. Qed.
+End map_filter_lookup.
 
-  Lemma map_filter_lookup_eq m1 m2 :
-    (∀ k x, P (k,x) → m1 !! k = Some x ↔ m2 !! k = Some x) →
-    filter P m1 = filter P m2.
+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.
   Proof.
-    intros HP. apply map_eq. intros i. apply option_eq; intros x.
+    intros HPiff. apply map_eq. intros i. apply option_eq; intros x.
     rewrite !map_filter_lookup_Some. naive_solver.
   Qed.
+  Lemma map_filter_ext (m : M A) :
+    (∀ 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.
+End map_filter_ext.
+
+Section map_filter_insert_and_delete.
+  Context {A} (P : K * A → Prop) `{!∀ x, Decision (P x)}.
+  Implicit Types m : M A.
 
   Lemma map_filter_insert m i x :
-    P (i,x) → filter P (<[i:=x]> m) = <[i:=x]> (filter P m).
+    P (i, x) → filter P (<[i:=x]> m) = <[i:=x]> (filter P m).
   Proof.
     intros HP. apply map_eq. intros j. apply option_eq; intros y.
-    destruct (decide (j = i)) as [->|?].
-    - rewrite map_filter_lookup_Some, !lookup_insert. naive_solver.
-    - rewrite lookup_insert_ne, !map_filter_lookup_Some, lookup_insert_ne by done.
-      naive_solver.
+    rewrite map_filter_lookup_Some. destruct (decide (i = j)) as [->|?].
+    - rewrite !lookup_insert. naive_solver.
+    - rewrite !lookup_insert_ne by done. symmetry. apply map_filter_lookup_Some.
   Qed.
 
   Lemma map_filter_insert_not' m i x :
     ¬ P (i, x) → (∀ y, m !! i = Some y → ¬ P (i, y)) →
     filter P (<[i:=x]> m) = filter P m.
   Proof.
-    intros Hx HP. apply map_filter_lookup_eq. intros j y Hy.
+    intros Hx HP. apply map_filter_strong_ext. intros j y.
     rewrite lookup_insert_Some. naive_solver.
   Qed.
-
   Lemma map_filter_insert_not m i x :
     (∀ y, ¬ P (i, y)) → filter P (<[i:=x]> m) = filter P m.
   Proof. intros HP. by apply map_filter_insert_not'. Qed.
@@ -1341,9 +1352,15 @@ Section map_filter.
   Lemma map_filter_delete_not m i:
     (∀ y, ¬ P (i, y)) → filter P (delete i m) = filter P m.
   Proof.
-    intros HP. apply map_filter_lookup_eq; intros j y Hy.
-    by rewrite lookup_delete_ne by naive_solver.
+    intros ?. case (m !! i) as [x|] eqn:?.
+    - by rewrite <-(map_filter_insert_not_delete _ _ x), insert_id by done.
+    - by rewrite delete_notin.
   Qed.
+End map_filter_insert_and_delete.
+
+Section map_filter_misc.
+  Context {A} (P : K * A → Prop) `{!∀ x, Decision (P x)}.
+  Implicit Types m : M A.
 
   Lemma map_filter_empty : filter P (∅ : M A) = ∅.
   Proof. apply map_fold_empty. Qed.
@@ -1357,25 +1374,30 @@ Section map_filter.
       by rewrite map_to_list_insert, IH by (rewrite map_filter_lookup_None; auto).
     - by rewrite map_filter_insert_not' by naive_solver.
   Qed.
-End map_filter.
 
-Lemma map_filter_fmap {A A2} (P : K * A → Prop) `{!∀ x, Decision (P x)}
-    (f : A2 → A) (m : M A2) :
-  filter P (f <$> m) = f <$> filter (λ '(k, v), P (k, (f v))) m.
-Proof.
-  apply map_eq. intros i. apply option_eq; intros x.
-  repeat (rewrite lookup_fmap, fmap_Some || setoid_rewrite map_filter_lookup_Some).
-  naive_solver.
-Qed.
+  Lemma map_filter_fmap {B} (f : B → A) (m : M B) :
+    filter P (f <$> m) = f <$> filter (λ '(i, x), P (i, (f x))) m.
+  Proof.
+    apply map_eq. intros i. apply option_eq; intros x.
+    repeat (rewrite lookup_fmap, fmap_Some || setoid_rewrite map_filter_lookup_Some).
+    naive_solver.
+  Qed.
 
-Lemma map_filter_iff {A} (P1 P2 : K * A → Prop)
-    `{!∀ x, Decision (P1 x), !∀ x, Decision (P2 x)} (m : M A) :
-  (∀ x, P1 x ↔ P2 x) →
-  filter P1 m = filter P2 m.
-Proof.
-  intros HPiff. rewrite !map_filter_alt.
-  f_equal. apply list_filter_iff. done.
-Qed.
+  Lemma map_filter_filter Q `{!∀ x, Decision (Q x)} m :
+    filter P (filter Q m) = filter (λ '(i, x), P (i, x) ∧ Q (i, x)) m.
+  Proof.
+    apply map_filter_strong_ext. intros ??.
+    rewrite map_filter_lookup_Some. naive_solver.
+  Qed.
+  Lemma map_filter_filter_l Q `{!∀ x, Decision (Q x)} m :
+    (∀ i x, m !! i = Some x → P (i, x) → Q (i, x)) →
+    filter P (filter Q m) = filter P m.
+  Proof. intros ?. rewrite map_filter_filter. apply map_filter_ext. naive_solver. Qed.
+  Lemma map_filter_filter_r Q `{!∀ x, Decision (Q x)} m :
+    (∀ i x, m !! i = Some x → Q (i, x) → P (i, x)) →
+    filter P (filter Q m) = filter Q m.
+  Proof. intros ?. rewrite map_filter_filter. apply map_filter_ext. naive_solver. Qed.
+End map_filter_misc.
 
 (** ** Properties of the [map_Forall] predicate *)
 Section map_Forall.
@@ -2036,6 +2058,15 @@ Proof.
   intro. rewrite insert_union_singleton_l, map_union_comm; [done |].
   by apply map_disjoint_singleton_l.
 Qed.
+Lemma union_singleton_r {A} (m : M A) i x y :
+  m !! i = Some x → m ∪ {[i := y]} = m.
+Proof.
+  intro Hlkup. apply map_eq. intros j. rewrite lookup_union.
+  destruct (decide (i = j)); subst.
+  - by rewrite !lookup_singleton, Hlkup.
+  - rewrite lookup_singleton_ne by done.
+    by destruct (m !! j).
+Qed.
 Lemma map_disjoint_insert_l {A} (m1 m2 : M A) i x :
   <[i:=x]>m1 ##ₘ m2 ↔ m2 !! i = None ∧ m1 ##ₘ m2.
 Proof.
diff --git a/theories/fin_sets.v b/theories/fin_sets.v
index 2813dfb6..3b856ab5 100644
--- a/theories/fin_sets.v
+++ b/theories/fin_sets.v
@@ -116,6 +116,11 @@ Proof.
   intros x. rewrite !elem_of_elements; auto.
 Qed.
 
+Lemma list_to_set_elements X : list_to_set (elements X) ≡ X.
+Proof. intros ?. rewrite elem_of_list_to_set. apply elem_of_elements. Qed.
+Lemma list_to_set_elements_L `{!LeibnizEquiv C} X : list_to_set (elements X) = X.
+Proof. unfold_leibniz. apply list_to_set_elements. Qed.
+
 (** * The [size] operation *)
 Global Instance set_size_proper: Proper ((≡) ==> (=)) (@size C _).
 Proof. intros ?? E. apply Permutation_length. by rewrite E. Qed.
diff --git a/theories/list.v b/theories/list.v
index d859626e..68ca3f6e 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -1819,6 +1819,34 @@ Proof.
   - rewrite !filter_cons_False by naive_solver. by rewrite IH.
 Qed.
 
+Lemma list_filter_filter (P1 P2 : A → Prop)
+    `{!∀ x, Decision (P1 x), !∀ x, Decision (P2 x)} (l : list A) :
+  filter P1 (filter P2 l) = filter (λ a, P1 a ∧ P2 a) l.
+Proof.
+  induction l as [|x l IH]; [done|].
+  rewrite !filter_cons. case (decide (P2 x)) as [HP2|HP2].
+  - rewrite filter_cons, IH. apply decide_iff. naive_solver.
+  - rewrite IH. symmetry. apply decide_False. by intros [_ ?].
+Qed.
+
+Lemma list_filter_filter_l (P1 P2 : A → Prop)
+    `{!∀ x, Decision (P1 x), !∀ x, Decision (P2 x)} (l : list A) :
+  (∀ x, P1 x → P2 x) →
+  filter P1 (filter P2 l) = filter P1 l.
+Proof.
+  intros HPimp. rewrite list_filter_filter.
+  apply list_filter_iff. naive_solver.
+Qed.
+
+Lemma list_filter_filter_r (P1 P2 : A → Prop)
+    `{!∀ x, Decision (P1 x), !∀ x, Decision (P2 x)} (l : list A) :
+  (∀ x, P2 x → P1 x) →
+  filter P1 (filter P2 l) = filter P2 l.
+Proof.
+  intros HPimp. rewrite list_filter_filter.
+  apply list_filter_iff. naive_solver.
+Qed.
+
 (** ** Properties of the [prefix] and [suffix] predicates *)
 Global Instance: PreOrder (@prefix A).
 Proof.
@@ -2465,6 +2493,12 @@ Global Instance list_subseteq_po : PreOrder (⊆@{list A}).
 Proof. split; firstorder. Qed.
 Lemma list_subseteq_nil l : [] ⊆ l.
 Proof. intros x. by rewrite elem_of_nil. Qed.
+Lemma list_nil_subseteq l : l ⊆ [] → l = [].
+Proof.
+  intro Hl. destruct l as [|x l1]; [done|]. exfalso.
+  rewrite <-(elem_of_nil x).
+  apply Hl, elem_of_cons. by left.
+Qed.
 
 Global Instance list_subseteq_Permutation: Proper ((≡ₚ) ==> (≡ₚ) ==> (↔)) (⊆@{list A}) .
 Proof. intros l1 l2 Hl k1 k2 Hk. apply forall_proper; intros x. by rewrite Hl, Hk. Qed.
-- 
GitLab