Commit 463f24ef authored by Robbert's avatar Robbert

Merge branch 'seal_big_opM' into 'master'

Seal big_sepM2

See merge request iris/iris!352
parents d6c5699b bdaec8c5
...@@ -44,6 +44,8 @@ Coq development, but not every API-breaking change is listed. Changes marked ...@@ -44,6 +44,8 @@ Coq development, but not every API-breaking change is listed. Changes marked
STS RA. STS RA.
* Added the type `siProp` of "plain" step-indexed propositions, together with * Added the type `siProp` of "plain" step-indexed propositions, together with
basic proofmode support. basic proofmode support.
* Sealed the definitions of `big_opS`, `big_opMS`, `big_opM` and `big_sepM2`
to prevent undesired simplification.
## Iris 3.2.0 (released 2019-08-29) ## Iris 3.2.0 (released 2019-08-29)
......
...@@ -35,11 +35,13 @@ Notation "'[^' o 'list]' x ∈ l , P" := (big_opL o (λ _ x, P) l) ...@@ -35,11 +35,13 @@ Notation "'[^' o 'list]' x ∈ l , P" := (big_opL o (λ _ x, P) l)
(at level 200, o at level 1, l at level 10, x at level 1, right associativity, (at level 200, o at level 1, l at level 10, x at level 1, right associativity,
format "[^ o list] x ∈ l , P") : stdpp_scope. format "[^ o list] x ∈ l , P") : stdpp_scope.
Definition big_opM `{Monoid M o} `{Countable K} {A} (f : K A M) Definition big_opM_def `{Monoid M o} `{Countable K} {A} (f : K A M)
(m : gmap K A) : M := big_opL o (λ _, curry f) (map_to_list m). (m : gmap K A) : M := big_opL o (λ _, curry f) (map_to_list m).
Definition big_opM_aux : seal (@big_opM_def). by eexists. Qed.
Definition big_opM := big_opM_aux.(unseal).
Arguments big_opM {M} o {_ K _ _ A} _ _.
Definition big_opM_eq : @big_opM = @big_opM_def := big_opM_aux.(seal_eq).
Instance: Params (@big_opM) 7 := {}. Instance: Params (@big_opM) 7 := {}.
Arguments big_opM {M} o {_ K _ _ A} _ _ : simpl never.
Typeclasses Opaque big_opM.
Notation "'[^' o 'map]' k ↦ x ∈ m , P" := (big_opM o (λ k x, P) m) Notation "'[^' o 'map]' k ↦ x ∈ m , P" := (big_opM o (λ k x, P) m)
(at level 200, o at level 1, m at level 10, k, x at level 1, right associativity, (at level 200, o at level 1, m at level 10, k, x at level 1, right associativity,
format "[^ o map] k ↦ x ∈ m , P") : stdpp_scope. format "[^ o map] k ↦ x ∈ m , P") : stdpp_scope.
...@@ -47,20 +49,24 @@ Notation "'[^' o 'map]' x ∈ m , P" := (big_opM o (λ _ x, P) m) ...@@ -47,20 +49,24 @@ Notation "'[^' o 'map]' x ∈ m , P" := (big_opM o (λ _ x, P) m)
(at level 200, o at level 1, m at level 10, x at level 1, right associativity, (at level 200, o at level 1, m at level 10, x at level 1, right associativity,
format "[^ o map] x ∈ m , P") : stdpp_scope. format "[^ o map] x ∈ m , P") : stdpp_scope.
Definition big_opS `{Monoid M o} `{Countable A} (f : A M) Definition big_opS_def `{Monoid M o} `{Countable A} (f : A M)
(X : gset A) : M := big_opL o (λ _, f) (elements X). (X : gset A) : M := big_opL o (λ _, f) (elements X).
Definition big_opS_aux : seal (@big_opS_def). by eexists. Qed.
Definition big_opS := big_opS_aux.(unseal).
Arguments big_opS {M} o {_ A _ _} _ _.
Definition big_opS_eq : @big_opS = @big_opS_def := big_opS_aux.(seal_eq).
Instance: Params (@big_opS) 6 := {}. Instance: Params (@big_opS) 6 := {}.
Arguments big_opS {M} o {_ A _ _} _ _ : simpl never.
Typeclasses Opaque big_opS.
Notation "'[^' o 'set]' x ∈ X , P" := (big_opS o (λ x, P) X) Notation "'[^' o 'set]' x ∈ X , P" := (big_opS o (λ x, P) X)
(at level 200, o at level 1, X at level 10, x at level 1, right associativity, (at level 200, o at level 1, X at level 10, x at level 1, right associativity,
format "[^ o set] x ∈ X , P") : stdpp_scope. format "[^ o set] x ∈ X , P") : stdpp_scope.
Definition big_opMS `{Monoid M o} `{Countable A} (f : A M) Definition big_opMS_def `{Monoid M o} `{Countable A} (f : A M)
(X : gmultiset A) : M := big_opL o (λ _, f) (elements X). (X : gmultiset A) : M := big_opL o (λ _, f) (elements X).
Instance: Params (@big_opMS) 7 := {}. Definition big_opMS_aux : seal (@big_opMS_def). by eexists. Qed.
Arguments big_opMS {M} o {_ A _ _} _ _ : simpl never. Definition big_opMS := big_opMS_aux.(unseal).
Typeclasses Opaque big_opMS. Arguments big_opMS {M} o {_ A _ _} _ _.
Definition big_opMS_eq : @big_opMS = @big_opMS_def := big_opMS_aux.(seal_eq).
Instance: Params (@big_opMS) 6 := {}.
Notation "'[^' o 'mset]' x ∈ X , P" := (big_opMS o (λ x, P) X) Notation "'[^' o 'mset]' x ∈ X , P" := (big_opMS o (λ x, P) X)
(at level 200, o at level 1, X at level 10, x at level 1, right associativity, (at level 200, o at level 1, X at level 10, x at level 1, right associativity,
format "[^ o mset] x ∈ X , P") : stdpp_scope. format "[^ o mset] x ∈ X , P") : stdpp_scope.
...@@ -171,7 +177,7 @@ Section gmap. ...@@ -171,7 +177,7 @@ Section gmap.
( k x, m !! k = Some x R (f k x) (g k x)) ( k x, m !! k = Some x R (f k x) (g k x))
R ([^o map] k x m, f k x) ([^o map] k x m, g k x). R ([^o map] k x m, f k x) ([^o map] k x m, g k x).
Proof. Proof.
intros ?? Hf. apply (big_opL_forall R); auto. intros ?? Hf. rewrite big_opM_eq. apply (big_opL_forall R); auto.
intros k [i x] ?%elem_of_list_lookup_2. by apply Hf, elem_of_map_to_list. intros k [i x] ?%elem_of_list_lookup_2. by apply Hf, elem_of_map_to_list.
Qed. Qed.
...@@ -194,12 +200,12 @@ Section gmap. ...@@ -194,12 +200,12 @@ Section gmap.
Proof. intros f g Hf m ? <-. apply big_opM_forall; apply _ || intros; apply Hf. Qed. Proof. intros f g Hf m ? <-. apply big_opM_forall; apply _ || intros; apply Hf. Qed.
Lemma big_opM_empty f : ([^o map] kx , f k x) = monoid_unit. Lemma big_opM_empty f : ([^o map] kx , f k x) = monoid_unit.
Proof. by rewrite /big_opM map_to_list_empty. Qed. Proof. by rewrite big_opM_eq /big_opM_def map_to_list_empty. Qed.
Lemma big_opM_insert f m i x : Lemma big_opM_insert f m i x :
m !! i = None m !! i = None
([^o map] ky <[i:=x]> m, f k y) f i x `o` [^o map] ky m, f k y. ([^o map] ky <[i:=x]> m, f k y) f i x `o` [^o map] ky m, f k y.
Proof. intros ?. by rewrite /big_opM map_to_list_insert. Qed. Proof. intros ?. by rewrite big_opM_eq /big_opM_def map_to_list_insert. Qed.
Lemma big_opM_delete f m i x : Lemma big_opM_delete f m i x :
m !! i = Some x m !! i = Some x
...@@ -216,12 +222,12 @@ Section gmap. ...@@ -216,12 +222,12 @@ Section gmap.
Qed. Qed.
Lemma big_opM_unit m : ([^o map] ky m, monoid_unit) (monoid_unit : M). Lemma big_opM_unit m : ([^o map] ky m, monoid_unit) (monoid_unit : M).
Proof. induction m using map_ind; rewrite /= ?big_opM_insert ?left_id //. Qed. Proof. by induction m using map_ind; rewrite /= ?big_opM_insert ?left_id // big_opM_eq. Qed.
Lemma big_opM_fmap {B} (h : A B) (f : K B M) m : Lemma big_opM_fmap {B} (h : A B) (f : K B M) m :
([^o map] ky h <$> m, f k y) ([^o map] ky m, f k (h y)). ([^o map] ky h <$> m, f k y) ([^o map] ky m, f k (h y)).
Proof. Proof.
rewrite /big_opM map_to_list_fmap big_opL_fmap. rewrite big_opM_eq /big_opM_def map_to_list_fmap big_opL_fmap.
by apply big_opL_proper=> ? [??]. by apply big_opL_proper=> ? [??].
Qed. Qed.
...@@ -262,7 +268,7 @@ Section gmap. ...@@ -262,7 +268,7 @@ Section gmap.
Lemma big_opM_op f g m : Lemma big_opM_op f g m :
([^o map] kx m, f k x `o` g k x) ([^o map] kx m, f k x `o` g k x)
([^o map] kx m, f k x) `o` ([^o map] kx m, g k x). ([^o map] kx m, f k x) `o` ([^o map] kx m, g k x).
Proof. rewrite /big_opM -big_opL_op. by apply big_opL_proper=> ? [??]. Qed. Proof. rewrite big_opM_eq /big_opM_def -big_opL_op. by apply big_opL_proper=> ? [??]. Qed.
End gmap. End gmap.
...@@ -277,7 +283,7 @@ Section gset. ...@@ -277,7 +283,7 @@ Section gset.
( x, x X R (f x) (g x)) ( x, x X R (f x) (g x))
R ([^o set] x X, f x) ([^o set] x X, g x). R ([^o set] x X, f x) ([^o set] x X, g x).
Proof. Proof.
intros ?? Hf. apply (big_opL_forall R); auto. rewrite big_opS_eq. intros ?? Hf. apply (big_opL_forall R); auto.
intros k x ?%elem_of_list_lookup_2. by apply Hf, elem_of_elements. intros k x ?%elem_of_list_lookup_2. by apply Hf, elem_of_elements.
Qed. Qed.
...@@ -298,11 +304,11 @@ Section gset. ...@@ -298,11 +304,11 @@ Section gset.
Proof. intros f g Hf m ? <-. apply big_opS_forall; apply _ || intros; apply Hf. Qed. Proof. intros f g Hf m ? <-. apply big_opS_forall; apply _ || intros; apply Hf. Qed.
Lemma big_opS_empty f : ([^o set] x , f x) = monoid_unit. Lemma big_opS_empty f : ([^o set] x , f x) = monoid_unit.
Proof. by rewrite /big_opS elements_empty. Qed. Proof. by rewrite big_opS_eq /big_opS_def elements_empty. Qed.
Lemma big_opS_insert f X x : Lemma big_opS_insert f X x :
x X ([^o set] y {[ x ]} X, f y) (f x `o` [^o set] y X, f y). x X ([^o set] y {[ x ]} X, f y) (f x `o` [^o set] y X, f y).
Proof. intros. by rewrite /big_opS elements_union_singleton. Qed. Proof. intros. by rewrite big_opS_eq /big_opS_def elements_union_singleton. Qed.
Lemma big_opS_fn_insert {B} (f : A B M) h X x b : Lemma big_opS_fn_insert {B} (f : A B M) h X x b :
x X x X
([^o set] y {[ x ]} X, f y (<[x:=b]> h y)) ([^o set] y {[ x ]} X, f y (<[x:=b]> h y))
...@@ -334,22 +340,22 @@ Section gset. ...@@ -334,22 +340,22 @@ Section gset.
Qed. Qed.
Lemma big_opS_singleton f x : ([^o set] y {[ x ]}, f y) f x. Lemma big_opS_singleton f x : ([^o set] y {[ x ]}, f y) f x.
Proof. intros. by rewrite /big_opS elements_singleton /= right_id. Qed. Proof. intros. by rewrite big_opS_eq /big_opS_def elements_singleton /= right_id. Qed.
Lemma big_opS_unit X : ([^o set] y X, monoid_unit) (monoid_unit : M). Lemma big_opS_unit X : ([^o set] y X, monoid_unit) (monoid_unit : M).
Proof. Proof.
induction X using set_ind_L; rewrite /= ?big_opS_insert ?left_id //. by induction X using set_ind_L; rewrite /= ?big_opS_insert ?left_id // big_opS_eq.
Qed. Qed.
Lemma big_opS_op f g X : Lemma big_opS_op f g X :
([^o set] y X, f y `o` g y) ([^o set] y X, f y) `o` ([^o set] y X, g y). ([^o set] y X, f y `o` g y) ([^o set] y X, f y) `o` ([^o set] y X, g y).
Proof. by rewrite /big_opS -big_opL_op. Qed. Proof. by rewrite big_opS_eq /big_opS_def -big_opL_op. Qed.
End gset. End gset.
Lemma big_opM_dom `{Countable K} {A} (f : K M) (m : gmap K A) : Lemma big_opM_dom `{Countable K} {A} (f : K M) (m : gmap K A) :
([^o map] k_ m, f k) ([^o set] k dom _ m, f k). ([^o map] k_ m, f k) ([^o set] k dom _ m, f k).
Proof. Proof.
induction m as [|i x ?? IH] using map_ind; [by rewrite dom_empty_L|]. induction m as [|i x ?? IH] using map_ind; [by rewrite big_opM_eq big_opS_eq dom_empty_L|].
by rewrite dom_insert_L big_opM_insert // IH big_opS_insert ?not_elem_of_dom. by rewrite dom_insert_L big_opM_insert // IH big_opS_insert ?not_elem_of_dom.
Qed. Qed.
...@@ -364,7 +370,7 @@ Section gmultiset. ...@@ -364,7 +370,7 @@ Section gmultiset.
( x, x X R (f x) (g x)) ( x, x X R (f x) (g x))
R ([^o mset] x X, f x) ([^o mset] x X, g x). R ([^o mset] x X, f x) ([^o mset] x X, g x).
Proof. Proof.
intros ?? Hf. apply (big_opL_forall R); auto. rewrite big_opMS_eq. intros ?? Hf. apply (big_opL_forall R); auto.
intros k x ?%elem_of_list_lookup_2. by apply Hf, gmultiset_elem_of_elements. intros k x ?%elem_of_list_lookup_2. by apply Hf, gmultiset_elem_of_elements.
Qed. Qed.
...@@ -385,15 +391,15 @@ Section gmultiset. ...@@ -385,15 +391,15 @@ Section gmultiset.
Proof. intros f g Hf m ? <-. apply big_opMS_forall; apply _ || intros; apply Hf. Qed. Proof. intros f g Hf m ? <-. apply big_opMS_forall; apply _ || intros; apply Hf. Qed.
Lemma big_opMS_empty f : ([^o mset] x , f x) = monoid_unit. Lemma big_opMS_empty f : ([^o mset] x , f x) = monoid_unit.
Proof. by rewrite /big_opMS gmultiset_elements_empty. Qed. Proof. by rewrite big_opMS_eq /big_opMS_def gmultiset_elements_empty. Qed.
Lemma big_opMS_disj_union f X Y : Lemma big_opMS_disj_union f X Y :
([^o mset] y X Y, f y) ([^o mset] y X, f y) `o` [^o mset] y Y, f y. ([^o mset] y X Y, f y) ([^o mset] y X, f y) `o` [^o mset] y Y, f y.
Proof. by rewrite /big_opMS gmultiset_elements_disj_union big_opL_app. Qed. Proof. by rewrite big_opMS_eq /big_opMS_def gmultiset_elements_disj_union big_opL_app. Qed.
Lemma big_opMS_singleton f x : ([^o mset] y {[ x ]}, f y) f x. Lemma big_opMS_singleton f x : ([^o mset] y {[ x ]}, f y) f x.
Proof. Proof.
intros. by rewrite /big_opMS gmultiset_elements_singleton /= right_id. intros. by rewrite big_opMS_eq /big_opMS_def gmultiset_elements_singleton /= right_id.
Qed. Qed.
Lemma big_opMS_delete f X x : Lemma big_opMS_delete f X x :
...@@ -405,13 +411,13 @@ Section gmultiset. ...@@ -405,13 +411,13 @@ Section gmultiset.
Lemma big_opMS_unit X : ([^o mset] y X, monoid_unit) (monoid_unit : M). Lemma big_opMS_unit X : ([^o mset] y X, monoid_unit) (monoid_unit : M).
Proof. Proof.
induction X using gmultiset_ind; by induction X using gmultiset_ind;
rewrite /= ?big_opMS_disj_union ?big_opMS_singleton ?left_id //. rewrite /= ?big_opMS_disj_union ?big_opMS_singleton ?left_id // big_opMS_eq.
Qed. Qed.
Lemma big_opMS_op f g X : Lemma big_opMS_op f g X :
([^o mset] y X, f y `o` g y) ([^o mset] y X, f y) `o` ([^o mset] y X, g y). ([^o mset] y X, f y `o` g y) ([^o mset] y X, f y) `o` ([^o mset] y X, g y).
Proof. by rewrite /big_opMS -big_opL_op. Qed. Proof. by rewrite big_opMS_eq /big_opMS_def -big_opL_op. Qed.
End gmultiset. End gmultiset.
End big_op. End big_op.
......
...@@ -13,7 +13,7 @@ Qed. ...@@ -13,7 +13,7 @@ Qed.
Lemma big_opM_None {M : cmraT} `{Countable K} {A} (f : K A option M) m : Lemma big_opM_None {M : cmraT} `{Countable K} {A} (f : K A option M) m :
([^op map] kx m, f k x) = None k x, m !! k = Some x f k x = None. ([^op map] kx m, f k x) = None k x, m !! k = Some x f k x = None.
Proof. Proof.
induction m as [|i x m ? IH] using map_ind=> //=. induction m as [|i x m ? IH] using map_ind=> /=; first by rewrite big_opM_eq.
rewrite -equiv_None big_opM_insert // equiv_None op_None IH. split. rewrite -equiv_None big_opM_insert // equiv_None op_None IH. split.
{ intros [??] k y. rewrite lookup_insert_Some; naive_solver. } { intros [??] k y. rewrite lookup_insert_Some; naive_solver. }
intros Hm; split. intros Hm; split.
...@@ -23,7 +23,7 @@ Qed. ...@@ -23,7 +23,7 @@ Qed.
Lemma big_opS_None {M : cmraT} `{Countable A} (f : A option M) X : Lemma big_opS_None {M : cmraT} `{Countable A} (f : A option M) X :
([^op set] x X, f x) = None x, x X f x = None. ([^op set] x X, f x) = None x, x X f x = None.
Proof. Proof.
induction X as [|x X ? IH] using set_ind_L; [done|]. induction X as [|x X ? IH] using set_ind_L; [by rewrite big_opS_eq |].
rewrite -equiv_None big_opS_insert // equiv_None op_None IH. set_solver. rewrite -equiv_None big_opS_insert // equiv_None op_None IH. set_solver.
Qed. Qed.
Lemma big_opMS_None {M : cmraT} `{Countable A} (f : A option M) X : Lemma big_opMS_None {M : cmraT} `{Countable A} (f : A option M) X :
......
...@@ -100,7 +100,7 @@ Qed. ...@@ -100,7 +100,7 @@ Qed.
Lemma box_alloc : box N True%I. Lemma box_alloc : box N True%I.
Proof. Proof.
iIntros. iExists (λ _, True)%I. iSplit; by auto. iIntros. iExists (λ _, True)%I. by rewrite !big_opM_empty.
Qed. Qed.
Lemma slice_insert_empty E q f Q P : Lemma slice_insert_empty E q f Q P :
......
This diff is collapsed.
...@@ -295,7 +295,7 @@ Section plainly_affine_bi. ...@@ -295,7 +295,7 @@ Section plainly_affine_bi.
Lemma impl_wand_plainly P Q : ( P Q) ( P - Q). Lemma impl_wand_plainly P Q : ( P Q) ( P - Q).
Proof. Proof.
apply (anti_symm ()). by rewrite -impl_wand_1. by rewrite impl_wand_plainly_2. apply (anti_symm ()). by rewrite -impl_wand_1. by rewrite impl_wand_plainly_2.
Qed. Qed.
End plainly_affine_bi. End plainly_affine_bi.
(* Conditional plainly *) (* Conditional plainly *)
...@@ -419,7 +419,7 @@ Proof. apply (big_opM_commute _). Qed. ...@@ -419,7 +419,7 @@ Proof. apply (big_opM_commute _). Qed.
Lemma big_sepM2_plainly `{BiAffine PROP, Countable K} {A B} (Φ : K A B PROP) m1 m2 : Lemma big_sepM2_plainly `{BiAffine PROP, Countable K} {A B} (Φ : K A B PROP) m1 m2 :
([ map] kx1;x2 m1;m2, Φ k x1 x2) [ map] kx1;x2 m1;m2, (Φ k x1 x2). ([ map] kx1;x2 m1;m2, Φ k x1 x2) [ map] kx1;x2 m1;m2, (Φ k x1 x2).
Proof. by rewrite /big_sepM2 plainly_and plainly_pure big_sepM_plainly. Qed. Proof. by rewrite big_sepM2_eq /big_sepM2_def plainly_and plainly_pure big_sepM_plainly. Qed.
Lemma big_sepS_plainly `{BiAffine PROP, Countable A} (Φ : A PROP) X : Lemma big_sepS_plainly `{BiAffine PROP, Countable A} (Φ : A PROP) X :
([ set] y X, Φ y) [ set] y X, (Φ y). ([ set] y X, Φ y) [ set] y X, (Φ y).
...@@ -510,34 +510,34 @@ Proof. rewrite big_sepL2_alt. apply _. Qed. ...@@ -510,34 +510,34 @@ Proof. rewrite big_sepL2_alt. apply _. Qed.
Global Instance big_sepM_empty_plain `{BiAffine PROP, Countable K} {A} (Φ : K A PROP) : Global Instance big_sepM_empty_plain `{BiAffine PROP, Countable K} {A} (Φ : K A PROP) :
Plain ([ map] kx , Φ k x). Plain ([ map] kx , Φ k x).
Proof. rewrite /big_opM map_to_list_empty. apply _. Qed. Proof. rewrite big_opM_eq /big_opM_def map_to_list_empty. apply _. Qed.
Global Instance big_sepM_plain `{BiAffine PROP, Countable K} {A} (Φ : K A PROP) m : Global Instance big_sepM_plain `{BiAffine PROP, Countable K} {A} (Φ : K A PROP) m :
( k x, Plain (Φ k x)) Plain ([ map] kx m, Φ k x). ( k x, Plain (Φ k x)) Plain ([ map] kx m, Φ k x).
Proof. intros. apply (big_sepL_plain _ _)=> _ [??]; apply _. Qed. Proof. rewrite big_opM_eq. intros. apply (big_sepL_plain _ _)=> _ [??]; apply _. Qed.
Global Instance big_sepM2_empty_plain `{BiAffine PROP, Countable K} Global Instance big_sepM2_empty_plain `{BiAffine PROP, Countable K}
{A B} (Φ : K A B PROP) : {A B} (Φ : K A B PROP) :
Plain ([ map] kx1;x2 ;, Φ k x1 x2). Plain ([ map] kx1;x2 ;, Φ k x1 x2).
Proof. rewrite /big_sepM2 map_zip_with_empty. apply _. Qed. Proof. rewrite big_sepM2_eq /big_sepM2_def map_zip_with_empty. apply _. Qed.
Global Instance big_sepM2_plain `{BiAffine PROP, Countable K} Global Instance big_sepM2_plain `{BiAffine PROP, Countable K}
{A B} (Φ : K A B PROP) m1 m2 : {A B} (Φ : K A B PROP) m1 m2 :
( k x1 x2, Plain (Φ k x1 x2)) ( k x1 x2, Plain (Φ k x1 x2))
Plain ([ map] kx1;x2 m1;m2, Φ k x1 x2). Plain ([ map] kx1;x2 m1;m2, Φ k x1 x2).
Proof. intros. rewrite /big_sepM2. apply _. Qed. Proof. intros. rewrite big_sepM2_eq. apply _. Qed.
Global Instance big_sepS_empty_plain `{BiAffine PROP, Countable A} (Φ : A PROP) : Global Instance big_sepS_empty_plain `{BiAffine PROP, Countable A} (Φ : A PROP) :
Plain ([ set] x , Φ x). Plain ([ set] x , Φ x).
Proof. rewrite /big_opS elements_empty. apply _. Qed. Proof. rewrite big_opS_eq /big_opS_def elements_empty. apply _. Qed.
Global Instance big_sepS_plain `{BiAffine PROP, Countable A} (Φ : A PROP) X : Global Instance big_sepS_plain `{BiAffine PROP, Countable A} (Φ : A PROP) X :
( x, Plain (Φ x)) Plain ([ set] x X, Φ x). ( x, Plain (Φ x)) Plain ([ set] x X, Φ x).
Proof. rewrite /big_opS. apply _. Qed. Proof. rewrite big_opS_eq. apply _. Qed.
Global Instance big_sepMS_empty_plain `{BiAffine PROP, Countable A} (Φ : A PROP) : Global Instance big_sepMS_empty_plain `{BiAffine PROP, Countable A} (Φ : A PROP) :
Plain ([ mset] x , Φ x). Plain ([ mset] x , Φ x).
Proof. rewrite /big_opMS gmultiset_elements_empty. apply _. Qed. Proof. rewrite big_opMS_eq /big_opMS_def gmultiset_elements_empty. apply _. Qed.
Global Instance big_sepMS_plain `{BiAffine PROP, Countable A} (Φ : A PROP) X : Global Instance big_sepMS_plain `{BiAffine PROP, Countable A} (Φ : A PROP) X :
( x, Plain (Φ x)) Plain ([ mset] x X, Φ x). ( x, Plain (Φ x)) Plain ([ mset] x X, Φ x).
Proof. rewrite /big_opMS. apply _. Qed. Proof. rewrite big_opMS_eq. apply _. Qed.
(* Interaction with equality *) (* Interaction with equality *)
Lemma plainly_internal_eq {A:ofeT} (a b : A) : (a b) @{PROP} a b. Lemma plainly_internal_eq {A:ofeT} (a b : A) : (a b) @{PROP} a b.
......
Markdown is supported
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