Commit 9ef1998d by Robbert Krebbers Committed by Ralf Jung

### Tweak proofs.

parent 0bd1de5b
 ... ... @@ -1184,32 +1184,26 @@ Section map. Lemma big_sepM_pure_1 (φ : K → A → Prop) m : ([∗ map] k↦x ∈ m, ⌜φ k x⌝) ⊢@{PROP} ⌜map_Forall φ m⌝. Proof. induction m using map_ind; simpl. - rewrite pure_True; first by apply True_intro. apply map_Forall_empty. - rewrite -> big_sepM_insert by auto. rewrite -> map_Forall_insert by auto. rewrite IHm sep_and -pure_and. apply pure_mono. done. induction m as [|k x m ? IH] using map_ind. { apply pure_intro, map_Forall_empty. } rewrite big_sepM_insert // IH sep_and -pure_and. by rewrite -map_Forall_insert. Qed. Lemma big_sepM_affinely_pure_2 (φ : K → A → Prop) m : ⌜map_Forall φ m⌝ ⊢@{PROP} ([∗ map] k↦x ∈ m, ⌜φ k x⌝). Proof. induction m using map_ind; simpl. - rewrite big_sepM_empty. apply affinely_elim_emp. - rewrite -> big_sepM_insert by auto. rewrite -> map_Forall_insert by auto. rewrite pure_and affinely_and IHm persistent_and_sep_1. done. induction m as [|k x m ? IH] using map_ind. { rewrite big_sepM_empty. apply affinely_elim_emp. } rewrite big_sepM_insert // -IH. by rewrite -persistent_and_sep_1 -affinely_and -pure_and map_Forall_insert. Qed. (** The general backwards direction requires [BiAffine] to cover the empty case. *) Lemma big_sepM_pure `{!BiAffine PROP} (φ : K → A → Prop) m : ([∗ map] k↦x ∈ m, ⌜φ k x⌝) ⊣⊢@{PROP} ⌜map_Forall φ m⌝. Proof. apply (anti_symm (⊢)); first by apply big_sepM_pure_1. rewrite -(affine_affinely (⌜map_Forall φ m⌝)%I). rewrite big_sepM_affinely_pure_2. apply big_sepM_mono=>???. rewrite affine_affinely. done. rewrite -(affine_affinely ⌜_⌝%I). rewrite big_sepM_affinely_pure_2. by setoid_rewrite affinely_elim. Qed. Lemma big_sepM_persistently `{BiAffine PROP} Φ m : ... ...
 ... ... @@ -198,9 +198,10 @@ Global Instance into_pure_persistently P φ : IntoPure P φ → IntoPure ( P) φ. Proof. rewrite /IntoPure=> ->. apply: persistently_elim. Qed. Global Instance into_pure_big_sepM {K A} `{Countable K} (Φ : K → A → PROP) (φ : K → A → Prop) (m: gmap K A) : (∀ k v, IntoPure (Φ k v) (φ k v)) → IntoPure ([∗ map] k↦x ∈ m, Φ k x) (map_Forall φ m). Global Instance into_pure_big_sepM `{Countable K} {A} (Φ : K → A → PROP) (φ : K → A → Prop) (m : gmap K A) : (∀ k x, IntoPure (Φ k x) (φ k x)) → IntoPure ([∗ map] k↦x ∈ m, Φ k x) (map_Forall φ m). Proof. rewrite /IntoPure. intros HΦ. setoid_rewrite HΦ. rewrite big_sepM_pure_1. done. ... ... @@ -297,18 +298,17 @@ Proof. by rewrite -persistent_absorbingly_affinely_2. Qed. Global Instance from_pure_big_sepM {K A} `{Countable K} a (Φ : K → A → PROP) (φ : K → A → Prop) (m: gmap K A) : (∀ k v, FromPure a (Φ k v) (φ k v)) → Global Instance from_pure_big_sepM `{Countable K} {A} a (Φ : K → A → PROP) (φ : K → A → Prop) (m : gmap K A) : (∀ k x, FromPure a (Φ k x) (φ k x)) → TCOr (TCEq a true) (BiAffine PROP) → FromPure a ([∗ map] k↦x ∈ m, Φ k x) (map_Forall φ m). Proof. rewrite /FromPure. destruct a; simpl; intros HΦ Haffine. - rewrite big_sepM_affinely_pure_2. setoid_rewrite HΦ. done. - destruct Haffine as [?%TCEq_eq|?]; first done. rewrite -big_sepM_pure. setoid_rewrite HΦ. done. - destruct Haffine as [[=]%TCEq_eq|?]. rewrite -big_sepM_pure. setoid_rewrite HΦ. done. Qed. (** IntoPersistent *) ... ...
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment