Commit 0c89ae1c authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Rename `equiv_spec` → `equiv_entails` to be consistent with conventions in std++.

Hence, also rename (the old) `equiv_entails` → `equiv_entails_1_1` and
`equiv_entails_sym` → `equiv_entails_1_2`, and add `equiv_entails_2` for completeness.
parent d4c1face
......@@ -101,6 +101,8 @@ HeapLang, which is now in a separate package `coq-iris-heap-lang`.
`big_sepS` lemmas.
* Add lemmas for big-ops of magic wands: `big_sepL_wand`, `big_sepL2_wand`,
`big_sepM_wand`, `big_sepM2_wand`, `big_sepS_wand`, `big_sepMS_wand`.
* Rename `equiv_entails``equiv_entails_1_1`,
`equiv_entails_sym``equiv_entails_1_2`, and `equiv_spec``equiv_entails`.
**Changes in `proofmode`:**
......@@ -267,6 +269,10 @@ s/\b(gmultiset_op)_disj_union\b/\1/g
s/\b(gmultiset_core)_empty\b/\1/g
s/\b(nat_op)_plus\b/\1/g
s/\b(max_nat_op)_max\b/\1/g
# equiv_spec
s/\bequiv_entails\b/equiv_entails_1_1/g
s/\bequiv_entails_sym\b/equiv_entails_1_2/g
s/\bequiv_spec\b/equiv_entails/g
EOF
```
......
......@@ -18,7 +18,7 @@ Lemma uPred_bi_mixin (M : ucmra) :
Proof.
split.
- exact: entails_po.
- exact: equiv_spec.
- exact: equiv_entails.
- exact: pure_ne.
- exact: and_ne.
- exact: or_ne.
......
......@@ -467,7 +467,7 @@ Proof.
Qed.
Lemma entails_anti_sym : AntiSymm () ().
Proof. intros P Q HPQ HQP; split=> x n; by split; [apply HPQ|apply HQP]. Qed.
Lemma equiv_spec P Q : (P Q) (P Q) (Q P).
Lemma equiv_entails P Q : (P Q) (P Q) (Q P).
Proof.
split.
- intros HPQ; split; split=> x i; apply HPQ.
......
......@@ -499,7 +499,7 @@ Section sep_list2.
([ list] k y1;y2 l1;l2, Φ k y1 y2) [ list] k y1;y2 l1;l2, Ψ k y1 y2.
Proof.
intros; apply (anti_symm _);
apply big_sepL2_mono; auto using equiv_entails, equiv_entails_sym.
apply big_sepL2_mono; auto using equiv_entails_1_1, equiv_entails_1_2.
Qed.
Lemma big_sepL2_proper_2 `{!Equiv A, !Equiv B} Φ Ψ l1 l2 l1' l2' :
l1 l1' l2 l2'
......@@ -1375,7 +1375,7 @@ Section map2.
([ map] k y1;y2 m1;m2, Φ k y1 y2) [ map] k y1;y2 m1;m2, Ψ k y1 y2.
Proof.
intros; apply (anti_symm _);
apply big_sepM2_mono; auto using equiv_entails, equiv_entails_sym.
apply big_sepM2_mono; auto using equiv_entails_1_1, equiv_entails_1_2.
Qed.
Lemma big_sepM2_proper_2 `{!Equiv A, !Equiv B} Φ Ψ m1 m2 m1' m2' :
m1 m1' m2 m2'
......
......@@ -29,15 +29,18 @@ Notation "P ⊣⊢ Q" := (P ⊣⊢@{PROP} Q).
(* Derived stuff about the entailment *)
Global Instance entails_anti_sym : AntiSymm () (@bi_entails PROP).
Proof. intros P Q ??. by apply equiv_spec. Qed.
Lemma equiv_entails P Q : (P Q) (P Q).
Proof. apply equiv_spec. Qed.
Lemma equiv_entails_sym P Q : (Q P) (P Q).
Proof. apply equiv_spec. Qed.
Proof. intros P Q ??. by apply equiv_entails. Qed.
Lemma equiv_entails_1_1 P Q : (P Q) (P Q).
Proof. apply equiv_entails. Qed.
Lemma equiv_entails_1_2 P Q : (P Q) (Q P).
Proof. apply equiv_entails. Qed.
Lemma equiv_entails_2 P Q : (P Q) (Q P) (P Q).
Proof. intros. by apply equiv_entails. Qed.
Global Instance entails_proper :
Proper (() ==> () ==> iff) (() : relation PROP).
Proof.
move => P1 P2 /equiv_spec [HP1 HP2] Q1 Q2 /equiv_spec [HQ1 HQ2]; split=>?.
move => P1 P2 /equiv_entails [HP1 HP2] Q1 Q2 /equiv_entails [HQ1 HQ2]; split=>?.
- by trans P1; [|trans Q1].
- by trans P2; [|trans Q2].
Qed.
......@@ -119,14 +122,14 @@ Local Hint Immediate False_elim : core.
Lemma entails_eq_True P Q : (P Q) ((P Q)%I True%I).
Proof.
split=>EQ.
- apply bi.equiv_spec; split; [by apply True_intro|].
- apply bi.equiv_entails; split; [by apply True_intro|].
apply impl_intro_r. rewrite and_elim_r //.
- trans (P True)%I.
+ apply and_intro; first done. by apply pure_intro.
+ rewrite -EQ impl_elim_r. done.
Qed.
Lemma entails_impl_True P Q : (P Q) (True (P Q)).
Proof. rewrite entails_eq_True equiv_spec; naive_solver. Qed.
Proof. rewrite entails_eq_True equiv_entails; naive_solver. Qed.
Lemma and_mono P P' Q Q' : (P Q) (P' Q') P P' Q Q'.
Proof. auto. Qed.
......@@ -229,7 +232,7 @@ Qed.
Lemma exist_impl_forall {A} P (Ψ : A PROP) :
(( x : A, Ψ x) P) x : A, Ψ x P.
Proof.
apply equiv_spec; split.
apply equiv_entails; split.
- apply forall_intro=>x. by rewrite -exist_intro.
- apply impl_intro_r, impl_elim_r', exist_elim=>x.
apply impl_intro_r. by rewrite (forall_elim x) impl_elim_r.
......@@ -457,7 +460,7 @@ Proof. by apply forall_intro=> a; rewrite forall_elim. Qed.
Lemma exist_wand_forall {A} P (Ψ : A PROP) :
(( x : A, Ψ x) - P) x : A, Ψ x - P.
Proof.
apply equiv_spec; split.
apply equiv_entails; split.
- apply forall_intro=>x. by rewrite -exist_intro.
- apply wand_intro_r, wand_elim_r', exist_elim=>x.
apply wand_intro_r. by rewrite (forall_elim x) wand_elim_r.
......@@ -1598,7 +1601,7 @@ Lemma limit_preserving_equiv {A : ofe} `{Cofe A} (Φ Ψ : A → PROP) :
NonExpansive Φ NonExpansive Ψ LimitPreserving (λ x, Φ x Ψ x).
Proof.
intros HΦ HΨ. eapply limit_preserving_ext.
{ intros x. symmetry; apply equiv_spec. }
{ intros x. symmetry; apply equiv_entails. }
apply limit_preserving_and; by apply limit_preserving_entails.
Qed.
Global Instance limit_preserving_Persistent {A:ofe} `{Cofe A} (Φ : A PROP) :
......
......@@ -134,7 +134,7 @@ Section embed.
Global Instance embed_inj : Inj () () embed.
Proof.
intros P Q EQ. apply bi.equiv_spec, conj; apply (inj embed); rewrite EQ //.
intros P Q EQ. apply bi.equiv_entails, conj; apply (inj embed); rewrite EQ //.
Qed.
Lemma embed_emp_valid (P : PROP1) : ( P) ( P).
......@@ -149,12 +149,12 @@ Section embed.
Lemma embed_forall A (Φ : A PROP1) : x, Φ x x, ⎡Φ x.
Proof.
apply bi.equiv_spec; split; [|apply embed_forall_2].
apply bi.equiv_entails; split; [|apply embed_forall_2].
apply bi.forall_intro=>?. by rewrite bi.forall_elim.
Qed.
Lemma embed_exist A (Φ : A PROP1) : x, Φ x x, ⎡Φ x.
Proof.
apply bi.equiv_spec; split; [apply embed_exist_1|].
apply bi.equiv_entails; split; [apply embed_exist_1|].
apply bi.exist_elim=>?. by rewrite -bi.exist_intro.
Qed.
Lemma embed_and P Q : P Q P Q.
......@@ -163,18 +163,18 @@ Section embed.
Proof. rewrite !bi.or_alt embed_exist. by f_equiv=>-[]. Qed.
Lemma embed_impl P Q : P Q (P Q).
Proof.
apply bi.equiv_spec; split; [|apply embed_impl_2].
apply bi.equiv_entails; split; [|apply embed_impl_2].
apply bi.impl_intro_l. by rewrite -embed_and bi.impl_elim_r.
Qed.
Lemma embed_wand P Q : P - Q (P - Q).
Proof.
apply bi.equiv_spec; split; [|apply embed_wand_2].
apply bi.equiv_entails; split; [|apply embed_wand_2].
apply bi.wand_intro_l. by rewrite -embed_sep bi.wand_elim_r.
Qed.
Lemma embed_pure φ : ⎡⌜φ⌝⎤ ⌜φ⌝.
Proof.
rewrite (@bi.pure_alt PROP1) (@bi.pure_alt PROP2) embed_exist.
do 2 f_equiv. apply bi.equiv_spec. split; [apply bi.True_intro|].
do 2 f_equiv. apply bi.equiv_entails. split; [apply bi.True_intro|].
rewrite -(_ : (emp emp : PROP1) True) ?embed_impl;
last apply bi.True_intro.
apply bi.impl_intro_l. by rewrite right_id.
......@@ -293,7 +293,7 @@ Section embed.
Lemma embed_internal_eq (A : ofe) (x y : A) : x y @{PROP2} x y.
Proof.
apply bi.equiv_spec; split; [apply embed_internal_eq_1|].
apply bi.equiv_entails; split; [apply embed_internal_eq_1|].
etrans; [apply (internal_eq_rewrite x y (λ y, x y%I)); solve_proper|].
rewrite -(internal_eq_refl True%I) embed_pure.
eapply bi.impl_elim; [done|]. apply bi.True_intro.
......
......@@ -47,7 +47,7 @@ Section bi_mixin.
Record BiMixin := {
bi_mixin_entails_po : PreOrder bi_entails;
bi_mixin_equiv_spec P Q : (P Q) (P Q) (Q P);
bi_mixin_equiv_entails P Q : (P Q) (P Q) (Q P);
(** Non-expansiveness *)
bi_mixin_pure_ne n : Proper (iff ==> dist n) bi_pure;
......@@ -278,8 +278,8 @@ Implicit Types A : Type.
(* About the entailment *)
Global Instance entails_po : PreOrder (@bi_entails PROP).
Proof. eapply bi_mixin_entails_po, bi_bi_mixin. Qed.
Lemma equiv_spec P Q : P Q (P Q) (Q P).
Proof. eapply bi_mixin_equiv_spec, bi_bi_mixin. Qed.
Lemma equiv_entails P Q : P Q (P Q) (Q P).
Proof. eapply bi_mixin_equiv_entails, bi_bi_mixin. Qed.
(* Non-expansiveness *)
Global Instance pure_ne n : Proper (iff ==> dist n) (@bi_pure PROP).
......
......@@ -169,7 +169,7 @@ Module inv. Section inv.
Proof. intros P Q ?. by apply fupd_mono. Qed.
Global Instance fupd_proper E : Proper (() ==> ()) (fupd E).
Proof.
intros P Q; rewrite !bi.equiv_spec=> -[??]; split; by apply fupd_mono.
intros P Q; rewrite !bi.equiv_entails=> -[??]; split; by apply fupd_mono.
Qed.
Lemma fupd_frame_r E P Q : fupd E P Q fupd E (P Q).
......@@ -307,7 +307,7 @@ Module linear. Section linear.
Proof. intros P Q ?. by apply fupd_mono. Qed.
Global Instance fupd_proper E1 E2 : Proper (() ==> ()) (fupd E1 E2).
Proof.
intros P Q; rewrite !bi.equiv_spec=> -[??]; split; by apply fupd_mono.
intros P Q; rewrite !bi.equiv_entails=> -[??]; split; by apply fupd_mono.
Qed.
Lemma fupd_frame_r E1 E2 P Q : fupd E1 E2 P Q fupd E1 E2 (P Q).
......
......@@ -98,7 +98,7 @@ Global Instance monPred_at_ne (R : relation I) :
n, Proper (dist n ==> R ==> dist n) monPred_at.
Proof.
intros ????? [Hd] ?? HR. rewrite Hd.
apply equiv_dist, bi.equiv_spec; split; f_equiv; rewrite ->HR; done.
apply equiv_dist, bi.equiv_entails; split; f_equiv; rewrite ->HR; done.
Qed.
Global Instance monPred_at_proper (R : relation I) :
Proper (R ==> R ==> iff) () Reflexive R
......@@ -255,8 +255,8 @@ Proof.
+ intros P. by split.
+ intros P Q R [H1] [H2]. split => ?. by rewrite H1 H2.
- split.
+ intros [HPQ]. split; split => i; move: (HPQ i); by apply bi.equiv_spec.
+ intros [[] []]. split=>i. by apply bi.equiv_spec.
+ intros [HPQ]. split; split => i; move: (HPQ i); by apply bi.equiv_entails.
+ intros [[] []]. split=>i. by apply bi.equiv_entails.
- intros P φ ?. split=> i. by apply bi.pure_intro.
- intros φ P HP. split=> i. apply bi.pure_elim'=> ?. by apply HP.
- intros P Q. split=> i. by apply bi.and_elim_l.
......@@ -508,18 +508,18 @@ Lemma monPred_objectively_elim P : <obj> P ⊢ P.
Proof. rewrite monPred_objectively_unfold. unseal. split=>?. apply bi.forall_elim. Qed.
Lemma monPred_objectively_idemp P : <obj> <obj> P <obj> P.
Proof.
apply bi.equiv_spec; split; [by apply monPred_objectively_elim|].
apply bi.equiv_entails; split; [by apply monPred_objectively_elim|].
unseal. split=>i /=. by apply bi.forall_intro=>_.
Qed.
Lemma monPred_objectively_forall {A} (Φ : A monPred) : <obj> ( x, Φ x) x, <obj> (Φ x).
Proof.
unseal. split=>i. apply bi.equiv_spec; split=>/=;
unseal. split=>i. apply bi.equiv_entails; split=>/=;
do 2 apply bi.forall_intro=>?; by do 2 rewrite bi.forall_elim.
Qed.
Lemma monPred_objectively_and P Q : <obj> (P Q) <obj> P <obj> Q.
Proof.
unseal. split=>i. apply bi.equiv_spec; split=>/=.
unseal. split=>i. apply bi.equiv_entails; split=>/=.
- apply bi.and_intro; do 2 f_equiv.
+ apply bi.and_elim_l.
+ apply bi.and_elim_r.
......@@ -539,12 +539,12 @@ Lemma monPred_objectively_sep_2 P Q : <obj> P ∗ <obj> Q ⊢ <obj> (P ∗ Q).
Proof. unseal. split=>i /=. apply bi.forall_intro=>?. by rewrite !bi.forall_elim. Qed.
Lemma monPred_objectively_sep `{BiIndexBottom bot} P Q : <obj> (P Q) <obj> P <obj> Q.
Proof.
apply bi.equiv_spec, conj, monPred_objectively_sep_2. unseal. split=>i /=.
apply bi.equiv_entails, conj, monPred_objectively_sep_2. unseal. split=>i /=.
rewrite (bi.forall_elim bot). by f_equiv; apply bi.forall_intro=>j; f_equiv.
Qed.
Lemma monPred_objectively_embed (P : PROP) : <obj> P P.
Proof.
apply bi.equiv_spec; split; unseal; split=>i /=.
apply bi.equiv_entails; split; unseal; split=>i /=.
- by rewrite (bi.forall_elim inhabitant).
- by apply bi.forall_intro.
Qed.
......@@ -567,12 +567,12 @@ Proof.
Qed.
Lemma monPred_subjectively_exist {A} (Φ : A monPred) : <subj> ( x, Φ x) x, <subj> (Φ x).
Proof.
unseal. split=>i. apply bi.equiv_spec; split=>/=;
unseal. split=>i. apply bi.equiv_entails; split=>/=;
do 2 apply bi.exist_elim=>?; by do 2 rewrite -bi.exist_intro.
Qed.
Lemma monPred_subjectively_or P Q : <subj> (P Q) <subj> P <subj> Q.
Proof.
unseal. split=>i. apply bi.equiv_spec; split=>/=.
unseal. split=>i. apply bi.equiv_entails; split=>/=.
- apply bi.exist_elim=>?. by rewrite -!bi.exist_intro.
- apply bi.or_elim; do 2 f_equiv.
+ apply bi.or_intro_l.
......@@ -584,7 +584,7 @@ Proof. unseal. split=>i /=. apply bi.exist_elim=>?. by rewrite -!bi.exist_intro.
Lemma monPred_subjectively_idemp P : <subj> <subj> P <subj> P.
Proof.
apply bi.equiv_spec; split; [|by apply monPred_subjectively_intro].
apply bi.equiv_entails; split; [|by apply monPred_subjectively_intro].
unseal. split=>i /=. by apply bi.exist_elim=>_.
Qed.
......@@ -869,7 +869,7 @@ Proof. rewrite monPred_internal_eq_unfold. by apply monPred_at_embed. Qed.
Lemma monPred_equivI `{!BiInternalEq PROP'} P Q :
P Q @{PROP'} i, P i Q i.
Proof.
apply bi.equiv_spec. split.
apply bi.equiv_entails. split.
- apply bi.forall_intro=> ?. apply (f_equivI (flip monPred_at _)).
- by rewrite -{2}(sig_monPred_sig P) -{2}(sig_monPred_sig Q)
-f_equivI -sig_equivI !discrete_fun_equivI.
......
......@@ -439,7 +439,7 @@ Global Instance of_envs_proper' :
Proper (env_Forall2 () ==> env_Forall2 () ==> ()) (@of_envs' PROP).
Proof.
intros Γp1 Γp2 Hp Γs1 Γs2 Hs; apply (anti_symm ()); apply of_envs_mono';
eapply (env_Forall2_impl ()); by eauto using equiv_entails.
eapply (env_Forall2_impl ()); by eauto using equiv_entails_1_1.
Qed.
Global Instance of_envs_mono : Proper (envs_Forall2 () ==> ()) (@of_envs PROP).
......
......@@ -136,7 +136,7 @@ Section modality.
Global Instance modality_flip_mono' : Proper (flip () ==> flip ()) M.
Proof. intros P Q. apply modality_mono. Qed.
Global Instance modality_proper : Proper (() ==> ()) M.
Proof. intros P Q. rewrite !equiv_spec=> -[??]; eauto using modality_mono. Qed.
Proof. intros P Q. rewrite !equiv_entails=> -[??]; eauto using modality_mono. Qed.
End modality.
Section modality1.
......
......@@ -9,7 +9,7 @@ Section modalities.
Lemma modality_persistently_mixin :
modality_mixin (@bi_persistently PROP) MIEnvId MIEnvClear.
Proof.
split; simpl; eauto using equiv_entails_sym, persistently_intro,
split; simpl; eauto using equiv_entails_1_2, persistently_intro,
persistently_mono, persistently_sep_2 with typeclass_instances.
Qed.
Definition modality_persistently :=
......@@ -18,7 +18,7 @@ Section modalities.
Lemma modality_affinely_mixin :
modality_mixin (@bi_affinely PROP) MIEnvId (MIEnvForall Affine).
Proof.
split; simpl; eauto using equiv_entails_sym, affinely_intro, affinely_mono,
split; simpl; eauto using equiv_entails_1_2, affinely_intro, affinely_mono,
affinely_sep_2 with typeclass_instances.
Qed.
Definition modality_affinely :=
......@@ -27,7 +27,7 @@ Section modalities.
Lemma modality_intuitionistically_mixin :
modality_mixin (@bi_intuitionistically PROP) MIEnvId MIEnvIsEmpty.
Proof.
split; simpl; eauto using equiv_entails_sym, intuitionistically_emp,
split; simpl; eauto using equiv_entails_1_2, intuitionistically_emp,
affinely_mono, persistently_mono, intuitionistically_idemp,
intuitionistically_sep_2 with typeclass_instances.
Qed.
......@@ -39,7 +39,7 @@ Section modalities.
(MIEnvTransform IntoEmbed) (MIEnvTransform IntoEmbed).
Proof.
split; simpl; split_and?;
eauto using equiv_entails_sym, embed_emp_2, embed_sep, embed_and.
eauto using equiv_entails_1_2, embed_emp_2, embed_sep, embed_and.
- intros P Q. rewrite /IntoEmbed=> ->. by rewrite embed_intuitionistically_2.
- by intros P Q ->.
Qed.
......@@ -49,7 +49,7 @@ Section modalities.
Lemma modality_plainly_mixin `{BiPlainly PROP} :
modality_mixin (@plainly PROP _) (MIEnvForall Plain) MIEnvClear.
Proof.
split; simpl; split_and?; eauto using equiv_entails_sym, plainly_intro,
split; simpl; split_and?; eauto using equiv_entails_1_2, plainly_intro,
plainly_mono, plainly_and, plainly_sep_2 with typeclass_instances.
Qed.
Definition modality_plainly `{BiPlainly PROP} :=
......@@ -59,7 +59,7 @@ Section modalities.
modality_mixin (@bi_laterN PROP n)
(MIEnvTransform (MaybeIntoLaterN false n)) (MIEnvTransform (MaybeIntoLaterN false n)).
Proof.
split; simpl; split_and?; eauto using equiv_entails_sym, laterN_intro,
split; simpl; split_and?; eauto using equiv_entails_1_2, laterN_intro,
laterN_mono, laterN_and, laterN_sep with typeclass_instances.
rewrite /MaybeIntoLaterN=> P Q ->. by rewrite laterN_intuitionistically_2.
Qed.
......
......@@ -36,7 +36,7 @@ Section modalities.
Proof.
split; simpl; split_and?; intros;
try select (TCDiag _ _ _) (fun H => destruct H);
eauto using bi.equiv_entails_sym, objective_objectively,
eauto using bi.equiv_entails_1_2, objective_objectively,
monPred_objectively_mono, monPred_objectively_and,
monPred_objectively_sep_2 with typeclass_instances.
Qed.
......
......@@ -25,7 +25,7 @@ Lemma siProp_bi_mixin :
Proof.
split.
- exact: entails_po.
- exact: equiv_spec.
- exact: equiv_entails.
- exact: pure_ne.
- exact: and_ne.
- exact: or_ne.
......
......@@ -155,7 +155,7 @@ Proof.
Qed.
Lemma entails_anti_symm : AntiSymm () siProp_entails.
Proof. intros P Q HPQ HQP; split=> n; by split; [apply HPQ|apply HQP]. Qed.
Lemma equiv_spec P Q : (P Q) (P Q) (Q P).
Lemma equiv_entails P Q : (P Q) (P Q) (Q P).
Proof.
split.
- intros HPQ; split; split=> i; apply HPQ.
......
Supports Markdown
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