Commit 96501a4f authored by Robbert Krebbers's avatar Robbert Krebbers Committed by Jacques-Henri Jourdan

Define `Persistent P` as `P ⊢ □ P` instead of `□ P ⊣⊢ P`.

Otherwise, ownership of cores in our ordered RA model will not be persistent.
parent 77056b1b
......@@ -38,8 +38,8 @@ Proof. intros P. rewrite /Affine. by apply bi.pure_intro. Qed.
(* Own and valid derived *)
Lemma persistently_ownM (a : M) : CoreId a uPred_ownM a uPred_ownM a.
Proof.
intros; apply (anti_symm _); first by apply: persistently_elim_absorbing.
by rewrite {1}persistently_ownM_core core_id_core.
intros; apply (anti_symm _); first 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.
Proof. by intros; rewrite ownM_valid cmra_valid_elim. Qed.
......@@ -49,7 +49,7 @@ Lemma ownM_unit' : uPred_ownM ε ⊣⊢ True.
Proof. apply (anti_symm _); first by apply pure_intro. apply ownM_empty. Qed.
Lemma persistently_cmra_valid {A : cmraT} (a : A) : a a.
Proof.
intros; apply (anti_symm _); first by apply: persistently_elim_absorbing.
intros; apply (anti_symm _); first by rewrite persistently_elim.
apply:persistently_cmra_valid_1.
Qed.
......@@ -93,7 +93,7 @@ Qed.
(* Derived lemmas for persistence *)
Global Instance limit_preserving_Persistent {A:ofeT} `{Cofe A} (Φ : A uPred M) :
NonExpansive Φ LimitPreserving (λ x, Persistent (Φ x)).
Proof. intros. apply limit_preserving_equiv; solve_proper. Qed.
Proof. intros. apply limit_preserving_entails; solve_proper. Qed.
(* Persistence *)
Global Instance cmra_valid_persistent {A : cmraT} (a : A) :
......
......@@ -200,6 +200,6 @@ Section proofmode_classes.
FromAnd (own γ a) (own γ b1) (own γ b2).
Proof.
intros ? Hb. rewrite /FromAnd (is_op a) own_op.
destruct Hb. by rewrite persistent_and_sep_l. by rewrite persistent_and_sep_r.
destruct Hb; by rewrite persistent_and_sep.
Qed.
End proofmode_classes.
......@@ -79,7 +79,7 @@ Global Instance from_sep_ownM_core_id (a b1 b2 : M) :
FromAnd (uPred_ownM a) (uPred_ownM b1) (uPred_ownM b2).
Proof.
intros ? H. rewrite /FromAnd (is_op a) ownM_op.
destruct H. by rewrite persistent_and_sep_l. by rewrite persistent_and_sep_r.
destruct H; by rewrite persistent_and_sep.
Qed.
Global Instance into_and_ownM p (a b1 b2 : M) :
......
......@@ -137,7 +137,7 @@ Section sep_list.
{ apply forall_intro=> k; apply forall_intro=> x.
apply impl_intro_l, pure_elim_l=> ?; by apply: big_sepL_lookup. }
revert Φ HΦ. induction l as [|x l IH]=> Φ HΦ; [by auto using big_sepL_nil'|].
rewrite big_sepL_cons. rewrite -persistent_and_sep_l; apply and_intro.
rewrite big_sepL_cons. rewrite -persistent_and_sep; apply and_intro.
- by rewrite (forall_elim 0) (forall_elim x) pure_True // True_impl.
- rewrite -IH. apply forall_intro=> k; by rewrite (forall_elim (S k)).
Qed.
......@@ -158,21 +158,13 @@ Section sep_list.
apply forall_intro=> k. by rewrite (forall_elim (S k)).
Qed.
Global Instance big_sepL_nil_persistent `{AffineBI PROP} Φ :
Global Instance big_sepL_nil_persistent Φ :
Persistent ([ list] kx [], Φ k x).
Proof. simpl; apply _. Qed.
Global Instance big_sepL_persistent1 Φ l :
( k x, Persistent (Φ k x))
l []
Persistent ([ list] kx l, Φ k x).
Proof.
intros. rewrite /Persistent (big_opL_commute1 bi_persistently (R:=())) //.
apply big_opL_proper=> k y ?. by apply persistent_persistently.
Qed.
Global Instance big_sepL_persistent `{AffineBI PROP} Φ l :
Global Instance big_sepL_persistent Φ l :
( k x, Persistent (Φ k x)) Persistent ([ list] kx l, Φ k x).
Proof. revert Φ. induction l as [|x l IH]=> Φ ? /=; apply _. Qed.
Global Instance big_sepL_persistent_id `{AffineBI PROP} Ps :
Global Instance big_sepL_persistent_id Ps :
TCForall Persistent Ps Persistent ([] Ps).
Proof. induction 1; simpl; apply _. Qed.
End sep_list.
......@@ -404,7 +396,7 @@ Section gmap.
{ apply forall_intro=> k; apply forall_intro=> x.
apply impl_intro_l, pure_elim_l=> ?; by apply: big_sepM_lookup. }
induction m as [|i x m ? IH] using map_ind; auto using big_sepM_empty'.
rewrite big_sepM_insert // -persistent_and_sep_l. apply and_intro.
rewrite big_sepM_insert // -persistent_and_sep. 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.
......@@ -431,15 +423,14 @@ Section gmap.
by rewrite pure_True // True_impl.
Qed.
Global Instance big_sepM_empty_persistent `{AffineBI PROP} Φ :
Global Instance big_sepM_empty_persistent Φ :
Persistent ([ map] kx , Φ k x).
Proof. rewrite /big_opM map_to_list_empty. apply _. Qed.
Global Instance big_sepM_persistent `{AffineBI PROP} Φ m :
Global Instance big_sepM_persistent Φ m :
( k x, Persistent (Φ k x)) Persistent ([ map] kx m, Φ k x).
Proof. intros. apply big_sepL_persistent=> _ [??]; apply _. Qed.
End gmap.
(** ** Big ops over finite sets *)
Section gset.
Context `{Countable A}.
......@@ -562,7 +553,7 @@ Section gset.
{ apply forall_intro=> x.
apply impl_intro_l, pure_elim_l=> ?; by apply: big_sepS_elem_of. }
induction X as [|x X ? IH] using collection_ind_L; auto using big_sepS_empty'.
rewrite big_sepS_insert // -persistent_and_sep_l. apply and_intro.
rewrite big_sepS_insert // -persistent_and_sep. apply and_intro.
- by rewrite (forall_elim x) pure_True ?True_impl; last set_solver.
- rewrite -IH. apply forall_mono=> y. apply impl_intro_l, pure_elim_l=> ?.
by rewrite pure_True ?True_impl; last set_solver.
......@@ -583,11 +574,10 @@ 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_persistent `{AffineBI PROP} Φ :
Global Instance big_sepS_empty_persistent Φ :
Persistent ([ set] x , Φ x).
Proof. rewrite /big_opS elements_empty. apply _. Qed.
Global Instance big_sepS_persistent `{AffineBI PROP} Φ X :
Global Instance big_sepS_persistent Φ X :
( x, Persistent (Φ x)) Persistent ([ set] x X, Φ x).
Proof. rewrite /big_opS. apply _. Qed.
End gset.
......@@ -658,10 +648,10 @@ Section gmultiset.
([ mset] y X, Φ y) ([ mset] y X, Φ y).
Proof. apply (big_opMS_commute _). Qed.
Global Instance big_sepMS_empty_persistent `{AffineBI PROP} Φ :
Global Instance big_sepMS_empty_persistent Φ :
Persistent ([ mset] x , Φ x).
Proof. rewrite /big_opMS gmultiset_elements_empty. apply _. Qed.
Global Instance big_sepMS_persistent `{AffineBI PROP} Φ X :
Global Instance big_sepMS_persistent Φ X :
( x, Persistent (Φ x)) Persistent ([ mset] x X, Φ x).
Proof. rewrite /big_opMS. apply _. Qed.
End gmultiset.
......
This diff is collapsed.
......@@ -51,8 +51,8 @@ Section fractional.
(** Fractional and logical connectives *)
Global Instance persistent_fractional P :
Persistent P Fractional (λ _, P).
Proof. intros HP q q'. by apply bi.persistent_sep_dup. Qed.
Persistent P Absorbing P Fractional (λ _, P).
Proof. intros ?? q q'. by apply bi.persistent_sep_dup. Qed.
Global Instance fractional_sep Φ Ψ :
Fractional Φ Fractional Ψ Fractional (λ q, Φ q Ψ q)%I.
......
......@@ -13,7 +13,7 @@ Global Instance into_internal_eq_internal_eq {A : ofeT} (x y : A) :
Proof. by rewrite /IntoInternalEq. Qed.
Global Instance into_internal_eq_persistently {A : ofeT} (x y : A) P :
IntoInternalEq P x y IntoInternalEq ( P) x y.
Proof. rewrite /IntoInternalEq=> ->. by rewrite persistently_elim_absorbing. Qed.
Proof. rewrite /IntoInternalEq=> ->. by rewrite persistently_elim. Qed.
Global Instance into_internal_eq_bare {A : ofeT} (x y : A) P :
IntoInternalEq P x y IntoInternalEq ( P) x y.
Proof. rewrite /IntoInternalEq=> ->. by rewrite bare_elim. Qed.
......@@ -87,7 +87,7 @@ Proof. rewrite /FromPure /IntoPure=> <- ->. by rewrite pure_impl impl_wand_2. Qe
Global Instance into_pure_bare P φ : IntoPure P φ IntoPure ( P) φ.
Proof. rewrite /IntoPure=> ->. apply bare_elim. Qed.
Global Instance into_pure_persistently P φ : IntoPure P φ IntoPure ( P) φ.
Proof. rewrite /IntoPure=> ->. apply: persistently_elim_absorbing. Qed.
Proof. rewrite /IntoPure=> ->. apply: persistently_elim. Qed.
(* FromPure *)
Global Instance from_pure_pure φ : @FromPure PROP ⌜φ⌝ φ.
......@@ -115,7 +115,7 @@ Proof. rewrite /FromPure=>Hx. rewrite pure_forall. by setoid_rewrite Hx. Qed.
Global Instance from_pure_pure_sep (φ1 φ2 : Prop) P1 P2 :
FromPure P1 φ1 FromPure P2 φ2 FromPure (P1 P2) (φ1 φ2).
Proof. rewrite /FromPure=> <- <-. by rewrite pure_and persistent_and_sep_l_1. Qed.
Proof. rewrite /FromPure=> <- <-. by rewrite pure_and persistent_and_sep_1. Qed.
Global Instance from_pure_pure_wand (φ1 φ2 : Prop) P1 P2 :
IntoPure P1 φ1 FromPure P2 φ2 FromPure (P1 - P2) (φ1 φ2).
Proof.
......@@ -140,7 +140,7 @@ Global Instance into_persistent_persistently P : IntoPersistent true P P | 1.
Proof. by rewrite /IntoPersistent. Qed.
Global Instance into_persistent_persistent P :
Persistent P IntoPersistent false P P | 100.
Proof. intros. by rewrite /IntoPersistent /= persistent_persistently. Qed.
Proof. intros. by rewrite /IntoPersistent. Qed.
(* FromPersistent *)
Global Instance from_persistent_persistently P : FromPersistent ( P) P | 1.
......@@ -169,7 +169,7 @@ Global Instance into_wand_impl_false_true P Q P' :
Proof.
rewrite /IntoWand /FromAssumption /= => ? HP. apply wand_intro_l.
rewrite -(bare_persistently_idemp P) HP.
by rewrite -persistently_and_bare_sep_l persistently_elim_absorbing impl_elim_r.
by rewrite -persistently_and_bare_sep_l persistently_elim impl_elim_r.
Qed.
Global Instance into_wand_impl_true_false P Q P' :
......@@ -205,7 +205,7 @@ Global Instance into_wand_persistently_true q R P Q :
Proof. by rewrite /IntoWand /= persistently_idemp. Qed.
Global Instance into_wand_persistently_false `{!AffineBI PROP} q R P Q :
IntoWand false q R P Q IntoWand false q ( R) P Q.
Proof. by rewrite /IntoWand persistently_elim_absorbing. Qed.
Proof. by rewrite /IntoWand persistently_elim. Qed.
Global Instance into_wand_bare_persistently p q R P Q :
IntoWand p q R P Q IntoWand p q ( R) P Q.
......@@ -217,17 +217,17 @@ Proof. by rewrite /FromAnd. Qed.
Global Instance from_and_sep_persistent_l P1 P1' P2 :
FromBare P1 P1' Persistent P1' FromAnd (P1 P2) P1' P2 | 9.
Proof.
rewrite /FromBare /FromAnd=> <- ?. by rewrite persistent_and_bare_sep_l.
rewrite /FromBare /FromAnd=> <- ?. by rewrite persistent_and_bare_sep_l_1.
Qed.
Global Instance from_and_sep_persistent_r P1 P2 P2' :
FromBare P2 P2' Persistent P2' FromAnd (P1 P2) P1 P2' | 10.
Proof.
rewrite /FromBare /FromAnd=> <- ?. by rewrite persistent_and_bare_sep_r.
rewrite /FromBare /FromAnd=> <- ?. by rewrite persistent_and_bare_sep_r_1.
Qed.
Global Instance from_and_sep_persistent P1 P2 :
Persistent P1 Persistent P2 FromAnd (P1 P2) P1 P2 | 11.
Proof.
rewrite /FromBare /FromAnd. intros ??. by rewrite -persistent_sep_and.
rewrite /FromBare /FromAnd. intros ??. by rewrite -persistent_and_sep_1.
Qed.
Global Instance from_and_pure φ ψ : @FromAnd PROP ⌜φ ψ⌝ ⌜φ⌝ ⌜ψ⌝.
......@@ -243,28 +243,21 @@ Global Instance from_and_persistently_sep P Q1 Q2 :
FromSep P Q1 Q2 FromAnd ( P) ( Q1) ( Q2) | 11.
Proof. rewrite /FromAnd=> <-. by rewrite -persistently_and persistently_and_sep. Qed.
Hint Extern 10 => assumption : typeclass_instances. (* TODO: move *)
Global Instance from_and_big_sepL_cons_persistent {A} (Φ : nat A PROP) x l :
Persistent (Φ 0 x)
FromAnd ([ list] k y x :: l, Φ k y) (Φ 0 x) ([ list] k y l, Φ (S k) y).
Proof. intros. by rewrite /FromAnd big_opL_cons persistent_and_sep_l_1. Qed.
Proof. intros. by rewrite /FromAnd big_opL_cons persistent_and_sep_1. Qed.
Global Instance from_and_big_sepL_app_persistent {A} (Φ : nat A PROP) l1 l2 :
( k y, Persistent (Φ k y))
FromAnd ([ list] k y l1 ++ l2, Φ k y)
([ list] k y l1, Φ k y) ([ list] k y l2, Φ (length l1 + k) y).
Proof.
intros. rewrite /FromAnd big_opL_app.
destruct (decide (l1 = [])) as [->|]; simpl.
- by rewrite left_id and_elim_r.
- by rewrite persistent_and_sep_l_1.
Qed.
Proof. intros. by rewrite /FromAnd big_opL_app persistent_and_sep_1. Qed.
(* FromSep *)
Global Instance from_sep_sep P1 P2 : FromSep (P1 P2) P1 P2 | 100.
Proof. by rewrite /FromSep. Qed.
Global Instance from_sep_and P1 P2 :
TCOr (Affine P1) (Absorbing P2) TCOr (Affine P2) (Absorbing P1)
TCOr (TCAnd (Affine P1) (Affine P2)) (TCAnd (Absorbing P1) (Absorbing P2))
FromSep (P1 P2) P1 P2 | 101.
Proof. intros. by rewrite /FromSep sep_and. Qed.
......@@ -323,18 +316,18 @@ Global Instance into_sep_and_persistent_l P P' Q :
Persistent P FromBare P' P IntoSep false (P Q) P' Q.
Proof.
rewrite /FromBare /IntoSep /=. intros ? <-.
by rewrite persistent_and_bare_sep_l.
by rewrite persistent_and_bare_sep_l_1.
Qed.
Global Instance into_sep_and_persistent_r P Q Q' :
Persistent Q FromBare Q' Q IntoSep false (P Q) P Q'.
Proof.
rewrite /FromBare /IntoSep /=. intros ? <-.
by rewrite persistent_and_bare_sep_r.
by rewrite persistent_and_bare_sep_r_1.
Qed.
Global Instance into_sep_pure p φ ψ : @IntoSep PROP p ⌜φ ψ⌝ ⌜φ⌝ ⌜ψ⌝.
Proof.
by rewrite /IntoSep pure_and persistent_and_sep_l_1 bare_persistently_if_sep.
by rewrite /IntoSep pure_and persistent_and_sep_1 bare_persistently_if_sep.
Qed.
Global Instance into_sep_bare p P Q1 Q2 :
......
......@@ -518,7 +518,7 @@ Proof.
rewrite right_id. apply impl_intro_l. rewrite bare_and_l persistently_and_sep_r_1.
by rewrite bare_sep bare_persistently_elim bare_elim wand_elim_r.
- apply impl_intro_l. rewrite envs_app_sound //; simpl.
by rewrite persistent_and_sep_l_1 right_id wand_elim_r.
by rewrite persistent_and_sep_1 right_id wand_elim_r.
Qed.
Lemma tac_impl_intro_persistent Δ Δ' i P P' Q :
IntoPersistent false P P'
......@@ -635,11 +635,11 @@ Proof.
intros [? ->]%envs_lookup_delete_Some ??? HP1 <-.
rewrite envs_lookup_sound //.
rewrite -(idemp bi_and (envs_delete _ _ _)).
rewrite {2}envs_simple_replace_sound' //; simpl.
rewrite {1}HP1 persistent_and_bare_sep_l -(persistent_persistently P1) assoc.
rewrite {2}envs_simple_replace_sound' //; rewrite /= right_id.
rewrite {1}HP1 (persistent_persistently_2 P1) persistently_and_bare_sep_l assoc.
rewrite -bare_persistently_if_idemp -bare_persistently_idemp.
rewrite (bare_persistently_bare_persistently_if q) -bare_persistently_if_sep.
by rewrite into_wand wand_elim_l right_id wand_elim_r.
by rewrite into_wand wand_elim_l wand_elim_r.
Qed.
Lemma tac_specialize_persistent_helper Δ Δ'' j q P R R' Q :
......@@ -709,7 +709,8 @@ Lemma tac_assert_persistent Δ Δ1 Δ2 Δ' lr js j P P' Q :
(Δ1 P) (Δ' Q) Δ Q.
Proof.
intros ???? HP <-. rewrite -(idemp bi_and Δ) {1}envs_split_sound //.
rewrite HP sep_elim_l persistent_and_bare_sep_l from_bare.
rewrite HP. rewrite (persistent_persistently_2 P) sep_elim_l.
rewrite persistently_and_bare_sep_l -bare_idemp bare_persistently_elim from_bare.
rewrite envs_app_sound //; simpl.
by rewrite right_id wand_elim_r.
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