Commit 065bfdfc authored by Robbert Krebbers's avatar Robbert Krebbers

Rename absolutely → objectively and relatively → subjectively.

sed -i 's/absolute/objective/g; s/relative/subjective/g; s/Absolute/Objective/g; s/Relative/Subjective/g' $(find ./ -name \*.v)
parent 352292a8
......@@ -117,7 +117,7 @@ Modalities
- `iModIntro mod` : introduction of a modality. The type class `FromModal` is
used to specify which modalities this tactic should introduce. Instances of
that type class include: later, except 0, basic update and fancy update,
persistently, affinely, plainly, absorbingly, absolutely, and relatively.
persistently, affinely, plainly, absorbingly, objectively, and subjectively.
The optional argument `mod` can be used to specify what modality to introduce
in case of ambiguity, e.g. `⎡|==> P⎤`.
- `iAlways` : a deprecated alias of `iModIntro`.
......
......@@ -233,6 +233,6 @@ End sbi_embed.
(* Not defined using an ordinary [Instance] because the default
[class_apply @bi_embed_plainly] shelves the [BiPlainly] premise, making proof
search for the other premises fail. See the proof of [monPred_absolutely_plain]
search for the other premises fail. See the proof of [monPred_objectively_plain]
for an example where it would fail with a regular [Instance].*)
Hint Extern 4 (Plain _) => eapply @embed_plain : typeclass_instances.
This diff is collapsed.
......@@ -98,7 +98,7 @@ introduce, [sel] should be an evar.
For modalities [N] that do not need to augment the proof mode environment, one
can define an instance [FromModal modality_id (N P) P]. Defining such an
instance only imposes the proof obligation [P ⊢ N P]. Examples of such
modalities [N] are [bupd], [fupd], [except_0], [monPred_relatively] and
modalities [N] are [bupd], [fupd], [except_0], [monPred_subjectively] and
[bi_absorbingly]. *)
Class FromModal {PROP1 PROP2 : bi} {A}
(M : modality PROP1 PROP2) (sel : A) (P : PROP2) (Q : PROP1) :=
......
......@@ -154,7 +154,7 @@ End modality1.
[P ⊢ M P]. This is done by defining an instance [FromModal modality_id (M P) P],
which will instruct [iModIntro] to introduce the modality without modifying the
proof mode context. Examples of such modalities are [bupd], [fupd], [except_0],
[monPred_relatively] and [bi_absorbingly]. *)
[monPred_subjectively] and [bi_absorbingly]. *)
Lemma modality_id_mixin {PROP : bi} : modality_mixin (@id PROP) MIEnvId MIEnvId.
Proof. split; simpl; eauto. Qed.
Definition modality_id {PROP : bi} := Modality (@id PROP) modality_id_mixin.
......@@ -18,18 +18,18 @@ Hint Extern 1 (IsBiIndexRel _ _) => unfold IsBiIndexRel; assumption
Section modalities.
Context {I : biIndex} {PROP : bi}.
Lemma modality_absolutely_mixin :
modality_mixin (@monPred_absolutely I PROP)
(MIEnvFilter Absolute) (MIEnvFilter Absolute).
Lemma modality_objectively_mixin :
modality_mixin (@monPred_objectively I PROP)
(MIEnvFilter Objective) (MIEnvFilter Objective).
Proof.
split; simpl; split_and?; intros;
try match goal with H : TCDiag _ _ _ |- _ => destruct H end;
eauto using bi.equiv_entails_sym, absolute_absolutely,
monPred_absolutely_mono, monPred_absolutely_and,
monPred_absolutely_sep_2 with typeclass_instances.
eauto using bi.equiv_entails_sym, objective_objectively,
monPred_objectively_mono, monPred_objectively_and,
monPred_objectively_sep_2 with typeclass_instances.
Qed.
Definition modality_absolutely :=
Modality _ modality_absolutely_mixin.
Definition modality_objectively :=
Modality _ modality_objectively_mixin.
End modalities.
Section bi.
......@@ -42,12 +42,12 @@ Implicit Types 𝓟 𝓠 𝓡 : PROP.
Implicit Types φ : Prop.
Implicit Types i j : I.
Global Instance from_modal_absolutely P :
FromModal modality_absolutely ( P) ( P) P | 1.
Global Instance from_modal_objectively P :
FromModal modality_objectively ( P) ( P) P | 1.
Proof. by rewrite /FromModal. Qed.
Global Instance from_modal_relatively P :
Global Instance from_modal_subjectively P :
FromModal modality_id ( P) ( P) P | 1.
Proof. by rewrite /FromModal /= -monPred_relatively_intro. Qed.
Proof. by rewrite /FromModal /= -monPred_subjectively_intro. Qed.
Global Instance from_modal_affinely_monPred_at `(sel : A) P Q 𝓠 i :
FromModal modality_affinely sel P Q MakeMonPredAt i Q 𝓠
......@@ -135,12 +135,12 @@ Proof.
apply bi.affinely_persistently_if_elim.
Qed.
Global Instance from_assumption_make_monPred_absolutely P Q :
Global Instance from_assumption_make_monPred_objectively P Q :
FromAssumption p P Q FromAssumption p ( P) Q.
Proof. intros ?. by rewrite /FromAssumption monPred_absolutely_elim. Qed.
Global Instance from_assumption_make_monPred_relatively P Q :
Proof. intros ?. by rewrite /FromAssumption monPred_objectively_elim. Qed.
Global Instance from_assumption_make_monPred_subjectively P Q :
FromAssumption p P Q FromAssumption p P ( Q).
Proof. intros ?. by rewrite /FromAssumption -monPred_relatively_intro. Qed.
Proof. intros ?. by rewrite /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.
......@@ -292,26 +292,26 @@ Proof.
by rewrite monPred_at_exist.
Qed.
Global Instance from_forall_monPred_at_absolutely P (Φ : I PROP) i :
Global Instance from_forall_monPred_at_objectively P (Φ : I PROP) i :
( i, MakeMonPredAt i P (Φ i)) FromForall (( P) i)%I Φ.
Proof.
rewrite /FromForall /MakeMonPredAt monPred_at_absolutely=>H. by setoid_rewrite <- H.
rewrite /FromForall /MakeMonPredAt monPred_at_objectively=>H. by setoid_rewrite <- H.
Qed.
Global Instance into_forall_monPred_at_absolutely P (Φ : I PROP) i :
Global Instance into_forall_monPred_at_objectively P (Φ : I PROP) i :
( i, MakeMonPredAt i P (Φ i)) IntoForall (( P) i) Φ.
Proof.
rewrite /IntoForall /MakeMonPredAt monPred_at_absolutely=>H. by setoid_rewrite <- H.
rewrite /IntoForall /MakeMonPredAt monPred_at_objectively=>H. by setoid_rewrite <- H.
Qed.
Global Instance from_exist_monPred_at_ex P (Φ : I PROP) i :
( i, MakeMonPredAt i P (Φ i)) FromExist (( P) i) Φ.
Proof.
rewrite /FromExist /MakeMonPredAt monPred_at_relatively=>H. by setoid_rewrite <- H.
rewrite /FromExist /MakeMonPredAt monPred_at_subjectively=>H. by setoid_rewrite <- H.
Qed.
Global Instance into_exist_monPred_at_ex P (Φ : I PROP) i :
( i, MakeMonPredAt i P (Φ i)) IntoExist (( P) i) Φ.
Proof.
rewrite /IntoExist /MakeMonPredAt monPred_at_relatively=>H. by setoid_rewrite <- H.
rewrite /IntoExist /MakeMonPredAt monPred_at_subjectively=>H. by setoid_rewrite <- H.
Qed.
Global Instance from_forall_monPred_at {A} P (Φ : A monPred) (Ψ : A PROP) i :
......@@ -346,11 +346,11 @@ Proof.
?monPred_at_persistently monPred_at_embed.
Qed.
Global Instance into_embed_absolute P :
Absolute P IntoEmbed P ( i, P i).
Global Instance into_embed_objective P :
Objective P IntoEmbed P ( i, P i).
Proof.
rewrite /IntoEmbed=> ?.
by rewrite {1}(absolute_absolutely P) monPred_absolutely_unfold.
by rewrite {1}(objective_objectively P) monPred_objectively_unfold.
Qed.
Global Instance elim_modal_at_bupd_goal `{BiBUpd PROP} φ 𝓟 𝓟' Q Q' i :
......
......@@ -69,14 +69,14 @@ Section tests.
iIntros "H HP". by iApply "H".
Qed.
Lemma test_absolutely P Q : emp - P - Q - (P Q).
Lemma test_objectively P Q : emp - P - Q - (P Q).
Proof. iIntros "#? HP HQ". iAlways. by iSplitL "HP". Qed.
Lemma test_absolutely_absorbing P Q R `{!Absorbing P} :
Lemma test_objectively_absorbing P Q R `{!Absorbing P} :
emp - P - Q - R - (P Q).
Proof. iIntros "#? HP HQ HR". iAlways. by iSplitL "HP". Qed.
Lemma test_absolutely_affine P Q R `{!Affine R} :
Lemma test_objectively_affine P Q R `{!Affine R} :
emp - P - Q - R - (P Q).
Proof. iIntros "#? HP HQ HR". iAlways. by iSplitL "HP". Qed.
......@@ -84,7 +84,7 @@ Section tests.
P - Q - ⎡𝓟⎤ - ⎡𝓠⎤ - 𝓟 𝓠 .
Proof. iIntros "#H1 _ H2 H3". iAlways. iFrame. Qed.
Lemma test_iModIntro_embed_absolute P `{!Absolute Q} 𝓟 𝓠 :
Lemma test_iModIntro_embed_objective P `{!Objective Q} 𝓟 𝓠 :
P - Q - ⎡𝓟⎤ - ⎡𝓠⎤ - i, 𝓟 𝓠 Q i .
Proof. iIntros "#H1 H2 H3 H4". iAlways. iFrame. Qed.
......
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