Commit 4201b3b2 authored by Robbert's avatar Robbert

Merge branch 'robbert/big_sepM2' into 'master'

big_sepM2 and associated lemmas

See merge request !228
parents 5f53a267 c24e0bb2
......@@ -11,5 +11,5 @@ install: [make "install"]
remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/iris"]
depends: [
"coq" { (>= "8.7.1" & < "8.10~") | (= "dev") }
"coq-stdpp" { (= "dev.2019-03-16.1.700545bb") | (= "dev") }
"coq-stdpp" { (= "dev.2019-03-26.0.d98ab4e4") | (= "dev") }
]
This diff is collapsed.
......@@ -245,6 +245,13 @@ Proof.
- rewrite -(exist_intro ()). done.
Qed.
Lemma impl_curry P Q R : (P Q R) (P Q R).
Proof.
apply (anti_symm _).
- apply impl_intro_l. by rewrite (comm _ P) -and_assoc !impl_elim_r.
- do 2 apply impl_intro_l. by rewrite assoc (comm _ Q) impl_elim_r.
Qed.
Lemma or_and_l P Q R : P Q R (P Q) (P R).
Proof.
apply (anti_symm ()); first auto.
......
......@@ -127,6 +127,13 @@ Reserved Notation "'[∗' 'map]' x ∈ m , P"
(at level 200, m at level 10, x at level 1, right associativity,
format "[∗ map] x ∈ m , P").
Reserved Notation "'[∗' 'map]' k ↦ x1 ; x2 ∈ m1 ; m2 , P"
(at level 200, m1, m2 at level 10, k, x1, x2 at level 1, right associativity,
format "[∗ map] k ↦ x1 ; x2 ∈ m1 ; m2 , P").
Reserved Notation "'[∗' 'map]' x1 ; x2 ∈ m1 ; m2 , P"
(at level 200, m1, m2 at level 10, x1, x2 at level 1, right associativity,
format "[∗ map] x1 ; x2 ∈ m1 ; m2 , P").
Reserved Notation "'[∗' 'set]' x ∈ X , P"
(at level 200, X at level 10, x at level 1, right associativity,
format "[∗ set] x ∈ X , P").
......
......@@ -650,6 +650,14 @@ Proof.
rewrite /IntoLaterN /MaybeIntoLaterN=> ?.
rewrite big_opM_commute. by apply big_sepM_mono.
Qed.
Global Instance into_laterN_big_sepM2 n `{Countable K} {A B}
(Φ Ψ : K A B PROP) (m1 : gmap K A) (m2 : gmap K B) :
( x1 x2 k, IntoLaterN false n (Φ k x1 x2) (Ψ k x1 x2))
IntoLaterN false n ([ map] k x1;x2 m1;m2, Φ k x1 x2) ([ map] k x1;x2 m1;m2, Ψ k x1 x2).
Proof.
rewrite /IntoLaterN /MaybeIntoLaterN=> HΦΨ.
rewrite -big_sepM2_laterN_2. by apply big_sepM2_mono.
Qed.
Global Instance into_laterN_big_sepS n `{Countable A}
(Φ Ψ : A PROP) (X : gset A) :
( x, IntoLaterN false n (Φ x) (Ψ x))
......
......@@ -2414,6 +2414,8 @@ Hint Extern 0 (envs_entails _ (big_sepL2 _ _ _)) =>
rewrite envs_entails_eq; apply big_sepL2_nil' : core.
Hint Extern 0 (envs_entails _ (big_opM _ _ _)) =>
rewrite envs_entails_eq; apply big_sepM_empty' : core.
Hint Extern 0 (envs_entails _ (big_sepM2 _ _ _)) =>
rewrite envs_entails_eq; apply big_sepM2_empty' : core.
Hint Extern 0 (envs_entails _ (big_opS _ _ _)) =>
rewrite envs_entails_eq; apply big_sepS_empty' : core.
Hint Extern 0 (envs_entails _ (big_opMS _ _ _)) =>
......
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