Commit 526f472c authored by Ralf Jung's avatar Ralf Jung

rename valid -> emp_valid

parent b1ddcc68
......@@ -118,7 +118,7 @@ Lemma own_alloc_strong a (G : gset gname) :
Proof.
intros Ha.
rewrite -(bupd_mono ( m, γ, γ G m = iRes_singleton γ a uPred_ownM m)%I).
- rewrite /uPred_valid /bi_valid ownM_unit.
- rewrite /uPred_valid /bi_emp_valid ownM_unit.
eapply bupd_ownM_updateP, (ofe_fun_singleton_updateP_empty (inG_id _));
first (eapply alloc_updateP_strong', cmra_transport_valid, Ha);
naive_solver.
......@@ -127,7 +127,7 @@ Proof.
Qed.
Lemma own_alloc a : a (|==> γ, own γ a)%I.
Proof.
intros Ha. rewrite /uPred_valid /bi_valid (own_alloc_strong a ) //; [].
intros Ha. rewrite /uPred_valid /bi_emp_valid (own_alloc_strong a ) //; [].
apply bupd_mono, exist_mono=>?. eauto with I.
Qed.
......@@ -168,7 +168,7 @@ Arguments own_update_3 {_ _} [_] _ _ _ _ _ _.
Lemma own_unit A `{inG Σ (A:ucmraT)} γ : (|==> own γ ε)%I.
Proof.
rewrite /uPred_valid /bi_valid ownM_unit !own_eq /own_def.
rewrite /uPred_valid /bi_emp_valid ownM_unit !own_eq /own_def.
apply bupd_ownM_update, ofe_fun_singleton_update_empty.
apply (alloc_unit_singleton_update (cmra_transport inG_prf ε)); last done.
- apply cmra_transport_valid, ucmra_unit_valid.
......
......@@ -54,7 +54,7 @@ Proof. rewrite /ownI. apply _. Qed.
Lemma ownE_empty : (|==> ownE )%I.
Proof.
rewrite /uPred_valid /bi_valid.
rewrite /uPred_valid /bi_emp_valid.
by rewrite (own_unit (coPset_disjUR) enabled_name).
Qed.
Lemma ownE_op E1 E2 : E1 ## E2 ownE (E1 E2) ownE E1 ownE E2.
......@@ -72,7 +72,7 @@ Proof. rewrite ownE_disjoint. iIntros (?); set_solver. Qed.
Lemma ownD_empty : (|==> ownD )%I.
Proof.
rewrite /uPred_valid /bi_valid.
rewrite /uPred_valid /bi_emp_valid.
by rewrite (own_unit (gset_disjUR positive) disabled_name).
Qed.
Lemma ownD_op E1 E2 : E1 ## E2 ownD (E1 E2) ownD E1 ownD E2.
......
......@@ -540,7 +540,7 @@ Canonical Structure uPredSI (M : ucmraT) : sbi :=
{| sbi_ofe_mixin := ofe_mixin_of (uPred M);
sbi_bi_mixin := uPred_bi_mixin M; sbi_sbi_mixin := uPred_sbi_mixin M |}.
Coercion uPred_valid {M} : uPred M Prop := bi_valid.
Coercion uPred_valid {M} : uPred M Prop := bi_emp_valid.
(* Latest notation *)
Notation "✓ x" := (uPred_cmra_valid x) (at level 20) : bi_scope.
......@@ -671,7 +671,7 @@ Proof.
rewrite /bi_persistently /=. unseal.
split=> n x Hx /=. by apply cmra_core_monoN.
Qed.
Lemma ownM_unit : bi_valid (uPred_ownM (ε:M)).
Lemma ownM_unit : bi_emp_valid (uPred_ownM (ε:M)).
Proof. unseal; split=> n x ??; by exists x; rewrite left_id. Qed.
Lemma later_ownM (a : M) : uPred_ownM a b, uPred_ownM b (a b).
Proof.
......@@ -691,7 +691,7 @@ Proof.
unseal; split=> n x Hv [a' ?]; ofe_subst; eauto using cmra_validN_op_l.
Qed.
Lemma cmra_valid_intro {A : cmraT} (a : A) :
a bi_valid (PROP:=uPredI M) ( a).
a bi_emp_valid (PROP:=uPredI M) ( a).
Proof. unseal=> ?; split=> n x ? _ /=; by apply cmra_valid_validN. Qed.
Lemma cmra_valid_elim {A : cmraT} (a : A) : ¬ {0} a a (False : uPred M).
Proof.
......
......@@ -35,12 +35,12 @@ Lemma entails_equiv_l P Q R : (P ⊣⊢ Q) → (Q ⊢ R) → (P ⊢ R).
Proof. by intros ->. Qed.
Lemma entails_equiv_r P Q R : (P Q) (Q R) (P R).
Proof. by intros ? <-. Qed.
Global Instance bi_valid_proper : Proper (() ==> iff) (@bi_valid PROP).
Global Instance bi_emp_valid_proper : Proper (() ==> iff) (@bi_emp_valid PROP).
Proof. solve_proper. Qed.
Global Instance bi_valid_mono : Proper (() ==> impl) (@bi_valid PROP).
Global Instance bi_emp_valid_mono : Proper (() ==> impl) (@bi_emp_valid PROP).
Proof. solve_proper. Qed.
Global Instance bi_valid_flip_mono :
Proper (flip () ==> flip impl) (@bi_valid PROP).
Global Instance bi_emp_valid_flip_mono :
Proper (flip () ==> flip impl) (@bi_emp_valid PROP).
Proof. solve_proper. Qed.
(* Propers *)
......@@ -313,13 +313,13 @@ Proof. rewrite -{1}[P](left_id emp%I bi_sep). auto using sep_mono. Qed.
Lemma sep_True_2 P : P P True.
Proof. by rewrite comm -True_sep_2. Qed.
Lemma sep_intro_valid_l P Q R : P (R Q) R P Q.
Lemma sep_intro_emp_valid_l P Q R : P (R Q) R P Q.
Proof. intros ? ->. rewrite -{1}(left_id emp%I _ Q). by apply sep_mono. Qed.
Lemma sep_intro_valid_r P Q R : (R P) Q R P Q.
Proof. intros -> ?. rewrite comm. by apply sep_intro_valid_l. Qed.
Lemma sep_elim_valid_l P Q R : P (P R Q) R Q.
Lemma sep_intro_emp_valid_r P Q R : (R P) Q R P Q.
Proof. intros -> ?. rewrite comm. by apply sep_intro_emp_valid_l. Qed.
Lemma sep_elim_emp_valid_l P Q R : P (P R Q) R Q.
Proof. intros <- <-. by rewrite left_id. Qed.
Lemma sep_elim_valid_r P Q R : P (R P Q) R Q.
Lemma sep_elim_emp_valid_r P Q R : P (R P Q) R Q.
Proof. intros <- <-. by rewrite right_id. Qed.
Lemma wand_intro_l P Q R : (Q P R) P Q - R.
......@@ -402,7 +402,7 @@ Proof. intros ->; apply wand_iff_refl. Qed.
Lemma wand_iff_equiv P Q : (P - Q)%I (P Q).
Proof.
intros HPQ; apply (anti_symm ());
apply wand_entails; rewrite /bi_valid HPQ /bi_wand_iff; auto.
apply wand_entails; rewrite /bi_emp_valid HPQ /bi_wand_iff; auto.
Qed.
Lemma entails_impl P Q : (P Q) (P Q)%I.
......@@ -415,7 +415,7 @@ Proof. intros ->; apply iff_refl. Qed.
Lemma iff_equiv P Q `{!Affine P, !Affine Q} : (P Q)%I (P Q).
Proof.
intros HPQ; apply (anti_symm ());
apply: impl_entails; rewrite /bi_valid HPQ /bi_iff; auto.
apply: impl_entails; rewrite /bi_emp_valid HPQ /bi_iff; auto.
Qed.
(* Pure stuff *)
......
......@@ -99,9 +99,9 @@ Section embed.
rewrite EQ //.
Qed.
Lemma embed_valid (P : PROP1) : P%I P.
Lemma embed_emp_valid (P : PROP1) : P%I P.
Proof.
by rewrite /bi_valid -embed_emp; split=>?; [apply (inj embed)|f_equiv].
by rewrite /bi_emp_valid -embed_emp; split=>?; [apply (inj embed)|f_equiv].
Qed.
Lemma embed_forall A (Φ : A PROP1) : x, Φ x x, ⎡Φ x.
......
......@@ -294,11 +294,11 @@ Notation "'<pers>' P" := (bi_persistently P) : bi_scope.
Infix "≡" := sbi_internal_eq : bi_scope.
Notation "▷ P" := (sbi_later P) : bi_scope.
Coercion bi_valid {PROP : bi} (P : PROP) : Prop := emp P.
Coercion sbi_valid {PROP : sbi} : PROP Prop := bi_valid.
Coercion bi_emp_valid {PROP : bi} (P : PROP) : Prop := emp P.
Coercion sbi_emp_valid {PROP : sbi} : PROP Prop := bi_emp_valid.
Arguments bi_valid {_} _%I : simpl never.
Typeclasses Opaque bi_valid.
Arguments bi_emp_valid {_} _%I : simpl never.
Typeclasses Opaque bi_emp_valid.
Module bi.
Section bi_laws.
......
......@@ -992,18 +992,18 @@ Global Instance into_embed_embed {PROP' : bi} `{BiEmbed PROP PROP'} P :
IntoEmbed P P.
Proof. by rewrite /IntoEmbed. Qed.
(* AsValid *)
Global Instance as_valid_valid {PROP : bi} (P : PROP) : AsValid0 (bi_valid P) P | 0.
Proof. by rewrite /AsValid. Qed.
Global Instance as_valid_entails {PROP : bi} (P Q : PROP) : AsValid0 (P Q) (P - Q).
(* AsEmpValid *)
Global Instance as_emp_valid_emp_valid {PROP : bi} (P : PROP) : AsEmpValid0 (bi_emp_valid P) P | 0.
Proof. by rewrite /AsEmpValid. Qed.
Global Instance as_emp_valid_entails {PROP : bi} (P Q : PROP) : AsEmpValid0 (P Q) (P - Q).
Proof. split. apply bi.entails_wand. apply bi.wand_entails. Qed.
Global Instance as_valid_equiv {PROP : bi} (P Q : PROP) : AsValid0 (P Q) (P - Q).
Global Instance as_emp_valid_equiv {PROP : bi} (P Q : PROP) : AsEmpValid0 (P Q) (P - Q).
Proof. split. apply bi.equiv_wand_iff. apply bi.wand_iff_equiv. Qed.
Global Instance as_valid_forall {A : Type} (φ : A Prop) (P : A PROP) :
( x, AsValid (φ x) (P x)) AsValid ( x, φ x) ( x, P x).
Global Instance as_emp_valid_forall {A : Type} (φ : A Prop) (P : A PROP) :
( x, AsEmpValid (φ x) (P x)) AsEmpValid ( x, φ x) ( x, P x).
Proof.
rewrite /AsValid=>H1. split=>H2.
rewrite /AsEmpValid=>H1. split=>H2.
- apply bi.forall_intro=>?. apply H1, H2.
- intros x. apply H1. revert H2. by rewrite (bi.forall_elim x).
Qed.
......@@ -1014,10 +1014,10 @@ Qed.
The first [`{BiEmbed PROP PROP'}] is not considered as a premise by
Coq TC search mechanism because the rest of the hypothesis is dependent
on it. *)
Global Instance as_valid_embed `{BiEmbed PROP PROP'} (φ : Prop) (P : PROP) :
Global Instance as_emp_valid_embed `{BiEmbed PROP PROP'} (φ : Prop) (P : PROP) :
BiEmbed PROP PROP'
AsValid0 φ P AsValid φ P.
Proof. rewrite /AsValid0 /AsValid=> _ ->. rewrite embed_valid //. Qed.
AsEmpValid0 φ P AsEmpValid φ P.
Proof. rewrite /AsEmpValid0 /AsEmpValid=> _ ->. rewrite embed_emp_valid //. Qed.
End bi_instances.
Section sbi_instances.
......
......@@ -455,29 +455,29 @@ Arguments IntoEmbed {_ _ _} _%I _%I.
Arguments into_embed {_ _ _} _%I _%I {_}.
Hint Mode IntoEmbed + + + ! - : typeclass_instances.
(* We use two type classes for [AsValid], in order to avoid loops in
typeclass search. Indeed, the [as_valid_embed] instance would try
(* We use two type classes for [AsEmpValid], in order to avoid loops in
typeclass search. Indeed, the [as_emp_valid_embed] instance would try
to add an arbitrary number of embeddings. To avoid this, the
[AsValid0] type class cannot handle embeddings, and therefore
[as_valid_embed] only tries to add one embedding, and we never try
[AsEmpValid0] type class cannot handle embeddings, and therefore
[as_emp_valid_embed] only tries to add one embedding, and we never try
to insert nested embeddings. This has the additional advantage of
always trying [as_valid_embed] as a second option, so that this
always trying [as_emp_valid_embed] as a second option, so that this
instance is never used when the BI is unknown.
No Hint Modes are declared here. The appropriate one would be
[Hint Mode - ! -], but the fact that Coq ignores primitive
projections for hints modes would make this fail.*)
Class AsValid {PROP : bi} (φ : Prop) (P : PROP) := as_valid : φ P.
Arguments AsValid {_} _%type _%I.
Class AsValid0 {PROP : bi} (φ : Prop) (P : PROP) :=
as_valid_here : AsValid φ P.
Arguments AsValid0 {_} _%type _%I.
Existing Instance as_valid_here | 0.
Lemma as_valid_1 (φ : Prop) {PROP : bi} (P : PROP) `{!AsValid φ P} : φ P.
Proof. by apply as_valid. Qed.
Lemma as_valid_2 (φ : Prop) {PROP : bi} (P : PROP) `{!AsValid φ P} : P φ.
Proof. by apply as_valid. Qed.
Class AsEmpValid {PROP : bi} (φ : Prop) (P : PROP) := as_emp_valid : φ P.
Arguments AsEmpValid {_} _%type _%I.
Class AsEmpValid0 {PROP : bi} (φ : Prop) (P : PROP) :=
as_emp_valid_here : AsEmpValid φ P.
Arguments AsEmpValid0 {_} _%type _%I.
Existing Instance as_emp_valid_here | 0.
Lemma as_emp_valid_1 (φ : Prop) {PROP : bi} (P : PROP) `{!AsEmpValid φ P} : φ P.
Proof. by apply as_emp_valid. Qed.
Lemma as_emp_valid_2 (φ : Prop) {PROP : bi} (P : PROP) `{!AsEmpValid φ P} : P φ.
Proof. by apply as_emp_valid. Qed.
(* Input: [P]; Outputs: [N],
Extracts the namespace associated with an invariant assertion. Used for [iInv]. *)
......
......@@ -148,30 +148,30 @@ Proof.
by rewrite /KnownRFromAssumption /FromAssumption -monPred_subjectively_intro.
Qed.
Global Instance as_valid_monPred_at φ P (Φ : I PROP) :
AsValid0 φ P ( i, MakeMonPredAt i P (Φ i)) AsValid φ ( i, Φ i) | 100.
Global Instance as_emp_valid_monPred_at φ P (Φ : I PROP) :
AsEmpValid0 φ P ( i, MakeMonPredAt i P (Φ i)) AsEmpValid φ ( i, Φ i) | 100.
Proof.
rewrite /MakeMonPredAt /AsValid0 /AsValid /bi_valid=> -> EQ.
rewrite /MakeMonPredAt /AsEmpValid0 /AsEmpValid /bi_emp_valid=> -> EQ.
setoid_rewrite <-EQ. split.
- move=>[H]. apply bi.forall_intro=>i. rewrite -H. by rewrite monPred_at_emp.
- move=>HP. split=>i. rewrite monPred_at_emp HP bi.forall_elim //.
Qed.
Global Instance as_valid_monPred_at_wand φ P Q (Φ Ψ : I PROP) :
AsValid0 φ (P - Q)
Global Instance as_emp_valid_monPred_at_wand φ P Q (Φ Ψ : I PROP) :
AsEmpValid0 φ (P - Q)
( i, MakeMonPredAt i P (Φ i)) ( i, MakeMonPredAt i Q (Ψ i))
AsValid φ ( i, Φ i - Ψ i).
AsEmpValid φ ( i, Φ i - Ψ i).
Proof.
rewrite /AsValid0 /AsValid /MakeMonPredAt. intros -> EQ1 EQ2.
rewrite /AsEmpValid0 /AsEmpValid /MakeMonPredAt. intros -> EQ1 EQ2.
setoid_rewrite <-EQ1. setoid_rewrite <-EQ2. split.
- move=>/bi.wand_entails HP. setoid_rewrite HP. by iIntros (i) "$".
- move=>HP. apply bi.entails_wand. split=>i. iIntros "H". by iApply HP.
Qed.
Global Instance as_valid_monPred_at_equiv φ P Q (Φ Ψ : I PROP) :
AsValid0 φ (P - Q)
Global Instance as_emp_valid_monPred_at_equiv φ P Q (Φ Ψ : I PROP) :
AsEmpValid0 φ (P - Q)
( i, MakeMonPredAt i P (Φ i)) ( i, MakeMonPredAt i Q (Ψ i))
AsValid φ ( i, Φ i - Ψ i).
AsEmpValid φ ( i, Φ i - Ψ i).
Proof.
rewrite /AsValid0 /AsValid /MakeMonPredAt. intros -> EQ1 EQ2.
rewrite /AsEmpValid0 /AsEmpValid /MakeMonPredAt. intros -> EQ1 EQ2.
setoid_rewrite <-EQ1. setoid_rewrite <-EQ2. split.
- move=>/bi.wand_iff_equiv HP. setoid_rewrite HP. iIntros. iSplit; iIntros "$".
- move=>HP. apply bi.equiv_wand_iff. split=>i. by iSplit; iIntros; iApply HP.
......
......@@ -63,7 +63,7 @@ Tactic Notation "iMatchHyp" tactic1(tac) :=
Tactic Notation "iStartProof" :=
lazymatch goal with
| |- envs_entails _ _ => idtac
| |- ?φ => notypeclasses refine (as_valid_2 φ _ _);
| |- ?φ => notypeclasses refine (as_emp_valid_2 φ _ _);
[apply _ || fail "iStartProof: not a Bi entailment"
|apply tac_adequate]
end.
......@@ -79,12 +79,12 @@ Tactic Notation "iStartProof" uconstr(PROP) :=
type_term has a non-negligeable performance impact. *)
let x := type_term (eq_refl : @eq Type PROP PROP') in idtac
(* We eta-expand [as_valid_2], in order to make sure that
(* We eta-expand [as_emp_valid_2], in order to make sure that
[iStartProof PROP] works even if [PROP] is the carrier type. In
this case, typing this expression will end up unifying PROP with
[bi_car _], and hence trigger the canonical structures mechanism
to find the corresponding bi. *)
| |- ?φ => notypeclasses refine ((λ P : PROP, @as_valid_2 φ _ P) _ _ _);
| |- ?φ => notypeclasses refine ((λ P : PROP, @as_emp_valid_2 φ _ P) _ _ _);
[apply _ || fail "iStartProof: not a Bi entailment"
|apply tac_adequate]
end.
......@@ -684,13 +684,13 @@ Tactic Notation "iIntoValid" open_constr(t) :=
not necessarilly opaque, and could be unfolded by [hnf].
However, for calling type class search, we only use [cbv zeta]
in order to make sure we do not unfold [bi_valid]. *)
in order to make sure we do not unfold [bi_emp_valid]. *)
let tT := type of t in
first
[ let tT' := eval hnf in tT in go_specialize t tT'
| let tT' := eval cbv zeta in tT in go_specialize t tT'
| let tT' := eval cbv zeta in tT in
notypeclasses refine (as_valid_1 tT _ _);
notypeclasses refine (as_emp_valid_1 tT _ _);
[iSolveTC || fail "iPoseProof: not a BI assertion"
|exact t]]
with go_specialize t tT :=
......
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