Commit 58b8eafa authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan

Renaming: sink->absorbingly bare->affinely.

parent a38db108
......@@ -36,9 +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 bare_persistently_ownM (a : M) : CoreId a uPred_ownM a uPred_ownM a.
Lemma affinely_persistently_ownM (a : M) : CoreId a uPred_ownM a uPred_ownM a.
Proof.
rewrite affine_bare=>?; apply (anti_symm _); [by rewrite persistently_elim|].
rewrite affine_affinely=>?; apply (anti_symm _); [by rewrite persistently_elim|].
by rewrite {1}persistently_ownM_core core_id_core.
Qed.
Lemma ownM_invalid (a : M) : ¬ {0} a uPred_ownM a False.
......@@ -47,9 +47,9 @@ 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 bare_persistently_cmra_valid {A : cmraT} (a : A) : a a.
Lemma affinely_persistently_cmra_valid {A : cmraT} (a : A) : a a.
Proof.
rewrite affine_bare. intros; apply (anti_symm _); first by rewrite persistently_elim.
rewrite affine_affinely. intros; apply (anti_symm _); first by rewrite persistently_elim.
apply:persistently_cmra_valid_1.
Qed.
......
......@@ -157,14 +157,14 @@ Section proofmode_classes.
IntoWand false false R P Q
IntoWand p q (|={E}=> R) (|={E}=> P) (|={E}=> Q).
Proof.
rewrite /IntoWand /= => HR. rewrite !bare_persistently_if_elim HR.
rewrite /IntoWand /= => HR. rewrite !affinely_persistently_if_elim HR.
apply wand_intro_l. by rewrite fupd_sep wand_elim_r.
Qed.
Global Instance into_wand_fupd_persistent E1 E2 p q R P Q :
IntoWand false q R P Q IntoWand p q (|={E1,E2}=> R) P (|={E1,E2}=> Q).
Proof.
rewrite /IntoWand /= => HR. rewrite bare_persistently_if_elim HR.
rewrite /IntoWand /= => HR. rewrite affinely_persistently_if_elim HR.
apply wand_intro_l. by rewrite fupd_frame_l wand_elim_r.
Qed.
......@@ -172,7 +172,7 @@ Section proofmode_classes.
IntoWand p false R P Q IntoWand' p q R (|={E1,E2}=> P) (|={E1,E2}=> Q).
Proof.
rewrite /IntoWand' /IntoWand /= => ->.
apply wand_intro_l. by rewrite bare_persistently_if_elim fupd_wand_r.
apply wand_intro_l. by rewrite affinely_persistently_if_elim fupd_wand_r.
Qed.
Global Instance from_sep_fupd E P Q1 Q2 :
......
......@@ -82,7 +82,7 @@ Proof. iIntros "!# HP". by iApply inv_alloc. Qed.
Lemma wand_fupd_alt E1 E2 P Q : (P ={E1,E2}= Q) R, R (P R ={E1,E2}=> Q).
Proof.
rewrite bi.wand_alt. do 2 f_equiv. setoid_rewrite bi.affine_bare; last apply _.
rewrite bi.wand_alt. do 2 f_equiv. setoid_rewrite bi.affine_affinely; last apply _.
by rewrite bi.persistently_impl_wand.
Qed.
End vs.
......@@ -31,14 +31,14 @@ Qed.
Global Instance into_wand_bupd p q R P Q :
IntoWand false false R P Q IntoWand p q (|==> R) (|==> P) (|==> Q).
Proof.
rewrite /IntoWand /= => HR. rewrite !bare_persistently_if_elim HR.
rewrite /IntoWand /= => HR. rewrite !affinely_persistently_if_elim HR.
apply wand_intro_l. by rewrite bupd_sep wand_elim_r.
Qed.
Global Instance into_wand_bupd_persistent p q R P Q :
IntoWand false q R P Q IntoWand p q (|==> R) P (|==> Q).
Proof.
rewrite /IntoWand /= => HR. rewrite bare_persistently_if_elim HR.
rewrite /IntoWand /= => HR. rewrite affinely_persistently_if_elim HR.
apply wand_intro_l. by rewrite bupd_frame_l wand_elim_r.
Qed.
......@@ -46,7 +46,7 @@ Global Instance into_wand_bupd_args p q R P Q :
IntoWand p false R P Q IntoWand' p q R (|==> P) (|==> Q).
Proof.
rewrite /IntoWand' /IntoWand /= => ->.
apply wand_intro_l. by rewrite bare_persistently_if_elim bupd_wand_r.
apply wand_intro_l. by rewrite affinely_persistently_if_elim bupd_wand_r.
Qed.
(* FromOp *)
......@@ -85,7 +85,7 @@ Qed.
Global Instance into_and_ownM p (a b1 b2 : M) :
IsOp a b1 b2 IntoAnd p (uPred_ownM a) (uPred_ownM b1) (uPred_ownM b2).
Proof.
intros. apply bare_persistently_if_mono. by rewrite (is_op a) ownM_op sep_and.
intros. apply affinely_persistently_if_mono. by rewrite (is_op a) ownM_op sep_and.
Qed.
Global Instance into_sep_ownM (a b1 b2 : M) :
......
......@@ -150,12 +150,12 @@ Section sep_list.
Proof.
apply wand_intro_l. revert Φ Ψ. induction l as [|x l IH]=> Φ Ψ /=.
{ by rewrite sep_elim_r. }
rewrite bare_persistently_sep_dup -assoc [( _ _)%I]comm -!assoc assoc.
rewrite affinely_persistently_sep_dup -assoc [( _ _)%I]comm -!assoc assoc.
apply sep_mono.
- rewrite (forall_elim 0) (forall_elim x) pure_True // True_impl.
by rewrite bare_persistently_elim wand_elim_l.
by rewrite affinely_persistently_elim wand_elim_l.
- rewrite comm -(IH (Φ S) (Ψ S)) /=.
apply sep_mono_l, bare_mono, persistently_mono.
apply sep_mono_l, affinely_mono, persistently_mono.
apply forall_intro=> k. by rewrite (forall_elim (S k)).
Qed.
......@@ -424,12 +424,12 @@ Section gmap.
Proof.
apply wand_intro_l. induction m as [|i x m ? IH] using map_ind.
{ by rewrite sep_elim_r. }
rewrite !big_sepM_insert // bare_persistently_sep_dup.
rewrite !big_sepM_insert // affinely_persistently_sep_dup.
rewrite -assoc [( _ _)%I]comm -!assoc assoc. apply sep_mono.
- rewrite (forall_elim i) (forall_elim x) pure_True ?lookup_insert //.
by rewrite True_impl bare_persistently_elim wand_elim_l.
by rewrite True_impl affinely_persistently_elim wand_elim_l.
- rewrite comm -IH /=.
apply sep_mono_l, bare_mono, persistently_mono, forall_mono=> k.
apply sep_mono_l, affinely_mono, persistently_mono, 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.
......@@ -585,11 +585,11 @@ Section gset.
Proof.
apply wand_intro_l. induction X as [|x X ? IH] using collection_ind_L.
{ by rewrite sep_elim_r. }
rewrite !big_sepS_insert // bare_persistently_sep_dup.
rewrite !big_sepS_insert // affinely_persistently_sep_dup.
rewrite -assoc [( _ _)%I]comm -!assoc assoc. apply sep_mono.
- rewrite (forall_elim x) pure_True; last set_solver.
by rewrite True_impl bare_persistently_elim wand_elim_l.
- rewrite comm -IH /=. apply sep_mono_l, bare_mono, persistently_mono.
by rewrite True_impl affinely_persistently_elim wand_elim_l.
- rewrite comm -IH /=. apply sep_mono_l, affinely_mono, persistently_mono.
apply forall_mono=> y. apply impl_intro_l, pure_elim_l=> ?.
by rewrite pure_True ?True_impl; last set_solver.
Qed.
......
This diff is collapsed.
......@@ -173,6 +173,6 @@ Section fractional.
- rewrite fractional /Frame /MakeSep=><-<-. by rewrite assoc.
- rewrite fractional /Frame /MakeSep=><-<-=>_.
by rewrite (comm _ Q (Φ q0)) !assoc (comm _ (Φ _)).
- move=>-[-> _]->. by rewrite bi.bare_persistently_if_elim -fractional Qp_div_2.
- move=>-[-> _]->. by rewrite bi.affinely_persistently_if_elim -fractional Qp_div_2.
Qed.
End fractional.
......@@ -37,7 +37,7 @@ Global Instance ht_proper E :
Proof. solve_proper. Qed.
Lemma ht_mono E P P' Φ Φ' e :
(P P') ( v, Φ' v Φ v) {{ P' }} e @ E {{ Φ' }} {{ P }} e @ E {{ Φ }}.
Proof. intros. by apply bare_mono, persistently_mono, wand_mono, wp_mono. Qed.
Proof. intros. by apply affinely_mono, persistently_mono, wand_mono, wp_mono. Qed.
Global Instance ht_mono' E :
Proper (flip () ==> eq ==> pointwise_relation _ () ==> ()) (ht E).
Proof. solve_proper. Qed.
......
This diff is collapsed.
......@@ -56,23 +56,23 @@ Arguments into_persistent {_} _ _%I _%I {_}.
Hint Mode IntoPersistent + + ! - : typeclass_instances.
Class FromPersistent {PROP : bi} (a p : bool) (P Q : PROP) :=
from_persistent : bi_bare_if a (bi_persistently_if p Q) P.
from_persistent : bi_affinely_if a (bi_persistently_if p Q) P.
Arguments FromPersistent {_} _ _ _%I _%I : simpl never.
Arguments from_persistent {_} _ _ _%I _%I {_}.
Hint Mode FromPersistent + - - ! - : typeclass_instances.
Class FromBare {PROP : bi} (P Q : PROP) :=
from_bare : bi_bare Q P.
Arguments FromBare {_} _%I _%type_scope : simpl never.
Arguments from_bare {_} _%I _%type_scope {_}.
Hint Mode FromBare + ! - : typeclass_instances.
Hint Mode FromBare + - ! : typeclass_instances.
Class IntoSink {PROP : bi} (P Q : PROP) := into_sink : P Q.
Arguments IntoSink {_} _%I _%I.
Arguments into_sink {_} _%I _%I {_}.
Hint Mode IntoSink + ! - : typeclass_instances.
Hint Mode IntoSink + - ! : typeclass_instances.
Class FromAffinely {PROP : bi} (P Q : PROP) :=
from_affinely : bi_affinely Q P.
Arguments FromAffinely {_} _%I _%type_scope : simpl never.
Arguments from_affinely {_} _%I _%type_scope {_}.
Hint Mode FromAffinely + ! - : typeclass_instances.
Hint Mode FromAffinely + - ! : typeclass_instances.
Class IntoAbsorbingly {PROP : bi} (P Q : PROP) := into_absorbingly : P Q.
Arguments IntoAbsorbingly {_} _%I _%I.
Arguments into_absorbingly {_} _%I _%I {_}.
Hint Mode IntoAbsorbingly + ! - : typeclass_instances.
Hint Mode IntoAbsorbingly + - ! : typeclass_instances.
Class IntoInternalEq {PROP : bi} {A : ofeT} (P : PROP) (x y : A) :=
into_internal_eq : P x y.
......
This diff is collapsed.
......@@ -1269,8 +1269,8 @@ Instance copy_destruct_impl {PROP : bi} (P Q : PROP) :
CopyDestruct Q CopyDestruct (P Q).
Instance copy_destruct_wand {PROP : bi} (P Q : PROP) :
CopyDestruct Q CopyDestruct (P - Q).
Instance copy_destruct_bare {PROP : bi} (P : PROP) :
CopyDestruct P CopyDestruct (bi_bare P).
Instance copy_destruct_affinely {PROP : bi} (P : PROP) :
CopyDestruct P CopyDestruct (bi_affinely P).
Instance copy_destruct_persistently {PROP : bi} (P : PROP) :
CopyDestruct P CopyDestruct (bi_persistently P).
......@@ -1771,7 +1771,7 @@ Hint Extern 1 (of_envs _ ⊢ _ ∧ _) => iSplit.
Hint Extern 1 (of_envs _ _ _) => iSplit.
Hint Extern 1 (of_envs _ _) => iNext.
Hint Extern 1 (of_envs _ bi_persistently _) => iAlways.
Hint Extern 1 (of_envs _ bi_bare _) => iAlways.
Hint Extern 1 (of_envs _ bi_affinely _) => iAlways.
Hint Extern 1 (of_envs _ _, _) => iExists _.
Hint Extern 1 (of_envs _ _) => iModIntro.
Hint Extern 1 (of_envs _ _ _) => iLeft.
......
......@@ -44,7 +44,7 @@ Lemma test_unfold_constants : bar.
Proof. iIntros (P) "HP //". Qed.
Lemma test_iRewrite {A : ofeT} (x y : A) P :
( z, P - bi_bare (z y)) - (P - P (x,x) (y,x)).
( z, P - bi_affinely (z y)) - (P - P (x,x) (y,x)).
Proof.
iIntros "#H1 H2".
iRewrite (bi.internal_eq_sym x x with "[# //]").
......@@ -53,7 +53,7 @@ Proof.
Qed.
Lemma test_iDestruct_and_emp P Q `{!Persistent P, !Persistent Q} :
P emp - emp Q - bi_bare (P Q).
P emp - emp Q - bi_affinely (P Q).
Proof. iIntros "[#? _] [_ #?]". auto. Qed.
Lemma test_iIntros_persistent P Q `{!Persistent Q} : (P Q P Q)%I.
......@@ -110,17 +110,18 @@ Lemma test_iSpecialize_tc P : (∀ x y z : gset positive, P) -∗ P.
Proof. iIntros "H". iSpecialize ("H" $! {[ 1%positive ]} ). done. Qed.
Lemma test_iFrame_pure {A : ofeT} (φ : Prop) (y z : A) :
φ bi_bare y z - ( φ φ y z : PROP).
φ bi_affinely y z - ( φ φ y z : PROP).
Proof. iIntros (Hv) "#Hxy". iFrame (Hv) "Hxy". Qed.
Lemma test_iAssert_modality P : False - P.
Proof.
iIntros "HF".
iAssert (bi_bare False)%I with "[> -]" as %[].
iAssert (bi_affinely False)%I with "[> -]" as %[].
by iMod "HF".
Qed.
Lemma test_iMod_bare_timeless P `{!Timeless P} : bi_bare ( P) - bi_bare P.
Lemma test_iMod_affinely_timeless P `{!Timeless P} :
bi_affinely ( P) - bi_affinely P.
Proof. iIntros "H". iMod "H". done. Qed.
Lemma test_iAssumption_False P : False - P.
......@@ -220,7 +221,8 @@ Lemma test_iIntros_let P :
Q, let R := emp%I in P - R - Q - P Q.
Proof. iIntros (Q R) "$ _ $". Qed.
Lemma test_foo P Q : bi_bare ( (Q P)) - bi_bare ( Q) - bi_bare ( P).
Lemma test_foo P Q :
bi_affinely ( (Q P)) - bi_affinely ( Q) - bi_affinely ( P).
Proof.
iIntros "#HPQ HQ !#". iNext. by iRewrite "HPQ" in "HQ".
Qed.
......@@ -234,10 +236,10 @@ Proof.
Qed.
Lemma test_iNext_affine P Q :
bi_bare ( (Q P)) - bi_bare ( Q) - bi_bare ( P).
bi_affinely ( (Q P)) - bi_affinely ( Q) - bi_affinely ( P).
Proof. iIntros "#HPQ HQ !#". iNext. by iRewrite "HPQ" in "HQ". Qed.
Lemma test_iAlways P Q R :
P - bi_persistently Q R - bi_persistently (bi_bare (bi_bare P)) Q.
P - bi_persistently Q R - bi_persistently (bi_affinely (bi_affinely P)) Q.
Proof. iIntros "#HP #HQ HR". iSplitL. iAlways. done. iAlways. done. Qed.
End tests.
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