Commit 91dfd8b9 authored by Ralf Jung's avatar Ralf Jung

Merge branch 'master' of gitlab.mpi-sws.org:iris/iris

parents ccf8bc36 195d3beb
......@@ -111,6 +111,9 @@ Separation logic-specific tactics
framed.
- `iCombine "H1" "H2" as "pat"` : combines `H1 : P1` and `H2 : P2` into
`H: P1 ∗ P2`, then calls `iDestruct H as pat` on the combined hypothesis.
- `iAccu` : solves a goal that is an evar by instantiating it with a all
hypotheses from the spatial context joined together with a separating
conjunction (or `emp` in case the spatial context is empty).
Modalities
----------
......@@ -234,11 +237,13 @@ appear at the top level:
For example, given:
∀ x, x = 0 ⊢ □ (P → False ∨ □ (Q ∧ ▷ R) -∗ P ∗ ▷ (R ∗ Q ∧ x = pred 2)).
∀ x, <affine> ⌜ x = 0 ⌝ ⊢
□ (P → False ∨ □ (Q ∧ ▷ R) -∗
P ∗ ▷ (R ∗ Q ∧ ⌜ x = pred 2 ⌝)).
You can write
iIntros (x) "% !# $ [[] | #[HQ HR]] /= !>".
iIntros (x Hx) "!# $ [[] | #[HQ HR]] /= !>".
which results in:
......
......@@ -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-26.0.d98ab4e4") | (= "dev") }
"coq-stdpp" { (= "dev.2019-04-26.2.32eab16e") | (= "dev") }
]
......@@ -45,21 +45,21 @@ Section mixin.
Record CmraMixin A `{Dist A, Equiv A, PCore A, Op A, Valid A, ValidN A} := {
(* setoids *)
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;
mixin_cmra_validN_ne n : Proper (dist n ==> impl) (validN n);
(* valid *)
mixin_cmra_valid_validN x : x n, {n} x;
mixin_cmra_validN_S n x : {S n} x {n} x;
mixin_cmra_valid_validN (x : A) : x n, {n} x;
mixin_cmra_validN_S n (x : A) : {S n} x {n} x;
(* monoid *)
mixin_cmra_assoc : Assoc () ();
mixin_cmra_comm : Comm () ();
mixin_cmra_pcore_l x 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_mono x y cx :
mixin_cmra_assoc : Assoc (@{A}) ();
mixin_cmra_comm : Comm (@{A}) ();
mixin_cmra_pcore_l (x : A) cx : pcore x = Some cx cx x x;
mixin_cmra_pcore_idemp (x : A) cx : pcore x = Some cx pcore cx Some cx;
mixin_cmra_pcore_mono (x y : A) cx :
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_extend n x y1 y2 :
mixin_cmra_validN_op_l n (x y : A) : {n} (x y) {n} x;
mixin_cmra_extend n (x y1 y2 : A) :
{n} x x {n} y1 y2
{ z1 : A & { z2 | x z1 z2 z1 {n} y1 z2 {n} y2 } }
}.
......@@ -187,7 +187,7 @@ Class Unit (A : Type) := ε : A.
Arguments ε {_ _}.
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_pcore_unit : pcore ε Some ε
}.
......@@ -861,17 +861,17 @@ End cmra_transport.
Record RAMixin A `{Equiv A, PCore A, Op A, Valid A} := {
(* setoids *)
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;
ra_validN_proper : Proper (() ==> impl) valid;
ra_validN_proper : Proper ((@{A}) ==> impl) valid;
(* monoid *)
ra_assoc : Assoc () ();
ra_comm : Comm () ();
ra_pcore_l x cx : pcore x = Some cx cx x x;
ra_pcore_idemp x cx : pcore x = Some cx pcore cx Some cx;
ra_pcore_mono x y cx :
ra_assoc : Assoc (@{A}) ();
ra_comm : Comm (@{A}) ();
ra_pcore_l (x : A) cx : pcore x = Some cx cx x x;
ra_pcore_idemp (x : A) cx : pcore x = Some cx pcore cx Some cx;
ra_pcore_mono (x y : A) cx :
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.
......@@ -1491,7 +1491,7 @@ Proof.
by intros ? A1 A2 B1 B2 n f g Hfg; apply optionC_map_ne, rFunctor_contractive.
Qed.
(* Dependently-typed functions over a finite discrete domain *)
(* Dependently-typed functions over a discrete domain *)
Section ofe_fun_cmra.
Context `{B : A ucmraT}.
Implicit Types f g : ofe_fun B.
......
......@@ -3,26 +3,27 @@ Set Default Proof Using "Type".
Record DraMixin A `{Equiv A, Core A, Disjoint A, Op A, Valid A} := {
(* setoids *)
mixin_dra_equivalence : Equivalence (() : relation A);
mixin_dra_op_proper : Proper (() ==> () ==> ()) ();
mixin_dra_core_proper : Proper (() ==> ()) core;
mixin_dra_valid_proper : Proper (() ==> impl) valid;
mixin_dra_disjoint_proper x : Proper (() ==> impl) (disjoint x);
mixin_dra_equivalence : Equivalence (@{A});
mixin_dra_op_proper : Proper ((@{A}) ==> () ==> ()) ();
mixin_dra_core_proper : Proper ((@{A}) ==> ()) core;
mixin_dra_valid_proper : Proper ((@{A}) ==> impl) valid;
mixin_dra_disjoint_proper (x : A) : Proper (() ==> impl) (disjoint x);
(* validity *)
mixin_dra_op_valid x y : x y x ## y (x y);
mixin_dra_core_valid x : x core x;
mixin_dra_op_valid (x y : A) : x y x ## y (x y);
mixin_dra_core_valid (x : A) : x core x;
(* 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;
mixin_dra_disjoint_ll x y z : x y z x ## y x y ## z x ## z;
mixin_dra_disjoint_move_l x y z :
mixin_dra_disjoint_ll (x y z : A) :
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;
mixin_dra_symmetric : Symmetric (@disjoint A _);
mixin_dra_comm x y : x y x ## y x y y x;
mixin_dra_core_disjoint_l x : x core x ## x;
mixin_dra_core_l x : x core x x x;
mixin_dra_core_idemp x : x core (core x) core x;
mixin_dra_core_mono x y :
mixin_dra_comm (x y : A) : x y x ## y x y y x;
mixin_dra_core_disjoint_l (x : A) : x core x ## x;
mixin_dra_core_l (x : A) : x core x x x;
mixin_dra_core_idemp (x : A) : x core (core x) core x;
mixin_dra_core_mono (x y : A) :
z, x y x ## y core (x y) core x z z core x ## z
}.
Structure draT := DraT {
......
......@@ -12,17 +12,23 @@ Hint Mode Embed - ! : typeclass_instances.
(* Mixins allow us to create instances easily without having to use Program *)
Record BiEmbedMixin (PROP1 PROP2 : bi) `(Embed PROP1 PROP2) := {
bi_embed_mixin_ne : NonExpansive embed;
bi_embed_mixin_mono : Proper (() ==> ()) embed;
bi_embed_mixin_ne : NonExpansive (embed (A:=PROP1) (B:=PROP2));
bi_embed_mixin_mono : Proper (() ==> ()) (embed (A:=PROP1) (B:=PROP2));
bi_embed_mixin_emp_valid_inj (P : PROP1) :
bi_emp_valid (PROP:=PROP2) P bi_emp_valid P;
bi_embed_mixin_emp_2 : emp emp;
bi_embed_mixin_impl_2 P Q : (P Q) P Q;
bi_embed_mixin_forall_2 A (Φ : A PROP1) : ( x, ⎡Φ x) x, Φ x;
bi_embed_mixin_exist_1 A (Φ : A PROP1) : x, Φ x x, ⎡Φ x;
bi_embed_mixin_sep P Q : P Q P Q;
bi_embed_mixin_wand_2 P Q : (P - Q) P - Q;
bi_embed_mixin_persistently P : <pers> P <pers> P
bi_embed_mixin_emp_2 : emp @{PROP2} emp;
bi_embed_mixin_impl_2 (P Q : PROP1) :
(P Q) @{PROP2} P Q;
bi_embed_mixin_forall_2 A (Φ : A PROP1) :
( x, ⎡Φ x) @{PROP2} x, Φ x;
bi_embed_mixin_exist_1 A (Φ : A PROP1) :
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) := {
......@@ -302,7 +308,8 @@ Section sbi_embed.
⎡■?p P ?p P.
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.
Global Instance embed_timeless P : Timeless P Timeless P.
......
......@@ -288,7 +288,7 @@ Section lemmas.
rewrite atomic_update_eq {1}/atomic_update_def /=.
iIntros (??? HAU) "[#HP 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.
Qed.
......
......@@ -30,11 +30,11 @@ Section fractional.
Lemma fractional_split_1 P P1 P2 Φ q1 q2 :
AsFractional P Φ (q1 + q2) AsFractional P1 Φ q1 AsFractional P2 Φ q2
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 :
AsFractional P Φ (q1 + q2) AsFractional P1 Φ q1 AsFractional P2 Φ q2
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 :
AsFractional P Φ q AsFractional P12 Φ (q/2)
......@@ -43,11 +43,11 @@ Section fractional.
Lemma fractional_half_1 P P12 Φ q :
AsFractional P Φ q AsFractional P12 Φ (q/2)
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 :
AsFractional P Φ q AsFractional P12 Φ (q/2)
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 *)
Global Instance persistent_fractional P :
......
......@@ -7,7 +7,7 @@ Structure biIndex :=
{ bi_index_type :> Type;
bi_index_inhabited : Inhabited 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.
(* We may want to instantiate monPred with the reflexivity relation in
......
......@@ -9,11 +9,11 @@ Notation "■ P" := (plainly P) : bi_scope.
(* Mixins allow us to create instances easily without having to use Program *)
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_elim_persistently P : P <pers> P;
bi_plainly_mixin_plainly_idemp_2 P : P P;
bi_plainly_mixin_plainly_mono (P Q : PROP) : (P Q) P Q;
bi_plainly_mixin_plainly_elim_persistently (P : PROP) : P <pers> P;
bi_plainly_mixin_plainly_idemp_2 (P : PROP) : P P;
bi_plainly_mixin_plainly_forall_2 {A} (Ψ : A PROP) :
( a, (Ψ a)) ( a, Ψ a);
......@@ -21,17 +21,18 @@ Record BiPlainlyMixin (PROP : sbi) `(Plainly PROP) := {
(* 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 :=
∀ 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);
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_absorb P Q : P Q P;
bi_plainly_mixin_plainly_emp_intro (P : PROP) : P emp;
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_2 P : P P;
bi_plainly_mixin_later_plainly_1 (P : PROP) : P P;
bi_plainly_mixin_later_plainly_2 (P : PROP) : P P;
}.
Class BiPlainly (PROP : sbi) := {
......
......@@ -39,7 +39,7 @@ Notation "P ={ E1 , E2 }▷=∗^ n Q" := (P -∗ |={E1,E2}▷=>^n Q)%I : bi_scop
(** Bundled versions *)
(* Mixins allow us to create instances easily without having to use Program *)
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_mono (P Q : PROP) : (P Q) (|==> P) == Q;
bi_bupd_mixin_bupd_trans (P : PROP) : (|==> |==> P) == P;
......@@ -47,7 +47,7 @@ Record BiBUpdMixin (PROP : bi) `(BUpd 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_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;
......
From iris.program_logic Require Export language ectx_language ectxi_language.
From iris.algebra Require Export ofe.
From stdpp Require Export strings.
From stdpp Require Export binders strings.
From stdpp Require Import gmap.
Set Default Proof Using "Type".
......@@ -42,22 +42,6 @@ Inductive bin_op : Set :=
| ShiftLOp | ShiftROp (* Shifts *)
| LeOp | LtOp | EqOp. (* Relations *)
Inductive binder := BAnon | BNamed : string binder.
Delimit Scope binder_scope with bind.
Bind Scope binder_scope with binder.
Definition cons_binder (mx : binder) (X : list string) : list string :=
match mx with BAnon => X | BNamed x => x :: X end.
Infix ":b:" := cons_binder (at level 60, right associativity).
Instance binder_eq_dec_eq : EqDecision binder.
Proof. solve_decision. Defined.
Instance set_unfold_cons_binder x mx X P :
SetUnfold (x X) P SetUnfold (x mx :b: X) (BNamed x = mx P).
Proof.
constructor. rewrite -(set_unfold (x X) P).
destruct mx; rewrite /= ?elem_of_cons; naive_solver.
Qed.
Inductive expr :=
(* Values *)
| Val (v : val)
......@@ -244,11 +228,6 @@ Proof.
| 10 => LeOp | 11 => LtOp | _ => EqOp
end) _); by intros [].
Qed.
Instance binder_countable : Countable binder.
Proof.
refine (inj_countable' (λ b, match b with BNamed s => Some s | BAnon => None end)
(λ b, match b with Some s => BNamed s | None => BAnon end) _); by intros [].
Qed.
Instance expr_countable : Countable expr.
Proof.
set (enc :=
......
......@@ -19,7 +19,7 @@ Class atomic_heap {Σ} `{!heapG Σ} := AtomicHeap {
mapsto_fractional l v :> Fractional (λ q, mapsto l q v);
mapsto_as_fractional l q v :>
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 -- *)
alloc_spec (v : val) :
{{{ True }}} alloc v {{{ l, RET #l; mapsto l 1 v }}};
......
......@@ -15,9 +15,6 @@ Coercion Val : val >-> expr.
Coercion Var : string >-> expr.
Coercion BNamed : string >-> binder.
Notation "<>" := BAnon : binder_scope.
(* No scope for the values, does not conflict and scope is often not inferred
properly. *)
Notation "# l" := (LitV l%Z%V) (at level 8, format "# l").
......@@ -50,11 +47,11 @@ Moreover, if the branches do not fit on a single line, it will be printed as:
end
*)
Notation "'match:' e0 'with' 'InjL' x1 => e1 | 'InjR' x2 => e2 'end'" :=
(Match e0 x1%bind e1 x2%bind e2)
(Match e0 x1%binder e1 x2%binder e2)
(e0, x1, e1, x2, e2 at level 200,
format "'[hv' 'match:' e0 'with' '/ ' '[' 'InjL' x1 => '/ ' e1 ']' '/' '[' | 'InjR' x2 => '/ ' e2 ']' '/' 'end' ']'") : expr_scope.
Notation "'match:' e0 'with' 'InjR' x1 => e1 | 'InjL' x2 => e2 'end'" :=
(Match e0 x2%bind e2 x1%bind e1)
(Match e0 x2%binder e2 x1%binder e1)
(e0, x1, e1, x2, e2 at level 200, only parsing) : expr_scope.
Notation "()" := LitUnit : val_scope.
......@@ -81,10 +78,10 @@ Notation "e1 <- e2" := (Store e1%E e2%E) (at level 80) : expr_scope.
(* The breaking point '/ ' makes sure that the body of the rec is indented
by two spaces in case the whole rec does not fit on a single line. *)
Notation "'rec:' f x := e" := (Rec f%bind x%bind e%E)
Notation "'rec:' f x := e" := (Rec f%binder x%binder e%E)
(at level 200, f at level 1, x at level 1, e at level 200,
format "'[' 'rec:' f x := '/ ' e ']'") : expr_scope.
Notation "'rec:' f x := e" := (RecV f%bind x%bind e%E)
Notation "'rec:' f x := e" := (RecV f%binder x%binder e%E)
(at level 200, f at level 1, x at level 1, e at level 200,
format "'[' 'rec:' f x := '/ ' e ']'") : val_scope.
Notation "'if:' e1 'then' e2 'else' e3" := (If e1%E e2%E e3%E)
......@@ -94,30 +91,30 @@ Notation "'if:' e1 'then' e2 'else' e3" := (If e1%E e2%E e3%E)
are stated explicitly instead of relying on the Notations Let and Seq as
defined above. This is needed because App is now a coercion, and these
notations are otherwise not pretty printed back accordingly. *)
Notation "'rec:' f x y .. z := e" := (Rec f%bind x%bind (Lam y%bind .. (Lam z%bind e%E) ..))
Notation "'rec:' f x y .. z := e" := (Rec f%binder x%binder (Lam y%binder .. (Lam z%binder e%E) ..))
(at level 200, f, x, y, z at level 1, e at level 200,
format "'[' 'rec:' f x y .. z := '/ ' e ']'") : expr_scope.
Notation "'rec:' f x y .. z := e" := (RecV f%bind x%bind (Lam y%bind .. (Lam z%bind e%E) ..))
Notation "'rec:' f x y .. z := e" := (RecV f%binder x%binder (Lam y%binder .. (Lam z%binder e%E) ..))
(at level 200, f, x, y, z at level 1, e at level 200,
format "'[' 'rec:' f x y .. z := '/ ' e ']'") : val_scope.
(* The breaking point '/ ' makes sure that the body of the λ: is indented
by two spaces in case the whole λ: does not fit on a single line. *)
Notation "λ: x , e" := (Lam x%bind e%E)
Notation "λ: x , e" := (Lam x%binder e%E)
(at level 200, x at level 1, e at level 200,
format "'[' 'λ:' x , '/ ' e ']'") : expr_scope.
Notation "λ: x y .. z , e" := (Lam x%bind (Lam y%bind .. (Lam z%bind e%E) ..))
Notation "λ: x y .. z , e" := (Lam x%binder (Lam y%binder .. (Lam z%binder e%E) ..))
(at level 200, x, y, z at level 1, e at level 200,
format "'[' 'λ:' x y .. z , '/ ' e ']'") : expr_scope.
Notation "λ: x , e" := (LamV x%bind e%E)
Notation "λ: x , e" := (LamV x%binder e%E)
(at level 200, x at level 1, e at level 200,
format "'[' 'λ:' x , '/ ' e ']'") : val_scope.
Notation "λ: x y .. z , e" := (LamV x%bind (Lam y%bind .. (Lam z%bind e%E) .. ))
Notation "λ: x y .. z , e" := (LamV x%binder (Lam y%binder .. (Lam z%binder e%E) .. ))
(at level 200, x, y, z at level 1, e at level 200,
format "'[' 'λ:' x y .. z , '/ ' e ']'") : val_scope.
Notation "'let:' x := e1 'in' e2" := (Lam x%bind e2%E e1%E)
Notation "'let:' x := e1 'in' e2" := (Lam x%binder e2%E e1%E)
(at level 200, x at level 1, e1, e2 at level 200,
format "'[' 'let:' x := '[' e1 ']' 'in' '/' e2 ']'") : expr_scope.
Notation "e1 ;; e2" := (Lam BAnon e2%E e1%E)
......@@ -137,10 +134,10 @@ Notation SOME x := (InjR x) (only parsing).
Notation SOMEV x := (InjRV x) (only parsing).
Notation "'match:' e0 'with' 'NONE' => e1 | 'SOME' x => e2 'end'" :=
(Match e0 BAnon e1 x%bind e2)
(Match e0 BAnon e1 x%binder e2)
(e0, e1, x, e2 at level 200, only parsing) : expr_scope.
Notation "'match:' e0 'with' 'SOME' x => e2 | 'NONE' => e1 'end'" :=
(Match e0 BAnon e1 x%bind e2)
(Match e0 BAnon e1 x%binder e2)
(e0, e1, x, e2 at level 200, only parsing) : expr_scope.
Notation "'resolve_proph:' p 'to:' v" := (ResolveProph p v) (at level 100) : expr_scope.
......@@ -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'.
Proof.
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.
Qed.
......@@ -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'.
Proof.
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.
Qed.
......
......@@ -392,7 +392,7 @@ Proof. by rewrite /FromModal. Qed.
Global Instance from_modal_plainly_embed `{BiPlainly PROP, BiPlainly PROP',
BiEmbedPlainly PROP PROP', !SbiEmbed PROP PROP'} `(sel : A) 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.
(** IntoInternalEq *)
......
......@@ -285,7 +285,7 @@ Proof. done. Qed.
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 {_}.
Hint Mode Frame + + ! ! - : typeclass_instances.
(* The boolean [progress] indicates whether actual framing has been performed.
......
......@@ -109,7 +109,7 @@ Qed.
Lemma tac_pure_intro Δ Q φ af :
env_spatial_is_nil Δ = af FromPure af Q φ φ envs_entails Δ Q.
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.
f_equiv. by apply pure_intro.
- by apply pure_intro.
......@@ -145,7 +145,7 @@ Lemma tac_intuitionistic Δ Δ' i p P P' Q :
Proof.
rewrite envs_entails_eq=>?? HPQ ? HQ. rewrite envs_replace_singleton_sound //=.
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.
+ rewrite -(affine_affinely P) (_ : P = <pers>?false P)%I //
(into_persistent _ P) wand_elim_r //.
......@@ -165,10 +165,10 @@ Proof.
rewrite /FromImpl envs_entails_eq => <- ??? <-. destruct (env_spatial_is_nil Δ) eqn:?.
- rewrite (env_spatial_is_nil_intuitionistically Δ) //; simpl. apply impl_intro_l.
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.
- 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.
Lemma tac_impl_intro_intuitionistic Δ Δ' i P P' Q R :
FromImpl R P Q
......@@ -251,7 +251,7 @@ Proof.
destruct (envs_app _ _ _) eqn:?; simplify_eq/=.
rewrite envs_lookup_sound // envs_split_sound //.
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.
Qed.
......@@ -272,7 +272,7 @@ Lemma tac_specialize_frame Δ Δ' j q R P1 P2 P1' Q Q' :
Proof.
rewrite envs_entails_eq. intros [? ->]%envs_lookup_delete_Some ?? HPQ ->.
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.
Qed.
......@@ -284,7 +284,8 @@ Lemma tac_specialize_assert_pure Δ Δ' j q R P1 P2 φ Q :
φ envs_entails Δ' Q envs_entails Δ Q.
Proof.
rewrite envs_entails_eq=> ????? <-. rewrite envs_simple_replace_singleton_sound //=.
rewrite -intuitionistically_if_idemp into_wand /= -(from_pure _ P1) /bi_intuitionistically.
rewrite -intuitionistically_if_idemp (into_wand q true) /=.
rewrite -(from_pure true P1) /bi_intuitionistically.
rewrite pure_True //= persistently_affinely_elim persistently_pure
affinely_True_emp affinely_emp.
by rewrite emp_wand wand_elim_r.
......@@ -302,11 +303,11 @@ Proof.
rewrite envs_lookup_sound //.
rewrite -(idemp bi_and (of_envs (envs_delete _ _ _ _))).
rewrite {2}envs_simple_replace_singleton_sound' //; simpl.
rewrite {1}HP1 (into_absorbingly P1') (persistent_persistently_2 P1).
rewrite {1}HP1 (into_absorbingly P1' P1) (persistent_persistently_2 P1).
rewrite absorbingly_elim_persistently persistently_and_intuitionistically_sep_l assoc.
rewrite -intuitionistically_if_idemp -intuitionistically_idemp.
rewrite (intuitionistically_intuitionistically_if q).
by rewrite intuitionistically_if_sep_2 into_wand wand_elim_l wand_elim_r.
by rewrite intuitionistically_if_sep_2 (into_wand q true) wand_elim_l wand_elim_r.
Qed.
Lemma tac_specialize_intuitionistic_helper Δ Δ'' j q P R R' Q :
......@@ -402,7 +403,7 @@ Lemma tac_apply Δ Δ' i p R P1 P2 :
envs_entails Δ' P1 envs_entails Δ P2.
Proof.
rewrite envs_entails_eq => ?? HP1. rewrite envs_lookup_delete_sound //.
by rewrite into_wand /= HP1 wand_elim_l.
by rewrite (into_wand p false) /= HP1 wand_elim_l.
Qed.
(** * Conjunction splitting *)
......@@ -487,7 +488,7 @@ Qed.
Lemma tac_frame_pure Δ (φ : Prop) P Q :
φ Frame true ⌜φ⌝ P Q envs_entails Δ Q envs_entails Δ P.
Proof.
rewrite envs_entails_eq => ?? ->. rewrite -(frame ⌜φ⌝ P) /=.
rewrite envs_entails_eq => ?? ->. rewrite -(frame true ⌜φ⌝ P) /=.
rewrite -persistently_and_intuitionistically_sep_l persistently_pure.
auto using and_intro, pure_intro.
Qed.
......@@ -498,7 +499,7 @@ Lemma tac_frame Δ Δ' i p R P Q :
envs_entails Δ' Q envs_entails Δ P.
Proof.
rewrite envs_entails_eq. intros [? ->]%envs_lookup_delete_Some ? HQ.
rewrite (envs_lookup_sound' _ false) //. by rewrite -(frame R P) HQ.
rewrite (envs_lookup_sound' _ false) //. by rewrite -(frame p R P) HQ.
Qed.
(** * Disjunction *)
......
......@@ -33,10 +33,10 @@ Proof.
Qed.
Global Instance make_embed_pure `{BiEmbed PROP PROP'} φ :
KnownMakeEmbed ⌜φ⌝ ⌜φ⌝.
KnownMakeEmbed (PROP:=PROP) ⌜φ⌝ ⌜φ⌝.
Proof. apply embed_pure. Qed.
Global Instance make_embed_emp `{BiEmbedEmp PROP PROP'} :
KnownMakeEmbed emp emp.
KnownMakeEmbed (PROP:=PROP) emp emp.
Proof. apply embed_emp. Qed.
Global Instance make_embed_default `{BiEmbed PROP PROP'} P :
MakeEmbed P P | 100.
......@@ -296,14 +296,14 @@ Global Instance make_laterN_default P : MakeLaterN n P (▷^n P) | 100.
Proof. by rewrite /MakeLaterN. Qed.
Global Instance frame_later p R R' P Q Q' :
NoBackTrack (MaybeIntoLaterN true 1 R' R)