Commit e53c8a39 by Ralf Jung

add '@' to type ascription notation for disambiguation

parent c0be693a
 ... ... @@ -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] k↦y ∈ l, emp) ⊣⊢{PROP} emp. Lemma big_sepL_emp l : ([∗ list] k↦y ∈ 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" := (P ⊢{PROP} Q). Notation "P ⊣⊢ Q" := (P ⊣⊢{PROP} Q). 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). ... ...
 ... ... @@ -13,8 +13,8 @@ Implicit Types Ps : list PROP. Implicit Types A : Type. (* Force implicit argument PROP *) Notation "P ⊢ Q" := (P ⊢{PROP} Q). Notation "P ⊣⊢ Q" := (P ⊣⊢{PROP} Q). 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. ... ...
 ... ... @@ -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⎤ ⊢{PROP'} (P ≡ Q); 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⎤ ⊣⊢{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⎤ ⊣⊢{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,7 +2,9 @@ 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 "P '⊢@{' PROP } Q" (at level 99, Q at level 200, right associativity, format "P '⊢@{' PROP '}' Q"). Reserved Notation "P ⊣⊢ Q" (at level 95, no associativity). Reserved Notation "P '⊣⊢@{' PROP } Q" (at level 95, no 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). ... ... @@ -266,13 +268,11 @@ 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 "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 "P ⊣⊢ Q" := (equiv (A:=bi_car _) P%I Q%I) : stdpp_scope. Notation "P ⊣⊢@{ PROP } Q" := (equiv (A:=bi_car PROP) P%I Q%I) : stdpp_scope. Notation "(⊣⊢)" := (equiv (A:=bi_car _)) (only parsing) : stdpp_scope. Notation "P -∗ Q" := (P ⊢ Q) : stdpp_scope. ... ... @@ -344,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. ... ... @@ -398,7 +398,7 @@ Proof. eapply bi_mixin_persistently_mono, bi_bi_mixin. Qed. Lemma persistently_idemp_2 P : P ⊢ P. Proof. eapply bi_mixin_persistently_idemp_2, bi_bi_mixin. Qed. Lemma persistently_emp_2 : emp ⊢{PROP} emp. Lemma persistently_emp_2 : emp ⊢@{PROP} emp. Proof. eapply bi_mixin_persistently_emp_2, bi_bi_mixin. Qed. Lemma persistently_forall_2 {A} (Ψ : A → PROP) : ... ... @@ -430,22 +430,22 @@ Lemma internal_eq_rewrite {A : ofeT} a b (Ψ : A → PROP) : 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) ⊢{PROP} f ≡ g. (∀ 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 ⊢{PROP} x ≡ y. `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 ⊢{PROP} ⌜a ≡ b⌝. 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 ⊢{PROP} ▷ (x ≡ y). 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) ⊢{PROP} Next x ≡ Next y. 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 : P ≡ Q ⊣⊢{PROP'} ∀ 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 φ : ■ ⌜φ⌝ ⊣⊢{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 ⊣⊢{PROP} ■ emp. 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 ⊣⊢{PROP} emp. 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 ⌜φ⌝ ⊣⊢{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. ... ... @@ -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) : ■ (a ≡ b) ⊣⊢{PROP} a ≡ b. Lemma plainly_internal_eq {A:ofeT} (a b : A) : ■ (a ≡ b) ⊣⊢@{PROP} a ≡ b. Proof. apply (anti_symm (⊢)). { by rewrite plainly_elim. } ... ...
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!