Commit 2a92f265 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Replace/remove some occurences of `persistently` into `persistent` where the...

Replace/remove some occurences of `persistently` into `persistent` where the property instead of the modality is used.
parent b4567fbd
...@@ -134,7 +134,7 @@ Section list. ...@@ -134,7 +134,7 @@ Section list.
apply impl_intro_l, pure_elim_l=> ?; by apply big_sepL_lookup. } apply impl_intro_l, pure_elim_l=> ?; by apply big_sepL_lookup. }
revert Φ HΦ. induction l as [|x l IH]=> Φ HΦ. revert Φ HΦ. induction l as [|x l IH]=> Φ HΦ.
{ rewrite big_sepL_nil; auto with I. } { rewrite big_sepL_nil; auto with I. }
rewrite big_sepL_cons. rewrite -persistently_and_sep_l; apply and_intro. rewrite big_sepL_cons. rewrite -and_sep_l; apply and_intro.
- by rewrite (forall_elim 0) (forall_elim x) pure_True // True_impl. - by rewrite (forall_elim 0) (forall_elim x) pure_True // True_impl.
- rewrite -IH. apply forall_intro=> k; by rewrite (forall_elim (S k)). - rewrite -IH. apply forall_intro=> k; by rewrite (forall_elim (S k)).
Qed. Qed.
...@@ -146,7 +146,7 @@ Section list. ...@@ -146,7 +146,7 @@ Section list.
rewrite persistently_and_sep_l. do 2 setoid_rewrite persistently_forall. rewrite persistently_and_sep_l. do 2 setoid_rewrite persistently_forall.
setoid_rewrite persistently_impl; setoid_rewrite persistently_pure. setoid_rewrite persistently_impl; setoid_rewrite persistently_pure.
rewrite -big_sepL_forall -big_sepL_sepL. apply big_sepL_mono; auto=> k x ?. rewrite -big_sepL_forall -big_sepL_sepL. apply big_sepL_mono; auto=> k x ?.
by rewrite -persistently_wand_impl persistently_elim wand_elim_l. by rewrite persistently_impl_wand persistently_elim wand_elim_l.
Qed. Qed.
Global Instance big_sepL_nil_persistent Φ : Global Instance big_sepL_nil_persistent Φ :
...@@ -323,7 +323,7 @@ Section gmap. ...@@ -323,7 +323,7 @@ Section gmap.
{ apply forall_intro=> k; apply forall_intro=> x. { apply forall_intro=> k; apply forall_intro=> x.
apply impl_intro_l, pure_elim_l=> ?; by apply big_sepM_lookup. } apply impl_intro_l, pure_elim_l=> ?; by apply big_sepM_lookup. }
induction m as [|i x m ? IH] using map_ind; [rewrite ?big_sepM_empty; auto|]. induction m as [|i x m ? IH] using map_ind; [rewrite ?big_sepM_empty; auto|].
rewrite big_sepM_insert // -persistently_and_sep_l. apply and_intro. rewrite big_sepM_insert // -and_sep_l. apply and_intro.
- rewrite (forall_elim i) (forall_elim x) lookup_insert. - rewrite (forall_elim i) (forall_elim x) lookup_insert.
by rewrite pure_True // True_impl. by rewrite pure_True // True_impl.
- rewrite -IH. apply forall_mono=> k; apply forall_mono=> y. - rewrite -IH. apply forall_mono=> k; apply forall_mono=> y.
...@@ -339,7 +339,7 @@ Section gmap. ...@@ -339,7 +339,7 @@ Section gmap.
rewrite persistently_and_sep_l. do 2 setoid_rewrite persistently_forall. rewrite persistently_and_sep_l. do 2 setoid_rewrite persistently_forall.
setoid_rewrite persistently_impl; setoid_rewrite persistently_pure. setoid_rewrite persistently_impl; setoid_rewrite persistently_pure.
rewrite -big_sepM_forall -big_sepM_sepM. apply big_sepM_mono; auto=> k x ?. rewrite -big_sepM_forall -big_sepM_sepM. apply big_sepM_mono; auto=> k x ?.
by rewrite -persistently_wand_impl persistently_elim wand_elim_l. by rewrite persistently_impl_wand persistently_elim wand_elim_l.
Qed. Qed.
Global Instance big_sepM_empty_persistent Φ : Global Instance big_sepM_empty_persistent Φ :
...@@ -475,7 +475,7 @@ Section gset. ...@@ -475,7 +475,7 @@ Section gset.
apply impl_intro_l, pure_elim_l=> ?; by apply big_sepS_elem_of. } apply impl_intro_l, pure_elim_l=> ?; by apply big_sepS_elem_of. }
induction X as [|x X ? IH] using collection_ind_L. induction X as [|x X ? IH] using collection_ind_L.
{ rewrite big_sepS_empty; auto. } { rewrite big_sepS_empty; auto. }
rewrite big_sepS_insert // -persistently_and_sep_l. apply and_intro. rewrite big_sepS_insert // -and_sep_l. apply and_intro.
- by rewrite (forall_elim x) pure_True ?True_impl; last set_solver. - 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=> ?. - rewrite -IH. apply forall_mono=> y. apply impl_intro_l, pure_elim_l=> ?.
by rewrite pure_True ?True_impl; last set_solver. by rewrite pure_True ?True_impl; last set_solver.
...@@ -487,7 +487,7 @@ Section gset. ...@@ -487,7 +487,7 @@ Section gset.
rewrite persistently_and_sep_l persistently_forall. rewrite persistently_and_sep_l persistently_forall.
setoid_rewrite persistently_impl; setoid_rewrite persistently_pure. setoid_rewrite persistently_impl; setoid_rewrite persistently_pure.
rewrite -big_sepS_forall -big_sepS_sepS. apply big_sepS_mono; auto=> x ?. rewrite -big_sepS_forall -big_sepS_sepS. apply big_sepS_mono; auto=> x ?.
by rewrite -persistently_wand_impl persistently_elim wand_elim_l. by rewrite persistently_impl_wand persistently_elim wand_elim_l.
Qed. Qed.
Global Instance big_sepS_empty_persistent Φ : Persistent ([ set] x , Φ x). Global Instance big_sepS_empty_persistent Φ : Persistent ([ set] x , Φ x).
......
...@@ -432,7 +432,7 @@ Qed. ...@@ -432,7 +432,7 @@ Qed.
Lemma sep_and P Q : (P Q) (P Q). Lemma sep_and P Q : (P Q) (P Q).
Proof. auto. Qed. Proof. auto. Qed.
Lemma impl_wand P Q : (P Q) P - Q. Lemma impl_wand_1 P Q : (P Q) P - Q.
Proof. apply wand_intro_r, impl_elim with P; auto. Qed. Proof. apply wand_intro_r, impl_elim with P; auto. Qed.
Lemma pure_elim_sep_l φ Q R : (φ Q R) ⌜φ⌝ Q R. Lemma pure_elim_sep_l φ Q R : (φ Q R) ⌜φ⌝ Q R.
Proof. intros; apply pure_elim with φ; eauto. Qed. Proof. intros; apply pure_elim with φ; eauto. Qed.
...@@ -518,38 +518,38 @@ Proof. ...@@ -518,38 +518,38 @@ Proof.
rewrite -(internal_eq_refl a) persistently_pure; auto. rewrite -(internal_eq_refl a) persistently_pure; auto.
Qed. Qed.
Lemma persistently_and_sep_l' P Q : P Q P Q. Lemma persistently_and_sep_l P Q : P Q P Q.
Proof. apply (anti_symm ()); auto using persistently_and_sep_l_1. Qed. Proof. apply (anti_symm ()); auto using persistently_and_sep_l_1. Qed.
Lemma persistently_and_sep_r' P Q : P Q P Q. Lemma persistently_and_sep_r P Q : P Q P Q.
Proof. by rewrite !(comm _ P) persistently_and_sep_l'. Qed. Proof. by rewrite !(comm _ P) persistently_and_sep_l. Qed.
Lemma persistently_sep_dup' P : P P P. Lemma persistently_sep_dup P : P P P.
Proof. by rewrite -persistently_and_sep_l' idemp. Qed. Proof. by rewrite -persistently_and_sep_l idemp. Qed.
Lemma persistently_and_sep P Q : (P Q) (P Q). Lemma persistently_and_sep P Q : (P Q) (P Q).
Proof. Proof.
apply (anti_symm ()); auto. apply (anti_symm ()); auto.
rewrite -{1}persistently_idemp persistently_and persistently_and_sep_l'; auto. rewrite -{1}persistently_idemp persistently_and persistently_and_sep_l; auto.
Qed. Qed.
Lemma persistently_sep P Q : (P Q) P Q. Lemma persistently_sep P Q : (P Q) P Q.
Proof. by rewrite -persistently_and_sep -persistently_and_sep_l' persistently_and. Qed. Proof. by rewrite -persistently_and_sep -persistently_and_sep_l persistently_and. Qed.
Lemma persistently_wand P Q : (P - Q) P - Q. Lemma persistently_wand P Q : (P - Q) P - Q.
Proof. by apply wand_intro_r; rewrite -persistently_sep wand_elim_l. Qed. Proof. by apply wand_intro_r; rewrite -persistently_sep wand_elim_l. Qed.
Lemma persistently_wand_impl P Q : (P - Q) (P Q). Lemma persistently_impl_wand P Q : (P Q) (P - Q).
Proof. Proof.
apply (anti_symm ()); [|by rewrite -impl_wand]. apply (anti_symm ()); [by rewrite -impl_wand_1|].
apply persistently_intro', impl_intro_r. apply persistently_intro', impl_intro_r.
by rewrite persistently_and_sep_l' persistently_elim wand_elim_l. by rewrite persistently_and_sep_l persistently_elim wand_elim_l.
Qed. Qed.
Lemma wand_impl_persistently P Q : (( P) - Q) (( P) Q). Lemma impl_wand_persistently P Q : ( P Q) ( P - Q).
Proof. Proof.
apply (anti_symm ()); [|by rewrite -impl_wand]. apply (anti_symm ()); [by rewrite -impl_wand_1|].
apply impl_intro_l. by rewrite persistently_and_sep_l' wand_elim_r. apply impl_intro_l. by rewrite persistently_and_sep_l wand_elim_r.
Qed. Qed.
Lemma persistently_entails_l' P Q : (P Q) P Q P. Lemma persistently_entails_l P Q : (P Q) P Q P.
Proof. intros; rewrite -persistently_and_sep_l'; auto. Qed. Proof. intros; rewrite -persistently_and_sep_l; auto. Qed.
Lemma persistently_entails_r' P Q : (P Q) P P Q. Lemma persistently_entails_r P Q : (P Q) P P Q.
Proof. intros; rewrite -persistently_and_sep_r'; auto. Qed. Proof. intros; rewrite -persistently_and_sep_r; auto. Qed.
Lemma persistently_laterN n P : ^n P ^n P. Lemma persistently_laterN n P : ^n P ^n P.
Proof. induction n as [|n IH]; simpl; auto. by rewrite persistently_later IH. Qed. Proof. induction n as [|n IH]; simpl; auto. by rewrite persistently_later IH. Qed.
...@@ -560,7 +560,7 @@ Proof. ...@@ -560,7 +560,7 @@ Proof.
- rewrite -(right_id True%I uPred_sep (P - Q)%I) -(exist_intro (P - Q)%I). - rewrite -(right_id True%I uPred_sep (P - Q)%I) -(exist_intro (P - Q)%I).
apply sep_mono_r. rewrite -persistently_pure. apply persistently_mono, impl_intro_l. apply sep_mono_r. rewrite -persistently_pure. apply persistently_mono, impl_intro_l.
by rewrite wand_elim_r right_id. by rewrite wand_elim_r right_id.
- apply exist_elim=> R. apply wand_intro_l. rewrite assoc -persistently_and_sep_r'. - apply exist_elim=> R. apply wand_intro_l. rewrite assoc -persistently_and_sep_r.
by rewrite persistently_elim impl_elim_r. by rewrite persistently_elim impl_elim_r.
Qed. Qed.
Lemma impl_alt P Q : (P Q) R, R (P R - Q). Lemma impl_alt P Q : (P Q) R, R (P R - Q).
...@@ -569,7 +569,7 @@ Proof. ...@@ -569,7 +569,7 @@ Proof.
- rewrite -(right_id True%I uPred_and (P Q)%I) -(exist_intro (P Q)%I). - rewrite -(right_id True%I uPred_and (P Q)%I) -(exist_intro (P Q)%I).
apply and_mono_r. rewrite -persistently_pure. apply persistently_mono, wand_intro_l. apply and_mono_r. rewrite -persistently_pure. apply persistently_mono, wand_intro_l.
by rewrite impl_elim_r right_id. by rewrite impl_elim_r right_id.
- apply exist_elim=> R. apply impl_intro_l. rewrite assoc persistently_and_sep_r'. - apply exist_elim=> R. apply impl_intro_l. rewrite assoc persistently_and_sep_r.
by rewrite persistently_elim wand_elim_r. by rewrite persistently_elim wand_elim_r.
Qed. Qed.
...@@ -727,7 +727,7 @@ Lemma except_0_sep P Q : ◇ (P ∗ Q) ⊣⊢ ◇ P ∗ ◇ Q. ...@@ -727,7 +727,7 @@ Lemma except_0_sep P Q : ◇ (P ∗ Q) ⊣⊢ ◇ P ∗ ◇ Q.
Proof. Proof.
rewrite /uPred_except_0. apply (anti_symm _). rewrite /uPred_except_0. apply (anti_symm _).
- apply or_elim; last by auto. - apply or_elim; last by auto.
by rewrite -!or_intro_l -persistently_pure -persistently_later -persistently_sep_dup'. by rewrite -!or_intro_l -persistently_pure -persistently_later -persistently_sep_dup.
- rewrite sep_or_r sep_elim_l sep_or_l; auto. - rewrite sep_or_r sep_elim_l sep_or_l; auto.
Qed. Qed.
Lemma except_0_forall {A} (Φ : A uPred M) : ( a, Φ a) a, Φ a. Lemma except_0_forall {A} (Φ : A uPred M) : ( a, Φ a) a, Φ a.
...@@ -823,8 +823,8 @@ Proof. ...@@ -823,8 +823,8 @@ Proof.
apply or_mono, wand_intro_l; first done. apply or_mono, wand_intro_l; first done.
rewrite -{2}(löb Q); apply impl_intro_l. rewrite -{2}(löb Q); apply impl_intro_l.
rewrite HQ /uPred_except_0 !and_or_r. apply or_elim; last auto. rewrite HQ /uPred_except_0 !and_or_r. apply or_elim; last auto.
rewrite -(persistently_pure) -persistently_later persistently_and_sep_l'. rewrite -(persistently_pure) -persistently_later persistently_and_sep_l.
by rewrite assoc (comm _ _ P) -assoc -persistently_and_sep_l' impl_elim_r wand_elim_r. by rewrite assoc (comm _ _ P) -assoc -persistently_and_sep_l impl_elim_r wand_elim_r.
Qed. Qed.
Global Instance forall_timeless {A} (Ψ : A uPred M) : Global Instance forall_timeless {A} (Ψ : A uPred M) :
( x, Timeless (Ψ x)) Timeless ( x, Ψ x). ( x, Timeless (Ψ x)) Timeless ( x, Ψ x).
...@@ -867,26 +867,26 @@ Global Instance limit_preserving_Persistent {A:ofeT} `{Cofe A} (Φ : A → uPred ...@@ -867,26 +867,26 @@ Global Instance limit_preserving_Persistent {A:ofeT} `{Cofe A} (Φ : A → uPred
NonExpansive Φ LimitPreserving (λ x, Persistent (Φ x)). NonExpansive Φ LimitPreserving (λ x, Persistent (Φ x)).
Proof. intros. apply limit_preserving_entails; solve_proper. Qed. Proof. intros. apply limit_preserving_entails; solve_proper. Qed.
Lemma persistently_persistently P `{!Persistent P} : P P. Lemma persistent_persistently P `{!Persistent P} : P P.
Proof. apply (anti_symm ()); auto using persistently_elim. Qed. Proof. apply (anti_symm ()); auto using persistently_elim. Qed.
Lemma persistently_if_persistently p P `{!Persistent P} : ?p P P. Lemma persistent_persistently_if p P `{!Persistent P} : ?p P P.
Proof. destruct p; simpl; auto using persistently_persistently. Qed. Proof. destruct p; simpl; auto using persistent_persistently. Qed.
Lemma persistently_intro P Q `{!Persistent P} : (P Q) P Q. Lemma persistently_intro P Q `{!Persistent P} : (P Q) P Q.
Proof. rewrite -(persistently_persistently P); apply persistently_intro'. Qed. Proof. rewrite -(persistent_persistently P); apply persistently_intro'. Qed.
Lemma persistently_and_sep_l P Q `{!Persistent P} : P Q P Q. Lemma and_sep_l P Q `{!Persistent P} : P Q P Q.
Proof. by rewrite -(persistently_persistently P) persistently_and_sep_l'. Qed. Proof. by rewrite -(persistent_persistently P) persistently_and_sep_l. Qed.
Lemma persistently_and_sep_r P Q `{!Persistent Q} : P Q P Q. Lemma and_sep_r P Q `{!Persistent Q} : P Q P Q.
Proof. by rewrite -(persistently_persistently Q) persistently_and_sep_r'. Qed. Proof. by rewrite -(persistent_persistently Q) persistently_and_sep_r. Qed.
Lemma persistently_sep_dup P `{!Persistent P} : P P P. Lemma sep_dup P `{!Persistent P} : P P P.
Proof. by rewrite -(persistently_persistently P) -persistently_sep_dup'. Qed. Proof. by rewrite -(persistent_persistently P) -persistently_sep_dup. Qed.
Lemma persistently_entails_l P Q `{!Persistent Q} : (P Q) P Q P. Lemma sep_entails_l P Q `{!Persistent Q} : (P Q) P Q P.
Proof. by rewrite -(persistently_persistently Q); apply persistently_entails_l'. Qed. Proof. by rewrite -(persistent_persistently Q); apply persistently_entails_l. Qed.
Lemma persistently_entails_r P Q `{!Persistent Q} : (P Q) P P Q. Lemma sep_entails_r P Q `{!Persistent Q} : (P Q) P P Q.
Proof. by rewrite -(persistently_persistently Q); apply persistently_entails_r'. Qed. Proof. by rewrite -(persistent_persistently Q); apply persistently_entails_r. Qed.
Lemma persistently_impl_wand P `{!Persistent P} Q : (P Q) (P - Q). Lemma impl_wand P `{!Persistent P} Q : (P Q) (P - Q).
Proof. Proof.
apply (anti_symm _); auto using impl_wand. apply (anti_symm _); auto using impl_wand_1.
apply impl_intro_l. by rewrite persistently_and_sep_l wand_elim_r. apply impl_intro_l. by rewrite and_sep_l wand_elim_r.
Qed. Qed.
(* Persistence *) (* Persistence *)
...@@ -900,7 +900,7 @@ Qed. ...@@ -900,7 +900,7 @@ Qed.
Global Instance pure_wand_persistent φ Q : Global Instance pure_wand_persistent φ Q :
Persistent Q Persistent (⌜φ⌝ - Q)%I. Persistent Q Persistent (⌜φ⌝ - Q)%I.
Proof. Proof.
rewrite /Persistent -persistently_impl_wand pure_impl_forall persistently_forall. rewrite /Persistent -impl_wand pure_impl_forall persistently_forall.
auto using forall_mono. auto using forall_mono.
Qed. Qed.
Global Instance persistently_persistent P : Persistent ( P). Global Instance persistently_persistent P : Persistent ( P).
......
...@@ -51,7 +51,7 @@ Section fractional. ...@@ -51,7 +51,7 @@ Section fractional.
(** Fractional and logical connectives *) (** Fractional and logical connectives *)
Global Instance persistent_fractional P : Global Instance persistent_fractional P :
Persistent P Fractional (λ _, P). Persistent P Fractional (λ _, P).
Proof. intros HP q q'. by apply uPred.persistently_sep_dup. Qed. Proof. intros HP q q'. by apply uPred.sep_dup. Qed.
Global Instance fractional_sep Φ Ψ : Global Instance fractional_sep Φ Ψ :
Fractional Φ Fractional Ψ Fractional (λ q, Φ q Ψ q)%I. Fractional Φ Fractional Ψ Fractional (λ q, Φ q Ψ q)%I.
......
...@@ -102,7 +102,7 @@ Proof. apply wand_intro_r. by rewrite -own_op own_valid. Qed. ...@@ -102,7 +102,7 @@ Proof. apply wand_intro_r. by rewrite -own_op own_valid. Qed.
Lemma own_valid_3 γ a1 a2 a3 : own γ a1 - own γ a2 - own γ a3 - (a1 a2 a3). Lemma own_valid_3 γ a1 a2 a3 : own γ a1 - own γ a2 - own γ a3 - (a1 a2 a3).
Proof. do 2 apply wand_intro_r. by rewrite -!own_op own_valid. Qed. Proof. do 2 apply wand_intro_r. by rewrite -!own_op own_valid. Qed.
Lemma own_valid_r γ a : own γ a own γ a a. Lemma own_valid_r γ a : own γ a own γ a a.
Proof. apply: uPred.persistently_entails_r. apply own_valid. Qed. Proof. apply: uPred.sep_entails_r. apply own_valid. Qed.
Lemma own_valid_l γ a : own γ a a own γ a. Lemma own_valid_l γ a : own γ a a own γ a.
Proof. by rewrite comm -own_valid_r. Qed. Proof. by rewrite comm -own_valid_r. Qed.
......
...@@ -81,5 +81,5 @@ Lemma vs_alloc N P : ▷ P ={↑N}=> inv N P. ...@@ -81,5 +81,5 @@ Lemma vs_alloc N P : ▷ P ={↑N}=> inv N P.
Proof. iIntros "!# HP". by iApply inv_alloc. Qed. 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). Lemma wand_fupd_alt E1 E2 P Q : (P ={E1,E2}= Q) R, R (P R ={E1,E2}=> Q).
Proof. rewrite uPred.wand_alt. by setoid_rewrite <-uPred.persistently_wand_impl. Qed. Proof. rewrite uPred.wand_alt. by setoid_rewrite uPred.persistently_impl_wand. Qed.
End vs. End vs.
...@@ -17,7 +17,7 @@ Proof. destruct p; rewrite /FromAssumption /= ?persistently_pure; apply False_el ...@@ -17,7 +17,7 @@ Proof. destruct p; rewrite /FromAssumption /= ?persistently_pure; apply False_el
Global Instance from_assumption_persistently_r P Q : Global Instance from_assumption_persistently_r P Q :
FromAssumption true P Q FromAssumption true P ( Q). FromAssumption true P Q FromAssumption true P ( Q).
Proof. rewrite /FromAssumption=><-. by rewrite persistently_persistently. Qed. Proof. rewrite /FromAssumption=><-. by rewrite persistent_persistently. Qed.
Global Instance from_assumption_persistently_l p P Q : Global Instance from_assumption_persistently_l p P Q :
FromAssumption p P Q FromAssumption p ( P) Q. FromAssumption p P Q FromAssumption p ( P) Q.
...@@ -65,9 +65,7 @@ Global Instance into_pure_pure_impl (φ1 φ2 : Prop) P1 P2 : ...@@ -65,9 +65,7 @@ Global Instance into_pure_pure_impl (φ1 φ2 : Prop) P1 P2 :
Proof. rewrite /FromPure /IntoPure pure_impl. by intros -> ->. Qed. Proof. rewrite /FromPure /IntoPure pure_impl. by intros -> ->. Qed.
Global Instance into_pure_pure_wand (φ1 φ2 : Prop) P1 P2 : Global Instance into_pure_pure_wand (φ1 φ2 : Prop) P1 P2 :
FromPure P1 φ1 IntoPure P2 φ2 IntoPure (P1 - P2) (φ1 φ2). FromPure P1 φ1 IntoPure P2 φ2 IntoPure (P1 - P2) (φ1 φ2).
Proof. Proof. rewrite /FromPure /IntoPure pure_impl impl_wand. by intros -> ->. Qed.
rewrite /FromPure /IntoPure pure_impl persistently_impl_wand. by intros -> ->.
Qed.
Global Instance into_pure_exist {X : Type} (Φ : X uPred M) (φ : X Prop) : Global Instance into_pure_exist {X : Type} (Φ : X uPred M) (φ : X Prop) :
( x, @IntoPure M (Φ x) (φ x)) @IntoPure M ( x, Φ x) ( x, φ x). ( x, @IntoPure M (Φ x) (φ x)) @IntoPure M ( x, Φ x) ( x, φ x).
...@@ -113,7 +111,7 @@ Global Instance from_pure_pure_and (φ1 φ2 : Prop) P1 P2 : ...@@ -113,7 +111,7 @@ Global Instance from_pure_pure_and (φ1 φ2 : Prop) P1 P2 :
Proof. rewrite /FromPure pure_and. by intros -> ->. Qed. Proof. rewrite /FromPure pure_and. by intros -> ->. Qed.
Global Instance from_pure_pure_sep (φ1 φ2 : Prop) P1 P2 : Global Instance from_pure_pure_sep (φ1 φ2 : Prop) P1 P2 :
FromPure P1 φ1 FromPure P2 φ2 FromPure (P1 P2) (φ1 φ2). FromPure P1 φ1 FromPure P2 φ2 FromPure (P1 P2) (φ1 φ2).
Proof. rewrite /FromPure pure_and persistently_and_sep_l. by intros -> ->. Qed. Proof. rewrite /FromPure pure_and and_sep_l. by intros -> ->. Qed.
Global Instance from_pure_pure_or (φ1 φ2 : Prop) P1 P2 : Global Instance from_pure_pure_or (φ1 φ2 : Prop) P1 P2 :
FromPure P1 φ1 FromPure P2 φ2 FromPure (P1 P2) (φ1 φ2). FromPure P1 φ1 FromPure P2 φ2 FromPure (P1 P2) (φ1 φ2).
Proof. rewrite /FromPure pure_or. by intros -> ->. Qed. Proof. rewrite /FromPure pure_or. by intros -> ->. Qed.
...@@ -122,9 +120,7 @@ Global Instance from_pure_pure_impl (φ1 φ2 : Prop) P1 P2 : ...@@ -122,9 +120,7 @@ Global Instance from_pure_pure_impl (φ1 φ2 : Prop) P1 P2 :
Proof. rewrite /FromPure /IntoPure pure_impl. by intros -> ->. Qed. Proof. rewrite /FromPure /IntoPure pure_impl. by intros -> ->. Qed.
Global Instance from_pure_pure_wand (φ1 φ2 : Prop) P1 P2 : Global Instance from_pure_pure_wand (φ1 φ2 : Prop) P1 P2 :
IntoPure P1 φ1 FromPure P2 φ2 FromPure (P1 - P2) (φ1 φ2). IntoPure P1 φ1 FromPure P2 φ2 FromPure (P1 - P2) (φ1 φ2).
Proof. Proof. rewrite /FromPure /IntoPure pure_impl impl_wand. by intros -> ->. Qed.
rewrite /FromPure /IntoPure pure_impl persistently_impl_wand. by intros -> ->.
Qed.
Global Instance from_pure_exist {X : Type} (Φ : X uPred M) (φ : X Prop) : Global Instance from_pure_exist {X : Type} (Φ : X uPred M) (φ : X Prop) :
( x, @FromPure M (Φ x) (φ x)) @FromPure M ( x, Φ x) ( x, φ x). ( x, @FromPure M (Φ x) (φ x)) @FromPure M ( x, Φ x) ( x, φ x).
...@@ -142,7 +138,7 @@ Qed. ...@@ -142,7 +138,7 @@ Qed.
(* IntoPersistent *) (* IntoPersistent *)
Global Instance into_persistent_persistently_trans p P Q : Global Instance into_persistent_persistently_trans p P Q :
IntoPersistent true P Q IntoPersistent p ( P) Q | 0. IntoPersistent true P Q IntoPersistent p ( P) Q | 0.
Proof. rewrite /IntoPersistent /==> ->. by rewrite persistently_if_persistently. Qed. Proof. rewrite /IntoPersistent /==> ->. by rewrite persistent_persistently_if. Qed.
Global Instance into_persistent_persistently P : IntoPersistent true P P | 1. Global Instance into_persistent_persistently P : IntoPersistent true P P | 1.
Proof. done. Qed. Proof. done. Qed.
Global Instance into_persistent_persistent P : Global Instance into_persistent_persistent P :
...@@ -298,14 +294,14 @@ Global Instance into_wand_wand p P P' Q Q' : ...@@ -298,14 +294,14 @@ Global Instance into_wand_wand p P P' Q Q' :
Proof. done. Qed. Proof. done. Qed.
Global Instance into_wand_impl p P P' Q Q' : Global Instance into_wand_impl p P P' Q Q' :
WandWeaken p P Q P' Q' IntoWand p (P Q) P' Q'. WandWeaken p P Q P' Q' IntoWand p (P Q) P' Q'.
Proof. rewrite /WandWeaken /IntoWand /= => <-. apply impl_wand. Qed. Proof. rewrite /WandWeaken /IntoWand /= => <-. apply impl_wand_1. Qed.
Global Instance into_wand_iff_l p P P' Q Q' : Global Instance into_wand_iff_l p P P' Q Q' :
WandWeaken p P Q P' Q' IntoWand p (P Q) P' Q'. WandWeaken p P Q P' Q' IntoWand p (P Q) P' Q'.
Proof. rewrite /WandWeaken /IntoWand=> <-. apply and_elim_l', impl_wand. Qed. Proof. rewrite /WandWeaken /IntoWand=> <-. apply and_elim_l', impl_wand_1. Qed.
Global Instance into_wand_iff_r p P P' Q Q' : Global Instance into_wand_iff_r p P P' Q Q' :
WandWeaken p Q P Q' P' IntoWand p (P Q) Q' P'. WandWeaken p Q P Q' P' IntoWand p (P Q) Q' P'.
Proof. rewrite /WandWeaken /IntoWand=> <-. apply and_elim_r', impl_wand. Qed. Proof. rewrite /WandWeaken /IntoWand=> <-. apply and_elim_r', impl_wand_1. Qed.
Global Instance into_wand_forall {A} p (Φ : A uPred M) P Q x : Global Instance into_wand_forall {A} p (Φ : A uPred M) P Q x :
IntoWand p (Φ x) P Q IntoWand p ( x, Φ x) P Q. IntoWand p (Φ x) P Q IntoWand p ( x, Φ x) P Q.
...@@ -340,10 +336,10 @@ Global Instance from_and_sep P1 P2 : FromAnd false (P1 ∗ P2) P1 P2 | 100. ...@@ -340,10 +336,10 @@ Global Instance from_and_sep P1 P2 : FromAnd false (P1 ∗ P2) P1 P2 | 100.
Proof. done. Qed. Proof. done. Qed.
Global Instance from_and_sep_persistent_l P1 P2 : Global Instance from_and_sep_persistent_l P1 P2 :
Persistent P1 FromAnd true (P1 P2) P1 P2 | 9. Persistent P1 FromAnd true (P1 P2) P1 P2 | 9.
Proof. intros. by rewrite /FromAnd persistently_and_sep_l. Qed. Proof. intros. by rewrite /FromAnd and_sep_l. Qed.
Global Instance from_and_sep_persistent_r P1 P2 : Global Instance from_and_sep_persistent_r P1 P2 :
Persistent P2 FromAnd true (P1 P2) P1 P2 | 10. Persistent P2 FromAnd true (P1 P2) P1 P2 | 10.
Proof. intros. by rewrite /FromAnd persistently_and_sep_r. Qed. Proof. intros. by rewrite /FromAnd and_sep_r. Qed.
Global Instance from_and_pure p φ ψ : @FromAnd M p ⌜φ ψ⌝ ⌜φ⌝ ⌜ψ⌝. Global Instance from_and_pure p φ ψ : @FromAnd M p ⌜φ ψ⌝ ⌜φ⌝ ⌜ψ⌝.
Proof. apply mk_from_and_and. by rewrite pure_and. Qed. Proof. apply mk_from_and_and. by rewrite pure_and. Qed.
...@@ -351,7 +347,7 @@ Global Instance from_and_persistently p P Q1 Q2 : ...@@ -351,7 +347,7 @@ Global Instance from_and_persistently p P Q1 Q2 :
FromAnd false P Q1 Q2 FromAnd p ( P) ( Q1) ( Q2). FromAnd false P Q1 Q2 FromAnd p ( P) ( Q1) ( Q2).
Proof. Proof.
intros. apply mk_from_and_and. intros. apply mk_from_and_and.
by rewrite persistently_and_sep_l' -persistently_sep -(from_and _ P). by rewrite persistently_and_sep_l -persistently_sep -(from_and _ P).
Qed. Qed.
Global Instance from_and_later p P Q1 Q2 : Global Instance from_and_later p P Q1 Q2 :
FromAnd p P Q1 Q2 FromAnd p ( P) ( Q1) ( Q2). FromAnd p P Q1 Q2 FromAnd p ( P) ( Q1) ( Q2).
...@@ -387,7 +383,7 @@ Proof. by rewrite /FromAnd big_sepL_cons. Qed. ...@@ -387,7 +383,7 @@ Proof. by rewrite /FromAnd big_sepL_cons. Qed.
Global Instance from_and_big_sepL_cons_persistent {A} (Φ : nat A uPred M) x l : Global Instance from_and_big_sepL_cons_persistent {A} (Φ : nat A uPred M) x l :
Persistent (Φ 0 x) Persistent (Φ 0 x)
FromAnd true ([ list] k y x :: l, Φ k y) (Φ 0 x) ([ list] k y l, Φ (S k) y). FromAnd true ([ list] k y x :: l, Φ k y) (Φ 0 x) ([ list] k y l, Φ (S k) y).
Proof. intros. by rewrite /FromAnd big_opL_cons persistently_and_sep_l. Qed. Proof. intros. by rewrite /FromAnd big_opL_cons and_sep_l. Qed.
Global Instance from_and_big_sepL_app {A} (Φ : nat A uPred M) l1 l2 : Global Instance from_and_big_sepL_app {A} (Φ : nat A uPred M) l1 l2 :
FromAnd false ([ list] k y l1 ++ l2, Φ k y) FromAnd false ([ list] k y l1 ++ l2, Φ k y)
...@@ -397,7 +393,7 @@ Global Instance from_sep_big_sepL_app_persistent {A} (Φ : nat → A → uPred M ...@@ -397,7 +393,7 @@ Global Instance from_sep_big_sepL_app_persistent {A} (Φ : nat → A → uPred M
( k y, Persistent (Φ k y)) ( k y, Persistent (Φ k y))
FromAnd true ([ list] k y l1 ++ l2, Φ k y) FromAnd true ([ list] k y l1 ++ l2, Φ k y)
([ list] k y l1, Φ k y) ([ list] k y l2, Φ (length l1 + k) y). ([ list] k y l1, Φ k y) ([ list] k y l2, Φ (length l1 + k) y).
Proof. intros. by rewrite /FromAnd big_opL_app persistently_and_sep_l. Qed. Proof. intros. by rewrite /FromAnd big_opL_app and_sep_l. Qed.
(* FromOp *) (* FromOp *)
(* TODO: Worst case there could be a lot of backtracking on these instances, (* TODO: Worst case there could be a lot of backtracking on these instances,
...@@ -431,13 +427,13 @@ Global Instance into_and_and P Q : IntoAnd true (P ∧ Q) P Q. ...@@ -431,13 +427,13 @@ Global Instance into_and_and P Q : IntoAnd true (P ∧ Q) P Q.
Proof. done. Qed. Proof. done. Qed.
Global Instance into_and_and_persistent_l P Q : Global Instance into_and_and_persistent_l P Q :
Persistent P IntoAnd false (P Q) P Q. Persistent P IntoAnd false (P Q) P Q.
Proof. intros; by rewrite /IntoAnd /= persistently_and_sep_l. Qed. Proof. intros; by rewrite /IntoAnd /= and_sep_l. Qed.
Global Instance into_and_and_persistent_r P Q : Global Instance into_and_and_persistent_r P Q :
Persistent Q IntoAnd false (P Q) P Q. Persistent Q IntoAnd false (P Q) P Q.
Proof. intros; by rewrite /IntoAnd /= persistently_and_sep_r. Qed. Proof. intros; by rewrite /IntoAnd /= and_sep_r. Qed.
Global Instance into_and_pure p φ ψ : @IntoAnd M p ⌜φ ψ⌝ ⌜φ⌝ ⌜ψ⌝. Global Instance into_and_pure p φ ψ : @IntoAnd M p ⌜φ ψ⌝ ⌜φ⌝ ⌜ψ⌝.
Proof. apply mk_into_and_sep. by rewrite pure_and persistently_and_sep_r. Qed. Proof. apply mk_into_and_sep. by rewrite pure_and and_sep_r. Qed.
Global Instance into_and_persistently p P Q1 Q2 : Global Instance into_and_persistently p P Q1 Q2 :
IntoAnd true P Q1 Q2 IntoAnd p ( P) ( Q1) ( Q2). IntoAnd true P Q1 Q2 IntoAnd p ( P) ( Q1) ( Q2).