Commit 4cfb6ef8 authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan
Browse files

Merge commit 'f5a5f' into gen_proofmode

parents 58b8eafa f5a5f1f1
......@@ -31,7 +31,7 @@ Context management
- `iRevert (x1 ... xn) "selpat"` : revert the hypotheses given by the selection
pattern `selpat` into wands, and the Coq level hypotheses/variables
`x1 ... xn` into universal quantifiers. Persistent hypotheses are wrapped into
the always modality.
the persistence modality.
- `iRename "H1" into "H2"` : rename the hypothesis `H1` into `H2`.
- `iSpecialize pm_trm` : instantiate universal quantifiers and eliminate
implications/wands of a hypothesis `pm_trm`. See proof mode terms below.
......@@ -162,8 +162,8 @@ Miscellaneous
introduces pure connectives.
- The proof mode adds hints to the core `eauto` database so that `eauto`
automatically introduces: conjunctions and disjunctions, universal and
existential quantifiers, implications and wand, always, later and update
modalities, and pure connectives.
existential quantifiers, implications and wand, plainness, persistence, later
and update modalities, and pure connectives.
Selection patterns
==================
......@@ -207,7 +207,9 @@ appear at the top level:
Items of the selection pattern can be prefixed with `$`, which cause them to
be framed instead of cleared.
- `!%` : introduce a pure goal (and leave the proof mode).
- `!#` : introduce an always modality and clear the spatial context.
- `!#` : introduce an persistence or plainness modality and clear the spatial
context. In case of a plainness modality, it will prune all persistent
hypotheses that are not plain.
- `!>` : introduce a modality.
- `/=` : perform `simpl`.
- `//` : perform `try done` on all goals.
......
......@@ -36,6 +36,9 @@ Global Instance uPred_affine : AffineBI (uPredI M) | 0.
Proof. intros P. rewrite /Affine. by apply bi.pure_intro. Qed.
(* Own and valid derived *)
Lemma persistently_cmra_valid_1 {A : cmraT} (a : A) :
a bi_persistently ( a : uPred M).
Proof. by rewrite {1}plainly_cmra_valid_1 plainly_elim_persistently. Qed.
Lemma affinely_persistently_ownM (a : M) : CoreId a uPred_ownM a uPred_ownM a.
Proof.
rewrite affine_affinely=>?; apply (anti_symm _); [by rewrite persistently_elim|].
......@@ -47,6 +50,11 @@ Global Instance ownM_mono : Proper (flip (≼) ==> (⊢)) (@uPred_ownM M).
Proof. intros a b [b' ->]. by rewrite ownM_op sep_elim_l. Qed.
Lemma ownM_unit' : uPred_ownM ε True.
Proof. apply (anti_symm _); first by apply pure_intro. apply ownM_empty. Qed.
Lemma affinely_plainly_cmra_valid {A : cmraT} (a : A) : a a.
Proof.
rewrite affine_affinely.
apply (anti_symm _), plainly_cmra_valid_1. apply plainly_elim, _.
Qed.
Lemma affinely_persistently_cmra_valid {A : cmraT} (a : A) : a a.
Proof.
rewrite affine_affinely. intros; apply (anti_symm _); first by rewrite persistently_elim.
......@@ -90,12 +98,24 @@ Proof.
auto using and_elim_l, and_elim_r.
Qed.
(* Derived lemmas for persistence *)
Global Instance limit_preserving_Persistent {A:ofeT} `{Cofe A} (Φ : A uPred M) :
NonExpansive Φ LimitPreserving (λ x, Persistent (Φ x)).
(* Plainness *)
Global Instance limit_preserving_Plain {A:ofeT} `{Cofe A} (Φ : A uPred M) :
NonExpansive Φ LimitPreserving (λ x, Plain (Φ x)).
Proof. intros. apply limit_preserving_entails; solve_proper. Qed.
Global Instance cmra_valid_plain {A : cmraT} (a : A) :
Plain ( a : uPred M)%I.
Proof. rewrite /Persistent. apply plainly_cmra_valid_1. Qed.
Lemma bupd_affinely_plainly P : (|==> P) P.
Proof. by rewrite affine_affinely bupd_plainly. Qed.
Lemma bupd_plain P `{!Plain P} : (|==> P) P.
Proof. by rewrite -{1}(plain_plainly P) bupd_plainly. Qed.
(* Persistence *)
Global Instance limit_preserving_Persistent {A:ofeT} `{Cofe A} (Φ : A uPred M) :
NonExpansive Φ LimitPreserving (λ x, Persistent (Φ x)).
Proof. intros. apply limit_preserving_entails; solve_proper. Qed.
Global Instance cmra_valid_persistent {A : cmraT} (a : A) :
Persistent ( a : uPred M)%I.
Proof. rewrite /Persistent. apply persistently_cmra_valid_1. Qed.
......
......@@ -3,19 +3,9 @@ From iris.proofmode Require Import tactics.
Set Default Proof Using "Type".
Import uPred.
(** The "core" of an assertion is its maximal persistent part.
It can be defined entirely within the logic... at least
in the shallow embedding.
WARNING: The function "coreP" is NOT NON-EXPANSIVE.
This is because the turnstile is not non-expansive as a function
from iProp to (discreteC Prop).
To obtain a core that's non-expansive, we would have to add another
modality to the logic: a box that removes access to *all* resources,
not just restricts access to the core.
*)
(** The "core" of an assertion is its maximal persistent part. *)
Definition coreP {M : ucmraT} (P : uPred M) : uPred M :=
( `(!Persistent Q), P Q Q)%I.
( Q, (Q Q) (P Q) Q)%I.
Instance: Params (@coreP) 1.
Typeclasses Opaque coreP.
......@@ -24,25 +14,31 @@ Section core.
Implicit Types P Q : uPred M.
Lemma coreP_intro P : P - coreP P.
Proof. rewrite /coreP. iIntros "HP". by iIntros (Q HQ ->). Qed.
Proof. rewrite /coreP. iIntros "HP" (Q) "_ HPQ". by iApply "HPQ". Qed.
Global Instance coreP_persistent P : Persistent (coreP P).
Proof. rewrite /coreP. apply _. Qed.
Global Instance coreP_mono : Proper (() ==> ()) (@coreP M).
Proof.
rewrite /coreP. iIntros (P P' ?) "H"; iIntros (Q ??).
iApply ("H" $! Q with "[%]"). by etrans.
rewrite /coreP /Persistent. iIntros "HC" (Q). rewrite !affine_affinely.
iApply persistently_impl_plainly. iIntros "#HQ".
iApply persistently_impl_plainly. iIntros "#HPQ".
iApply "HQ". by iApply "HC"; rewrite !affine_affinely.
Qed.
Global Instance coreP_ne : NonExpansive (@coreP M).
Proof. solve_proper. Qed.
Global Instance coreP_proper : Proper (() ==> ()) (@coreP M).
Proof. intros P Q. rewrite !equiv_spec=>-[??]. by split; apply coreP_mono. Qed.
Proof. solve_proper. Qed.
Global Instance coreP_mono : Proper (() ==> ()) (@coreP M).
Proof.
rewrite /coreP. iIntros (P P' HP) "H"; iIntros (Q) "#HQ #HPQ".
iApply ("H" $! Q with "[]"); first done. by rewrite HP.
Qed.
Lemma coreP_elim P : Persistent P coreP P - P.
Proof. rewrite /coreP. iIntros (?) "HCP". unshelve iApply ("HCP" $! P); auto. Qed.
Proof. rewrite /coreP. iIntros (?) "HCP". iApply ("HCP" $! P); auto. Qed.
Lemma coreP_wand P Q :
(coreP P Q) (P Q).
Lemma coreP_wand P Q : (coreP P Q) (P Q).
Proof.
split.
- iIntros (HP) "HP". iDestruct (coreP_intro with "HP") as "#HcP".
......
......@@ -115,6 +115,12 @@ Proof. apply bupd_intro. Qed.
Global Instance elim_modal_bupd P Q : ElimModal (|==> P) P (|==> Q) (|==> Q).
Proof. by rewrite /ElimModal bupd_frame_r wand_elim_r bupd_trans. Qed.
Global Instance elim_modal_bupd_plain_goal P Q : Plain Q ElimModal (|==> P) P Q Q.
Proof. intros. by rewrite /ElimModal bupd_frame_r wand_elim_r bupd_plain. Qed.
Global Instance elim_modal_bupd_plain P Q : Plain P ElimModal (|==> P) P Q Q.
Proof. intros. by rewrite /ElimModal bupd_plain wand_elim_r. Qed.
Global Instance is_except_0_bupd P : IsExcept0 P IsExcept0 (|==> P).
Proof.
rewrite /IsExcept0=> HP.
......
......@@ -6,22 +6,16 @@ Section adequacy.
Context {M : ucmraT}.
(** Consistency and adequancy statements *)
Lemma soundness φ n :
bi_valid (PROP:=uPredI M) (Nat.iter n (λ P, |==> P) ( φ ))%I φ.
Lemma soundness φ n : (^n φ : uPred M)%I φ.
Proof.
cut ( x, {n} x Nat.iter n (λ P, |==> P)%I (@uPred_pure M φ) n x φ).
{ intros help H. eapply (help ); eauto using ucmra_unit_validN.
eapply H; first by eauto using ucmra_unit_validN.
rewrite /bi_emp /= /uPred_emp. by unseal. }
unseal. induction n as [|n IH]=> x Hx Hupd; auto.
destruct (Hupd (S n) ε) as (x'&?&?); rewrite ?right_id; auto.
eapply IH with x'; eauto using cmra_validN_S, cmra_validN_op_l.
cut ((^n φ : uPred M)%I n ε φ).
{ intros help H. eapply help, H; eauto using ucmra_unit_validN. by unseal. }
rewrite /bi_laterN; unseal. induction n as [|n IH]=> H; auto.
Qed.
Corollary consistency_modal n :
¬bi_valid (PROP:=uPredI M) (Nat.iter n (λ P, |==> P) (False : uPred M))%I.
Corollary consistency_modal n : ¬ (^n False : uPred M)%I.
Proof. exact (soundness False n). Qed.
Corollary consistency : ¬bi_valid (PROP:=uPredI M) False.
Corollary consistency : ¬(False : uPred M)%I.
Proof. exact (consistency_modal 0). Qed.
End adequacy.
......@@ -248,6 +248,14 @@ Definition uPred_wand {M} := unseal uPred_wand_aux M.
Definition uPred_wand_eq :
@uPred_wand = @uPred_wand_def := seal_eq uPred_wand_aux.
Program Definition uPred_plainly_def {M} (P : uPred M) : uPred M :=
{| uPred_holds n x := P n ε |}.
Solve Obligations with naive_solver eauto using uPred_closed, ucmra_unit_validN.
Definition uPred_plainly_aux : seal (@uPred_plainly_def). by eexists. Qed.
Definition uPred_plainly {M} := unseal uPred_plainly_aux M.
Definition uPred_plainly_eq :
@uPred_plainly = @uPred_plainly_def := seal_eq uPred_plainly_aux.
Program Definition uPred_persistently_def {M} (P : uPred M) : uPred M :=
{| uPred_holds n x := P n (core x) |}.
Next Obligation.
......@@ -311,24 +319,25 @@ Module uPred_unseal.
Definition unseal_eqs :=
(uPred_pure_eq, uPred_and_eq, uPred_or_eq, uPred_impl_eq, uPred_forall_eq,
uPred_exist_eq, uPred_internal_eq_eq, uPred_sep_eq, uPred_wand_eq,
uPred_persistently_eq, uPred_later_eq, uPred_ownM_eq, uPred_cmra_valid_eq,
uPred_bupd_eq).
uPred_plainly_eq, uPred_persistently_eq, uPred_later_eq, uPred_ownM_eq,
uPred_cmra_valid_eq, uPred_bupd_eq).
Ltac unseal := rewrite
/bi_emp /= /uPred_emp /bi_pure /bi_and /bi_or /bi_impl
/bi_forall /bi_exist /bi_internal_eq /bi_sep /bi_wand /bi_persistently
/bi_later /=
/bi_forall /bi_exist /bi_internal_eq /bi_sep /bi_wand /bi_plainly
/bi_persistently /bi_later /=
/sbi_emp /sbi_pure /sbi_and /sbi_or /sbi_impl
/sbi_forall /sbi_exist /sbi_internal_eq /sbi_sep /sbi_wand /sbi_persistently /=
/sbi_forall /sbi_exist /sbi_internal_eq /sbi_sep /sbi_wand /sbi_plainly
/sbi_persistently /=
!unseal_eqs /=.
End uPred_unseal.
Import uPred_unseal.
Local Arguments uPred_holds {_} !_ _ _ /.
Lemma uPred_bi_mixin (M : ucmraT) : BIMixin
Lemma uPred_bi_mixin (M : ucmraT) : BIMixin (ofe_mixin_of (uPred M))
uPred_entails uPred_emp uPred_pure uPred_and uPred_or uPred_impl
(@uPred_forall M) (@uPred_exist M) (@uPred_internal_eq M)
uPred_sep uPred_wand uPred_persistently.
uPred_sep uPred_wand uPred_plainly uPred_persistently.
Proof.
split.
- (* PreOrder uPred_entails *)
......@@ -364,6 +373,9 @@ Proof.
intros n P P' HP Q Q' HQ; split=> n' x ??.
unseal; split; intros HPQ x' n'' ???;
apply HQ, HPQ, HP; eauto using cmra_validN_op_r.
- (* NonExpansive uPred_plainly *)
intros n P1 P2 HP.
unseal; split=> n' x; split; apply HP; eauto using @ucmra_unit_validN.
- (* NonExpansive uPred_persistently *)
intros n P1 P2 HP.
unseal; split=> n' x; split; apply HP; eauto using @cmra_core_validN.
......@@ -438,16 +450,43 @@ Proof.
- (* (P ⊢ Q -∗ R) → P ∗ Q ⊢ R *)
intros P Q R. unseal=> HPQR. split; intros n x ? (?&?&?&?&?). ofe_subst.
eapply HPQR; eauto using cmra_validN_op_l.
- (* (P ⊢ Q) → bi_plainly P ⊢ bi_plainly Q *)
intros P QR HP. unseal; split=> n x ? /=. by apply HP, ucmra_unit_validN.
- (* bi_plainly P ⊢ bi_persistently P *)
unseal; split; simpl; eauto using uPred_mono, @ucmra_unit_leastN.
- (* bi_plainly P ⊢ bi_plainly (bi_plainly P) *)
unseal; split=> n x ?? //.
- (* (∀ a, bi_plainly (Ψ a)) ⊢ bi_plainly (∀ a, Ψ a) *)
by unseal.
- (* bi_plainly (∃ a, Ψ a) ⊢ ∃ a, bi_plainly (Ψ a) *)
by unseal.
- (* bi_plainly ((P → Q) ∧ (Q → P)) ⊢ P ≡ Q *)
unseal; split=> n x ? /= HPQ; split=> n' x' ? HP;
split; eapply HPQ; eauto using @ucmra_unit_least.
- (* (bi_plainly P → bi_persistently Q) ⊢ bi_persistently (bi_plainly P → Q) *)
unseal; split=> /= n x ? HPQ n' x' ????.
eapply uPred_mono with (core x), cmra_included_includedN; auto.
apply (HPQ n' x); eauto using cmra_validN_le.
- (* (bi_plainly P → bi_plainly Q) ⊢ bi_plainly (bi_plainly P → Q) *)
unseal; split=> /= n x ? HPQ n' x' ????.
eapply uPred_mono with ε, cmra_included_includedN; auto.
apply (HPQ n' x); eauto using cmra_validN_le.
- (* P ⊢ bi_plainly emp (ADMISSIBLE) *)
by unseal.
- (* bi_plainly P ∗ Q ⊢ bi_plainly P *)
intros P Q. move: (uPred_persistently P)=> P'.
unseal; split; intros n x ? (x1&x2&?&?&_); ofe_subst;
eauto using uPred_mono, cmra_includedN_l.
- (* (P ⊢ Q) → bi_persistently P ⊢ bi_persistently Q *)
intros P QR HP. unseal; split=> n x ? /=. by apply HP, cmra_core_validN.
- (* bi_persistently P ⊢ bi_persistently (bi_persistently P) *)
intros P. unseal; split=> n x ?? /=. by rewrite cmra_core_idemp.
- (* bi_plainly (bi_persistently P) ⊢ bi_plainly P (ADMISSIBLE) *)
intros P. unseal; split=> n x ?? /=. by rewrite -(core_id_core ε).
- (* (∀ a, bi_persistently (Ψ a)) ⊢ bi_persistently (∀ a, Ψ a) *)
by unseal.
- (* bi_persistently (∃ a, Ψ a) ⊢ ∃ a, bi_persistently (Ψ a) *)
by unseal.
- (* P ⊢ bi_persistently emp (ADMISSIBLE) *)
intros P. unfold uPred_emp; unseal; by split=> n x ? _.
- (* bi_persistently P ∗ Q ⊢ bi_persistently P (ADMISSIBLE) *)
intros P Q. move: (uPred_persistently P)=> P'.
unseal; split; intros n x ? (x1&x2&?&?&_); ofe_subst;
......@@ -460,7 +499,7 @@ Qed.
Lemma uPred_sbi_mixin (M : ucmraT) : SBIMixin
uPred_entails uPred_pure uPred_or uPred_impl
(@uPred_forall M) (@uPred_exist M) (@uPred_internal_eq M)
uPred_sep uPred_persistently uPred_later.
uPred_sep uPred_plainly uPred_persistently uPred_later.
Proof.
split.
- (* Contractive bi_later *)
......@@ -489,6 +528,10 @@ Proof.
- (* ▷ P ∗ ▷ Q ⊢ ▷ (P ∗ Q) *)
intros P Q. unseal; split=> -[|n] x ? /=; [done|intros (x1&x2&Hx&?&?)].
exists x1, x2; eauto using dist_S.
- (* ▷ bi_plainly P ⊢ bi_plainly (▷ P) *)
by unseal.
- (* bi_plainly (▷ P) ⊢ ▷ bi_plainly P *)
by unseal.
- (* ▷ bi_persistently P ⊢ bi_persistently (▷ P) *)
by unseal.
- (* bi_persistently (▷ P) ⊢ ▷ bi_persistently P *)
......@@ -602,8 +645,7 @@ Lemma cmra_valid_elim {A : cmraT} (a : A) : ¬ ✓{0} a → ✓ a ⊢ (False : u
Proof.
intros Ha. unseal. split=> n x ??; apply Ha, cmra_validN_le with n; auto.
Qed.
Lemma persistently_cmra_valid_1 {A : cmraT} (a : A) :
a bi_persistently ( a : uPred M).
Lemma plainly_cmra_valid_1 {A : cmraT} (a : A) : a bi_plainly ( a : uPred M).
Proof. by unseal. Qed.
Lemma cmra_valid_weaken {A : cmraT} (a b : A) : (a b) ( a : uPred M).
Proof. unseal; split=> n x _; apply cmra_validN_op_l. Qed.
......@@ -646,5 +688,11 @@ Proof.
exists (y x3); split; first by rewrite -assoc.
exists y; eauto using cmra_includedN_l.
Qed.
Lemma bupd_plainly P : (|==> bi_plainly P) P.
Proof.
unseal; split => n x Hnx /= Hng.
destruct (Hng n ε) as [? [_ Hng']]; try rewrite right_id; auto.
eapply uPred_mono; eauto using ucmra_unit_leastN.
Qed.
End uPred.
End uPred.
......@@ -125,9 +125,13 @@ Section sep_list.
([ list] kx l, Φ k x) ([ list] kx l, Ψ k x).
Proof. auto using and_intro, big_sepL_mono, and_elim_l, and_elim_r. Qed.
Lemma big_sepL_plainly `{AffineBI PROP} Φ l :
bi_plainly ([ list] kx l, Φ k x) [ list] kx l, bi_plainly (Φ k x).
Proof. apply (big_opL_commute _). Qed.
Lemma big_sepL_persistently `{AffineBI PROP} Φ l :
(bi_persistently ([ list] kx l, Φ k x))
([ list] kx l, bi_persistently (Φ k x)).
bi_persistently ([ list] kx l, Φ k x)
[ list] kx l, bi_persistently (Φ k x).
Proof. apply (big_opL_commute _). Qed.
Lemma big_sepL_forall `{AffineBI PROP} Φ l :
......@@ -159,6 +163,16 @@ Section sep_list.
apply forall_intro=> k. by rewrite (forall_elim (S k)).
Qed.
Global Instance big_sepL_nil_plain Φ :
Plain ([ list] kx [], Φ k x).
Proof. simpl; apply _. Qed.
Global Instance big_sepL_plain Φ l :
( k x, Plain (Φ k x)) Plain ([ list] kx l, Φ k x).
Proof. revert Φ. induction l as [|x l IH]=> Φ ? /=; apply _. Qed.
Global Instance big_sepL_plain_id Ps :
TCForall Plain Ps Plain ([] Ps).
Proof. induction 1; simpl; apply _. Qed.
Global Instance big_sepL_nil_persistent Φ :
Persistent ([ list] kx [], Φ k x).
Proof. simpl; apply _. Qed.
......@@ -264,9 +278,13 @@ Section and_list.
([ list] kx l, Φ k x) ([ list] kx l, Ψ k x).
Proof. auto using and_intro, big_andL_mono, and_elim_l, and_elim_r. Qed.
Lemma big_andL_plainly Φ l :
bi_plainly ([ list] kx l, Φ k x) [ list] kx l, bi_plainly (Φ k x).
Proof. apply (big_opL_commute _). Qed.
Lemma big_andL_persistently Φ l :
(bi_persistently ([ list] kx l, Φ k x))
([ list] kx l, bi_persistently (Φ k x)).
bi_persistently ([ list] kx l, Φ k x)
[ list] kx l, bi_persistently (Φ k x).
Proof. apply (big_opL_commute _). Qed.
Lemma big_andL_forall `{AffineBI PROP} Φ l :
......@@ -281,6 +299,13 @@ Section and_list.
- rewrite -IH. apply forall_intro=> k; by rewrite (forall_elim (S k)).
Qed.
Global Instance big_andL_nil_plain Φ :
Plain ([ list] kx [], Φ k x).
Proof. simpl; apply _. Qed.
Global Instance big_andL_plain Φ l :
( k x, Plain (Φ k x)) Plain ([ list] kx l, Φ k x).
Proof. revert Φ. induction l as [|x l IH]=> Φ ? /=; apply _. Qed.
Global Instance big_andL_nil_persistent Φ :
Persistent ([ list] kx [], Φ k x).
Proof. simpl; apply _. Qed.
......@@ -395,6 +420,10 @@ Section gmap.
([ map] kx m, Φ k x) ([ map] kx m, Ψ k x).
Proof. auto using and_intro, big_sepM_mono, and_elim_l, and_elim_r. Qed.
Lemma big_sepM_plainly `{AffineBI PROP} Φ m :
bi_plainly ([ map] kx m, Φ k x) [ map] kx m, bi_plainly (Φ k x).
Proof. apply (big_opM_commute _). Qed.
Lemma big_sepM_persistently `{AffineBI PROP} Φ m :
(bi_persistently ([ map] kx m, Φ k x))
([ map] kx m, bi_persistently (Φ k x)).
......@@ -435,6 +464,12 @@ Section gmap.
by rewrite pure_True // True_impl.
Qed.
Global Instance big_sepM_empty_plain Φ : Plain ([ map] kx , Φ k x).
Proof. rewrite /big_opM map_to_list_empty. apply _. Qed.
Global Instance big_sepM_plain Φ m :
( k x, Plain (Φ k x)) Plain ([ map] kx m, Φ k x).
Proof. intros. apply (big_sepL_plain _ _)=> _ [??]; apply _. Qed.
Global Instance big_sepM_empty_persistent Φ :
Persistent ([ map] kx , Φ k x).
Proof. rewrite /big_opM map_to_list_empty. apply _. Qed.
......@@ -561,8 +596,12 @@ Section gset.
([ set] y X, Φ y Ψ y) ([ set] y X, Φ y) ([ set] y X, Ψ y).
Proof. auto using and_intro, big_sepS_mono, and_elim_l, and_elim_r. Qed.
Lemma big_sepS_plainly `{AffineBI PROP} Φ X :
bi_plainly ([ set] y X, Φ y) [ set] y X, bi_plainly (Φ y).
Proof. apply (big_opS_commute _). Qed.
Lemma big_sepS_persistently `{AffineBI PROP} Φ X :
bi_persistently ([ set] y X, Φ y) ([ set] y X, bi_persistently (Φ y)).
bi_persistently ([ set] y X, Φ y) [ set] y X, bi_persistently (Φ y).
Proof. apply (big_opS_commute _). Qed.
Lemma big_sepS_forall `{AffineBI PROP} Φ X :
......@@ -593,6 +632,13 @@ Section gset.
apply forall_mono=> y. apply impl_intro_l, pure_elim_l=> ?.
by rewrite pure_True ?True_impl; last set_solver.
Qed.
Global Instance big_sepS_empty_plain Φ : Plain ([ set] x , Φ x).
Proof. rewrite /big_opS elements_empty. apply _. Qed.
Global Instance big_sepS_plain Φ X :
( x, Plain (Φ x)) Plain ([ set] x X, Φ x).
Proof. rewrite /big_opS. apply _. Qed.
Global Instance big_sepS_empty_persistent Φ :
Persistent ([ set] x , Φ x).
Proof. rewrite /big_opS elements_empty. apply _. Qed.
......@@ -611,7 +657,6 @@ Lemma big_sepM_dom `{Countable K} {A} (Φ : K → PROP) (m : gmap K A) :
([ map] k_ m, Φ k) ([ set] k dom _ m, Φ k).
Proof. apply big_opM_dom. Qed.
(** ** Big ops over finite multisets *)
Section gmultiset.
Context `{Countable A}.
......@@ -669,11 +714,21 @@ Section gmultiset.
([ mset] y X, Φ y Ψ y) ([ mset] y X, Φ y) ([ mset] y X, Ψ y).
Proof. auto using and_intro, big_sepMS_mono, and_elim_l, and_elim_r. Qed.
Lemma big_sepMS_plainly `{AffineBI PROP} Φ X :
bi_plainly ([ mset] y X, Φ y) [ mset] y X, bi_plainly (Φ y).
Proof. apply (big_opMS_commute _). Qed.
Lemma big_sepMS_persistently `{AffineBI PROP} Φ X :
bi_persistently ([ mset] y X, Φ y)
([ mset] y X, bi_persistently (Φ y)).
[ mset] y X, bi_persistently (Φ y).
Proof. apply (big_opMS_commute _). Qed.
Global Instance big_sepMS_empty_plain Φ : Plain ([ mset] x , Φ x).
Proof. rewrite /big_opMS gmultiset_elements_empty. apply _. Qed.
Global Instance big_sepMS_plain Φ X :
( x, Plain (Φ x)) Plain ([ mset] x X, Φ x).
Proof. rewrite /big_opMS. apply _. Qed.
Global Instance big_sepMS_empty_persistent Φ :
Persistent ([ mset] x , Φ x).
Proof. rewrite /big_opMS gmultiset_elements_empty. apply _. Qed.
......
This diff is collapsed.
......@@ -142,7 +142,7 @@ Section fractional.
Proof. intros. rewrite /IntoSep [P]fractional_half //. Qed.
(* The instance [frame_fractional] can be tried at all the nodes of
the proof search. The proof search then fails almost persistently on
the proof search. The proof search then fails almost always on
[AsFractional R Φ r], but the slowdown is still noticeable. For
that reason, we factorize the three instances that could have been
defined for that purpose into one. *)
......
......@@ -8,7 +8,7 @@ Reserved Notation "P -∗ Q" (at level 99, Q at level 200, right associativity).
Reserved Notation "▷ P" (at level 20, right associativity).
Section bi_mixin.
Context {PROP : Type} `{Dist PROP, Equiv PROP}.
Context {PROP : Type} `{Dist PROP, Equiv PROP} (prop_ofe_mixin : OfeMixin PROP).
Context (bi_entails : PROP PROP Prop).
Context (bi_emp : PROP).
Context (bi_pure : Prop PROP).
......@@ -20,6 +20,7 @@ Section bi_mixin.
Context (bi_internal_eq : A : ofeT, A A PROP).
Context (bi_sep : PROP PROP PROP).
Context (bi_wand : PROP PROP PROP).
Context (bi_plainly : PROP PROP).
Context (bi_persistently : PROP PROP).
Context (bi_later : PROP PROP).
......@@ -55,6 +56,7 @@ Section bi_mixin.
Proper (pointwise_relation _ (dist n) ==> dist n) (bi_exist A);
bi_mixin_sep_ne : NonExpansive2 bi_sep;
bi_mixin_wand_ne : NonExpansive2 bi_wand;
bi_mixin_plainly_ne : NonExpansive bi_plainly;
bi_mixin_persistently_ne : NonExpansive bi_persistently;
bi_mixin_internal_eq_ne (A : ofeT) : NonExpansive2 (bi_internal_eq A);
......@@ -97,18 +99,40 @@ Section bi_mixin.
bi_mixin_wand_intro_r P Q R : (P Q R) P Q - R;
bi_mixin_wand_elim_l' P Q R : (P Q - R) P Q R;
(* Plainly *)
bi_mixin_plainly_mono P Q : (P Q) bi_plainly P bi_plainly Q;
bi_mixin_plainly_elim_persistently P : bi_plainly P bi_persistently P;
bi_mixin_plainly_idemp_2 P : bi_plainly P bi_plainly (bi_plainly P);
bi_mixin_plainly_forall_2 {A} (Ψ : A PROP) :
( a, bi_plainly (Ψ a)) bi_plainly ( a, Ψ a);
bi_mixin_plainly_exist_1 {A} (Ψ : A PROP) :
bi_plainly ( a, Ψ a) a, bi_plainly (Ψ a);
bi_mixin_prop_ext P Q : bi_plainly ((P Q) (Q P))
bi_internal_eq (OfeT PROP prop_ofe_mixin) P Q;
bi_mixin_persistently_impl_plainly P Q :
(bi_plainly P bi_persistently Q) bi_persistently (bi_plainly P Q);
bi_mixin_plainly_impl_plainly P Q :
(bi_plainly P bi_plainly Q) bi_plainly (bi_plainly P Q);
bi_mixin_plainly_emp_intro P : P bi_plainly emp;
bi_mixin_plainly_absorbing P Q : bi_plainly P Q bi_plainly P;
(* Persistently *)
bi_mixin_persistently_mono P Q :
(P Q) bi_persistently P bi_persistently Q;
bi_mixin_persistently_idemp_2 P :
bi_persistently P bi_persistently (bi_persistently P);
bi_mixin_plainly_persistently_1 P :
bi_plainly (bi_persistently P) bi_plainly P;