Commit 53ec94ec authored by Ralf Jung's avatar Ralf Jung
Browse files

Merge branch 'ralf/persistently-forall' into 'master'

move persistently_forall_2 out of BI interface

See merge request iris/iris!702
parents dd9a044e 049ac8e3
......@@ -6,11 +6,22 @@ lemma.
## Iris master
**Changes in `bi`:**
* Rename `least_fixpoint_ind` into `least_fixpoint_iter`,
rename `greatest_fixpoint_coind` into `greatest_fixpoint_coiter`,
rename `least_fixpoint_strong_ind` into `least_fixpoint_ind`,
add lemmas `least_fixpoint_{ind_wf, ne', strong_mono}`, and
add lemmas `greatest_fixpoint_{coind, paco, ne', strong_mono}`.
* Move `persistently_forall_2` (`∀ <pers> ⊢ <pers> ∀`) out of the BI interface
into a new typeclass, `BiPersistentlyForall`. The BI interface instead just
demands the equivalent property for conjunction (`(<pers> P) ∧ (<pers> Q) ⊢
<pers> (P ∧ Q)`). This enables the IPM to support logics where the
persistently modality is defined with an existential quantifier. This also
necessitates removing `persistently_impl_plainly` from `BiPlainly` into a new
typeclass `BiPersistentlyImplPlainly`.
Proofs that are generic in `PROP` might have to add those new classes as
assumptions to remain compatible, and code that instantiates the BI interface
needs to provide instances for the new classes.
The following `sed` script helps adjust your code to the renaming (on macOS,
replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`).
......
......@@ -53,10 +53,19 @@ Proof.
- exact: persistently_idemp_2.
- (* emp ⊢ <pers> emp (ADMISSIBLE) *)
trans (uPred_forall (M:=M) (λ _ : False, uPred_persistently uPred_emp)).
+ apply forall_intro=>[[]].
+ apply forall_intro=>-[].
+ etrans; first exact: persistently_forall_2.
apply persistently_mono. exact: pure_intro.
- exact: @persistently_forall_2.
- (* ((<pers> P) ∧ (<pers> Q)) ⊢ <pers> (P ∧ Q) (ADMISSIBLE) *)
intros P Q.
trans (uPred_forall (M:=M) (λ b : bool, uPred_persistently (if b then P else Q))).
+ apply forall_intro=>[[]].
* apply and_elim_l.
* apply and_elim_r.
+ etrans; first exact: persistently_forall_2.
apply persistently_mono. apply and_intro.
* etrans; first apply (forall_elim true). done.
* etrans; first apply (forall_elim false). done.
- exact: @persistently_exist_1.
- (* <pers> P ∗ Q ⊢ <pers> P (ADMISSIBLE) *)
intros. etrans; first exact: sep_comm'.
......@@ -89,12 +98,6 @@ Canonical Structure uPredI (M : ucmra) : bi :=
bi_bi_mixin := uPred_bi_mixin M;
bi_bi_later_mixin := uPred_bi_later_mixin M |}.
Global Instance uPred_pure_forall M : BiPureForall (uPredI M).
Proof. exact: @pure_forall_2. Qed.
Global Instance uPred_later_contractive {M} : BiLaterContractive (uPredI M).
Proof. apply later_contractive. Qed.
Lemma uPred_internal_eq_mixin M : BiInternalEqMixin (uPredI M) (@uPred_internal_eq M).
Proof.
split.
......@@ -118,7 +121,6 @@ Proof.
- exact: plainly_elim_persistently.
- exact: plainly_idemp_2.
- exact: @plainly_forall_2.
- exact: persistently_impl_plainly.
- exact: plainly_impl_plainly.
- (* P ⊢ ■ emp (ADMISSIBLE) *)
intros P.
......@@ -137,9 +139,6 @@ Qed.
Global Instance uPred_plainly M : BiPlainly (uPredI M) :=
{| bi_plainly_mixin := uPred_plainly_mixin M |}.
Global Instance uPred_prop_ext M : BiPropExt (uPredI M).
Proof. exact: prop_ext_2. Qed.
Lemma uPred_bupd_mixin M : BiBUpdMixin (uPredI M) uPred_bupd.
Proof.
split.
......@@ -151,9 +150,6 @@ Proof.
Qed.
Global Instance uPred_bi_bupd M : BiBUpd (uPredI M) := {| bi_bupd_mixin := uPred_bupd_mixin M |}.
Global Instance uPred_bi_bupd_plainly M : BiBUpdPlainly (uPredI M).
Proof. exact: bupd_plainly. Qed.
(** extra BI instances *)
Global Instance uPred_affine M : BiAffine (uPredI M) | 0.
......@@ -162,9 +158,27 @@ Proof. intros P. exact: pure_intro. Qed.
many lemmas that have [BiAffine] as a premise. *)
Global Hint Immediate uPred_affine : core.
Global Instance uPred_persistently_forall M : BiPersistentlyForall (uPredI M).
Proof. exact: @persistently_forall_2. Qed.
Global Instance uPred_pure_forall M : BiPureForall (uPredI M).
Proof. exact: @pure_forall_2. Qed.
Global Instance uPred_later_contractive {M} : BiLaterContractive (uPredI M).
Proof. apply later_contractive. Qed.
Global Instance uPred_persistently_impl_plainly M : BiPersistentlyImplPlainly (uPredI M).
Proof. exact: persistently_impl_plainly. Qed.
Global Instance uPred_plainly_exist_1 M : BiPlainlyExist (uPredI M).
Proof. exact: @plainly_exist_1. Qed.
Global Instance uPred_prop_ext M : BiPropExt (uPredI M).
Proof. exact: prop_ext_2. Qed.
Global Instance uPred_bi_bupd_plainly M : BiBUpdPlainly (uPredI M).
Proof. exact: bupd_plainly. Qed.
(** Re-state/export lemmas about Iris-specific primitive connectives (own, valid) *)
Module uPred.
......
......@@ -249,8 +249,11 @@ Section sep_list.
intros HΦ. apply (anti_symm _).
{ apply forall_intro=> k; apply forall_intro=> x.
apply impl_intro_l, pure_elim_l=> ?; by apply: big_sepL_lookup. }
rewrite -big_sepL_intro. setoid_rewrite pure_impl_forall.
by rewrite intuitionistic_intuitionistically.
revert Φ HΦ. induction l as [|x l IH]=> Φ HΦ /=.
{ apply: affine. }
rewrite -persistent_and_sep_1. apply and_intro.
- rewrite (forall_elim 0) (forall_elim x) pure_True // True_impl. done.
- rewrite -IH. apply forall_intro => k. by rewrite (forall_elim (S k)).
Qed.
Lemma big_sepL_impl Φ Ψ l :
......@@ -725,13 +728,18 @@ Section sep_list2.
length l1 = length l2
( k x1 x2, l1 !! k = Some x1 l2 !! k = Some x2 Φ k x1 x2).
Proof.
intros. apply (anti_symm _).
- apply and_intro; [apply big_sepL2_length|].
intros HΦ. apply (anti_symm _).
{ apply and_intro; [apply big_sepL2_length|].
apply forall_intro=> k. apply forall_intro=> x1. apply forall_intro=> x2.
do 2 (apply impl_intro_l; apply pure_elim_l=> ?). by apply :big_sepL2_lookup.
- apply pure_elim_l=> ?. rewrite -big_sepL2_intro //.
repeat setoid_rewrite pure_impl_forall.
by rewrite intuitionistic_intuitionistically.
do 2 (apply impl_intro_l; apply pure_elim_l=> ?). by apply: big_sepL2_lookup. }
apply pure_elim_l=> Hlen.
revert l2 Φ HΦ Hlen. induction l1 as [|x1 l1 IH]=> -[|x2 l2] Φ HΦ Hlen; simplify_eq/=.
{ by apply (affine _). }
rewrite -persistent_and_sep_1. apply and_intro.
- rewrite (forall_elim 0) (forall_elim x1) (forall_elim x2).
by rewrite !pure_True // !True_impl.
- rewrite -IH //.
by apply forall_intro=> k; by rewrite (forall_elim (S k)).
Qed.
Lemma big_sepL2_impl Φ Ψ l1 l2 :
......@@ -1453,11 +1461,18 @@ Section sep_map.
( k x, Persistent (Φ k x))
([ map] kx m, Φ k x) ( k x, m !! k = Some x Φ k x).
Proof.
intros. apply (anti_symm _).
intros HΦ. apply (anti_symm _).
{ apply forall_intro=> k; apply forall_intro=> x.
apply impl_intro_l, pure_elim_l=> ?; by apply: big_sepM_lookup. }
rewrite -big_sepM_intro. setoid_rewrite pure_impl_forall.
by rewrite intuitionistic_intuitionistically.
revert Φ HΦ. induction m as [|i x m ? IH] using map_ind=> Φ HΦ.
{ rewrite big_sepM_empty. apply: affine. }
rewrite big_sepM_insert // -persistent_and_sep_1. apply and_intro.
- rewrite (forall_elim i) (forall_elim x) lookup_insert.
by rewrite pure_True // True_impl.
- rewrite -IH. apply forall_mono=> k; apply forall_mono=> y.
apply impl_intro_l, pure_elim_l=> ?.
rewrite lookup_insert_ne; last by intros ?; simplify_map_eq.
by rewrite pure_True // True_impl.
Qed.
Lemma big_sepM_impl Φ Ψ m :
......@@ -2211,12 +2226,16 @@ Section map2.
( k x1 x2, m1 !! k = Some x1 m2 !! k = Some x2 Φ k x1 x2).
Proof.
intros. apply (anti_symm _).
- apply and_intro; [apply big_sepM2_lookup_iff|].
{ apply and_intro; [apply big_sepM2_lookup_iff|].
apply forall_intro=> k. apply forall_intro=> x1. apply forall_intro=> x2.
do 2 (apply impl_intro_l; apply pure_elim_l=> ?). by apply :big_sepM2_lookup.
- apply pure_elim_l=> ?. rewrite -big_sepM2_intro //.
repeat setoid_rewrite pure_impl_forall.
by rewrite intuitionistic_intuitionistically.
do 2 (apply impl_intro_l; apply pure_elim_l=> ?). by apply: big_sepM2_lookup. }
apply pure_elim_l=> Hdom. rewrite big_sepM2_eq /big_sepM2_def.
apply and_intro; [by apply pure_intro|].
rewrite big_sepM_forall. f_equiv=> k.
apply forall_intro=> -[x1 x2]. rewrite (forall_elim x1) (forall_elim x2).
apply impl_intro_l, pure_elim_l.
intros (?&?&[= <- <-]&?&?)%map_lookup_zip_with_Some.
by rewrite !pure_True // !True_impl.
Qed.
Lemma big_sepM2_impl Φ Ψ m1 m2 :
......@@ -2600,13 +2619,19 @@ Section gset.
Qed.
Lemma big_sepS_forall `{BiAffine PROP} Φ X :
( x, Persistent (Φ x)) ([ set] x X, Φ x) ( x, x X Φ x).
( x, Persistent (Φ x))
([ set] x X, Φ x) ( x, x X Φ x).
Proof.
intros. apply (anti_symm _).
intros HΦ. apply (anti_symm _).
{ apply forall_intro=> x.
apply impl_intro_l, pure_elim_l=> ?; by apply: big_sepS_elem_of. }
rewrite -big_sepS_intro. setoid_rewrite pure_impl_forall.
by rewrite intuitionistic_intuitionistically.
revert Φ HΦ. induction X as [|x X ? IH] using set_ind_L=> Φ HΦ.
{ rewrite big_sepS_empty. apply: affine. }
rewrite big_sepS_insert // -persistent_and_sep_1. apply and_intro.
- rewrite (forall_elim x) pure_True ?True_impl; last set_solver. done.
- rewrite -IH. apply forall_mono=> y.
apply impl_intro_l, pure_elim_l=> ?.
by rewrite pure_True ?True_impl; last set_solver.
Qed.
Lemma big_sepS_impl Φ Ψ X :
......@@ -2839,13 +2864,20 @@ Section gmultiset.
Qed.
Lemma big_sepMS_forall `{BiAffine PROP} Φ X :
( x, Persistent (Φ x)) ([ mset] x X, Φ x) ( x, x X Φ x).
( x, Persistent (Φ x))
([ mset] x X, Φ x) ( x, x X Φ x).
Proof.
intros. apply (anti_symm _).
intros HΦ. apply (anti_symm _).
{ apply forall_intro=> x.
apply impl_intro_l, pure_elim_l=> ?; by apply: big_sepMS_elem_of. }
rewrite -big_sepMS_intro. setoid_rewrite pure_impl_forall.
by rewrite intuitionistic_intuitionistically.
revert Φ HΦ. induction X as [|x X IH] using gmultiset_ind=> Φ HΦ.
{ rewrite big_sepMS_empty. apply: affine. }
rewrite big_sepMS_disj_union.
rewrite big_sepMS_singleton -persistent_and_sep_1. apply and_intro.
- rewrite (forall_elim x) pure_True ?True_impl; last multiset_solver. done.
- rewrite -IH. apply forall_mono=> y.
apply impl_intro_l, pure_elim_l=> ?.
by rewrite pure_True ?True_impl; last multiset_solver.
Qed.
Lemma big_sepMS_impl Φ Ψ X :
......
......@@ -846,20 +846,20 @@ Proof.
by rewrite /bi_absorbingly comm persistently_absorbing.
Qed.
Lemma persistently_forall {A} (Ψ : A PROP) :
Lemma persistently_forall_1 {A} (Ψ : A PROP) :
<pers> ( a, Ψ a) a, <pers> (Ψ a).
Proof. apply forall_intro=> x. by rewrite (forall_elim x). Qed.
Lemma persistently_forall `{!BiPersistentlyForall PROP} {A} (Ψ : A PROP) :
<pers> ( a, Ψ a) a, <pers> (Ψ a).
Proof.
apply (anti_symm _); auto using persistently_forall_2.
apply forall_intro=> x. by rewrite (forall_elim x).
Qed.
Proof. apply (anti_symm _); auto using persistently_forall_1, persistently_forall_2. Qed.
Lemma persistently_exist {A} (Ψ : A PROP) :
<pers> ( a, Ψ a) a, <pers> (Ψ a).
Proof.
apply (anti_symm _); auto using persistently_exist_1.
apply (anti_symm _); first by auto using persistently_exist_1.
apply exist_elim=> x. by rewrite (exist_intro x).
Qed.
Lemma persistently_and P Q : <pers> (P Q) <pers> P <pers> Q.
Proof. rewrite !and_alt persistently_forall. by apply forall_proper=> -[]. Qed.
Proof. apply (anti_symm _); by auto using persistently_and_2. Qed.
Lemma persistently_or P Q : <pers> (P Q) <pers> P <pers> Q.
Proof. rewrite !or_alt persistently_exist. by apply exist_proper=> -[]. Qed.
Lemma persistently_impl P Q : <pers> (P Q) <pers> P <pers> Q.
......@@ -875,6 +875,8 @@ Qed.
Lemma persistently_True_emp : <pers> True <pers> emp.
Proof. apply (anti_symm _); auto using persistently_emp_intro. Qed.
Lemma persistently_True : True <pers> True.
Proof. rewrite persistently_True_emp. apply persistently_emp_intro. Qed.
Lemma persistently_and_emp P : <pers> P <pers> (emp P).
Proof.
......@@ -922,9 +924,8 @@ Lemma persistently_pure φ : <pers> ⌜φ⌝ ⊣⊢ ⌜φ⌝.
Proof.
apply (anti_symm _).
{ by rewrite persistently_into_absorbingly absorbingly_pure. }
apply pure_elim'=> Hφ.
trans ( x : False, <pers> True : PROP)%I; [by apply forall_intro|].
rewrite persistently_forall_2. auto using persistently_mono, pure_intro.
apply pure_elim'=> Hφ. rewrite persistently_True.
auto using persistently_mono, pure_intro.
Qed.
Lemma persistently_sep_dup P : <pers> P <pers> P <pers> P.
......@@ -1083,7 +1084,7 @@ Qed.
Lemma intuitionistically_and P Q : (P Q) P Q.
Proof. by rewrite /bi_intuitionistically persistently_and affinely_and. Qed.
Lemma intuitionistically_forall {A} (Φ : A PROP) : ( x, Φ x) x, Φ x.
Proof. by rewrite /bi_intuitionistically persistently_forall affinely_forall. Qed.
Proof. by rewrite /bi_intuitionistically persistently_forall_1 affinely_forall. Qed.
Lemma intuitionistically_or P Q : (P Q) P Q.
Proof. by rewrite /bi_intuitionistically persistently_or affinely_or. Qed.
Lemma intuitionistically_exist {A} (Φ : A PROP) : ( x, Φ x) x, Φ x.
......@@ -1547,7 +1548,7 @@ Proof. intros. by rewrite /Persistent persistently_and -!persistent. Qed.
Global Instance or_persistent P Q :
Persistent P Persistent Q Persistent (P Q).
Proof. intros. by rewrite /Persistent persistently_or -!persistent. Qed.
Global Instance forall_persistent {A} (Ψ : A PROP) :
Global Instance forall_persistent `{!BiPersistentlyForall PROP} {A} (Ψ : A PROP) :
( x, Persistent (Ψ x)) Persistent ( x, Ψ x).
Proof.
intros. rewrite /Persistent persistently_forall.
......
......@@ -28,6 +28,13 @@ Global Arguments löb_weak {_ _} _ _.
Notation BiLaterContractive PROP :=
(Contractive (bi_later (PROP:=PROP))) (only parsing).
(** The class [BiPersistentlyForall] states that universal quantification
commutes with the persistently modality. The reverse direction of the entailment
described by this type class is derivable, so it is not included. *)
Class BiPersistentlyForall (PROP : bi) :=
persistently_forall_2 : {A} (Ψ : A PROP), ( a, <pers> (Ψ a)) <pers> ( a, Ψ a).
Global Hint Mode BiPersistentlyForall ! : typeclass_instances.
(** The class [BiPureForall] states that universal quantification commutes with
the embedding of pure propositions. The reverse direction of the entailment
described by this type class is derivable, so it is not included.
......@@ -36,3 +43,4 @@ An instance of [BiPureForall] itself is derivable if we assume excluded middle
in Coq, see the lemma [bi_pure_forall_em] in [derived_laws]. *)
Class BiPureForall (PROP : bi) :=
pure_forall_2 : {A} (φ : A Prop), ( a, φ a ) @{PROP} a, φ a .
Global Hint Mode BiPureForall ! : typeclass_instances.
......@@ -101,8 +101,13 @@ Section bi_mixin.
(* In the ordered RA model: [ε ≼ core x]. *)
bi_mixin_persistently_emp_2 : emp <pers> emp;
bi_mixin_persistently_forall_2 {A} (Ψ : A PROP) :
( a, <pers> (Ψ a)) <pers> ( a, Ψ a);
(* The laws of a "frame" (https://ncatlab.org/nlab/show/frame, not to be
confused with separation logic terminology): commuting with finite
conjunction and infinite disjunction.
The null-ary case, [persistently_True : True ⊢ <pers> True], is derivable from the
other laws. *)
bi_mixin_persistently_and_2 (P Q : PROP) :
(<pers> P) (<pers> Q) <pers> (P Q);
bi_mixin_persistently_exist_1 {A} (Ψ : A PROP) :
<pers> ( a, Ψ a) a, <pers> (Ψ a);
......@@ -364,9 +369,9 @@ Proof. eapply bi_mixin_persistently_idemp_2, bi_bi_mixin. Qed.
Lemma persistently_emp_2 : emp @{PROP} <pers> emp.
Proof. eapply bi_mixin_persistently_emp_2, bi_bi_mixin. Qed.
Lemma persistently_forall_2 {A} (Ψ : A PROP) :
( a, <pers> (Ψ a)) <pers> ( a, Ψ a).
Proof. eapply bi_mixin_persistently_forall_2, bi_bi_mixin. Qed.
Lemma persistently_and_2 (P Q : PROP) :
((<pers> P) (<pers> Q)) <pers> (P Q).
Proof. eapply bi_mixin_persistently_and_2, bi_bi_mixin. Qed.
Lemma persistently_exist_1 {A} (Ψ : A PROP) :
<pers> ( a, Ψ a) a, <pers> (Ψ a).
Proof. eapply bi_mixin_persistently_exist_1, bi_bi_mixin. Qed.
......
......@@ -26,7 +26,9 @@ Section core.
by iApply "HPQ".
Qed.
Global Instance coreP_persistent P : Persistent (coreP P).
Global Instance coreP_persistent
`{!BiPersistentlyForall PROP, !BiPersistentlyImplPlainly PROP} P :
Persistent (coreP P).
Proof.
rewrite /coreP /Persistent. iIntros "HC" (Q).
iApply persistently_wand_affinely_plainly. iIntros "#HQ".
......@@ -63,7 +65,8 @@ Section core.
[<affine>] modality makes it stronger since it appears in the LHS of the
[⊢] in the premise. As a user, you have to prove [<affine> coreP P ⊢ Q],
which is weaker than [coreP P ⊢ Q]. *)
Lemma coreP_entails P Q : (<affine> coreP P Q) (P <pers> Q).
Lemma coreP_entails `{!BiPersistentlyForall PROP, !BiPersistentlyImplPlainly PROP} P Q :
(<affine> coreP P Q) (P <pers> Q).
Proof.
split.
- iIntros (HP) "HP". iDestruct (coreP_intro with "HP") as "#HcP {HP}".
......@@ -71,7 +74,9 @@ Section core.
- iIntros (->) "HcQ". by iDestruct (coreP_elim with "HcQ") as "#HQ".
Qed.
(** A more convenient variant of the above lemma for affine [P]. *)
Lemma coreP_entails' P Q `{!Affine P} : (coreP P Q) (P Q).
Lemma coreP_entails' `{!BiPersistentlyForall PROP, !BiPersistentlyImplPlainly PROP}
P Q `{!Affine P} :
(coreP P Q) (P Q).
Proof.
rewrite -(affine_affinely (coreP P)) coreP_entails. split.
- rewrite -{2}(affine_affinely P). by intros ->.
......
......@@ -287,7 +287,7 @@ Proof.
- intros P Q [?]. split=> i /=. by f_equiv.
- intros P. split=> i. by apply bi.persistently_idemp_2.
- split=> i. by apply bi.persistently_emp_intro.
- intros A Ψ. split=> i. by apply bi.persistently_forall_2.
- intros A Ψ. split=> i. by apply bi.persistently_and_2.
- intros A Ψ. split=> i. by apply bi.persistently_exist_1.
- intros P Q. split=> i. apply bi.sep_elim_l, _.
- intros P Q. split=> i. by apply bi.persistently_and_sep_elim.
......@@ -401,6 +401,10 @@ Proof. unseal. split. solve_proper. Qed.
Global Instance monPred_in_flip_mono : Proper (() ==> flip ()) (@monPred_in I PROP).
Proof. solve_proper. Qed.
Global Instance monPred_persistently_forall :
BiPersistentlyForall PROP BiPersistentlyForall monPredI.
Proof. intros ? A φ. split=> /= i. unseal. by apply persistently_forall_2. Qed.
Global Instance monPred_pure_forall : BiPureForall PROP BiPureForall monPredI.
Proof. intros ? A φ. split=> /= i. unseal. by apply pure_forall_2. Qed.
......@@ -476,7 +480,8 @@ Global Instance monPred_objectively_flip_mono' :
Proper (flip () ==> flip ()) (@monPred_objectively I PROP).
Proof. intros ???. by apply monPred_objectively_mono. Qed.
Global Instance monPred_objectively_persistent P : Persistent P Persistent (<obj> P).
Global Instance monPred_objectively_persistent `{!BiPersistentlyForall PROP} P :
Persistent P Persistent (<obj> P).
Proof. rewrite monPred_objectively_unfold. apply _. Qed.
Global Instance monPred_objectively_absorbing P : Absorbing P Absorbing (<obj> P).
Proof. rewrite monPred_objectively_unfold. apply _. Qed.
......@@ -937,10 +942,6 @@ Proof.
rewrite -plainly_idemp_2. f_equiv. by apply bi.forall_intro=>_.
- intros A Ψ. split=> i /=. apply bi.forall_intro=> j.
rewrite plainly_forall. apply bi.forall_intro=> a. by rewrite !bi.forall_elim.
- intros P Q. split=> i /=. setoid_rewrite bi.pure_impl_forall.
setoid_rewrite <-plainly_forall.
do 2 setoid_rewrite bi.persistently_forall. do 4 f_equiv.
apply persistently_impl_plainly.
- intros P Q. split=> i /=.
setoid_rewrite bi.pure_impl_forall. rewrite 2!bi.forall_elim //.
do 2 setoid_rewrite <-plainly_forall.
......@@ -956,6 +957,17 @@ Qed.
Global Instance monPred_bi_plainly `{BiPlainly PROP} : BiPlainly monPredI :=
{| bi_plainly_mixin := monPred_plainly_mixin |}.
Global Instance minPred_bi_persistently_impl_plainly
`{!BiPlainly PROP, !BiPersistentlyForall PROP, !BiPersistentlyImplPlainly PROP} :
BiPersistentlyImplPlainly monPredI.
Proof.
intros P Q. rewrite monPred_plainly_eq. unseal.
split=> i /=. setoid_rewrite bi.pure_impl_forall.
setoid_rewrite <-plainly_forall.
do 2 setoid_rewrite bi.persistently_forall. do 4 f_equiv.
apply: persistently_impl_plainly.
Qed.
Global Instance monPred_bi_prop_ext
`{!BiPlainly PROP, !BiInternalEq PROP, !BiPropExt PROP} : BiPropExt monPredI.
Proof.
......
......@@ -23,11 +23,9 @@ Record BiPlainlyMixin (PROP : bi) `(Plainly PROP) := {
bi_plainly_mixin_plainly_forall_2 {A} (Ψ : A PROP) :
( a, (Ψ a)) ( a, Ψ a);
(* The following two laws are very similar, and indeed they hold not just
for persistently and plainly, but for any modality defined as `M P n x :=
∀ y, R x y → P n y`. *)
bi_plainly_mixin_persistently_impl_plainly (P Q : PROP) :
( P <pers> Q) <pers> ( P Q);
(* The following law and [persistently_impl_plainly] below are very similar,
and indeed they hold not just for persistently and plainly, but for any
modality defined as [M P n x := ∀ y, R x y → P n y]. *)
bi_plainly_mixin_plainly_impl_plainly (P Q : PROP) :
( P Q) ( P Q);
......@@ -45,6 +43,14 @@ Class BiPlainly (PROP : bi) := {
Global Hint Mode BiPlainly ! : typeclass_instances.
Global Arguments bi_plainly_plainly : simpl never.
Class BiPersistentlyImplPlainly `{!BiPlainly PROP} :=
persistently_impl_plainly (P Q : PROP) :
( P <pers> Q) <pers> ( P Q).
Global Arguments BiPersistentlyImplPlainly : clear implicits.
Global Arguments BiPersistentlyImplPlainly _ {_}.
Global Arguments persistently_impl_plainly _ {_ _} _.
Global Hint Mode BiPersistentlyImplPlainly ! - : typeclass_instances.
Class BiPlainlyExist `{!BiPlainly PROP} :=
plainly_exist_1 A (Ψ : A PROP) :
( a, Ψ a) a, (Ψ a).
......@@ -75,8 +81,6 @@ Section plainly_laws.
Proof. eapply bi_plainly_mixin_plainly_idemp_2, bi_plainly_mixin. Qed.
Lemma plainly_forall_2 {A} (Ψ : A PROP) : ( a, (Ψ a)) ( a, Ψ a).
Proof. eapply bi_plainly_mixin_plainly_forall_2, bi_plainly_mixin. Qed.
Lemma persistently_impl_plainly P Q : ( P <pers> Q) <pers> ( P Q).
Proof. eapply bi_plainly_mixin_persistently_impl_plainly, bi_plainly_mixin. Qed.
Lemma plainly_impl_plainly P Q : ( P Q) ( P Q).
Proof. eapply bi_plainly_mixin_plainly_impl_plainly, bi_plainly_mixin. Qed.
Lemma plainly_absorb P Q : P Q P.
......@@ -270,9 +274,9 @@ Proof. apply impl_intro_l. by rewrite plainly_and_sep_l_1 wand_elim_r. Qed.
Lemma impl_wand_affinely_plainly P Q : ( P Q) (<affine> P - Q).
Proof. by rewrite -(persistently_elim_plainly P) impl_wand_intuitionistically. Qed.
Lemma persistently_wand_affinely_plainly P Q :
Lemma persistently_wand_affinely_plainly `{!BiPersistentlyImplPlainly PROP} P Q :
(<affine> P - <pers> Q) <pers> (<affine> P - Q).
Proof. rewrite -!impl_wand_affinely_plainly. apply persistently_impl_plainly. Qed.
Proof. rewrite -!impl_wand_affinely_plainly. apply: persistently_impl_plainly. Qed.
Lemma plainly_wand_affinely_plainly P Q :
(<affine> P - Q) (<affine> P - Q).
......@@ -362,7 +366,7 @@ Proof. intros; destruct p; simpl; apply _. Qed.
Lemma plain_persistent P : Plain P Persistent P.
Proof. intros. by rewrite /Persistent -plainly_elim_persistently. Qed.
Global Instance impl_persistent P Q :
Global Instance impl_persistent `{!BiPersistentlyImplPlainly PROP} P Q :
Absorbing P Plain P Persistent Q Persistent (P Q).
Proof.
intros. by rewrite /Persistent {2}(plain P) -persistently_impl_plainly
......@@ -372,7 +376,7 @@ Qed.
Global Instance plainly_persistent P : Persistent ( P).
Proof. by rewrite /Persistent persistently_elim_plainly. Qed.
Global Instance wand_persistent P Q :
Global Instance wand_persistent `{!BiPersistentlyImplPlainly PROP} P Q :
Plain P Persistent Q Absorbing Q Persistent (P - Q).
Proof.
intros. rewrite /Persistent {2}(plain P). trans (<pers> ( P Q))%I.
......
......@@ -71,7 +71,7 @@ Section telescopes.
Global Instance bi_tforall_absorbing Ψ :
( x, Absorbing (Ψ x)) Absorbing (.. x, Ψ x).
Proof. rewrite bi_tforall_forall. apply _. Qed.
Global Instance bi_tforall_persistent Ψ :
Global Instance bi_tforall_persistent `{!BiPersistentlyForall PROP} Ψ :
( x, Persistent (Ψ x)) Persistent (.. x, Ψ x).
Proof. rewrite bi_tforall_forall. apply _. Qed.
......
......@@ -937,7 +937,7 @@ Proof. rewrite /IntoForall=> HP. by rewrite HP affinely_forall. Qed.
Global Instance into_forall_intuitionistically {A} P (Φ : A PROP) :
IntoForall P Φ IntoForall ( P) (λ a, (Φ a))%I.
Proof. rewrite /IntoForall=> HP. by rewrite HP intuitionistically_forall. Qed.
Global Instance into_forall_persistently {A} P (Φ : A PROP) :
Global Instance into_forall_persistently `{!BiPersistentlyForall PROP} {A} P (Φ : A PROP) :
IntoForall P Φ IntoForall (<pers> P) (λ a, <pers> (Φ a))%I.
Proof. rewrite /IntoForall=> HP. by rewrite HP persistently_forall. Qed.
......@@ -1003,13 +1003,15 @@ Proof.
- by rewrite (into_pure P) -pure_wand_forall wand_elim_l.
Qed.
Global Instance from_forall_intuitionistically `{BiAffine PROP} {A} P (Φ : A PROP) name :
Global Instance from_forall_intuitionistically `{!BiAffine PROP, !BiPersistentlyForall PROP}
{A} P (Φ : A PROP) name :
FromForall P Φ name FromForall ( P) (λ a, (Φ a))%I name.
Proof.
rewrite /FromForall=> <-. setoid_rewrite intuitionistically_into_persistently.