Commit 3442e7ae authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Turn some forgotten uses of `bi_emp_valid` into the new `⊢` notation.

parent ad3a71bf
Pipeline #25378 passed with stage
in 15 minutes and 40 seconds
......@@ -204,13 +204,13 @@ Lemma discrete_fun_validI {A} {B : A → ucmraT} (g : discrete_fun B) : ✓ g
Proof. exact: uPred_primitive.discrete_fun_validI. Qed.
(** Consistency/soundness statement *)
Lemma pure_soundness φ : bi_emp_valid (PROP:=uPredI M) φ φ.
Lemma pure_soundness φ : (@{uPredI M} φ ) φ.
Proof. apply pure_soundness. Qed.
Lemma internal_eq_soundness {A : ofeT} (x y : A) : (True x y) x y.
Lemma internal_eq_soundness {A : ofeT} (x y : A) : (@{uPredI M} x y) x y.
Proof. apply internal_eq_soundness. Qed.
Lemma later_soundness P : bi_emp_valid ( P) bi_emp_valid P.
Lemma later_soundness P : ( P) P.
Proof. apply later_soundness. Qed.
(** See [derived.v] for a similar soundness result for basic updates. *)
End restate.
......
......@@ -84,7 +84,7 @@ Global Instance uPred_ownM_sep_homomorphism :
Proof. split; [split; try apply _|]. apply ownM_op. apply ownM_unit'. Qed.
(** Consistency/soundness statement *)
Lemma bupd_plain_soundness P `{!Plain P} : bi_emp_valid (|==> P) bi_emp_valid P.
Lemma bupd_plain_soundness P `{!Plain P} : ( |==> P) P.
Proof.
eapply bi_emp_valid_mono. etrans; last exact: bupd_plainly. apply bupd_mono'.
apply: plain.
......
......@@ -59,8 +59,8 @@ Proof.
by iFrame.
Qed.
Lemma fupd_plain_soundness `{!invPreG Σ} E1 E2 (P: iProp Σ) `{!Plain P}:
( `{Hinv: !invG Σ}, bi_emp_valid (|={E1,E2}=> P)) bi_emp_valid P.
Lemma fupd_plain_soundness `{!invPreG Σ} E1 E2 (P: iProp Σ) `{!Plain P} :
( `{Hinv: !invG Σ}, |={E1,E2}=> P) P.
Proof.
iIntros (Hfupd). apply later_soundness. iMod wsat_alloc as (Hinv) "[Hw HE]".
iAssert (|={,E2}=> P)%I as "H".
......
......@@ -15,7 +15,7 @@ Record BiEmbedMixin (PROP1 PROP2 : bi) `(Embed PROP1 PROP2) := {
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;
(@{PROP2} P) P;
bi_embed_mixin_emp_2 : emp @{PROP2} emp;
bi_embed_mixin_impl_2 (P Q : PROP1) :
(P Q) @{PROP2} P Q;
......
......@@ -31,7 +31,7 @@ Implicit Types P Q R : PROP.
Implicit Types mP : option PROP.
(** AsEmpValid *)
Global Instance as_emp_valid_emp_valid P : AsEmpValid0 (bi_emp_valid P) P | 0.
Global Instance as_emp_valid_emp_valid P : AsEmpValid0 ( P) P | 0.
Proof. by rewrite /AsEmpValid. Qed.
Global Instance as_emp_valid_entails P Q : AsEmpValid0 (P Q) (P - Q).
Proof. split. apply bi.entails_wand. apply bi.wand_entails. Qed.
......@@ -986,10 +986,10 @@ Qed.
(* These instances must be used only after [into_forall_wand_pure] and
[into_forall_wand_pure] above. *)
Global Instance into_forall_wand P Q :
IntoForall (P - Q) (λ _ : bi_emp_valid P, Q) | 10.
IntoForall (P - Q) (λ _ : P, Q) | 10.
Proof. rewrite /IntoForall. apply forall_intro=><-. rewrite emp_wand //. Qed.
Global Instance into_forall_impl `{!BiAffine PROP} P Q :
IntoForall (P Q) (λ _ : bi_emp_valid P, Q) | 10.
IntoForall (P Q) (λ _ : P, Q) | 10.
Proof. rewrite /IntoForall. apply forall_intro=><-. rewrite -True_emp True_impl //. Qed.
(** FromForall *)
......
......@@ -492,7 +492,7 @@ Hint Mode IntoEmbed + + + ! - : typeclass_instances.
[Hint Mode - ! -], but the fact that Coq ignores primitive
projections for hints modes would make this fail.*)
Class AsEmpValid {PROP : bi} (φ : Prop) (P : PROP) :=
as_emp_valid : φ bi_emp_valid P.
as_emp_valid : φ P.
Arguments AsEmpValid {_} _%type _%I.
Class AsEmpValid0 {PROP : bi} (φ : Prop) (P : PROP) :=
as_emp_valid_0 : AsEmpValid φ P.
......@@ -500,10 +500,10 @@ Arguments AsEmpValid0 {_} _%type _%I.
Existing Instance as_emp_valid_0 | 0.
Lemma as_emp_valid_1 (φ : Prop) {PROP : bi} (P : PROP) `{!AsEmpValid φ P} :
φ bi_emp_valid P.
φ P.
Proof. by apply as_emp_valid. Qed.
Lemma as_emp_valid_2 (φ : Prop) {PROP : bi} (P : PROP) `{!AsEmpValid φ P} :
bi_emp_valid P φ.
( P) φ.
Proof. by apply as_emp_valid. Qed.
(* Input: [P]; Outputs: [N],
......
......@@ -15,7 +15,7 @@ Implicit Types Δ : envs PROP.
Implicit Types P Q : PROP.
(** * Starting and stopping the proof mode *)
Lemma tac_start P : envs_entails (Envs Enil Enil 1) P bi_emp_valid P.
Lemma tac_start P : envs_entails (Envs Enil Enil 1) P P.
Proof.
rewrite envs_entails_eq !of_envs_eq /=.
rewrite intuitionistically_True_emp left_id=><-.
......@@ -477,7 +477,7 @@ Proof.
by rewrite -(entails_wand P) // intuitionistically_emp emp_wand.
Qed.
Definition IntoEmpValid (φ : Type) (P : PROP) := φ bi_emp_valid P.
Definition IntoEmpValid (φ : Type) (P : PROP) := φ P.
(** These lemmas are [Defined] because the guardedness checker must see
through them. See https://gitlab.mpi-sws.org/iris/iris/issues/274. For the
same reason, their bodies use as little automation as possible. *)
......@@ -489,7 +489,7 @@ Proof. rewrite /IntoEmpValid => Hφ Hi1 Hi2. apply Hi1, Hi2, Hφ. Defined.
Lemma into_emp_valid_forall {A} (φ : A Type) P x :
IntoEmpValid (φ x) P IntoEmpValid ( x : A, φ x) P.
Proof. rewrite /IntoEmpValid => Hi1 Hi2. apply Hi1, Hi2. Defined.
Lemma into_emp_valid_proj φ P : IntoEmpValid φ P φ bi_emp_valid P.
Lemma into_emp_valid_proj φ P : IntoEmpValid φ P φ P.
Proof. intros HP. apply HP. Defined.
(** When called by the proof mode, the proof of [P] is produced by calling
......
......@@ -747,7 +747,7 @@ Tactic Notation "iPoseProofCoreHyp" constr(H) "as" constr(Hnew) :=
end.
(* The tactic [iIntoEmpValid] tactic "imports a Coq lemma into the proofmode",
i.e. it solves a goal [IntoEmpValid ψ ?Q]. The argument [ψ] must be of the
i.e., it solves a goal [IntoEmpValid ψ ?Q]. The argument [ψ] must be of the
following shape:
[∀ (x_1 : A_1) .. (x_n : A_n), φ]
......@@ -756,14 +756,14 @@ for which we have an instance [AsEmpValid φ ?Q].
Examples of such [φ]s are
- [bi_emp_valid P], in which case [?Q] is unified with [P].
- [ P], in which case [?Q] is unified with [P].
- [P1 ⊢ P2], in which case [?Q] is unified with [P1 -∗ P2].
- [P1 ⊣⊢ P2], in which case [?Q] is unified with [P1 ↔ P2].
The tactic instantiates each dependent argument [x_i : A_i] with an evar, and
generates a goal [A_i] for each non-dependent argument [x_i : A_i].
For example, if goal is [bi_emp_valid (∀ x, P x → R1 x ⊢ R2 x) ?Q], then the
For example, if goal is [IntoEmpValid (∀ x, P x → R1 x ⊢ R2 x) ?Q], then the
[iIntoEmpValid] tactic generates an evar [?x], a subgoal [P ?x], and unifies
[?Q] with [R1 ?x -∗ R2 ?x]. *)
Ltac iIntoEmpValid_go := first
......@@ -772,7 +772,7 @@ Ltac iIntoEmpValid_go := first
[(*goal for [φ] *)|iIntoEmpValid_go]
|(* Case [∀ x : A, φ] *)
notypeclasses refine (into_emp_valid_forall _ _ _ _); iIntoEmpValid_go
|(* Case [P ⊢ Q], [P ⊣⊢ Q], [bi_emp_valid P] *)
|(* Case [P ⊢ Q], [P ⊣⊢ Q], [ P] *)
notypeclasses refine (into_emp_valid_here _ _ _)].
Ltac iIntoEmpValid :=
......@@ -3191,7 +3191,7 @@ Tactic Notation "iAccu" :=
(** Automation *)
Hint Extern 0 (_ _) => iStartProof : core.
Hint Extern 0 (bi_emp_valid _) => iStartProof : core.
Hint Extern 0 ( _) => iStartProof : core.
(* Make sure that by and done solve trivial things in proof mode *)
Hint Extern 0 (envs_entails _ _) => iPureIntro; try done : core.
......
......@@ -159,13 +159,13 @@ Proof. done. Qed.
Module siProp.
Section restate.
Lemma pure_soundness φ : bi_emp_valid (PROP:=siPropI) φ φ.
Lemma pure_soundness φ : (@{siPropI} φ ) φ.
Proof. apply pure_soundness. Qed.
Lemma internal_eq_soundness {A : ofeT} (x y : A) : (True @{siPropI} x y) x y.
Lemma internal_eq_soundness {A : ofeT} (x y : A) : (@{siPropI} x y) x y.
Proof. apply internal_eq_soundness. Qed.
Lemma later_soundness P : bi_emp_valid (PROP:=siPropI) ( P) bi_emp_valid P.
Lemma later_soundness (P : siProp) : ( P) P.
Proof. apply later_soundness. Qed.
End restate.
End siProp.
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