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 [HP1|HnP1]. + - 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 [HP|HnP]. + + 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 [HP|HnP]. - + 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 [HP|HnP]. - + 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 [HP1|HnP1]. - - 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