Commit 384b9d0d authored by Ralf Jung's avatar Ralf Jung
Browse files

move bi_persistently_emp out of BI interface, and get a basic proof mode working again

parent 7fe2a5e1
......@@ -135,13 +135,13 @@ Section sep_list.
Proper (Forall2 () ==> ()) (big_opL (@bi_sep PROP) (λ _ P, P)).
Proof. by induction 1 as [|P Q Ps Qs HPQ ? IH]; rewrite /= ?HPQ ?IH. Qed.
Global Instance big_sepL_nil_persistent Φ :
Global Instance big_sepL_nil_persistent `{!BiPersistentlyEmp PROP} Φ :
Persistent ([ list] kx [], Φ k x).
Proof. simpl; apply _. Qed.
Global Instance big_sepL_persistent Φ l :
Global Instance big_sepL_persistent `{!BiPersistentlyEmp PROP} Φ 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 Ps :
Global Instance big_sepL_persistent_id `{!BiPersistentlyEmp PROP} Ps :
TCForall Persistent Ps Persistent ([] Ps).
Proof. induction 1; simpl; apply _. Qed.
......@@ -244,7 +244,7 @@ Section sep_list.
- apply list_lookup_singleton_Some in Hy as [Hk ->].
replace k with (length l) by lia. done.
Qed.
Lemma big_sepL_affinely_pure_2 (φ : nat A Prop) l :
Lemma big_sepL_affinely_pure_2 `{!BiPersistentlyEmp PROP} (φ : nat A Prop) l :
<affine> k x, l !! k = Some x φ k x @{PROP} ([ list] kx l, <affine> ⌜φ k x).
Proof.
induction l as [|x l IH] using rev_ind.
......@@ -257,7 +257,7 @@ Section sep_list.
rewrite Nat.sub_diag //.
Qed.
(** The general backwards direction requires [BiAffine] to cover the empty case. *)
Lemma big_sepL_pure `{!BiAffine PROP} (φ : nat A Prop) l :
Lemma big_sepL_pure `{!BiAffine PROP, !BiPersistentlyEmp PROP} (φ : nat A Prop) l :
([ list] kx l, ⌜φ k x) @{PROP} k x, l !! k = Some x φ k x.
Proof.
apply (anti_symm ()); first by apply big_sepL_pure_1.
......@@ -265,7 +265,7 @@ Section sep_list.
rewrite big_sepL_affinely_pure_2. by setoid_rewrite affinely_elim.
Qed.
Lemma big_sepL_persistently `{BiAffine PROP} Φ l :
Lemma big_sepL_persistently `{!BiAffine PROP, !BiPersistentlyEmp PROP} Φ l :
<pers> ([ list] kx l, Φ k x) [ list] kx l, <pers> (Φ k x).
Proof. apply (big_opL_commute _). Qed.
......@@ -591,10 +591,10 @@ Section sep_list2.
(big_sepL2 (PROP:=PROP) (A:=A) (B:=B)).
Proof. intros f g Hf l1 ? <- l2 ? <-. apply big_sepL2_proper; intros; apply Hf. Qed.
Global Instance big_sepL2_nil_persistent Φ :
Global Instance big_sepL2_nil_persistent `{!BiPersistentlyEmp PROP} Φ :
Persistent ([ list] ky1;y2 []; [], Φ k y1 y2).
Proof. simpl; apply _. Qed.
Global Instance big_sepL2_persistent Φ l1 l2 :
Global Instance big_sepL2_persistent `{!BiPersistentlyEmp PROP} Φ l1 l2 :
( k x1 x2, Persistent (Φ k x1 x2))
Persistent ([ list] ky1;y2 l1;l2, Φ k y1 y2).
Proof. rewrite big_sepL2_alt. apply _. Qed.
......@@ -685,7 +685,7 @@ Section sep_list2.
([ list] kx1;x2 l;replicate n x, Φ k x1 x2) [ list] kx1 l, Φ k x1 x.
Proof. intros <-. revert Φ. induction l as [|y l IH]=> //= Φ. by rewrite IH. Qed.
Lemma big_sepL2_sep Φ Ψ l1 l2 :
Lemma big_sepL2_sep Φ Ψ l1 l2 `{!BiPersistentlyEmp PROP} :
([ list] ky1;y2 l1;l2, Φ k y1 y2 Ψ k y1 y2)
([ list] ky1;y2 l1;l2, Φ k y1 y2) ([ list] ky1;y2 l1;l2, Ψ k y1 y2).
Proof.
......@@ -695,7 +695,7 @@ Section sep_list2.
by rewrite affinely_and_r persistent_and_affinely_sep_l idemp.
Qed.
Lemma big_sepL2_sep_2 Φ Ψ l1 l2 :
Lemma big_sepL2_sep_2 `{!BiPersistentlyEmp PROP} Φ Ψ l1 l2 :
([ list] ky1;y2 l1;l2, Φ k y1 y2) -
([ list] ky1;y2 l1;l2, Ψ k y1 y2) -
([ list] ky1;y2 l1;l2, Φ k y1 y2 Ψ k y1 y2).
......@@ -715,7 +715,7 @@ Section sep_list2.
eapply (Hlookup k (y1, y2)).
rewrite lookup_zip_with Hy1 /= Hy2 /= //.
Qed.
Lemma big_sepL2_affinely_pure_2 (φ : nat A B Prop) l1 l2 :
Lemma big_sepL2_affinely_pure_2 `{!BiPersistentlyEmp PROP} (φ : nat A B Prop) l1 l2 :
length l1 = length l2
<affine> k y1 y2, l1 !! k = Some y1 l2 !! k = Some y2 φ k y1 y2 @{PROP}
([ list] ky1;y2 l1;l2, <affine> ⌜φ k y1 y2).
......@@ -728,7 +728,7 @@ Section sep_list2.
by eapply Hforall.
Qed.
(** The general backwards direction requires [BiAffine] to cover the empty case. *)
Lemma big_sepL2_pure `{!BiAffine PROP} (φ : nat A B Prop) l1 l2 :
Lemma big_sepL2_pure `{!BiAffine PROP, !BiPersistentlyEmp PROP} (φ : nat A B Prop) l1 l2 :
([ list] ky1;y2 l1;l2, ⌜φ k y1 y2) @{PROP}
length l1 = length l2
k y1 y2, l1 !! k = Some y1 l2 !! k = Some y2 φ k y1 y2.
......@@ -743,7 +743,7 @@ Section sep_list2.
rewrite big_sepL2_affinely_pure_2 //. by setoid_rewrite affinely_elim.
Qed.
Lemma big_sepL2_persistently `{BiAffine PROP} Φ l1 l2 :
Lemma big_sepL2_persistently `{!BiAffine PROP, !BiPersistentlyEmp PROP} Φ l1 l2 :
<pers> ([ list] ky1;y2 l1;l2, Φ k y1 y2)
[ list] ky1;y2 l1;l2, <pers> (Φ k y1 y2).
Proof.
......@@ -784,7 +784,7 @@ Section sep_list2.
by apply forall_intro=> k; by rewrite (forall_elim (S k)).
Qed.
Lemma big_sepL2_impl Φ Ψ l1 l2 :
Lemma big_sepL2_impl `{!BiPersistentlyEmp PROP} Φ Ψ l1 l2 :
([ list] ky1;y2 l1;l2, Φ k y1 y2) -
( k x1 x2,
l1 !! k = Some x1 l2 !! k = Some x2 Φ k x1 x2 - Ψ k x1 x2) -
......@@ -795,7 +795,7 @@ Section sep_list2.
apply bi.wand_intro_l. rewrite -big_sepL2_sep. by setoid_rewrite wand_elim_l.
Qed.
Lemma big_sepL2_wand Φ Ψ l1 l2 :
Lemma big_sepL2_wand `{!BiPersistentlyEmp PROP} Φ Ψ l1 l2 :
([ list] ky1;y2 l1;l2, Φ k y1 y2) -
([ list] ky1;y2 l1;l2, Φ k y1 y2 - Ψ k y1 y2) -
[ list] ky1;y2 l1;l2, Ψ k y1 y2.
......@@ -828,7 +828,7 @@ Section sep_list2.
rewrite -decide_emp. by repeat case_decide.
Qed.
Lemma big_sepL2_lookup_acc_impl {Φ l1 l2} i x1 x2 :
Lemma big_sepL2_lookup_acc_impl `{!BiPersistentlyEmp PROP} {Φ l1 l2} i x1 x2 :
l1 !! i = Some x1
l2 !! i = Some x2
([ list] ky1;y2 l1;l2, Φ k y1 y2) -
......@@ -914,7 +914,7 @@ Lemma big_sepL2_const_sepL_r {A B} (Φ : nat → B → PROP) (l1 : list A) (l2
length l1 = length l2 ([ list] ky2 l2, Φ k y2).
Proof. by rewrite big_sepL2_flip big_sepL2_const_sepL_l (symmetry_iff (=)). Qed.
Lemma big_sepL2_sep_sepL_l {A B} (Φ : nat A PROP)
Lemma big_sepL2_sep_sepL_l `{!BiPersistentlyEmp PROP} {A B} (Φ : nat A PROP)
(Ψ : nat A B PROP) l1 l2 :
([ list] ky1;y2 l1;l2, Φ k y1 Ψ k y1 y2)
([ list] ky1 l1, Φ k y1) ([ list] ky1;y2 l1;l2, Ψ k y1 y2).
......@@ -928,7 +928,7 @@ Proof.
apply and_intro; last done.
apply pure_intro. done.
Qed.
Lemma big_sepL2_sep_sepL_r {A B} (Φ : nat A B PROP)
Lemma big_sepL2_sep_sepL_r `{!BiPersistentlyEmp PROP} {A B} (Φ : nat A B PROP)
(Ψ : nat B PROP) l1 l2 :
([ list] ky1;y2 l1;l2, Φ k y1 y2 Ψ k y2)
([ list] ky1;y2 l1;l2, Φ k y1 y2) ([ list] ky2 l2, Ψ k y2).
......@@ -1014,10 +1014,10 @@ Section and_list.
Proper (Forall2 () ==> ()) (big_opL (@bi_and PROP) (λ _ P, P)).
Proof. by induction 1 as [|P Q Ps Qs HPQ ? IH]; rewrite /= ?HPQ ?IH. Qed.
Global Instance big_andL_nil_persistent Φ :
Global Instance big_andL_nil_persistent `{!BiPersistentlyEmp PROP} Φ :
Persistent ([ list] kx [], Φ k x).
Proof. simpl; apply _. Qed.
Global Instance big_andL_persistent Φ l :
Global Instance big_andL_persistent `{!BiPersistentlyEmp PROP} Φ l :
( k x, Persistent (Φ k x)) Persistent ([ list] kx l, Φ k x).
Proof. revert Φ. induction l as [|x l IH]=> Φ ? /=; apply _. Qed.
......@@ -1055,7 +1055,7 @@ Section and_list.
([ list] kx l, Φ k x) ([ list] kx l, Ψ k x).
Proof. by rewrite big_opL_op. Qed.
Lemma big_andL_persistently Φ l :
Lemma big_andL_persistently `{!BiPersistentlyEmp PROP} Φ l :
<pers> ([ list] kx l, Φ k x) [ list] kx l, <pers> (Φ k x).
Proof. apply (big_opL_commute _). Qed.
......@@ -1207,7 +1207,7 @@ Section or_list.
([ list] kx l, Φ k x) ([ list] kx l, Ψ k x).
Proof. by rewrite big_opL_op. Qed.
Lemma big_orL_persistently Φ l :
Lemma big_orL_persistently `{!BiPersistentlyEmp PROP} Φ l :
<pers> ([ list] kx l, Φ k x) [ list] kx l, <pers> (Φ k x).
Proof. apply (big_opL_commute _). Qed.
......@@ -1233,14 +1233,14 @@ Section or_list.
rewrite -pure_and. done.
Qed.
Lemma big_orL_sep_l P Φ l :
Lemma big_orL_sep_l `{!BiPersistentlyEmp PROP} P Φ l :
P ([ list] kx l, Φ k x) ([ list] kx l, P Φ k x).
Proof.
rewrite !big_orL_exist sep_exist_l.
f_equiv=> k. rewrite sep_exist_l. f_equiv=> x.
by rewrite !persistent_and_affinely_sep_l !assoc (comm _ P).
Qed.
Lemma big_orL_sep_r Q Φ l :
Lemma big_orL_sep_r `{!BiPersistentlyEmp PROP} Q Φ l :
([ list] kx l, Φ k x) Q ([ list] kx l, Φ k x Q).
Proof. setoid_rewrite (comm bi_sep). apply big_orL_sep_l. Qed.
......@@ -1282,10 +1282,10 @@ Section sep_map.
(big_opM (@bi_sep PROP) (K:=K) (A:=A)).
Proof. intros f g Hf m ? <-. apply big_sepM_mono; intros; apply Hf. Qed.
Global Instance big_sepM_empty_persistent Φ :
Global Instance big_sepM_empty_persistent `{!BiPersistentlyEmp PROP} Φ :
Persistent ([ map] kx , Φ k x).
Proof. rewrite big_opM_empty. apply _. Qed.
Global Instance big_sepM_persistent Φ m :
Global Instance big_sepM_persistent `{!BiPersistentlyEmp PROP} Φ m :
( k x, Persistent (Φ k x)) Persistent ([ map] kx m, Φ k x).
Proof.
induction m using map_ind;
......@@ -1477,7 +1477,7 @@ Section sep_map.
rewrite big_sepM_insert // IH sep_and -pure_and.
by rewrite -map_Forall_insert.
Qed.
Lemma big_sepM_affinely_pure_2 (φ : K A Prop) m :
Lemma big_sepM_affinely_pure_2 `{!BiPersistentlyEmp PROP} (φ : K A Prop) m :
<affine> map_Forall φ m @{PROP} ([ map] kx m, <affine> ⌜φ k x).
Proof.
induction m as [|k x m ? IH] using map_ind.
......@@ -1486,7 +1486,7 @@ Section sep_map.
by rewrite -persistent_and_sep_1 -affinely_and -pure_and map_Forall_insert.
Qed.
(** The general backwards direction requires [BiAffine] to cover the empty case. *)
Lemma big_sepM_pure `{!BiAffine PROP} (φ : K A Prop) m :
Lemma big_sepM_pure `{!BiAffine PROP, !BiPersistentlyEmp PROP} (φ : K A Prop) m :
([ map] kx m, ⌜φ k x) @{PROP} map_Forall φ m.
Proof.
apply (anti_symm ()); first by apply big_sepM_pure_1.
......@@ -1494,7 +1494,7 @@ Section sep_map.
rewrite big_sepM_affinely_pure_2. by setoid_rewrite affinely_elim.
Qed.
Lemma big_sepM_persistently `{BiAffine PROP} Φ m :
Lemma big_sepM_persistently `{!BiAffine PROP, !BiPersistentlyEmp PROP} Φ m :
(<pers> ([ map] kx m, Φ k x)) ([ map] kx m, <pers> (Φ k x)).
Proof. apply (big_opM_commute _). Qed.
......@@ -1700,10 +1700,10 @@ Section and_map.
(big_opM (@bi_and PROP) (K:=K) (A:=A)).
Proof. intros f g Hf m ? <-. apply big_andM_mono; intros; apply Hf. Qed.
Global Instance big_andM_empty_persistent Φ :
Global Instance big_andM_empty_persistent `{!BiPersistentlyEmp PROP} Φ :
Persistent ([ map] kx , Φ k x).
Proof. rewrite big_opM_empty. apply _. Qed.
Global Instance big_andM_persistent Φ m :
Global Instance big_andM_persistent `{!BiPersistentlyEmp PROP} Φ m :
( k x, Persistent (Φ k x)) Persistent ([ map] kx m, Φ k x).
Proof.
induction m using map_ind;
......@@ -1808,7 +1808,7 @@ Section and_map.
([ map] kx m, Φ k x) ([ map] kx m, Ψ k x).
Proof. apply big_opM_op. Qed.
Lemma big_andM_persistently Φ m :
Lemma big_andM_persistently `{!BiPersistentlyEmp PROP} Φ m :
<pers> ([ map] kx m, Φ k x) ([ map] kx m, <pers> (Φ k x)).
Proof. apply (big_opM_commute _). Qed.
......@@ -1979,6 +1979,10 @@ Section map2.
==> (=) ==> (=) ==> ()) (big_sepM2 (PROP:=PROP) (K:=K) (A:=A) (B:=B)).
Proof. intros f g Hf m1 ? <- m2 ? <-. apply big_sepM2_proper; intros; apply Hf. Qed.
(* TODO: Support this on all BIs. *)
Context `{!BiPersistentlyEmp PROP}.
Local Set Default Proof Using "Type*".
Global Instance big_sepM2_empty_persistent Φ :
Persistent ([ map] ky1;y2 ; , Φ k y1 y2).
Proof. rewrite big_sepM2_empty. apply _. Qed.
......@@ -2424,7 +2428,7 @@ Section map2.
Qed.
End map2.
Lemma big_sepM2_union_inv_r `{Countable K} {A B}
Lemma big_sepM2_union_inv_r `{!BiPersistentlyEmp PROP} `{Countable K} {A B}
(Φ : K A B PROP) (m1 m2 : gmap K B) (m' : gmap K A) :
m1 ## m2
([ map] kx;y m';(m1 m2), Φ k x y)
......@@ -2493,10 +2497,10 @@ Section gset.
Proper (pointwise_relation _ () ==> (=) ==> ()) (big_opS (@bi_sep PROP) (A:=A)).
Proof. intros f g Hf m ? <-. by apply big_sepS_mono. Qed.
Global Instance big_sepS_empty_persistent Φ :
Global Instance big_sepS_empty_persistent `{!BiPersistentlyEmp PROP} Φ :
Persistent ([ set] x , Φ x).
Proof. rewrite big_opS_empty. apply _. Qed.
Global Instance big_sepS_persistent Φ X :
Global Instance big_sepS_persistent `{!BiPersistentlyEmp PROP} Φ X :
( x, Persistent (Φ x)) Persistent ([ set] x X, Φ x).
Proof.
induction X using set_ind_L;
......@@ -2683,7 +2687,7 @@ Section gset.
- apply set_Forall_singleton. done.
- done.
Qed.
Lemma big_sepS_affinely_pure_2 (φ : A Prop) X :
Lemma big_sepS_affinely_pure_2 `{!BiPersistentlyEmp PROP} (φ : A Prop) X :
<affine> set_Forall φ X @{PROP} ([ set] y X, <affine> ⌜φ y).
Proof.
induction X as [|x X ? IH] using set_ind_L.
......@@ -2695,7 +2699,7 @@ Section gset.
- apply set_Forall_union_inv_2 in HX. done.
Qed.
(** The general backwards direction requires [BiAffine] to cover the empty case. *)
Lemma big_sepS_pure `{!BiAffine PROP} (φ : A Prop) X :
Lemma big_sepS_pure `{!BiAffine PROP, !BiPersistentlyEmp PROP} (φ : A Prop) X :
([ set] y X, ⌜φ y) @{PROP} set_Forall φ X.
Proof.
apply (anti_symm ()); first by apply big_sepS_pure_1.
......@@ -2703,7 +2707,7 @@ Section gset.
rewrite big_sepS_affinely_pure_2. by setoid_rewrite affinely_elim.
Qed.
Lemma big_sepS_persistently `{BiAffine PROP} Φ X :
Lemma big_sepS_persistently `{!BiAffine PROP, !BiPersistentlyEmp PROP} Φ X :
<pers> ([ set] y X, Φ y) [ set] y X, <pers> (Φ y).
Proof. apply (big_opS_commute _). Qed.
......@@ -2829,10 +2833,10 @@ Section gmultiset.
Proper (pointwise_relation _ () ==> (=) ==> ()) (big_opMS (@bi_sep PROP) (A:=A)).
Proof. intros f g Hf m ? <-. by apply big_sepMS_mono. Qed.
Global Instance big_sepMS_empty_persistent Φ :
Global Instance big_sepMS_empty_persistent `{!BiPersistentlyEmp PROP} Φ :
Persistent ([ mset] x , Φ x).
Proof. rewrite big_opMS_empty. apply _. Qed.
Global Instance big_sepMS_persistent Φ X :
Global Instance big_sepMS_persistent `{!BiPersistentlyEmp PROP} Φ X :
( x, Persistent (Φ x)) Persistent ([ mset] x X, Φ x).
Proof.
induction X using gmultiset_ind;
......@@ -2940,7 +2944,7 @@ Section gmultiset.
- move=>/gmultiset_elem_of_singleton =>->. done.
- eauto.
Qed.
Lemma big_sepMS_affinely_pure_2 (φ : A Prop) X :
Lemma big_sepMS_affinely_pure_2 `{!BiPersistentlyEmp PROP} (φ : A Prop) X :
<affine> y : A, y X φ y @{PROP} ([ mset] y X, <affine> ⌜φ y).
Proof.
induction X as [|x X IH] using gmultiset_ind.
......@@ -2952,7 +2956,7 @@ Section gmultiset.
- intros y Hy. apply HX. multiset_solver.
Qed.
(** The general backwards direction requires [BiAffine] to cover the empty case. *)
Lemma big_sepMS_pure `{!BiAffine PROP} (φ : A Prop) X :
Lemma big_sepMS_pure `{!BiAffine PROP, !BiPersistentlyEmp PROP} (φ : A Prop) X :
([ mset] y X, ⌜φ y) @{PROP} y : A, y X φ y.
Proof.
apply (anti_symm ()); first by apply big_sepMS_pure_1.
......@@ -2960,7 +2964,7 @@ Section gmultiset.
rewrite big_sepMS_affinely_pure_2. by setoid_rewrite affinely_elim.
Qed.
Lemma big_sepMS_persistently `{BiAffine PROP} Φ X :
Lemma big_sepMS_persistently `{!BiAffine PROP, !BiPersistentlyEmp PROP} Φ X :
<pers> ([ mset] y X, Φ y) [ mset] y X, <pers> (Φ y).
Proof. apply (big_opMS_commute _). Qed.
......
......@@ -586,6 +586,42 @@ Proof.
- apply exist_elim=> x. eauto using pure_mono.
Qed.
Lemma pure_and_sep_assoc φ Q R :
⌜φ⌝ (Q R) (⌜φ⌝ Q) R.
Proof.
apply (anti_symm _).
- apply pure_elim_l=>H. rewrite pure_True // left_id. done.
- apply and_intro.
+ rewrite and_elim_l.
apply wand_elim_l', pure_elim'=> ?. apply wand_intro_l; auto.
+ rewrite and_elim_r. done.
Qed.
Lemma pure_and_affinely_sep_l φ Q:
⌜φ⌝ Q <affine> ⌜φ⌝ Q.
Proof. rewrite /bi_affinely (comm _ emp%I) -pure_and_sep_assoc left_id //. Qed.
Lemma pure_and_affinely_sep_r φ Q:
Q ⌜φ⌝ Q <affine> ⌜φ⌝.
Proof. rewrite comm pure_and_affinely_sep_l comm //. Qed.
Lemma pure_sep_absorbingly_and_l φ Q:
⌜φ⌝ Q ⌜φ⌝ <absorb> Q.
Proof. rewrite /bi_absorbingly pure_and_sep_assoc right_id //. Qed.
Lemma pure_sep_absorbingly_and_r φ Q:
Q ⌜φ⌝ <absorb> Q ⌜φ⌝.
Proof. rewrite comm pure_sep_absorbingly_and_l comm //. Qed.
Lemma pure_absorbingly_affinely φ :
<absorb> <affine> ⌜φ⌝ ⌜φ⌝.
Proof.
rewrite /bi_absorbingly /bi_affinely.
rewrite [(_ _)%I]comm [(_ _)%I]comm -pure_and_sep_assoc left_id right_id //.
Qed.
Lemma pure_impl_wand_affinely φ Q :
(⌜φ⌝ Q) (<affine> ⌜φ⌝ - Q).
Proof.
apply (anti_symm _).
- apply wand_intro_l. rewrite -pure_and_affinely_sep_l impl_elim_r //.
- apply impl_intro_l. rewrite pure_and_affinely_sep_l wand_elim_r //.
Qed.
Lemma bi_pure_forall_em : ( φ : Prop, φ ¬φ) BiPureForall PROP.
Proof.
intros Hem A φ. destruct (Hem ( a, ¬φ a)) as [[a Hφ]|Hφ].
......@@ -870,21 +906,21 @@ Proof.
apply persistently_mono, impl_elim with P; auto.
Qed.
Lemma persistently_emp_intro P : P <pers> emp.
Lemma persistently_emp_intro `{!BiPersistentlyEmp PROP} P : P <pers> emp.
Proof.
by rewrite -(left_id emp%I bi_sep P) {1}persistently_emp_2 persistently_absorbing.
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. apply (anti_symm _); auto using persistently_True_emp_1. Qed.
Lemma persistently_True `{!BiPersistentlyEmp PROP} : True <pers> True.
Proof. rewrite persistently_True_emp. apply persistently_emp_intro. Qed.
Lemma persistently_and_emp P : <pers> P <pers> (emp P).
Proof.
apply (anti_symm ()); last by rewrite and_elim_r.
rewrite persistently_and. apply and_intro; last done.
apply persistently_emp_intro.
etrans; last by apply persistently_True_emp_1. auto.
Qed.
Lemma persistently_and_sep_elim_emp P Q : <pers> P Q (emp P) Q.
......@@ -922,7 +958,12 @@ Proof. apply (anti_symm _); auto using persistently_idemp_1, persistently_idemp_
Lemma persistently_intro' P Q : (<pers> P Q) <pers> P <pers> Q.
Proof. intros <-. apply persistently_idemp_2. Qed.
Lemma persistently_pure φ : <pers> ⌜φ⌝ ⌜φ⌝.
Lemma persistently_False : <pers> False False.
Proof.
apply (anti_symm _); last by auto.
by rewrite persistently_into_absorbingly absorbingly_pure.
Qed.
Lemma persistently_pure `{!BiPersistentlyEmp PROP} φ : <pers> ⌜φ⌝ ⌜φ⌝.
Proof.
apply (anti_symm _).
{ by rewrite persistently_into_absorbingly absorbingly_pure. }
......@@ -955,8 +996,10 @@ Qed.
Lemma persistently_affinely_elim P : <pers> <affine> P <pers> P.
Proof.
by rewrite /bi_affinely persistently_and -persistently_True_emp
persistently_pure left_id.
rewrite /bi_affinely persistently_and -persistently_True_emp.
apply (anti_symm _).
- by rewrite and_elim_r.
- apply and_intro; auto.
Qed.
Lemma and_sep_persistently P Q : <pers> P <pers> Q <pers> P <pers> Q.
......@@ -1012,7 +1055,7 @@ Proof. apply impl_intro_l. by rewrite persistently_and_sep_l_1 wand_elim_r. Qed.
Section persistently_affine_bi.
Context `{BiAffine PROP}.
Lemma persistently_emp : <pers> emp emp.
Lemma persistently_emp `{!BiPersistentlyEmp PROP} : <pers> emp emp.
Proof. by rewrite -!True_emp persistently_pure. Qed.
Lemma persistently_and_sep_l P Q : <pers> P Q <pers> P Q.
......@@ -1037,7 +1080,7 @@ Section persistently_affine_bi.
- apply impl_wand_persistently_2.
Qed.
Lemma wand_alt P Q : (P - Q) R, R <pers> (P R Q).
Lemma wand_alt `{!BiPersistentlyEmp PROP} P Q : (P - Q) R, R <pers> (P R Q).
Proof.
apply (anti_symm ()).
- rewrite -(right_id True%I bi_sep (P - Q)%I) -(exist_intro (P - Q)%I).
......@@ -1071,14 +1114,14 @@ Proof.
by rewrite /bi_intuitionistically persistently_affinely_elim persistently_idemp.
Qed.
Lemma intuitionistically_emp : emp emp.
Lemma intuitionistically_emp `{!BiPersistentlyEmp PROP} : emp emp.
Proof.
by rewrite /bi_intuitionistically -persistently_True_emp persistently_pure
affinely_True_emp.
Qed.
Lemma intuitionistically_False : False False.
Proof. by rewrite /bi_intuitionistically persistently_pure affinely_False. Qed.
Lemma intuitionistically_True_emp : True emp.
Proof. by rewrite /bi_intuitionistically persistently_False affinely_False. Qed.
Lemma intuitionistically_True_emp `{!BiPersistentlyEmp PROP} : True emp.
Proof.
rewrite -intuitionistically_emp /bi_intuitionistically
persistently_True_emp //.
......@@ -1161,7 +1204,7 @@ Qed.
Lemma intuitionistically_impl_wand_2 P Q : (P - Q) (P Q).
Proof. by rewrite /bi_intuitionistically persistently_impl_wand_2. Qed.
Lemma impl_alt P Q : (P Q) R, R <pers> (P R - Q).
Lemma impl_alt `{!BiPersistentlyEmp PROP} P Q : (P Q) R, R <pers> (P R - Q).
Proof.
apply (anti_symm ()).
- rewrite -(right_id True%I bi_and (P Q)%I) -(exist_intro (P Q)%I).
......@@ -1294,7 +1337,7 @@ Proof. solve_proper. Qed.
Lemma persistently_if_mono p P Q : (P Q) <pers>?p P <pers>?p Q.
Proof. by intros ->. Qed.
Lemma persistently_if_pure p φ : <pers>?p ⌜φ⌝ ⌜φ⌝.
Lemma persistently_if_pure `{!BiPersistentlyEmp PROP} p φ : <pers>?p ⌜φ⌝ ⌜φ⌝.
Proof. destruct p; simpl; auto using persistently_pure. Qed.
Lemma persistently_if_and p P Q : <pers>?p (P Q) <pers>?p P <pers>?p Q.
Proof. destruct p; simpl; auto using persistently_and. Qed.
......@@ -1338,7 +1381,7 @@ Proof. destruct p; simpl; auto using intuitionistically_elim. Qed.
Lemma intuitionistically_if_intro' p P Q : (?p P Q) ?p P ?p Q.
Proof. destruct p; simpl; auto using intuitionistically_intro'. Qed.
Lemma intuitionistically_if_emp p : ?p emp emp.
Lemma intuitionistically_if_emp `{!BiPersistentlyEmp PROP} p : ?p emp emp.
Proof. destruct p; simpl; auto using intuitionistically_emp. Qed.
Lemma intuitionistically_if_False p : ?p False False.
Proof. destruct p; simpl; auto using intuitionistically_False. Qed.
......@@ -1371,9 +1414,13 @@ Lemma persistent_persistently P `{!Persistent P, !Absorbing P} : <pers> P ⊣⊢
Proof.
apply (anti_symm _); auto using persistent_persistently_2, persistently_elim.
Qed.
Lemma persistently_intro P Q `{!Persistent P} : (P Q) P <pers> Q.
Proof. intros HP. by rewrite (persistent P) HP. Qed.
Lemma persistent_and_sep_assoc P `{!Persistent P, !Absorbing P} Q R :
P (Q R) (P Q) R.
Proof. by rewrite -(persistent_persistently P) persistently_and_sep_assoc. Qed.
Lemma persistent_and_affinely_sep_l_1 P Q `{!Persistent P} : P Q <affine> P Q.
Proof.
rewrite {1}(persistent_persistently_2 P) persistently_and_intuitionistically_sep_l.
......@@ -1389,6 +1436,13 @@ Lemma persistent_and_affinely_sep_r P Q `{!Persistent Q, !Absorbing Q} :
P Q P <affine> Q.
Proof. by rewrite -(persistent_persistently Q) persistently_and_intuitionistically_sep_r. Qed.
Lemma persistent_sep_absorbingly_and_l P Q `{!Persistent P, !Absorbing P} :
P Q P <absorb> Q.
Proof.
trans ((P True) Q)%I; first by rewrite right_id.
rewrite persistent_and_sep_assoc //.
Qed.
Lemma persistent_and_sep_1 P Q `{HPQ : !TCOr (Persistent P) (Persistent Q)} :