Commit a9031f7f authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

More type annotations for https://github.com/coq/coq/pull/9996.

parent 3a0ab5e6
...@@ -11,5 +11,5 @@ install: [make "install"] ...@@ -11,5 +11,5 @@ install: [make "install"]
remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/iris"] remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/iris"]
depends: [ depends: [
"coq" { (>= "8.7.1" & < "8.10~") | (= "dev") } "coq" { (>= "8.7.1" & < "8.10~") | (= "dev") }
"coq-stdpp" { (= "dev.2019-04-25.0.0f2d2c8a") | (= "dev") } "coq-stdpp" { (= "dev.2019-04-25.1.d6eb24f2") | (= "dev") }
] ]
...@@ -45,21 +45,21 @@ Section mixin. ...@@ -45,21 +45,21 @@ Section mixin.
Record CmraMixin A `{Dist A, Equiv A, PCore A, Op A, Valid A, ValidN A} := { Record CmraMixin A `{Dist A, Equiv A, PCore A, Op A, Valid A, ValidN A} := {
(* setoids *) (* setoids *)
mixin_cmra_op_ne (x : A) : NonExpansive (op x); mixin_cmra_op_ne (x : A) : NonExpansive (op x);
mixin_cmra_pcore_ne n x y cx : mixin_cmra_pcore_ne n (x y : A) cx :
x {n} y pcore x = Some cx cy, pcore y = Some cy cx {n} cy; x {n} y pcore x = Some cx cy, pcore y = Some cy cx {n} cy;
mixin_cmra_validN_ne n : Proper (dist n ==> impl) (validN n); mixin_cmra_validN_ne n : Proper (dist n ==> impl) (validN n);
(* valid *) (* valid *)
mixin_cmra_valid_validN x : x n, {n} x; mixin_cmra_valid_validN (x : A) : x n, {n} x;
mixin_cmra_validN_S n x : {S n} x {n} x; mixin_cmra_validN_S n (x : A) : {S n} x {n} x;
(* monoid *) (* monoid *)
mixin_cmra_assoc : Assoc () (); mixin_cmra_assoc : Assoc (@{A}) ();
mixin_cmra_comm : Comm () (); mixin_cmra_comm : Comm (@{A}) ();
mixin_cmra_pcore_l x cx : pcore x = Some cx cx x x; mixin_cmra_pcore_l (x : A) cx : pcore x = Some cx cx x x;
mixin_cmra_pcore_idemp x cx : pcore x = Some cx pcore cx Some cx; mixin_cmra_pcore_idemp (x : A) cx : pcore x = Some cx pcore cx Some cx;
mixin_cmra_pcore_mono x y cx : mixin_cmra_pcore_mono (x y : A) cx :
x y pcore x = Some cx cy, pcore y = Some cy cx cy; x y pcore x = Some cx cy, pcore y = Some cy cx cy;
mixin_cmra_validN_op_l n x y : {n} (x y) {n} x; mixin_cmra_validN_op_l n (x y : A) : {n} (x y) {n} x;
mixin_cmra_extend n x y1 y2 : mixin_cmra_extend n (x y1 y2 : A) :
{n} x x {n} y1 y2 {n} x x {n} y1 y2
{ z1 : A & { z2 | x z1 z2 z1 {n} y1 z2 {n} y2 } } { z1 : A & { z2 | x z1 z2 z1 {n} y1 z2 {n} y2 } }
}. }.
...@@ -187,7 +187,7 @@ Class Unit (A : Type) := ε : A. ...@@ -187,7 +187,7 @@ Class Unit (A : Type) := ε : A.
Arguments ε {_ _}. Arguments ε {_ _}.
Record UcmraMixin A `{Dist A, Equiv A, PCore A, Op A, Valid A, Unit A} := { Record UcmraMixin A `{Dist A, Equiv A, PCore A, Op A, Valid A, Unit A} := {
mixin_ucmra_unit_valid : ε; mixin_ucmra_unit_valid : (ε : A);
mixin_ucmra_unit_left_id : LeftId () ε (); mixin_ucmra_unit_left_id : LeftId () ε ();
mixin_ucmra_pcore_unit : pcore ε Some ε mixin_ucmra_pcore_unit : pcore ε Some ε
}. }.
...@@ -861,17 +861,17 @@ End cmra_transport. ...@@ -861,17 +861,17 @@ End cmra_transport.
Record RAMixin A `{Equiv A, PCore A, Op A, Valid A} := { Record RAMixin A `{Equiv A, PCore A, Op A, Valid A} := {
(* setoids *) (* setoids *)
ra_op_proper (x : A) : Proper (() ==> ()) (op x); ra_op_proper (x : A) : Proper (() ==> ()) (op x);
ra_core_proper x y cx : ra_core_proper (x y : A) cx :
x y pcore x = Some cx cy, pcore y = Some cy cx cy; x y pcore x = Some cx cy, pcore y = Some cy cx cy;
ra_validN_proper : Proper (() ==> impl) valid; ra_validN_proper : Proper ((@{A}) ==> impl) valid;
(* monoid *) (* monoid *)
ra_assoc : Assoc () (); ra_assoc : Assoc (@{A}) ();
ra_comm : Comm () (); ra_comm : Comm (@{A}) ();
ra_pcore_l x cx : pcore x = Some cx cx x x; ra_pcore_l (x : A) cx : pcore x = Some cx cx x x;
ra_pcore_idemp x cx : pcore x = Some cx pcore cx Some cx; ra_pcore_idemp (x : A) cx : pcore x = Some cx pcore cx Some cx;
ra_pcore_mono x y cx : ra_pcore_mono (x y : A) cx :
x y pcore x = Some cx cy, pcore y = Some cy cx cy; x y pcore x = Some cx cy, pcore y = Some cy cx cy;
ra_valid_op_l x y : (x y) x ra_valid_op_l (x y : A) : (x y) x
}. }.
Section discrete. Section discrete.
......
...@@ -3,26 +3,27 @@ Set Default Proof Using "Type". ...@@ -3,26 +3,27 @@ Set Default Proof Using "Type".
Record DraMixin A `{Equiv A, Core A, Disjoint A, Op A, Valid A} := { Record DraMixin A `{Equiv A, Core A, Disjoint A, Op A, Valid A} := {
(* setoids *) (* setoids *)
mixin_dra_equivalence : Equivalence (() : relation A); mixin_dra_equivalence : Equivalence (@{A});
mixin_dra_op_proper : Proper (() ==> () ==> ()) (); mixin_dra_op_proper : Proper ((@{A}) ==> () ==> ()) ();
mixin_dra_core_proper : Proper (() ==> ()) core; mixin_dra_core_proper : Proper ((@{A}) ==> ()) core;
mixin_dra_valid_proper : Proper (() ==> impl) valid; mixin_dra_valid_proper : Proper ((@{A}) ==> impl) valid;
mixin_dra_disjoint_proper x : Proper (() ==> impl) (disjoint x); mixin_dra_disjoint_proper (x : A) : Proper (() ==> impl) (disjoint x);
(* validity *) (* validity *)
mixin_dra_op_valid x y : x y x ## y (x y); mixin_dra_op_valid (x y : A) : x y x ## y (x y);
mixin_dra_core_valid x : x core x; mixin_dra_core_valid (x : A) : x core x;
(* monoid *) (* monoid *)
mixin_dra_assoc x y z : mixin_dra_assoc (x y z : A) :
x y z x ## y x y ## z x (y z) (x y) z; x y z x ## y x y ## z x (y z) (x y) z;
mixin_dra_disjoint_ll x y z : x y z x ## y x y ## z x ## z; mixin_dra_disjoint_ll (x y z : A) :
mixin_dra_disjoint_move_l x y z : x y z x ## y x y ## z x ## z;
mixin_dra_disjoint_move_l (x y z : A) :
x y z x ## y x y ## z x ## y z; x y z x ## y x y ## z x ## y z;
mixin_dra_symmetric : Symmetric (@disjoint A _); mixin_dra_symmetric : Symmetric (@disjoint A _);
mixin_dra_comm x y : x y x ## y x y y x; mixin_dra_comm (x y : A) : x y x ## y x y y x;
mixin_dra_core_disjoint_l x : x core x ## x; mixin_dra_core_disjoint_l (x : A) : x core x ## x;
mixin_dra_core_l x : x core x x x; mixin_dra_core_l (x : A) : x core x x x;
mixin_dra_core_idemp x : x core (core x) core x; mixin_dra_core_idemp (x : A) : x core (core x) core x;
mixin_dra_core_mono x y : mixin_dra_core_mono (x y : A) :
z, x y x ## y core (x y) core x z z core x ## z z, x y x ## y core (x y) core x z z core x ## z
}. }.
Structure draT := DraT { Structure draT := DraT {
......
...@@ -12,17 +12,23 @@ Hint Mode Embed - ! : typeclass_instances. ...@@ -12,17 +12,23 @@ Hint Mode Embed - ! : typeclass_instances.
(* Mixins allow us to create instances easily without having to use Program *) (* Mixins allow us to create instances easily without having to use Program *)
Record BiEmbedMixin (PROP1 PROP2 : bi) `(Embed PROP1 PROP2) := { Record BiEmbedMixin (PROP1 PROP2 : bi) `(Embed PROP1 PROP2) := {
bi_embed_mixin_ne : NonExpansive embed; bi_embed_mixin_ne : NonExpansive (embed (A:=PROP1) (B:=PROP2));
bi_embed_mixin_mono : Proper (() ==> ()) embed; bi_embed_mixin_mono : Proper (() ==> ()) (embed (A:=PROP1) (B:=PROP2));
bi_embed_mixin_emp_valid_inj (P : PROP1) : bi_embed_mixin_emp_valid_inj (P : PROP1) :
bi_emp_valid (PROP:=PROP2) P bi_emp_valid P; bi_emp_valid (PROP:=PROP2) P bi_emp_valid P;
bi_embed_mixin_emp_2 : emp emp; bi_embed_mixin_emp_2 : emp @{PROP2} emp;
bi_embed_mixin_impl_2 P Q : (P Q) P Q; bi_embed_mixin_impl_2 (P Q : PROP1) :
bi_embed_mixin_forall_2 A (Φ : A PROP1) : ( x, ⎡Φ x) x, Φ x; (P Q) @{PROP2} P Q;
bi_embed_mixin_exist_1 A (Φ : A PROP1) : x, Φ x x, ⎡Φ x; bi_embed_mixin_forall_2 A (Φ : A PROP1) :
bi_embed_mixin_sep P Q : P Q P Q; ( x, ⎡Φ x) @{PROP2} x, Φ x;
bi_embed_mixin_wand_2 P Q : (P - Q) P - Q; bi_embed_mixin_exist_1 A (Φ : A PROP1) :
bi_embed_mixin_persistently P : <pers> P <pers> P x, Φ x @{PROP2} x, ⎡Φ x;
bi_embed_mixin_sep (P Q : PROP1) :
P Q @{PROP2} P Q;
bi_embed_mixin_wand_2 (P Q : PROP1) :
(P - Q) @{PROP2} P - Q;
bi_embed_mixin_persistently (P : PROP1) :
<pers> P @{PROP2} <pers> P
}. }.
Class BiEmbed (PROP1 PROP2 : bi) := { Class BiEmbed (PROP1 PROP2 : bi) := {
...@@ -302,7 +308,8 @@ Section sbi_embed. ...@@ -302,7 +308,8 @@ Section sbi_embed.
⎡■?p P ?p P. ⎡■?p P ?p P.
Proof. destruct p; simpl; auto using embed_plainly_1. Qed. Proof. destruct p; simpl; auto using embed_plainly_1. Qed.
Lemma embed_plain `{!BiPlainly PROP1, !BiPlainly PROP2} P : Plain P Plain P. Lemma embed_plain `{!BiPlainly PROP1, !BiPlainly PROP2} (P : PROP1) :
Plain P Plain (PROP:=PROP2) P.
Proof. intros ?. by rewrite /Plain {1}(plain P) embed_plainly_1. Qed. Proof. intros ?. by rewrite /Plain {1}(plain P) embed_plainly_1. Qed.
Global Instance embed_timeless P : Timeless P Timeless P. Global Instance embed_timeless P : Timeless P Timeless P.
......
...@@ -288,7 +288,7 @@ Section lemmas. ...@@ -288,7 +288,7 @@ Section lemmas.
rewrite atomic_update_eq {1}/atomic_update_def /=. rewrite atomic_update_eq {1}/atomic_update_def /=.
iIntros (??? HAU) "[#HP HQ]". iIntros (??? HAU) "[#HP HQ]".
iApply (greatest_fixpoint_coind _ (λ _, Q)); last done. iIntros "!#" ([]) "HQ". iApply (greatest_fixpoint_coind _ (λ _, Q)); last done. iIntros "!#" ([]) "HQ".
iApply (make_laterable_intro with "[] HQ"). iIntros "!# >HQ". iApply (make_laterable_intro Q with "[] HQ"). iIntros "!# >HQ".
iApply HAU. by iFrame. iApply HAU. by iFrame.
Qed. Qed.
......
...@@ -30,11 +30,11 @@ Section fractional. ...@@ -30,11 +30,11 @@ Section fractional.
Lemma fractional_split_1 P P1 P2 Φ q1 q2 : Lemma fractional_split_1 P P1 P2 Φ q1 q2 :
AsFractional P Φ (q1 + q2) AsFractional P1 Φ q1 AsFractional P2 Φ q2 AsFractional P Φ (q1 + q2) AsFractional P1 Φ q1 AsFractional P2 Φ q2
P - P1 P2. P - P1 P2.
Proof. intros. by rewrite -fractional_split. Qed. Proof. intros. by rewrite -(fractional_split P). Qed.
Lemma fractional_split_2 P P1 P2 Φ q1 q2 : Lemma fractional_split_2 P P1 P2 Φ q1 q2 :
AsFractional P Φ (q1 + q2) AsFractional P1 Φ q1 AsFractional P2 Φ q2 AsFractional P Φ (q1 + q2) AsFractional P1 Φ q1 AsFractional P2 Φ q2
P1 - P2 - P. P1 - P2 - P.
Proof. intros. apply bi.wand_intro_r. by rewrite -fractional_split. Qed. Proof. intros. apply bi.wand_intro_r. by rewrite -(fractional_split P). Qed.
Lemma fractional_half P P12 Φ q : Lemma fractional_half P P12 Φ q :
AsFractional P Φ q AsFractional P12 Φ (q/2) AsFractional P Φ q AsFractional P12 Φ (q/2)
...@@ -43,11 +43,11 @@ Section fractional. ...@@ -43,11 +43,11 @@ Section fractional.
Lemma fractional_half_1 P P12 Φ q : Lemma fractional_half_1 P P12 Φ q :
AsFractional P Φ q AsFractional P12 Φ (q/2) AsFractional P Φ q AsFractional P12 Φ (q/2)
P - P12 P12. P - P12 P12.
Proof. intros. by rewrite -fractional_half. Qed. Proof. intros. by rewrite -(fractional_half P). Qed.
Lemma fractional_half_2 P P12 Φ q : Lemma fractional_half_2 P P12 Φ q :
AsFractional P Φ q AsFractional P12 Φ (q/2) AsFractional P Φ q AsFractional P12 Φ (q/2)
P12 - P12 - P. P12 - P12 - P.
Proof. intros. apply bi.wand_intro_r. by rewrite -fractional_half. Qed. Proof. intros. apply bi.wand_intro_r. by rewrite -(fractional_half P). Qed.
(** Fractional and logical connectives *) (** Fractional and logical connectives *)
Global Instance persistent_fractional P : Global Instance persistent_fractional P :
......
...@@ -7,7 +7,7 @@ Structure biIndex := ...@@ -7,7 +7,7 @@ Structure biIndex :=
{ bi_index_type :> Type; { bi_index_type :> Type;
bi_index_inhabited : Inhabited bi_index_type; bi_index_inhabited : Inhabited bi_index_type;
bi_index_rel : SqSubsetEq bi_index_type; bi_index_rel : SqSubsetEq bi_index_type;
bi_index_rel_preorder : PreOrder () }. bi_index_rel_preorder : PreOrder (@{bi_index_type}) }.
Existing Instances bi_index_inhabited bi_index_rel bi_index_rel_preorder. Existing Instances bi_index_inhabited bi_index_rel bi_index_rel_preorder.
(* We may want to instantiate monPred with the reflexivity relation in (* We may want to instantiate monPred with the reflexivity relation in
......
...@@ -9,11 +9,11 @@ Notation "■ P" := (plainly P) : bi_scope. ...@@ -9,11 +9,11 @@ Notation "■ P" := (plainly P) : bi_scope.
(* Mixins allow us to create instances easily without having to use Program *) (* Mixins allow us to create instances easily without having to use Program *)
Record BiPlainlyMixin (PROP : sbi) `(Plainly PROP) := { Record BiPlainlyMixin (PROP : sbi) `(Plainly PROP) := {
bi_plainly_mixin_plainly_ne : NonExpansive plainly; bi_plainly_mixin_plainly_ne : NonExpansive (plainly (A:=PROP));
bi_plainly_mixin_plainly_mono P Q : (P Q) P Q; bi_plainly_mixin_plainly_mono (P Q : PROP) : (P Q) P Q;
bi_plainly_mixin_plainly_elim_persistently P : P <pers> P; bi_plainly_mixin_plainly_elim_persistently (P : PROP) : P <pers> P;
bi_plainly_mixin_plainly_idemp_2 P : P P; bi_plainly_mixin_plainly_idemp_2 (P : PROP) : P P;
bi_plainly_mixin_plainly_forall_2 {A} (Ψ : A PROP) : bi_plainly_mixin_plainly_forall_2 {A} (Ψ : A PROP) :
( a, (Ψ a)) ( a, Ψ a); ( a, (Ψ a)) ( a, Ψ a);
...@@ -21,17 +21,18 @@ Record BiPlainlyMixin (PROP : sbi) `(Plainly PROP) := { ...@@ -21,17 +21,18 @@ Record BiPlainlyMixin (PROP : sbi) `(Plainly PROP) := {
(* The following two laws are very similar, and indeed they hold not just (* The following two laws are very similar, and indeed they hold not just
for persistently and plainly, but for any modality defined as `M P n x := for persistently and plainly, but for any modality defined as `M P n x :=
∀ y, R x y → P n y`. *) ∀ y, R x y → P n y`. *)
bi_plainly_mixin_persistently_impl_plainly P Q : bi_plainly_mixin_persistently_impl_plainly (P Q : PROP) :
( P <pers> Q) <pers> ( P Q); ( P <pers> Q) <pers> ( P Q);
bi_plainly_mixin_plainly_impl_plainly P Q : ( P Q) ( P Q); bi_plainly_mixin_plainly_impl_plainly (P Q : PROP) :
( P Q) ( P Q);
bi_plainly_mixin_plainly_emp_intro P : P emp; bi_plainly_mixin_plainly_emp_intro (P : PROP) : P emp;
bi_plainly_mixin_plainly_absorb P Q : P Q P; bi_plainly_mixin_plainly_absorb (P Q : PROP) : P Q P;
bi_plainly_mixin_prop_ext P Q : ((P - Q) (Q - P)) P Q; bi_plainly_mixin_prop_ext (P Q : PROP) : ((P - Q) (Q - P)) P Q;
bi_plainly_mixin_later_plainly_1 P : P P; bi_plainly_mixin_later_plainly_1 (P : PROP) : P P;
bi_plainly_mixin_later_plainly_2 P : P P; bi_plainly_mixin_later_plainly_2 (P : PROP) : P P;
}. }.
Class BiPlainly (PROP : sbi) := { Class BiPlainly (PROP : sbi) := {
......
...@@ -39,7 +39,7 @@ Notation "P ={ E1 , E2 }▷=∗^ n Q" := (P -∗ |={E1,E2}▷=>^n Q)%I : bi_scop ...@@ -39,7 +39,7 @@ Notation "P ={ E1 , E2 }▷=∗^ n Q" := (P -∗ |={E1,E2}▷=>^n Q)%I : bi_scop
(** Bundled versions *) (** Bundled versions *)
(* Mixins allow us to create instances easily without having to use Program *) (* Mixins allow us to create instances easily without having to use Program *)
Record BiBUpdMixin (PROP : bi) `(BUpd PROP) := { Record BiBUpdMixin (PROP : bi) `(BUpd PROP) := {
bi_bupd_mixin_bupd_ne : NonExpansive bupd; bi_bupd_mixin_bupd_ne : NonExpansive (bupd (PROP:=PROP));
bi_bupd_mixin_bupd_intro (P : PROP) : P == P; bi_bupd_mixin_bupd_intro (P : PROP) : P == P;
bi_bupd_mixin_bupd_mono (P Q : PROP) : (P Q) (|==> P) == Q; bi_bupd_mixin_bupd_mono (P Q : PROP) : (P Q) (|==> P) == Q;
bi_bupd_mixin_bupd_trans (P : PROP) : (|==> |==> P) == P; bi_bupd_mixin_bupd_trans (P : PROP) : (|==> |==> P) == P;
...@@ -47,7 +47,7 @@ Record BiBUpdMixin (PROP : bi) `(BUpd PROP) := { ...@@ -47,7 +47,7 @@ Record BiBUpdMixin (PROP : bi) `(BUpd PROP) := {
}. }.
Record BiFUpdMixin (PROP : sbi) `(FUpd PROP) := { Record BiFUpdMixin (PROP : sbi) `(FUpd PROP) := {
bi_fupd_mixin_fupd_ne E1 E2 : NonExpansive (fupd E1 E2); bi_fupd_mixin_fupd_ne E1 E2 : NonExpansive (fupd (PROP:=PROP) E1 E2);
bi_fupd_mixin_fupd_intro_mask E1 E2 (P : PROP) : E2 E1 P |={E1,E2}=> |={E2,E1}=> P; bi_fupd_mixin_fupd_intro_mask E1 E2 (P : PROP) : E2 E1 P |={E1,E2}=> |={E2,E1}=> P;
bi_fupd_mixin_except_0_fupd E1 E2 (P : PROP) : (|={E1,E2}=> P) ={E1,E2}= P; bi_fupd_mixin_except_0_fupd E1 E2 (P : PROP) : (|={E1,E2}=> P) ={E1,E2}= P;
bi_fupd_mixin_fupd_mono E1 E2 (P Q : PROP) : (P Q) (|={E1,E2}=> P) |={E1,E2}=> Q; bi_fupd_mixin_fupd_mono E1 E2 (P Q : PROP) : (P Q) (|={E1,E2}=> P) |={E1,E2}=> Q;
......
...@@ -19,7 +19,7 @@ Class atomic_heap {Σ} `{!heapG Σ} := AtomicHeap { ...@@ -19,7 +19,7 @@ Class atomic_heap {Σ} `{!heapG Σ} := AtomicHeap {
mapsto_fractional l v :> Fractional (λ q, mapsto l q v); mapsto_fractional l v :> Fractional (λ q, mapsto l q v);
mapsto_as_fractional l q v :> mapsto_as_fractional l q v :>
AsFractional (mapsto l q v) (λ q, mapsto l q v) q; AsFractional (mapsto l q v) (λ q, mapsto l q v) q;
mapsto_agree l q1 q2 v1 v2 :> mapsto l q1 v1 - mapsto l q2 v2 - v1 = v2; mapsto_agree l q1 q2 v1 v2 : mapsto l q1 v1 - mapsto l q2 v2 - v1 = v2;
(* -- operation specs -- *) (* -- operation specs -- *)
alloc_spec (v : val) : alloc_spec (v : val) :
{{{ True }}} alloc v {{{ l, RET #l; mapsto l 1 v }}}; {{{ True }}} alloc v {{{ l, RET #l; mapsto l 1 v }}};
......
...@@ -730,7 +730,7 @@ Global Instance into_sep_and_persistent_l P P' Q Q' : ...@@ -730,7 +730,7 @@ Global Instance into_sep_and_persistent_l P P' Q Q' :
Persistent P AndIntoSep P P' Q Q' IntoSep (P Q) P' Q'. Persistent P AndIntoSep P P' Q Q' IntoSep (P Q) P' Q'.
Proof. Proof.
destruct 2 as [P Q Q'|P Q]; rewrite /IntoSep. destruct 2 as [P Q Q'|P Q]; rewrite /IntoSep.
- rewrite -(from_affinely Q') -(affine_affinely P) affinely_and_lr. - rewrite -(from_affinely Q' Q) -(affine_affinely P) affinely_and_lr.
by rewrite persistent_and_affinely_sep_l_1. by rewrite persistent_and_affinely_sep_l_1.
- by rewrite persistent_and_affinely_sep_l_1. - by rewrite persistent_and_affinely_sep_l_1.
Qed. Qed.
...@@ -738,7 +738,7 @@ Global Instance into_sep_and_persistent_r P P' Q Q' : ...@@ -738,7 +738,7 @@ Global Instance into_sep_and_persistent_r P P' Q Q' :
Persistent Q AndIntoSep Q Q' P P' IntoSep (P Q) P' Q'. Persistent Q AndIntoSep Q Q' P P' IntoSep (P Q) P' Q'.
Proof. Proof.
destruct 2 as [Q P P'|Q P]; rewrite /IntoSep. destruct 2 as [Q P P'|Q P]; rewrite /IntoSep.
- rewrite -(from_affinely P') -(affine_affinely Q) -affinely_and_lr. - rewrite -(from_affinely P' P) -(affine_affinely Q) -affinely_and_lr.
by rewrite persistent_and_affinely_sep_r_1. by rewrite persistent_and_affinely_sep_r_1.
- by rewrite persistent_and_affinely_sep_r_1. - by rewrite persistent_and_affinely_sep_r_1.
Qed. Qed.
......
...@@ -392,7 +392,7 @@ Proof. by rewrite /FromModal. Qed. ...@@ -392,7 +392,7 @@ Proof. by rewrite /FromModal. Qed.
Global Instance from_modal_plainly_embed `{BiPlainly PROP, BiPlainly PROP', Global Instance from_modal_plainly_embed `{BiPlainly PROP, BiPlainly PROP',
BiEmbedPlainly PROP PROP', !SbiEmbed PROP PROP'} `(sel : A) P Q : BiEmbedPlainly PROP PROP', !SbiEmbed PROP PROP'} `(sel : A) P Q :
FromModal modality_plainly sel P Q FromModal modality_plainly sel P Q
FromModal modality_plainly sel P Q | 100. FromModal (PROP2:=PROP') modality_plainly sel P Q | 100.
Proof. rewrite /FromModal /= =><-. by rewrite embed_plainly. Qed. Proof. rewrite /FromModal /= =><-. by rewrite embed_plainly. Qed.
(** IntoInternalEq *) (** IntoInternalEq *)
......
...@@ -285,7 +285,7 @@ Proof. done. Qed. ...@@ -285,7 +285,7 @@ Proof. done. Qed.
Class Frame {PROP : bi} (p : bool) (R P Q : PROP) := frame : ?p R Q P. Class Frame {PROP : bi} (p : bool) (R P Q : PROP) := frame : ?p R Q P.
Arguments Frame {_} _ _%I _%I _%I. Arguments Frame {_} _ _%I _%I _%I.
Arguments frame {_ _} _%I _%I _%I {_}. Arguments frame {_} _ _%I _%I _%I {_}.
Hint Mode Frame + + ! ! - : typeclass_instances. Hint Mode Frame + + ! ! - : typeclass_instances.
(* The boolean [progress] indicates whether actual framing has been performed. (* The boolean [progress] indicates whether actual framing has been performed.
......
...@@ -109,7 +109,7 @@ Qed. ...@@ -109,7 +109,7 @@ Qed.
Lemma tac_pure_intro Δ Q φ af : Lemma tac_pure_intro Δ Q φ af :
env_spatial_is_nil Δ = af FromPure af Q φ φ envs_entails Δ Q. env_spatial_is_nil Δ = af FromPure af Q φ φ envs_entails Δ Q.
Proof. Proof.
intros ???. rewrite envs_entails_eq -(from_pure _ Q). destruct af. intros ???. rewrite envs_entails_eq -(from_pure af Q). destruct af.
- rewrite env_spatial_is_nil_intuitionistically //= /bi_intuitionistically. - rewrite env_spatial_is_nil_intuitionistically //= /bi_intuitionistically.
f_equiv. by apply pure_intro. f_equiv. by apply pure_intro.
- by apply pure_intro. - by apply pure_intro.
...@@ -145,7 +145,7 @@ Lemma tac_intuitionistic Δ Δ' i p P P' Q : ...@@ -145,7 +145,7 @@ Lemma tac_intuitionistic Δ Δ' i p P P' Q :
Proof. Proof.
rewrite envs_entails_eq=>?? HPQ ? HQ. rewrite envs_replace_singleton_sound //=. rewrite envs_entails_eq=>?? HPQ ? HQ. rewrite envs_replace_singleton_sound //=.
destruct p; simpl; rewrite /bi_intuitionistically. destruct p; simpl; rewrite /bi_intuitionistically.
- by rewrite -(into_persistent _ P) /= wand_elim_r. - by rewrite -(into_persistent true P) /= wand_elim_r.
- destruct HPQ. - destruct HPQ.
+ rewrite -(affine_affinely P) (_ : P = <pers>?false P)%I // + rewrite -(affine_affinely P) (_ : P = <pers>?false P)%I //
(into_persistent _ P) wand_elim_r //. (into_persistent _ P) wand_elim_r //.
...@@ -165,10 +165,10 @@ Proof. ...@@ -165,10 +165,10 @@ Proof.
rewrite /FromImpl envs_entails_eq => <- ??? <-. destruct (env_spatial_is_nil Δ) eqn:?. rewrite /FromImpl envs_entails_eq => <- ??? <-. destruct (env_spatial_is_nil Δ) eqn:?.
- rewrite (env_spatial_is_nil_intuitionistically Δ) //; simpl. apply impl_intro_l. - rewrite (env_spatial_is_nil_intuitionistically Δ) //; simpl. apply impl_intro_l.
rewrite envs_app_singleton_sound //; simpl. rewrite envs_app_singleton_sound //; simpl.
rewrite -(from_affinely P') -affinely_and_lr. rewrite -(from_affinely P' P) -affinely_and_lr.
by rewrite persistently_and_intuitionistically_sep_r intuitionistically_elim wand_elim_r. by rewrite persistently_and_intuitionistically_sep_r intuitionistically_elim wand_elim_r.
- apply impl_intro_l. rewrite envs_app_singleton_sound //; simpl. - apply impl_intro_l. rewrite envs_app_singleton_sound //; simpl.
by rewrite -(from_affinely P') persistent_and_affinely_sep_l_1 wand_elim_r. by rewrite -(from_affinely P' P) persistent_and_affinely_sep_l_1 wand_elim_r.
Qed. Qed.
Lemma tac_impl_intro_intuitionistic Δ Δ' i P P' Q R : Lemma tac_impl_intro_intuitionistic Δ Δ' i P P' Q R :
FromImpl R P Q FromImpl R P Q
...@@ -251,7 +251,7 @@ Proof. ...@@ -251,7 +251,7 @@ Proof.
destruct (envs_app _ _ _) eqn:?; simplify_eq/=. destruct (envs_app _ _ _) eqn:?; simplify_eq/=.
rewrite envs_lookup_sound // envs_split_sound //. rewrite envs_lookup_sound // envs_split_sound //.
rewrite (envs_app_singleton_sound Δ2) //; simpl. rewrite (envs_app_singleton_sound Δ2) //; simpl.
rewrite HP1 into_wand /= -(add_modal P1' P1 Q). cancel [P1']. rewrite HP1 (into_wand q false) /= -(add_modal P1' P1 Q). cancel [P1'].
apply wand_intro_l. by rewrite assoc !wand_elim_r. apply wand_intro_l. by rewrite assoc !wand_elim_r.
Qed. Qed.
...@@ -272,7 +272,7 @@ Lemma tac_specialize_frame Δ Δ' j q R P1 P2 P1' Q Q' : ...@@ -272,7 +272,7 @@ Lemma tac_specialize_frame Δ Δ' j q R P1 P2 P1' Q Q' :
Proof. Proof.
rewrite envs_entails_eq. intros [? ->]%envs_lookup_delete_Some ?? HPQ ->. rewrite envs_entails_eq. intros [? ->]%envs_lookup_delete_Some ?? HPQ ->.
rewrite envs_lookup_sound //. rewrite HPQ -lock. rewrite envs_lookup_sound //. rewrite HPQ -lock.
rewrite into_wand -{2}(add_modal P1' P1 Q). cancel [P1']. rewrite (into_wand q false) -{2}(add_modal P1' P1 Q). cancel [P1'].
apply wand_intro_l. by rewrite assoc !wand_elim_r. apply wand_intro_l. by rewrite assoc !wand_elim_r.
Qed. Qed.
...@@ -284,7 +284,8 @@ Lemma tac_specialize_assert_pure Δ Δ' j q R P1 P2 φ Q : ...@@ -284,7 +284,8 @@ Lemma tac_specialize_assert_pure Δ Δ' j q R P1 P2 φ Q :
φ envs_entails Δ' Q envs_entails Δ Q. φ envs_entails Δ' Q envs_entails Δ Q.
Proof. Proof.