Commit 2f15e258 by Robbert

### Merge branch 'ralf/map_filter' into 'master'

```Lemmas about "filter" on maps

See merge request !172```
parents 5bdd73dd 653cb9db
Pipeline #31528 passed with stage
in 11 minutes and 16 seconds
 ... ... @@ -1132,6 +1132,17 @@ Section map_filter. + rewrite Eq, Hm, lookup_insert. naive_solver. + by rewrite lookup_insert_ne. Qed. 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 → P (i, x) → filter P m !! i = Some x. 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). ... ... @@ -1139,6 +1150,14 @@ 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. 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) → ... ... @@ -1170,6 +1189,14 @@ 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 by done. rewrite map_filter_insert_not'; [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. ... ... @@ -1200,6 +1227,24 @@ 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. 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. (** ** Properties of the [map_Forall] predicate *) Section map_Forall. Context {A} (P : K → A → Prop). ... ...
 ... ... @@ -1791,6 +1791,17 @@ 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)). - 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 *) Global Instance: PreOrder (@prefix A). Proof. ... ...
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!