Commit c0be693a authored by Ralf Jung's avatar Ralf Jung

add notation to define the PROP we use for a particular turnstile

Fixes #156
parent 44c5c039
......@@ -89,7 +89,7 @@ Section sep_list.
Proper (Forall2 () ==> ()) (big_opL (@bi_sep M) (λ _ P, P)).
Proof. by induction 1 as [|P Q Ps Qs HPQ ? IH]; rewrite /= ?HPQ ?IH. Qed.
Lemma big_sepL_emp l : ([ list] ky l, emp) (emp : PROP).
Lemma big_sepL_emp l : ([ list] ky l, emp) {PROP} emp.
Proof. by rewrite big_opL_unit. Qed.
Lemma big_sepL_lookup_acc Φ l i x :
......
......@@ -21,8 +21,8 @@ Implicit Types A : Type.
Hint Extern 100 (NonExpansive _) => solve_proper.
(* Force implicit argument PROP *)
Notation "P ⊢ Q" := (@bi_entails PROP P%I Q%I).
Notation "P ⊣⊢ Q" := (equiv (A:=bi_car PROP) P%I Q%I).
Notation "P ⊢ Q" := (P {PROP} Q).
Notation "P ⊣⊢ Q" := (P {PROP} Q).
(* Derived stuff about the entailment *)
Global Instance entails_anti_sym : AntiSymm () (@bi_entails PROP).
......@@ -629,9 +629,9 @@ Proof. rewrite /bi_affinely. apply (anti_symm _); auto. Qed.
Lemma absorbing_absorbingly P `{!Absorbing P} : <absorb> P P.
Proof. by apply (anti_symm _), absorbingly_intro. Qed.
Lemma True_affine_all_affine P : Affine (True%I : PROP) Affine P.
Lemma True_affine_all_affine P : Affine (PROP:=PROP) True Affine P.
Proof. rewrite /Affine=> <-; auto. Qed.
Lemma emp_absorbing_all_absorbing P : Absorbing (emp%I : PROP) Absorbing P.
Lemma emp_absorbing_all_absorbing P : Absorbing (PROP:=PROP) emp Absorbing P.
Proof.
intros. rewrite /Absorbing -{2}(left_id emp%I _ P).
by rewrite -(absorbing emp) absorbingly_sep_l left_id.
......@@ -1257,7 +1257,7 @@ Section persistent_bi_absorbing.
End persistent_bi_absorbing.
(* Affine instances *)
Global Instance emp_affine_l : Affine (emp%I : PROP).
Global Instance emp_affine_l : Affine (PROP:=PROP) emp.
Proof. by rewrite /Affine. Qed.
Global Instance and_affine_l P Q : Affine P Affine (P Q).
Proof. rewrite /Affine=> ->; auto. Qed.
......@@ -1280,7 +1280,7 @@ Global Instance intuitionistically_affine P : Affine (□ P).
Proof. rewrite /bi_intuitionistically. apply _. Qed.
(* Absorbing instances *)
Global Instance pure_absorbing φ : Absorbing (⌜φ⌝%I : PROP).
Global Instance pure_absorbing φ : Absorbing (PROP:=PROP) ⌜φ⌝.
Proof. by rewrite /Absorbing absorbingly_pure. Qed.
Global Instance and_absorbing P Q : Absorbing P Absorbing Q Absorbing (P Q).
Proof. intros. by rewrite /Absorbing absorbingly_and_1 !absorbing. Qed.
......@@ -1324,9 +1324,9 @@ Global Instance persistently_if_absorbing P p :
Proof. intros; destruct p; simpl; apply _. Qed.
(* Persistence instances *)
Global Instance pure_persistent φ : Persistent (⌜φ⌝%I : PROP).
Global Instance pure_persistent φ : Persistent (PROP:=PROP) ⌜φ⌝.
Proof. by rewrite /Persistent persistently_pure. Qed.
Global Instance emp_persistent : Persistent (emp%I : PROP).
Global Instance emp_persistent : Persistent (PROP:=PROP) emp.
Proof. rewrite /Persistent. apply persistently_emp_intro. Qed.
Global Instance and_persistent P Q :
Persistent P Persistent Q Persistent (P Q).
......
......@@ -13,8 +13,8 @@ Implicit Types Ps : list PROP.
Implicit Types A : Type.
(* Force implicit argument PROP *)
Notation "P ⊢ Q" := (@bi_entails PROP P%I Q%I).
Notation "P ⊣⊢ Q" := (equiv (A:=bi_car PROP) P%I Q%I).
Notation "P ⊢ Q" := (P {PROP} Q).
Notation "P ⊣⊢ Q" := (P {PROP} Q).
Hint Resolve or_elim or_intro_l' or_intro_r' True_intro False_elim.
Hint Resolve and_elim_l' and_elim_r' and_intro forall_intro.
......@@ -127,10 +127,10 @@ Proof.
Qed.
Global Instance internal_eq_absorbing {A : ofeT} (x y : A) :
Absorbing (x y : PROP)%I.
Absorbing (PROP:=PROP) (x y).
Proof. by rewrite /Absorbing absorbingly_internal_eq. Qed.
Global Instance internal_eq_persistent {A : ofeT} (a b : A) :
Persistent (a b : PROP)%I.
Persistent (PROP:=PROP) (a b).
Proof. by intros; rewrite /Persistent persistently_internal_eq. Qed.
(* Equality under a later. *)
......@@ -351,7 +351,7 @@ Proof. by rewrite {1}(except_0_intro P) except_0_sep. Qed.
Lemma except_0_frame_r P Q : P Q (P Q).
Proof. by rewrite {1}(except_0_intro Q) except_0_sep. Qed.
Lemma later_affinely_1 `{!Timeless (emp%I : PROP)} P : <affine> P <affine> P.
Lemma later_affinely_1 `{!Timeless (PROP:=PROP) emp} P : <affine> P <affine> P.
Proof.
rewrite /bi_affinely later_and (timeless emp%I) except_0_and.
by apply and_mono, except_0_intro.
......@@ -366,12 +366,12 @@ Proof. rewrite /sbi_except_0; apply _. Qed.
Global Instance Timeless_proper : Proper (() ==> iff) (@Timeless PROP).
Proof. solve_proper. Qed.
Global Instance pure_timeless φ : Timeless (⌜φ⌝ : PROP)%I.
Global Instance pure_timeless φ : Timeless (PROP:=PROP) ⌜φ⌝.
Proof.
rewrite /Timeless /sbi_except_0 pure_alt later_exist_false.
apply or_elim, exist_elim; [auto|]=> Hφ. rewrite -(exist_intro Hφ). auto.
Qed.
Global Instance emp_timeless `{BiAffine PROP} : Timeless (emp : PROP)%I.
Global Instance emp_timeless `{BiAffine PROP} : Timeless (PROP:=PROP) emp.
Proof. rewrite -True_emp. apply _. Qed.
Global Instance and_timeless P Q : Timeless P Timeless Q Timeless (P Q).
......@@ -420,13 +420,13 @@ Proof.
Qed.
Global Instance affinely_timeless P :
Timeless (emp%I : PROP) Timeless P Timeless (<affine> P).
Timeless (PROP:=PROP) emp Timeless P Timeless (<affine> P).
Proof. rewrite /bi_affinely; apply _. Qed.
Global Instance absorbingly_timeless P : Timeless P Timeless (<absorb> P).
Proof. rewrite /bi_absorbingly; apply _. Qed.
Global Instance eq_timeless {A : ofeT} (a b : A) :
Discrete a Timeless (a b : PROP)%I.
Discrete a Timeless (PROP:=PROP) (a b).
Proof. intros. rewrite /Discrete !discrete_eq. apply (timeless _). Qed.
Global Instance from_option_timeless {A} P (Ψ : A PROP) (mx : option A) :
( x, Timeless (Ψ x)) Timeless P Timeless (from_option Ψ P mx).
......
......@@ -36,21 +36,21 @@ Arguments bi_embed_embed : simpl never.
Class SbiEmbed (PROP1 PROP2 : sbi) `{BiEmbed PROP1 PROP2} := {
embed_internal_eq_1 (A : ofeT) (x y : A) : x y x y;
embed_later P : ⎡▷ P P;
embed_interal_inj (PROP' : sbi) (P Q : PROP1) : P Q (P Q : PROP');
embed_interal_inj (PROP' : sbi) (P Q : PROP1) : P Q {PROP'} (P Q);
}.
Hint Mode SbiEmbed ! - - : typeclass_instances.
Hint Mode SbiEmbed - ! - : typeclass_instances.
Class BiEmbedBUpd (PROP1 PROP2 : bi)
`{BiEmbed PROP1 PROP2, BiBUpd PROP1, BiBUpd PROP2} := {
embed_bupd P : |==> P bupd (PROP:=PROP2) P
embed_bupd P : |==> P {PROP2} |==> P
}.
Hint Mode BiEmbedBUpd - ! - - - : typeclass_instances.
Hint Mode BiEmbedBUpd ! - - - - : typeclass_instances.
Class BiEmbedFUpd (PROP1 PROP2 : sbi)
`{BiEmbed PROP1 PROP2, BiFUpd PROP1, BiFUpd PROP2} := {
embed_fupd E1 E2 P : |={E1,E2}=> P fupd (PROP:=PROP2) E1 E2 P
embed_fupd E1 E2 P : |={E1,E2}=> P {PROP2} |={E1,E2}=> P
}.
Hint Mode BiEmbedFUpd - ! - - - : typeclass_instances.
Hint Mode BiEmbedFUpd ! - - - - : typeclass_instances.
......
......@@ -2,6 +2,7 @@ From iris.algebra Require Export ofe.
Set Primitive Projections.
Reserved Notation "P ⊢ Q" (at level 99, Q at level 200, right associativity).
Reserved Notation "P ⊢{ PROP } Q" (at level 99, Q at level 200, right associativity, format "P '⊢{' PROP '}' Q").
Reserved Notation "'emp'".
Reserved Notation "'⌜' φ '⌝'" (at level 1, φ at level 200, format "⌜ φ ⌝").
Reserved Notation "P ∗ Q" (at level 80, right associativity).
......@@ -265,10 +266,13 @@ Instance bi_rewrite_relation (PROP : bi) : RewriteRelation (@bi_entails PROP).
Instance bi_inhabited {PROP : bi} : Inhabited PROP := populate (bi_pure True).
Notation "P ⊢ Q" := (bi_entails P%I Q%I) : stdpp_scope.
Notation "P ⊢{ PROP } Q" := (bi_entails (PROP:=PROP) P%I Q%I) : stdpp_scope.
Notation "(⊢)" := bi_entails (only parsing) : stdpp_scope.
Notation "P ⊣⊢ Q" := (equiv (A:=bi_car _) P%I Q%I)
(at level 95, no associativity) : stdpp_scope.
Notation "P ⊣⊢{ PROP } Q" := (equiv (A:=bi_car PROP) P%I Q%I)
(at level 95, no associativity) : stdpp_scope.
Notation "(⊣⊢)" := (equiv (A:=bi_car _)) (only parsing) : stdpp_scope.
Notation "P -∗ Q" := (P Q) : stdpp_scope.
......@@ -340,7 +344,7 @@ Lemma pure_intro P (φ : Prop) : φ → P ⊢ ⌜ φ ⌝.
Proof. eapply bi_mixin_pure_intro, bi_bi_mixin. Qed.
Lemma pure_elim' (φ : Prop) P : (φ True P) φ P.
Proof. eapply bi_mixin_pure_elim', bi_bi_mixin. Qed.
Lemma pure_forall_2 {A} (φ : A Prop) : ( a, φ a : PROP) a, φ a .
Lemma pure_forall_2 {A} (φ : A Prop) : ( a, φ a ) {PROP} a, φ a .
Proof. eapply bi_mixin_pure_forall_2, bi_bi_mixin. Qed.
Lemma and_elim_l P Q : P Q P.
......@@ -394,7 +398,7 @@ Proof. eapply bi_mixin_persistently_mono, bi_bi_mixin. Qed.
Lemma persistently_idemp_2 P : <pers> P <pers> <pers> P.
Proof. eapply bi_mixin_persistently_idemp_2, bi_bi_mixin. Qed.
Lemma persistently_emp_2 : (emp : PROP) <pers> emp.
Lemma persistently_emp_2 : emp {PROP} <pers> emp.
Proof. eapply bi_mixin_persistently_emp_2, bi_bi_mixin. Qed.
Lemma persistently_forall_2 {A} (Ψ : A PROP) :
......@@ -425,21 +429,23 @@ Lemma internal_eq_rewrite {A : ofeT} a b (Ψ : A → PROP) :
NonExpansive Ψ a b Ψ a Ψ b.
Proof. eapply sbi_mixin_internal_eq_rewrite, sbi_sbi_mixin. Qed.
Lemma fun_ext {A} {B : A ofeT} (f g : ofe_fun B) : ( x, f x g x) (f g : PROP).
Lemma fun_ext {A} {B : A ofeT} (f g : ofe_fun B) :
( x, f x g x) {PROP} f g.
Proof. eapply sbi_mixin_fun_ext, sbi_sbi_mixin. Qed.
Lemma sig_eq {A : ofeT} (P : A Prop) (x y : sig P) : `x `y (x y : PROP).
Lemma sig_eq {A : ofeT} (P : A Prop) (x y : sig P) :
`x `y {PROP} x y.
Proof. eapply sbi_mixin_sig_eq, sbi_sbi_mixin. Qed.
Lemma discrete_eq_1 {A : ofeT} (a b : A) :
Discrete a a b (a b : PROP).
Discrete a a b {PROP} a b.
Proof. eapply sbi_mixin_discrete_eq_1, sbi_sbi_mixin. Qed.
(* Later *)
Global Instance later_contractive : Contractive (@sbi_later PROP).
Proof. eapply sbi_mixin_later_contractive, sbi_sbi_mixin. Qed.
Lemma later_eq_1 {A : ofeT} (x y : A) : Next x Next y (x y : PROP).
Lemma later_eq_1 {A : ofeT} (x y : A) : Next x Next y {PROP} (x y).
Proof. eapply sbi_mixin_later_eq_1, sbi_sbi_mixin. Qed.
Lemma later_eq_2 {A : ofeT} (x y : A) : (x y) (Next x Next y : PROP).
Lemma later_eq_2 {A : ofeT} (x y : A) : (x y) {PROP} Next x Next y.
Proof. eapply sbi_mixin_later_eq_2, sbi_sbi_mixin. Qed.
Lemma later_mono P Q : (P Q) P Q.
......
......@@ -823,7 +823,7 @@ Lemma monPred_at_except_0 i P : (◇ P) i ⊣⊢ ◇ P i.
Proof. by unseal. Qed.
Lemma monPred_equivI {PROP' : sbi} P Q :
sbi_internal_eq (PROP:=PROP') P Q i, P i Q i.
P Q {PROP'} i, P i Q i.
Proof.
apply bi.equiv_spec. split.
- apply bi.forall_intro=>?. apply (bi.f_equiv (flip monPred_at _)).
......
......@@ -161,7 +161,7 @@ Proof. apply (anti_symm _); auto using plainly_idemp_1, plainly_idemp_2. Qed.
Lemma plainly_intro' P Q : ( P Q) P Q.
Proof. intros <-. apply plainly_idemp_2. Qed.
Lemma plainly_pure φ : ⌜φ⌝ bi_pure (PROP:=PROP) φ.
Lemma plainly_pure φ : ⌜φ⌝ {PROP} ⌜φ⌝.
Proof.
apply (anti_symm _); auto.
- by rewrite plainly_elim_persistently persistently_pure.
......@@ -204,7 +204,7 @@ Proof. by rewrite -{1}(left_id emp%I _ Q%I) plainly_and_sep_assoc and_elim_l. Qe
Lemma plainly_and_sep_r_1 P Q : P Q P Q.
Proof. by rewrite !(comm _ P) plainly_and_sep_l_1. Qed.
Lemma plainly_True_emp : True (@bi_emp PROP).
Lemma plainly_True_emp : True {PROP} emp.
Proof. apply (anti_symm _); eauto using plainly_mono, plainly_emp_intro. Qed.
Lemma plainly_and_sep P Q : (P Q) (P Q).
Proof.
......@@ -273,7 +273,7 @@ Proof. rewrite -!impl_wand_affinely_plainly. apply plainly_impl_plainly. Qed.
Section plainly_affine_bi.
Context `{BiAffine PROP}.
Lemma plainly_emp : emp bi_emp (PROP:=PROP).
Lemma plainly_emp : emp {PROP} emp.
Proof. by rewrite -!True_emp plainly_pure. Qed.
Lemma plainly_and_sep_l P Q : P Q P Q.
......@@ -311,7 +311,7 @@ Proof. solve_proper. Qed.
Lemma plainly_if_mono p P Q : (P Q) ?p P ?p Q.
Proof. by intros ->. Qed.
Lemma plainly_if_pure p φ : ?p ⌜φ⌝ bi_pure (PROP:=PROP) φ.
Lemma plainly_if_pure p φ : ?p ⌜φ⌝ {PROP} ⌜φ⌝.
Proof. destruct p; simpl; auto using plainly_pure. Qed.
Lemma plainly_if_and p P Q : ?p (P Q) ?p P ?p Q.
Proof. destruct p; simpl; auto using plainly_and. Qed.
......@@ -406,7 +406,7 @@ Global Instance limit_preserving_Plain {A:ofeT} `{Cofe A} (Φ : A → PROP) :
Proof. intros. apply limit_preserving_entails; solve_proper. Qed.
(* Plainness instances *)
Global Instance pure_plain φ : Plain (⌜φ⌝%I : PROP).
Global Instance pure_plain φ : Plain (PROP:=PROP) ⌜φ⌝.
Proof. by rewrite /Plain plainly_pure. Qed.
Global Instance emp_plain : Plain (PROP:=PROP) emp.
Proof. apply plainly_emp_intro. Qed.
......@@ -458,7 +458,7 @@ Global Instance from_option_plain {A} P (Ψ : A → PROP) (mx : option A) :
Proof. destruct mx; apply _. Qed.
(* Interaction with equality *)
Lemma plainly_internal_eq {A:ofeT} (a b : A) : plainly (A:=PROP) (a b) a b.
Lemma plainly_internal_eq {A:ofeT} (a b : A) : (a b) {PROP} a b.
Proof.
apply (anti_symm ()).
{ by rewrite plainly_elim. }
......@@ -511,7 +511,7 @@ Lemma except_0_plainly `{!BiPlainlyExist PROP} P : ◇ ■ P ⊣⊢ ■ ◇ P.
Proof. by rewrite /sbi_except_0 plainly_or -later_plainly plainly_pure. Qed.
Global Instance internal_eq_plain {A : ofeT} (a b : A) :
Plain (a b : PROP)%I.
Plain (PROP:=PROP) (a b).
Proof. by intros; rewrite /Plain plainly_internal_eq. Qed.
Global Instance later_plain P : Plain P Plain ( P).
......
......@@ -225,7 +225,7 @@ Global Instance into_sep_except_0 P Q1 Q2 :
Proof. rewrite /IntoSep=> ->. by rewrite except_0_sep. Qed.
(* FIXME: This instance is overly specific, generalize it. *)
Global Instance into_sep_affinely_later `{!Timeless (emp%I : PROP)} P Q1 Q2 :
Global Instance into_sep_affinely_later `{!Timeless (PROP:=PROP) emp} P Q1 Q2 :
IntoSep P Q1 Q2 Affine Q1 Affine Q2
IntoSep (<affine> P) (<affine> Q1) (<affine> Q2).
Proof.
......
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