Commit 4b43fcc2 authored by Ralf Jung's avatar Ralf Jung

make BUpdFacts depend on SBI

parent 98d8373b
...@@ -677,7 +677,7 @@ Lemma ofe_fun_validI `{Finite A} {B : A → ucmraT} (g : ofe_fun B) : ...@@ -677,7 +677,7 @@ Lemma ofe_fun_validI `{Finite A} {B : A → ucmraT} (g : ofe_fun B) :
Proof. by uPred.unseal. Qed. Proof. by uPred.unseal. Qed.
(* Basic update modality *) (* Basic update modality *)
Global Instance bupd_facts : BUpdFacts (uPredI M). Global Instance bupd_facts : BUpdFacts (uPredSI M).
Proof. Proof.
split. split.
- intros n P Q HPQ. - intros n P Q HPQ.
......
...@@ -252,11 +252,11 @@ Ltac unseal := ...@@ -252,11 +252,11 @@ Ltac unseal :=
unfold bi_affinely, bi_absorbingly, sbi_except_0, bi_pure, bi_emp, unfold bi_affinely, bi_absorbingly, sbi_except_0, bi_pure, bi_emp,
monPred_absolutely, monPred_relatively, monPred_upclosed, bi_and, bi_or, monPred_absolutely, monPred_relatively, monPred_upclosed, bi_and, bi_or,
bi_impl, bi_forall, bi_exist, sbi_internal_eq, bi_sep, bi_wand, bi_impl, bi_forall, bi_exist, sbi_internal_eq, bi_sep, bi_wand,
bi_persistently, bi_affinely, sbi_later; bi_persistently, bi_affinely, bi_plainly, sbi_later;
simpl; simpl;
unfold sbi_emp, sbi_pure, sbi_and, sbi_or, sbi_impl, sbi_forall, sbi_exist, unfold sbi_emp, sbi_pure, sbi_and, sbi_or, sbi_impl, sbi_forall, sbi_exist,
sbi_internal_eq, sbi_sep, sbi_wand, sbi_persistently, sbi_plainly, sbi_internal_eq, sbi_sep, sbi_wand, sbi_persistently, sbi_plainly;
bi_plainly; simpl; simpl;
unfold monPred_pure, monPred_emp, monPred_internal_eq, monPred_plainly; simpl; unfold monPred_pure, monPred_emp, monPred_internal_eq, monPred_plainly; simpl;
rewrite !unseal_eqs /=. rewrite !unseal_eqs /=.
End MonPred. End MonPred.
...@@ -472,22 +472,6 @@ Proof. ...@@ -472,22 +472,6 @@ Proof.
by apply bi.forall_intro. by rewrite bi.forall_elim. by apply bi.forall_intro. by rewrite bi.forall_elim.
Qed. Qed.
Global Instance monPred_bupd_facts `{BUpdFacts PROP} : BUpdFacts monPredI.
Proof.
split; unseal; unfold monPred_bupd_def, monPred_upclosed.
- intros n P Q HPQ. split=>/= i. by repeat f_equiv.
- intros P. split=>/= i. apply bi.forall_intro=>?. rewrite bi.pure_impl_forall.
apply bi.forall_intro=><-. apply bupd_intro.
- intros P Q HPQ. split=>/= i. by repeat f_equiv.
- intros P. split=>/= i. do 3 f_equiv. rewrite -(bupd_trans (P _))
bi.forall_elim bi.pure_impl_forall bi.forall_elim //.
- intros P Q. split=> /= i. apply bi.forall_intro=>?.
rewrite bi.pure_impl_forall. apply bi.forall_intro=><-.
rewrite -bupd_frame_r bi.forall_elim bi.pure_impl_forall bi.forall_elim //.
- intros P. split=> /= i. rewrite bi.forall_elim bi.pure_impl_forall
bi.forall_elim // -bi.plainly_forall bupd_plainly bi.forall_elim //.
Qed.
Global Instance monPred_absolutely_ne : NonExpansive (@monPred_absolutely I PROP). Global Instance monPred_absolutely_ne : NonExpansive (@monPred_absolutely I PROP).
Proof. rewrite /monPred_absolutely /=. solve_proper. Qed. Proof. rewrite /monPred_absolutely /=. solve_proper. Qed.
Global Instance monPred_absolutely_proper : Proper (() ==> ()) (@monPred_absolutely I PROP). Global Instance monPred_absolutely_proper : Proper (() ==> ()) (@monPred_absolutely I PROP).
...@@ -564,12 +548,6 @@ Lemma monPred_at_absolutely i P : (∀ᵢ P) i ⊣⊢ ∀ j, P j. ...@@ -564,12 +548,6 @@ Lemma monPred_at_absolutely i P : (∀ᵢ P) i ⊣⊢ ∀ j, P j.
Proof. by unseal. Qed. Proof. by unseal. Qed.
Lemma monPred_at_ex i P : ( P) i j, P j. Lemma monPred_at_ex i P : ( P) i j, P j.
Proof. by unseal. Qed. Proof. by unseal. Qed.
Lemma monPred_at_bupd `{BUpdFacts PROP} i P : (|==> P) i |==> P i.
Proof.
unseal. setoid_rewrite bi.pure_impl_forall. apply bi.equiv_spec; split.
- rewrite !bi.forall_elim //.
- do 2 apply bi.forall_intro=>?. by do 2 f_equiv.
Qed.
Lemma monPred_at_persistently_if i p P : Lemma monPred_at_persistently_if i p P :
bi_persistently_if p P i bi_persistently_if p (P i). bi_persistently_if p P i bi_persistently_if p (P i).
Proof. destruct p=>//=. apply monPred_at_persistently. Qed. Proof. destruct p=>//=. apply monPred_at_persistently. Qed.
...@@ -709,10 +687,6 @@ Global Instance persistently_absolute P `{!Absolute P} : ...@@ -709,10 +687,6 @@ Global Instance persistently_absolute P `{!Absolute P} :
Absolute (bi_persistently P). Absolute (bi_persistently P).
Proof. intros ??. unseal. by rewrite absolute_at. Qed. Proof. intros ??. unseal. by rewrite absolute_at. Qed.
Global Instance bupd_absolute `{BUpdFacts PROP} P `{!Absolute P} :
Absolute (|==> P)%I.
Proof. intros ??. by rewrite !monPred_at_bupd absolute_at. Qed.
Global Instance affinely_absolute P `{!Absolute P} : Absolute (bi_affinely P). Global Instance affinely_absolute P `{!Absolute P} : Absolute (bi_affinely P).
Proof. rewrite /bi_affinely. apply _. Qed. Proof. rewrite /bi_affinely. apply _. Qed.
Global Instance absorbingly_absolute P `{!Absolute P} : Global Instance absorbingly_absolute P `{!Absolute P} :
...@@ -740,15 +714,6 @@ Proof. ...@@ -740,15 +714,6 @@ Proof.
eapply bi.pure_elim; [apply bi.and_elim_l|]=>?. rewrite bi.and_elim_r. by f_equiv. eapply bi.pure_elim; [apply bi.and_elim_l|]=>?. rewrite bi.and_elim_r. by f_equiv.
Qed. Qed.
(** bupd *)
Lemma monPred_bupd_embed `{BUpdFacts PROP} (P : PROP) :
|==> P bupd (PROP:=monPredI) P.
Proof.
unseal. split=>i /=. setoid_rewrite bi.pure_impl_forall. apply bi.equiv_spec; split.
- by do 2 apply bi.forall_intro=>?.
- rewrite !bi.forall_elim //.
Qed.
(** Big op *) (** Big op *)
Global Instance monPred_at_monoid_and_homomorphism i : Global Instance monPred_at_monoid_and_homomorphism i :
MonoidHomomorphism bi_and bi_and () (flip monPred_at i). MonoidHomomorphism bi_and bi_and () (flip monPred_at i).
...@@ -847,6 +812,41 @@ Local Notation monPredSI := (monPredSI I PROP). ...@@ -847,6 +812,41 @@ Local Notation monPredSI := (monPredSI I PROP).
Implicit Types i : I. Implicit Types i : I.
Implicit Types P Q : monPred. Implicit Types P Q : monPred.
(** bupd *)
Global Instance monPred_bupd_facts `{BUpdFacts PROP} : BUpdFacts monPredSI.
Proof.
split; unseal; unfold monPred_bupd_def, monPred_upclosed.
- intros n P Q HPQ. split=>/= i. by repeat f_equiv.
- intros P. split=>/= i. apply bi.forall_intro=>?. rewrite bi.pure_impl_forall.
apply bi.forall_intro=><-. apply bupd_intro.
- intros P Q HPQ. split=>/= i. by repeat f_equiv.
- intros P. split=>/= i. do 3 f_equiv. rewrite -(bupd_trans (P _))
bi.forall_elim bi.pure_impl_forall bi.forall_elim //.
- intros P Q. split=> /= i. apply bi.forall_intro=>?.
rewrite bi.pure_impl_forall. apply bi.forall_intro=><-.
rewrite -bupd_frame_r bi.forall_elim bi.pure_impl_forall bi.forall_elim //.
- intros P. split=> /= i. rewrite bi.forall_elim bi.pure_impl_forall
bi.forall_elim // -bi.plainly_forall bupd_plainly bi.forall_elim //.
Qed.
Lemma monPred_at_bupd `{BUpdFacts PROP} i P : (|==> P) i |==> P i.
Proof.
unseal. setoid_rewrite bi.pure_impl_forall. apply bi.equiv_spec; split.
- rewrite !bi.forall_elim //.
- do 2 apply bi.forall_intro=>?. by do 2 f_equiv.
Qed.
Global Instance bupd_absolute `{BUpdFacts PROP} P `{!Absolute P} :
Absolute (|==> P)%I.
Proof. intros ??. by rewrite !monPred_at_bupd absolute_at. Qed.
Lemma monPred_bupd_embed `{BUpdFacts PROP} (P : PROP) :
|==> P bupd (PROP:=monPredSI) P.
Proof.
unseal. split=>i /=. setoid_rewrite bi.pure_impl_forall. apply bi.equiv_spec; split.
- by do 2 apply bi.forall_intro=>?.
- rewrite !bi.forall_elim //.
Qed.
Global Instance monPred_at_timeless P i : Timeless P Timeless (P i). Global Instance monPred_at_timeless P i : Timeless P Timeless (P i).
Proof. move => [] /(_ i). unfold Timeless. by unseal. Qed. Proof. move => [] /(_ i). unfold Timeless. by unseal. Qed.
Global Instance monPred_in_timeless i0 : Timeless (@monPred_in I PROP i0). Global Instance monPred_in_timeless i0 : Timeless (@monPred_in I PROP i0).
......
...@@ -51,13 +51,13 @@ Notation "P ={ E }▷=∗ Q" := (P ={E,E}▷=∗ Q)%I ...@@ -51,13 +51,13 @@ Notation "P ={ E }▷=∗ Q" := (P ={E,E}▷=∗ Q)%I
(** BUpd facts *) (** BUpd facts *)
Class BUpdFacts (PROP : bi) `{BUpd PROP} : Prop := Class BUpdFacts (PROP : sbi) `{BUpd PROP} : Prop :=
{ bupd_ne :> NonExpansive bupd; { bupd_ne :> NonExpansive bupd;
bupd_intro P : P == P; bupd_intro (P : PROP) : P == P;
bupd_mono P Q : (P Q) (|==> P) == Q; bupd_mono (P Q : PROP) : (P Q) (|==> P) == Q;
bupd_trans P : (|==> |==> P) == P; bupd_trans (P : PROP) : (|==> |==> P) == P;
bupd_frame_r P R : (|==> P) R == P R; bupd_frame_r (P R : PROP) : (|==> P) R == P R;
bupd_plainly P : (|==> bi_plainly P) - P }. bupd_plainly (P : PROP) : (|==> bi_plainly P) - P }.
Hint Mode BUpdFacts ! - : typeclass_instances. Hint Mode BUpdFacts ! - : typeclass_instances.
Section bupd_derived. Section bupd_derived.
......
This diff is collapsed.
...@@ -102,9 +102,6 @@ Global Instance make_monPred_at_in i j : MakeMonPredAt j (monPred_in i) ⌜i ⊑ ...@@ -102,9 +102,6 @@ Global Instance make_monPred_at_in i j : MakeMonPredAt j (monPred_in i) ⌜i ⊑
Proof. by rewrite /MakeMonPredAt monPred_at_in. Qed. Proof. by rewrite /MakeMonPredAt monPred_at_in. Qed.
Global Instance make_monPred_at_default i P : MakeMonPredAt i P (P i) | 100. Global Instance make_monPred_at_default i P : MakeMonPredAt i P (P i) | 100.
Proof. by rewrite /MakeMonPredAt. Qed. Proof. by rewrite /MakeMonPredAt. Qed.
Global Instance make_monPred_at_bupd `{BUpdFacts PROP} i P 𝓟 :
MakeMonPredAt i P 𝓟 MakeMonPredAt i (|==> P)%I (|==> 𝓟)%I.
Proof. by rewrite /MakeMonPredAt monPred_at_bupd=> <-. Qed.
Global Instance from_assumption_make_monPred_at_l p i j P 𝓟 : Global Instance from_assumption_make_monPred_at_l p i j P 𝓟 :
MakeMonPredAt i P 𝓟 IsBiIndexRel j i FromAssumption p (P j) 𝓟. MakeMonPredAt i P 𝓟 IsBiIndexRel j i FromAssumption p (P j) 𝓟.
...@@ -369,31 +366,6 @@ Global Instance from_modal_monPred_at i P Q 𝓠 : ...@@ -369,31 +366,6 @@ Global Instance from_modal_monPred_at i P Q 𝓠 :
FromModal P Q MakeMonPredAt i Q 𝓠 FromModal (P i) 𝓠. FromModal P Q MakeMonPredAt i Q 𝓠 FromModal (P i) 𝓠.
Proof. by rewrite /FromModal /MakeMonPredAt=> <- <-. Qed. Proof. by rewrite /FromModal /MakeMonPredAt=> <- <-. Qed.
Global Instance elim_modal_embed_bupd_goal `{BUpdFacts PROP} φ P P' 𝓠 𝓠' :
ElimModal φ P P' (|==> ⎡𝓠⎤)%I (|==> ⎡𝓠')%I
ElimModal φ P P' |==> 𝓠⎤ |==> 𝓠'.
Proof. by rewrite /ElimModal !monPred_bupd_embed. Qed.
Global Instance elim_modal_embed_bupd_hyp `{BUpdFacts PROP} φ 𝓟 P' Q Q' :
ElimModal φ (|==> ⎡𝓟⎤)%I P' Q Q'
ElimModal φ |==> 𝓟⎤ P' Q Q'.
Proof. by rewrite /ElimModal monPred_bupd_embed. Qed.
Global Instance add_modal_embed_bupd_goal `{BUpdFacts PROP} P P' 𝓠 :
AddModal P P' (|==> ⎡𝓠⎤)%I AddModal P P' |==> 𝓠⎤.
Proof. by rewrite /AddModal !monPred_bupd_embed. Qed.
Global Instance elim_modal_at_bupd_goal `{BUpdFacts PROP} φ 𝓟 𝓟' Q Q' i :
ElimModal φ 𝓟 𝓟' (|==> Q i) (|==> Q' i)
ElimModal φ 𝓟 𝓟' ((|==> Q) i) ((|==> Q') i).
Proof. by rewrite /ElimModal !monPred_at_bupd. Qed.
Global Instance elim_modal_at_bupd_hyp `{BUpdFacts PROP} φ P 𝓟' 𝓠 𝓠' i:
ElimModal φ (|==> P i) 𝓟' 𝓠 𝓠'
ElimModal φ ((|==> P) i) 𝓟' 𝓠 𝓠'.
Proof. by rewrite /ElimModal monPred_at_bupd. Qed.
Global Instance add_modal_at_bupd_goal `{BUpdFacts PROP} φ 𝓟 𝓟' Q i :
AddModal 𝓟 𝓟' (|==> Q i)%I AddModal 𝓟 𝓟' ((|==> Q) i).
Proof. by rewrite /AddModal !monPred_at_bupd. Qed.
End bi. End bi.
(* When P and/or Q are evars when doing typeclass search on [IntoWand (* When P and/or Q are evars when doing typeclass search on [IntoWand
...@@ -442,6 +414,9 @@ Proof. by rewrite /MakeMonPredAt monPred_at_later=><-. Qed. ...@@ -442,6 +414,9 @@ Proof. by rewrite /MakeMonPredAt monPred_at_later=><-. Qed.
Global Instance make_monPred_at_laterN i n P 𝓠 : Global Instance make_monPred_at_laterN i n P 𝓠 :
MakeMonPredAt i P 𝓠 MakeMonPredAt i (^n P)%I (^n 𝓠)%I. MakeMonPredAt i P 𝓠 MakeMonPredAt i (^n P)%I (^n 𝓠)%I.
Proof. rewrite /MakeMonPredAt=> <-. elim n=>//= ? <-. by rewrite monPred_at_later. Qed. Proof. rewrite /MakeMonPredAt=> <-. elim n=>//= ? <-. by rewrite monPred_at_later. Qed.
Global Instance make_monPred_at_bupd `{BUpdFacts PROP} i P 𝓟 :
MakeMonPredAt i P 𝓟 MakeMonPredAt i (|==> P)%I (|==> 𝓟)%I.
Proof. by rewrite /MakeMonPredAt monPred_at_bupd=> <-. Qed.
Global Instance make_monPred_at_fupd `{FUpdFacts PROP} i E1 E2 P 𝓟 : Global Instance make_monPred_at_fupd `{FUpdFacts PROP} i E1 E2 P 𝓟 :
MakeMonPredAt i P 𝓟 MakeMonPredAt i (|={E1,E2}=> P)%I (|={E1,E2}=> 𝓟)%I. MakeMonPredAt i P 𝓟 MakeMonPredAt i (|={E1,E2}=> P)%I (|={E1,E2}=> 𝓟)%I.
Proof. by rewrite /MakeMonPredAt monPred_at_fupd=> <-. Qed. Proof. by rewrite /MakeMonPredAt monPred_at_fupd=> <-. Qed.
...@@ -470,6 +445,32 @@ Proof. ...@@ -470,6 +445,32 @@ Proof.
by rewrite monPred_at_later. by rewrite monPred_at_later.
Qed. Qed.
Global Instance elim_modal_embed_bupd_goal `{BUpdFacts PROP} φ P P' 𝓠 𝓠' :
ElimModal φ P P' (|==> ⎡𝓠⎤)%I (|==> ⎡𝓠')%I
ElimModal φ P P' |==> 𝓠⎤ |==> 𝓠'.
Proof. by rewrite /ElimModal !monPred_bupd_embed. Qed.
Global Instance elim_modal_embed_bupd_hyp `{BUpdFacts PROP} φ 𝓟 P' Q Q' :
ElimModal φ (|==> ⎡𝓟⎤)%I P' Q Q'
ElimModal φ |==> 𝓟⎤ P' Q Q'.
Proof. by rewrite /ElimModal monPred_bupd_embed. Qed.
Global Instance add_modal_embed_bupd_goal `{BUpdFacts PROP} P P' 𝓠 :
AddModal P P' (|==> ⎡𝓠⎤)%I AddModal P P' |==> 𝓠⎤.
Proof. by rewrite /AddModal !monPred_bupd_embed. Qed.
Global Instance elim_modal_at_bupd_goal `{BUpdFacts PROP} φ 𝓟 𝓟' Q Q' i :
ElimModal φ 𝓟 𝓟' (|==> Q i) (|==> Q' i)
ElimModal φ 𝓟 𝓟' ((|==> Q) i) ((|==> Q') i).
Proof. by rewrite /ElimModal !monPred_at_bupd. Qed.
Global Instance elim_modal_at_bupd_hyp `{BUpdFacts PROP} φ P 𝓟' 𝓠 𝓠' i:
ElimModal φ (|==> P i) 𝓟' 𝓠 𝓠'
ElimModal φ ((|==> P) i) 𝓟' 𝓠 𝓠'.
Proof. by rewrite /ElimModal monPred_at_bupd. Qed.
Global Instance add_modal_at_bupd_goal `{BUpdFacts PROP} φ 𝓟 𝓟' Q i :
AddModal 𝓟 𝓟' (|==> Q i)%I AddModal 𝓟 𝓟' ((|==> Q) i).
Proof. by rewrite /AddModal !monPred_at_bupd. Qed.
Global Instance elim_modal_embed_fupd_goal `{FUpdFacts PROP} φ E1 E2 E3 P P' 𝓠 𝓠' : Global Instance elim_modal_embed_fupd_goal `{FUpdFacts PROP} φ E1 E2 E3 P P' 𝓠 𝓠' :
ElimModal φ P P' (|={E1,E3}=> ⎡𝓠⎤)%I (|={E2,E3}=> ⎡𝓠')%I ElimModal φ P P' (|={E1,E3}=> ⎡𝓠⎤)%I (|={E2,E3}=> ⎡𝓠')%I
ElimModal φ P P' |={E1,E3}=> 𝓠⎤ |={E2,E3}=> 𝓠'. ElimModal φ P P' |={E1,E3}=> 𝓠⎤ |={E2,E3}=> 𝓠'.
......
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