Commit a0e83ac1 authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan

Add BUpdFacts and FUpdFacts.

parent 17bfc2e7
......@@ -23,23 +23,14 @@ Hint Immediate True_intro False_elim : I.
Hint Immediate iff_refl internal_eq_refl : I.
(* Setup of the proof mode *)
Hint Extern 1 (coq_tactics.envs_entails _ (|==> _)) => iModIntro.
Section class_instances.
Context {M : ucmraT}.
Implicit Types P Q R : uPred M.
Global Instance from_assumption_bupd p P Q :
FromAssumption p P Q FromAssumption p P (|==> Q).
Proof. rewrite /FromAssumption=>->. apply bupd_intro. Qed.
Global Instance into_pure_cmra_valid `{CmraDiscrete A} (a : A) :
@IntoPure (uPredI M) ( a) ( a).
Proof. by rewrite /IntoPure discrete_valid. Qed.
Global Instance from_pure_bupd P φ : FromPure P φ FromPure (|==> P) φ.
Proof. rewrite /FromPure=> ->. apply bupd_intro. Qed.
Global Instance from_pure_cmra_valid {A : cmraT} (a : A) :
@FromPure (uPredI M) ( a) ( a).
Proof.
......@@ -47,27 +38,6 @@ Proof.
rewrite -cmra_valid_intro //. by apply pure_intro.
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 !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 affinely_persistently_if_elim HR.
apply wand_intro_l. by rewrite bupd_frame_l wand_elim_r.
Qed.
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 affinely_persistently_if_elim bupd_wand_r.
Qed.
(* FromOp *)
(* TODO: Worst case there could be a lot of backtracking on these instances,
try to refactor. *)
......@@ -110,45 +80,4 @@ Qed.
Global Instance into_sep_ownM (a b1 b2 : M) :
IsOp a b1 b2 IntoSep (uPred_ownM a) (uPred_ownM b1) (uPred_ownM b2).
Proof. intros. by rewrite /IntoSep (is_op a) ownM_op. Qed.
Global Instance from_sep_bupd P Q1 Q2 :
FromSep P Q1 Q2 FromSep (|==> P) (|==> Q1) (|==> Q2).
Proof. rewrite /FromSep=><-. apply bupd_sep. Qed.
Global Instance from_or_bupd P Q1 Q2 :
FromOr P Q1 Q2 FromOr (|==> P) (|==> Q1) (|==> Q2).
Proof.
rewrite /FromOr=><-.
apply or_elim; apply bupd_mono; auto using or_intro_l, or_intro_r.
Qed.
Global Instance from_exist_bupd {A} P (Φ : A uPred M) :
FromExist P Φ FromExist (|==> P) (λ a, |==> Φ a)%I.
Proof.
rewrite /FromExist=><-. apply exist_elim=> a. by rewrite -(exist_intro a).
Qed.
Global Instance from_modal_bupd P : FromModal (|==> P) P.
Proof. apply bupd_intro. Qed.
Global Instance elim_modal_bupd P Q : ElimModal (|==> P) P (|==> Q) (|==> Q).
Proof. by rewrite /ElimModal bupd_frame_r wand_elim_r bupd_trans. Qed.
Global Instance elim_modal_bupd_plain_goal P Q : Plain Q ElimModal (|==> P) P Q Q.
Proof. intros. by rewrite /ElimModal bupd_frame_r wand_elim_r bupd_plain. Qed.
Global Instance elim_modal_bupd_plain P Q : Plain P ElimModal (|==> P) P Q Q.
Proof. intros. by rewrite /ElimModal bupd_plain wand_elim_r. Qed.
Global Instance add_modal_bupd P Q : AddModal (|==> P) P (|==> Q).
Proof. by rewrite /AddModal bupd_frame_r wand_elim_r bupd_trans. Qed.
Global Instance is_except_0_bupd P : IsExcept0 P IsExcept0 (|==> P).
Proof.
rewrite /IsExcept0=> HP.
by rewrite -{2}HP -(except_0_idemp P) -except_0_bupd -(except_0_intro P).
Qed.
Global Instance frame_bupd p R P Q : Frame p R P Q Frame p R (|==> P) (|==> Q).
Proof. rewrite /Frame=><-. by rewrite bupd_frame_l. Qed.
End class_instances.
......@@ -40,31 +40,11 @@ Proof.
rewrite affine_affinely. intros; apply (anti_symm _); first by rewrite persistently_elim.
apply:persistently_cmra_valid_1.
Qed.
(** * Derived rules *)
Global Instance bupd_mono' : Proper (() ==> ()) (@bupd _ (@uPred_bupd M)).
Proof. intros P Q; apply bupd_mono. Qed.
Global Instance bupd_flip_mono' :
Proper (flip () ==> flip ()) (@bupd _ (@uPred_bupd M)).
Proof. intros P Q; apply bupd_mono. Qed.
Lemma bupd_frame_l R Q : (R |==> Q) == R Q.
Proof. rewrite !(comm _ R); apply bupd_frame_r. Qed.
Lemma bupd_wand_l P Q : (P - Q) (|==> P) == Q.
Proof. by rewrite bupd_frame_l wand_elim_l. Qed.
Lemma bupd_wand_r P Q : (|==> P) (P - Q) == Q.
Proof. by rewrite bupd_frame_r wand_elim_r. Qed.
Lemma bupd_sep P Q : (|==> P) (|==> Q) == P Q.
Proof. by rewrite bupd_frame_r bupd_frame_l bupd_trans. Qed.
Lemma bupd_ownM_update x y : x ~~> y uPred_ownM x |==> uPred_ownM y.
Proof.
intros; rewrite (bupd_ownM_updateP _ (y =)); last by apply cmra_update_updateP.
by apply bupd_mono, exist_elim=> y'; apply pure_elim_l=> ->.
Qed.
Lemma except_0_bupd P : (|==> P) (|==> P).
Proof.
rewrite /sbi_except_0. apply or_elim; eauto using bupd_mono, or_intro_r.
by rewrite -bupd_intro -or_intro_l.
Qed.
(* Timeless instances *)
Global Instance valid_timeless {A : cmraT} `{CmraDiscrete A} (a : A) :
......@@ -84,12 +64,6 @@ Global Instance cmra_valid_plain {A : cmraT} (a : A) :
Plain ( a : uPred M)%I.
Proof. rewrite /Persistent. apply plainly_cmra_valid_1. Qed.
Lemma bupd_affinely_plainly P : (|==> P) P.
Proof. by rewrite affine_affinely bupd_plainly. Qed.
Lemma bupd_plain P `{!Plain P} : (|==> P) P.
Proof. by rewrite -{1}(plain_plainly P) bupd_plainly. Qed.
(* Persistence *)
Global Instance cmra_valid_persistent {A : cmraT} (a : A) :
Persistent ( a : uPred M)%I.
......
This diff is collapsed.
......@@ -601,16 +601,6 @@ Qed.
Global Instance cmra_valid_proper {A : cmraT} :
Proper (() ==> ()) (@uPred_cmra_valid M A) := ne_proper _.
Global Instance bupd_ne : NonExpansive (@bupd _ (@uPred_bupd M)).
Proof.
intros n P Q HPQ.
unseal; split=> n' x; split; intros HP k yf ??;
destruct (HP k yf) as (x'&?&?); auto;
exists x'; split; auto; apply HPQ; eauto using cmra_validN_op_l.
Qed.
Global Instance bupd_proper :
Proper (() ==> ()) (@bupd _ (@uPred_bupd M)) := ne_proper _.
(** BI instances *)
Global Instance uPred_affine : BiAffine (uPredI M) | 0.
......@@ -686,27 +676,29 @@ Lemma ofe_fun_validI `{Finite A} {B : A → ucmraT} (g : ofe_fun B) :
Proof. by uPred.unseal. Qed.
(* Basic update modality *)
Lemma bupd_intro P : P == P.
Proof.
unseal. split=> n x ? HP k yf ?; exists x; split; first done.
apply uPred_mono with n x; eauto using cmra_validN_op_l.
Qed.
Lemma bupd_mono P Q : (P Q) (|==> P) == Q.
Global Instance bupd_facts : BUpdFacts (uPredI M).
Proof.
unseal. intros HPQ; split=> n x ? HP k yf ??.
destruct (HP k yf) as (x'&?&?); eauto.
exists x'; split; eauto using uPred_in_entails, cmra_validN_op_l.
Qed.
Lemma bupd_trans P : (|==> |==> P) == P.
Proof. unseal; split; naive_solver. Qed.
Lemma bupd_frame_r P R : (|==> P) R == P R.
Proof.
unseal. split; intros n x ? (x1&x2&Hx&HP&?) k yf ??.
destruct (HP k (x2 yf)) as (x'&?&?); eauto.
{ by rewrite assoc -(dist_le _ _ _ _ Hx); last lia. }
exists (x' x2); split; first by rewrite -assoc.
exists x', x2. eauto using uPred_mono, cmra_validN_op_l, cmra_validN_op_r.
split.
- intros n P Q HPQ.
unseal; split=> n' x; split; intros HP k yf ??;
destruct (HP k yf) as (x'&?&?); auto;
exists x'; split; auto; apply HPQ; eauto using cmra_validN_op_l.
- unseal. split=> n x ? HP k yf ?; exists x; split; first done.
apply uPred_mono with n x; eauto using cmra_validN_op_l.
- unseal. intros HPQ; split=> n x ? HP k yf ??.
destruct (HP k yf) as (x'&?&?); eauto.
exists x'; split; eauto using uPred_in_entails, cmra_validN_op_l.
- unseal; split; naive_solver.
- unseal. split; intros n x ? (x1&x2&Hx&HP&?) k yf ??.
destruct (HP k (x2 yf)) as (x'&?&?); eauto.
{ by rewrite assoc -(dist_le _ _ _ _ Hx); last lia. }
exists (x' x2); split; first by rewrite -assoc.
exists x', x2. eauto using uPred_mono, cmra_validN_op_l, cmra_validN_op_r.
- unseal; split => n x Hnx /= Hng.
destruct (Hng n ε) as [? [_ Hng']]; try rewrite right_id; auto.
eapply uPred_mono; eauto using ucmra_unit_leastN.
Qed.
Lemma bupd_ownM_updateP x (Φ : M Prop) :
x ~~>: Φ uPred_ownM x == y, ⌜Φ y uPred_ownM y.
Proof.
......@@ -716,11 +708,5 @@ Proof.
exists (y x3); split; first by rewrite -assoc.
exists y; eauto using cmra_includedN_l.
Qed.
Lemma bupd_plainly P : (|==> bi_plainly P) P.
Proof.
unseal; split => n x Hnx /= Hng.
destruct (Hng n ε) as [? [_ Hng']]; try rewrite right_id; auto.
eapply uPred_mono; eauto using ucmra_unit_leastN.
Qed.
End uPred.
End uPred.
From stdpp Require Import coPset.
From iris.bi Require Import interface.
From iris.bi Require Import interface derived_laws big_op.
Class BUpd (A : Type) : Type := bupd : A A.
Class BUpd (PROP : Type) : Type := bupd : PROP PROP.
Instance : Params (@bupd) 2.
Notation "|==> Q" := (bupd Q)
......@@ -11,7 +11,7 @@ Notation "P ==∗ Q" := (P ⊢ |==> Q)
Notation "P ==∗ Q" := (P - |==> Q)%I
(at level 99, Q at level 200, format "P ==∗ Q") : bi_scope.
Class FUpd (A : Type) : Type := fupd : coPset coPset A A.
Class FUpd (PROP : Type) : Type := fupd : coPset coPset PROP PROP.
Instance: Params (@fupd) 4.
Notation "|={ E1 , E2 }=> Q" := (fupd E1 E2 Q)
......@@ -46,3 +46,174 @@ Notation "|={ E }▷=> Q" := (|={E,E}▷=> Q)%I
Notation "P ={ E }▷=∗ Q" := (P ={E,E}= Q)%I
(at level 99, E at level 50, Q at level 200,
format "P ={ E }▷=∗ Q") : bi_scope.
(** BUpd facts *)
Class BUpdFacts (PROP : bi) `{BUpd PROP} : Prop :=
{ bupd_ne :> NonExpansive bupd;
bupd_intro P : P == P;
bupd_mono P Q : (P Q) (|==> P) == Q;
bupd_trans P : (|==> |==> P) == P;
bupd_frame_r P R : (|==> P) R == P R;
bupd_plainly P : (|==> bi_plainly P) - P }.
Section bupd_derived.
Context `{BUpdFacts PROP}.
Global Instance bupd_proper : Proper (() ==> ()) bupd := ne_proper _.
(** BUpd derived rules *)
Global Instance bupd_mono' : Proper (() ==> ()) bupd.
Proof. intros P Q; apply bupd_mono. Qed.
Global Instance bupd_flip_mono' : Proper (flip () ==> flip ()) bupd.
Proof. intros P Q; apply bupd_mono. Qed.
Lemma bupd_frame_l R Q : (R |==> Q) == R Q.
Proof. rewrite !(comm _ R); apply bupd_frame_r. Qed.
Lemma bupd_wand_l P Q : (P - Q) (|==> P) == Q.
Proof. by rewrite bupd_frame_l bi.wand_elim_l. Qed.
Lemma bupd_wand_r P Q : (|==> P) (P - Q) == Q.
Proof. by rewrite bupd_frame_r bi.wand_elim_r. Qed.
Lemma bupd_sep P Q : (|==> P) (|==> Q) == P Q.
Proof. by rewrite bupd_frame_r bupd_frame_l bupd_trans. Qed.
Lemma bupd_affinely_plainly `{BiAffine PROP} P : (|==> P) P.
Proof. by rewrite bi.affine_affinely bupd_plainly. Qed.
Lemma bupd_plain P `{!Plain P} : (|==> P) P.
Proof. by rewrite {1}(plain P) bupd_plainly. Qed.
End bupd_derived.
Lemma except_0_bupd {PROP : sbi} `{BUpdFacts PROP} (P : PROP) :
(|==> P) (|==> P).
Proof.
rewrite /sbi_except_0. apply bi.or_elim; eauto using bupd_mono, bi.or_intro_r.
by rewrite -bupd_intro -bi.or_intro_l.
Qed.
(** FUpd facts *)
(* Currently, this requires an SBI, because of [except_0_fupd] and
[later_fupd_plain]. If need be, we can generalize this to BIs by
extracting these propertes as lemmas to be proved by hand. *)
Class FUpdFacts (PROP : sbi) `{BUpd PROP, FUpd PROP} : Prop :=
{ fupd_bupd_facts :> BUpdFacts PROP;
fupd_ne E1 E2 :> NonExpansive (fupd E1 E2);
fupd_intro_mask E1 E2 P : E2 E1 P |={E1,E2}=> |={E2,E1}=> P;
bupd_fupd E P : (|==> P) ={E}= P;
except_0_fupd E1 E2 P : (|={E1,E2}=> P) ={E1,E2}= P;
fupd_mono E1 E2 P Q : (P Q) (|={E1,E2}=> P) |={E1,E2}=> Q;
fupd_trans E1 E2 E3 P : (|={E1,E2}=> |={E2,E3}=> P) |={E1,E3}=> P;
fupd_mask_frame_r' E1 E2 Ef P :
E1 ## Ef (|={E1,E2}=> E2 ## Ef P) ={E1 Ef,E2 Ef}= P;
fupd_frame_r E1 E2 P Q : (|={E1,E2}=> P) Q ={E1,E2}= P Q;
fupd_plain' E1 E2 E2' P Q `{!Plain P} :
E1 E2
(Q ={E1, E2'}= P) - (|={E1, E2}=> Q) ={E1}= (|={E1, E2}=> Q) P;
later_fupd_plain E P `{!Plain P} : ( |={E}=> P) ={E}= P }.
Section fupd_derived.
Context `{FUpdFacts PROP}.
Global Instance fupd_proper E1 E2 : Proper (() ==> ()) (fupd E1 E2) := ne_proper _.
(** FUpd derived rules *)
Global Instance fupd_mono' E1 E2 : Proper (() ==> ()) (fupd E1 E2).
Proof. intros P Q; apply fupd_mono. Qed.
Global Instance fupd_flip_mono' E1 E2 :
Proper (flip () ==> flip ()) (fupd E1 E2).
Proof. intros P Q; apply fupd_mono. Qed.
Lemma fupd_intro E P : P ={E}= P.
Proof. rewrite -bupd_fupd. apply bupd_intro. Qed.
Lemma fupd_intro_mask' E1 E2 : E2 E1 (|={E1,E2}=> |={E2,E1}=> emp)%I.
Proof. exact: fupd_intro_mask. Qed.
Lemma fupd_except_0 E1 E2 P : (|={E1,E2}=> P) ={E1,E2}= P.
Proof. by rewrite {1}(fupd_intro E2 P) except_0_fupd fupd_trans. Qed.
Lemma fupd_frame_l E1 E2 P Q : (P |={E1,E2}=> Q) ={E1,E2}= P Q.
Proof. rewrite !(comm _ P); apply fupd_frame_r. Qed.
Lemma fupd_wand_l E1 E2 P Q : (P - Q) (|={E1,E2}=> P) ={E1,E2}= Q.
Proof. by rewrite fupd_frame_l bi.wand_elim_l. Qed.
Lemma fupd_wand_r E1 E2 P Q : (|={E1,E2}=> P) (P - Q) ={E1,E2}= Q.
Proof. by rewrite fupd_frame_r bi.wand_elim_r. Qed.
Lemma fupd_trans_frame E1 E2 E3 P Q :
((Q ={E2,E3}= emp) |={E1,E2}=> (Q P)) ={E1,E3}= P.
Proof.
rewrite fupd_frame_l assoc -(comm _ Q) bi.wand_elim_r.
by rewrite fupd_frame_r left_id fupd_trans.
Qed.
Lemma fupd_mask_frame_r E1 E2 Ef P :
E1 ## Ef (|={E1,E2}=> P) ={E1 Ef,E2 Ef}= P.
Proof.
intros ?. rewrite -fupd_mask_frame_r' //. f_equiv.
apply bi.impl_intro_l, bi.and_elim_r.
Qed.
Lemma fupd_mask_mono E1 E2 P : E1 E2 (|={E1}=> P) ={E2}= P.
Proof.
intros (Ef&->&?)%subseteq_disjoint_union_L. by apply fupd_mask_frame_r.
Qed.
Lemma fupd_sep E P Q : (|={E}=> P) (|={E}=> Q) ={E}= P Q.
Proof. by rewrite fupd_frame_r fupd_frame_l fupd_trans. Qed.
Lemma fupd_big_sepL {A} E (Φ : nat A PROP) (l : list A) :
([ list] kx l, |={E}=> Φ k x) ={E}= [ list] kx l, Φ k x.
Proof.
apply (big_opL_forall (λ P Q, P ={E}= Q)); auto using fupd_intro.
intros P1 P2 HP Q1 Q2 HQ. by rewrite HP HQ -fupd_sep.
Qed.
Lemma fupd_big_sepM `{Countable K} {A} E (Φ : K A PROP) (m : gmap K A) :
([ map] kx m, |={E}=> Φ k x) ={E}= [ map] kx m, Φ k x.
Proof.
apply (big_opM_forall (λ P Q, P ={E}= Q)); auto using fupd_intro.
intros P1 P2 HP Q1 Q2 HQ. by rewrite HP HQ -fupd_sep.
Qed.
Lemma fupd_big_sepS `{Countable A} E (Φ : A PROP) X :
([ set] x X, |={E}=> Φ x) ={E}= [ set] x X, Φ x.
Proof.
apply (big_opS_forall (λ P Q, P ={E}= Q)); auto using fupd_intro.
intros P1 P2 HP Q1 Q2 HQ. by rewrite HP HQ -fupd_sep.
Qed.
Lemma fupd_plain E1 E2 P Q `{!Plain P} :
E1 E2 (Q - P) - (|={E1, E2}=> Q) ={E1}= (|={E1, E2}=> Q) P.
Proof.
intros HE. rewrite -(fupd_plain' _ _ E1) //. apply bi.wand_intro_l.
by rewrite bi.wand_elim_r -fupd_intro.
Qed.
(** Fancy updates that take a step derived rules. *)
Lemma step_fupd_wand E1 E2 P Q : (|={E1,E2}=> P) - (P - Q) - |={E1,E2}=> Q.
Proof.
apply bi.wand_intro_l.
by rewrite (bi.later_intro (P - Q)%I) fupd_frame_l -bi.later_sep fupd_frame_l
bi.wand_elim_l.
Qed.
Lemma step_fupd_mask_frame_r E1 E2 Ef P :
E1 ## Ef E2 ## Ef (|={E1,E2}=> P) |={E1 Ef,E2 Ef}=> P.
Proof.
intros. rewrite -fupd_mask_frame_r //. do 2 f_equiv. by apply fupd_mask_frame_r.
Qed.
Lemma step_fupd_mask_mono E1 E2 F1 F2 P :
F1 F2 E1 E2 (|={E1,F2}=> P) |={E2,F1}=> P.
Proof.
intros ??. rewrite -(left_id emp%I _ (|={E1,F2}=> P)%I).
rewrite (fupd_intro_mask E2 E1 emp%I) //.
rewrite fupd_frame_r -(fupd_trans E2 E1 F1). f_equiv.
rewrite fupd_frame_l -(fupd_trans E1 F2 F1). f_equiv.
rewrite (fupd_intro_mask F2 F1 (|={_,_}=> emp)%I) //.
rewrite fupd_frame_r. f_equiv.
rewrite [X in (X _)%I]bi.later_intro -bi.later_sep. f_equiv.
rewrite fupd_frame_r -(fupd_trans F1 F2 E2). f_equiv.
rewrite fupd_frame_l -(fupd_trans F2 E1 E2). f_equiv.
by rewrite fupd_frame_r left_id.
Qed.
Lemma step_fupd_intro E1 E2 P : E2 E1 P - |={E1,E2}=> P.
Proof. intros. by rewrite -(step_fupd_mask_mono E2 _ _ E2) // -!fupd_intro. Qed.
End fupd_derived.
This diff is collapsed.
......@@ -1853,5 +1853,8 @@ Hint Extern 1 (envs_entails _ (∃ _, _)) => iExists _.
Hint Extern 1 (envs_entails _ ( _)) => iModIntro.
Hint Extern 1 (envs_entails _ (_ _)) => iLeft.
Hint Extern 1 (envs_entails _ (_ _)) => iRight.
Hint Extern 1 (envs_entails _ (|==> _)) => iModIntro.
Hint Extern 2 (envs_entails _ (|={_}=> _)) => iModIntro.
Hint Extern 2 (envs_entails _ (_ _)) => progress iFrame : iFrame.
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