From f317ef9d9e65172c4751cc6152f0625302d8910a Mon Sep 17 00:00:00 2001
From: Ralf Jung
Date: Tue, 7 Jul 2020 13:24:30 +0200
Subject: [PATCH 1/5] add filter_iff lemmas

theories/fin_maps.v  8 ++++++++
theories/list.v  17 +++++++++++++++++
2 files changed, 25 insertions(+)
diff git a/theories/fin_maps.v b/theories/fin_maps.v
index fc357d44..23dc8f97 100644
 a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ 1200,6 +1200,14 @@ Section map_filter.
Qed.
End map_filter.
+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.
+
(** ** Properties of the [map_Forall] predicate *)
Section map_Forall.
Context {A} (P : K → A → Prop).
diff git a/theories/list.v b/theories/list.v
index c0f62879..7da129df 100644
 a/theories/list.v
+++ b/theories/list.v
@@ 1791,6 +1791,23 @@ Section filter.
Qed.
End filter.
+Lemma list_filter_iff (P1 P2 : A → Prop)
+ `{!∀ x, Decision (P1 x), !∀ x, Decision (P2 x)} (l : list A) :
+ (∀ x, P1 x ↔ P2 x) →
+ filter P1 l = filter P2 l.
+Proof.
+ intros HPiff. induction l as [a l IH]; [done].
+ destruct (decide (P1 a)) as [HP1HnP1].
+  rewrite !filter_cons_True.
+ + by rewrite IH.
+ + by apply HPiff.
+ + done.
+  rewrite !filter_cons_False.
+ + by rewrite IH.
+ + by rewrite <HPiff.
+ + done.
+Qed.
+
(** ** Properties of the [prefix] and [suffix] predicates *)
Global Instance: PreOrder (@prefix A).
Proof.

GitLab
From 7440006ed3bb7f2fe1a6d69acdd948ef68f4248d Mon Sep 17 00:00:00 2001
From: Ralf Jung
Date: Tue, 7 Jul 2020 13:34:12 +0200
Subject: [PATCH 2/5] add map_filter_fmap

theories/fin_maps.v  27 +++++++++++++++++++++++++++
1 file changed, 27 insertions(+)
diff git a/theories/fin_maps.v b/theories/fin_maps.v
index 23dc8f97..fe91a90d 100644
 a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ 1132,6 +1132,10 @@ Section map_filter.
+ rewrite Eq, Hm, lookup_insert. naive_solver.
+ by rewrite lookup_insert_ne.
Qed.
+ Lemma map_filter_lookup_Some_2 m i x :
+ m !! i = Some x ∧ P (i, x) →
+ filter P m !! i = Some x.
+ Proof. 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).
@@ 1139,6 +1143,10 @@ Section map_filter.
rewrite eq_None_not_Some. unfold is_Some.
setoid_rewrite map_filter_lookup_Some. naive_solver.
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.
Lemma map_filter_lookup_eq m1 m2 :
(∀ k x, P (k,x) → m1 !! k = Some x ↔ m2 !! k = Some x) →
@@ 1200,6 +1208,25 @@ Section map_filter.
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.
+ rewrite lookup_fmap.
+ destruct (m !! i) as [v] eqn:Hmi.
+  destruct (decide (P (i,f v))) as [HPHnP].
+ + erewrite !map_filter_lookup_Some_2; [done..].
+ * by rewrite Hmi.
+ * by rewrite lookup_fmap, Hmi.
+ + rewrite !map_filter_lookup_None_2; [done..]; right.
+ * intros v'. rewrite Hmi. intros [=<]. done.
+ * intros v'. rewrite lookup_fmap, Hmi. intros [=<]. done.
+  rewrite !map_filter_lookup_None_2; [done..]; left.
+ + done.
+ + rewrite lookup_fmap, Hmi. done.
+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.

GitLab
From ae08f1791dd3f4d1d262a3a6453850369f426485 Mon Sep 17 00:00:00 2001
From: Ralf Jung
Date: Tue, 7 Jul 2020 13:37:18 +0200
Subject: [PATCH 3/5] add map_filter_insert_not_delete
by Tej

theories/fin_maps.v  7 +++++++
1 file changed, 7 insertions(+)
diff git a/theories/fin_maps.v b/theories/fin_maps.v
index fe91a90d..fe519fcc 100644
 a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ 1178,6 +1178,13 @@ Section map_filter.
(∀ y, ¬ P (i, y)) → filter P (<[i:=x]> m) = filter P m.
Proof. intros HP. by apply map_filter_insert_not'. Qed.
+ Lemma map_filter_insert_not_delete m i x :
+ ¬ P (i, x) → filter P (<[i:=x]> m) = (filter P (delete i m)).
+ Proof.
+ intros. rewrite <insert_delete, map_filter_insert_not'; try done.
+ rewrite lookup_delete; done.
+ Qed.
+
Lemma map_filter_delete m i : filter P (delete i m) = delete i (filter P m).
Proof.
apply map_eq. intros j. apply option_eq; intros y.

GitLab
From ee66c750581c9cccca94d65cee7ac8a361ff2037 Mon Sep 17 00:00:00 2001
From: Ralf Jung
Date: Tue, 7 Jul 2020 14:04:20 +0200
Subject: [PATCH 4/5] apply review feedback

theories/fin_maps.v  23 ++++++++++++++++
1 file changed, 16 insertions(+), 7 deletions()
diff git a/theories/fin_maps.v b/theories/fin_maps.v
index fe519fcc..9d56dd62 100644
 a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ 1132,10 +1132,15 @@ Section map_filter.
+ rewrite Eq, Hm, lookup_insert. naive_solver.
+ by rewrite lookup_insert_ne.
Qed.
+ Lemma map_filter_lookup_Some_1 m i x :
+ filter P m !! i = Some x →
+ 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 ∧ P (i, x) →
+ m !! i = Some x →
+ P (i, x) →
filter P m !! i = Some x.
 Proof. apply map_filter_lookup_Some. Qed.
+ 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).
@@ 1143,6 +1148,10 @@ Section map_filter.
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).
+ 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.
@@ 1179,9 +1188,10 @@ Section map_filter.
Proof. intros HP. by apply map_filter_insert_not'. Qed.
Lemma map_filter_insert_not_delete m i x :
 ¬ P (i, x) → filter P (<[i:=x]> m) = (filter P (delete i m)).
+ ¬ P (i, x) → filter P (<[i:=x]> m) = filter P (delete i m).
Proof.
 intros. rewrite <insert_delete, map_filter_insert_not'; try done.
+ intros. rewrite <insert_delete by done.
+ rewrite map_filter_insert_not'; [done..].
rewrite lookup_delete; done.
Qed.
@@ 1223,9 +1233,8 @@ Proof.
rewrite lookup_fmap.
destruct (m !! i) as [v] eqn:Hmi.
 destruct (decide (P (i,f v))) as [HPHnP].
 + erewrite !map_filter_lookup_Some_2; [done..].
 * by rewrite Hmi.
 * by rewrite lookup_fmap, Hmi.
+ + erewrite !map_filter_lookup_Some_2; try done.
+ by rewrite lookup_fmap, Hmi.
+ rewrite !map_filter_lookup_None_2; [done..]; right.
* intros v'. rewrite Hmi. intros [=<]. done.
* intros v'. rewrite lookup_fmap, Hmi. intros [=<]. done.

GitLab
From d47170838a00ef0908cd2793409d0e53154a8f1f Mon Sep 17 00:00:00 2001
From: Ralf Jung
Date: Wed, 15 Jul 2020 18:48:22 +0200
Subject: [PATCH 5/5] shorter proofs and other feedback by Robbert

theories/fin_maps.v  30 ++++++++++++
theories/list.v  12 +++
2 files changed, 15 insertions(+), 27 deletions()
diff git a/theories/fin_maps.v b/theories/fin_maps.v
index 9d56dd62..447b6751 100644
 a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ 1132,9 +1132,11 @@ Section map_filter.
+ rewrite Eq, Hm, lookup_insert. naive_solver.
+ by rewrite lookup_insert_ne.
Qed.
 Lemma map_filter_lookup_Some_1 m i x :
 filter P m !! i = Some x →
 m !! i = Some x ∧ P (i,x).
+ Lemma map_filter_lookup_Some_11 m i x :
+ filter P m !! i = Some x → m !! i = Some x.
+ Proof. apply map_filter_lookup_Some. Qed.
+ Lemma map_filter_lookup_Some_12 m 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 →
@@ 1229,21 +1231,13 @@ 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.
 rewrite lookup_fmap.
 destruct (m !! i) as [v] eqn:Hmi.
  destruct (decide (P (i,f v))) as [HPHnP].
 + erewrite !map_filter_lookup_Some_2; try done.
 by rewrite lookup_fmap, Hmi.
 + rewrite !map_filter_lookup_None_2; [done..]; right.
 * intros v'. rewrite Hmi. intros [=<]. done.
 * intros v'. rewrite lookup_fmap, Hmi. intros [=<]. done.
  rewrite !map_filter_lookup_None_2; [done..]; left.
 + done.
 + rewrite lookup_fmap, Hmi. done.
Qed.

Lemma map_filter_iff {A} (P1 P2 : K * A → Prop) `{!∀ x, Decision (P1 x), !∀ x, Decision (P2 x)} (m : M A) :
+ 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.
diff git a/theories/list.v b/theories/list.v
index 7da129df..71af4c0f 100644
 a/theories/list.v
+++ b/theories/list.v
@@ 1797,15 +1797,9 @@ Lemma list_filter_iff (P1 P2 : A → Prop)
filter P1 l = filter P2 l.
Proof.
intros HPiff. induction l as [a l IH]; [done].
 destruct (decide (P1 a)) as [HP1HnP1].
  rewrite !filter_cons_True.
 + by rewrite IH.
 + by apply HPiff.
 + done.
  rewrite !filter_cons_False.
 + by rewrite IH.
 + by rewrite <HPiff.
 + done.
+ destruct (decide (P1 a)).
+  rewrite !filter_cons_True by naive_solver. by rewrite IH.
+  rewrite !filter_cons_False by naive_solver. by rewrite IH.
Qed.
(** ** Properties of the [prefix] and [suffix] predicates *)

GitLab