Skip to content
GitLab
Commit 6cad0bb1 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Bundle update type class.

parent 50a0de15
Hide whitespace changes
Inline Side-by-side
theories/base_logic/lib/fancy_updates.v
View file @ 6cad0bb1
From iris.base_logic.lib Require Export own.
From stdpp Require Export coPset.
From iris.base_logic.lib Require Import wsat.
From iris.algebra Require Import gmap.
From iris.proofmode Require Import tactics classes.
From iris.proofmode Require Import tactics.
Set Default Proof Using "Type".
Export invG.
Import uPred.
......@@ -10,18 +9,17 @@ Import uPred.
Definition uPred_fupd_def `{invG Σ} (E1 E2 : coPset) (P : iProp Σ) : iProp Σ :=
(wsat ∗ ownE E1 ==∗ ◇ (wsat ∗ ownE E2 ∗ P))%I.
Definition uPred_fupd_aux `{invG Σ} : seal uPred_fupd_def. by eexists. Qed.
Instance uPred_fupd `{invG Σ} : FUpd (iProp Σ):= unseal uPred_fupd_aux.
Definition uPred_fupd_eq `{invG Σ} : fupd = uPred_fupd_def := seal_eq uPred_fupd_aux.
Definition uPred_fupd `{invG Σ} : FUpd (iProp Σ):= unseal uPred_fupd_aux.
Definition uPred_fupd_eq `{invG Σ} : @fupd _ uPred_fupd = uPred_fupd_def :=
seal_eq uPred_fupd_aux.
Instance fupd_facts `{invG Σ} : FUpdFacts (uPredSI (iResUR Σ)).
Lemma uPred_fupd_mixin `{invG Σ} : BiFUpdMixin (uPredSI (iResUR Σ)) uPred_fupd.
Proof.
split.
- apply _.
- rewrite uPred_fupd_eq. solve_proper.
- intros E1 E2 P (E1''&->&?)%subseteq_disjoint_union_L.
rewrite uPred_fupd_eq /uPred_fupd_def ownE_op //.
by iIntros "$ ($ & $ & HE) !> !> [$ $] !> !>" .
- rewrite uPred_fupd_eq. by iIntros (E P) ">? [$ $] !> !>".
by iIntros "$ ($ & $ & HE) !> !> [$ $] !> !>" .
- rewrite uPred_fupd_eq. iIntros (E1 E2 P) ">H [Hw HE]". iApply "H"; by iFrame.
- rewrite uPred_fupd_eq. iIntros (E1 E2 P Q HPQ) "HP HwE". rewrite -HPQ. by iApply "HP".
- rewrite uPred_fupd_eq. iIntros (E1 E2 E3 P) "HP HwE".
......@@ -42,3 +40,8 @@ Proof.
iAssert (▷ ◇ P)%I with "[-]" as "#$"; last by iFrame.
iNext. by iMod ("HP" with "[$]") as "(_ & _ & HP)".
Qed.
Instance uPred_bi_fupd `{invG Σ} : BiFUpd (uPredSI (iResUR Σ)) :=
{| bi_fupd_mixin := uPred_fupd_mixin |}.
Instance uPred_bi_bupd_fupd `{invG Σ} : BiBUpdFUpd (uPredSI (iResUR Σ)).
Proof. rewrite /BiBUpdFUpd uPred_fupd_eq. by iIntros (E P) ">? [$ $] !> !>". Qed.
theories/base_logic/upred.v
View file @ 6cad0bb1
......@@ -336,7 +336,7 @@ Next Obligation.
eauto using uPred_mono, cmra_includedN_l.
Qed.
Definition uPred_bupd_aux {M} : seal (@uPred_bupd_def M). by eexists. Qed.
Instance uPred_bupd {M} : BUpd (uPred M) := unseal uPred_bupd_aux.
Definition uPred_bupd {M} : BUpd (uPred M) := unseal uPred_bupd_aux.
Definition uPred_bupd_eq {M} :
@bupd _ uPred_bupd = @uPred_bupd_def M := seal_eq uPred_bupd_aux.
......@@ -575,6 +575,30 @@ Coercion uPred_valid {M} : uPred M → Prop := bi_valid.
(* Latest notation *)
Notation "✓ x" := (uPred_cmra_valid x) (at level 20) : bi_scope.
Lemma uPred_bupd_mixin M : BiBUpdMixin (uPredI M) uPred_bupd.
Proof.
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.
Instance uPred_bi_bupd M : BiBUpd (uPredI M) := {| bi_bupd_mixin := uPred_bupd_mixin M |}.
Module uPred.
Include uPred_unseal.
Section uPred.
......@@ -675,30 +699,6 @@ Lemma ofe_fun_validI `{B : A → ucmraT} (g : ofe_fun B) :
(✓ g : uPred M) ⊣⊢ ∀ i, ✓ g i.
Proof. by uPred.unseal. Qed.
(* Basic update modality *)
Global Instance bupd_facts : BUpdFacts (uPredSI M).
Proof.
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.
......
theories/bi/lib/atomic.v
View file @ 6cad0bb1
......@@ -3,7 +3,7 @@ From stdpp Require Import coPset.
From iris.proofmode Require Import tactics.
Set Default Proof Using "Type".
Definition atomic_shift {PROP: sbi} `{!FUpd PROP} {A B : Type}
Definition atomic_shift `{BiFUpd PROP} {A B : Type}
(α : A → PROP) (* atomic pre-condition *)
(β : A → B → PROP) (* atomic post-condition *)
(Eo Em : coPset) (* outside/module masks *)
......@@ -14,7 +14,7 @@ Definition atomic_shift {PROP: sbi} `{!FUpd PROP} {A B : Type}
((α x ={E∖Em, E}=∗ P) ∧ (∀ y, β x y ={E∖Em, E}=∗ Q x y)))
)%I.
Definition atomic_update {PROP: sbi} `{!FUpd PROP} {A B : Type}
Definition atomic_update `{BiFUpd PROP} {A B : Type}
(α : A → PROP) (* atomic pre-condition *)
(β : A → B → PROP) (* atomic post-condition *)
(Eo Em : coPset) (* outside/module masks *)
......@@ -25,7 +25,7 @@ Definition atomic_update {PROP: sbi} `{!FUpd PROP} {A B : Type}
)%I.
Section lemmas.
Context {PROP: sbi} `{FUpdFacts PROP} {A B : Type}.
Context `{BiFUpd PROP} {A B : Type}.
Implicit Types (α : A → PROP) (β: A → B → PROP) (P : PROP) (Q : A → B → PROP).
Lemma aupd_acc α β Eo Em Q E :
......
theories/bi/monpred.v
View file @ 6cad0bb1
......@@ -205,8 +205,8 @@ Definition monPred_bupd_def `{BUpd PROP} (P : monPred) : monPred :=
terms in logical terms. *)
monPred_upclosed (λ i, |==> P i)%I.
Definition monPred_bupd_aux `{BUpd PROP} : seal monPred_bupd_def. by eexists. Qed.
Global Instance monPred_bupd `{BUpd PROP} : BUpd _ := unseal monPred_bupd_aux.
Definition monPred_bupd_eq `{BUpd PROP} : @bupd monPred _ = _ := seal_eq _.
Definition monPred_bupd `{BUpd PROP} : BUpd _ := unseal monPred_bupd_aux.
Definition monPred_bupd_eq `{BUpd PROP} : @bupd _ monPred_bupd = _ := seal_eq _.
End Bi.
Arguments monPred_absolutely {_ _} _%I.
......@@ -237,8 +237,8 @@ Definition monPred_fupd_def `{FUpd PROP} (E1 E2 : coPset) (P : monPred) : monPre
terms in logical terms. *)
monPred_upclosed (λ i, |={E1,E2}=> P i)%I.
Definition monPred_fupd_aux `{FUpd PROP} : seal monPred_fupd_def. by eexists. Qed.
Global Instance monPred_fupd `{FUpd PROP} : FUpd _ := unseal monPred_fupd_aux.
Definition monPred_fupd_eq `{FUpd PROP} : @fupd monPred _ = _ := seal_eq _.
Definition monPred_fupd `{FUpd PROP} : FUpd _ := unseal monPred_fupd_aux.
Definition monPred_fupd_eq `{FUpd PROP} : @fupd _ monPred_fupd = _ := seal_eq _.
End Sbi.
Module MonPred.
......@@ -411,7 +411,6 @@ Implicit Types i : I.
Implicit Types P Q : monPred.
(** Instances *)
Global Instance monPred_at_mono :
Proper ((⊢) ==> (⊑) ==> (⊢)) monPred_at.
Proof. by move=> ?? [?] ?? ->. Qed.
......@@ -802,17 +801,8 @@ Global Instance big_sepMS_absolute `{Countable A} (Φ : A → monPred)
Absolute ([∗ mset] y ∈ X, Φ y)%I.
Proof. intros ??. rewrite !monPred_at_big_sepMS. do 2 f_equiv. by apply absolute_at. Qed.
End bi_facts.
Section sbi_facts.
Context {I : biIndex} {PROP : sbi}.
Local Notation monPred := (monPred I PROP).
Local Notation monPredSI := (monPredSI I PROP).
Implicit Types i : I.
Implicit Types P Q : monPred.
(** bupd *)
Global Instance monPred_bupd_facts `{BUpdFacts PROP} : BUpdFacts monPredSI.
Lemma monPred_bupd_mixin `{BiBUpd PROP} : BiBUpdMixin monPredI monPred_bupd.
Proof.
split; unseal; unfold monPred_bupd_def, monPred_upclosed.
(* Note: Notation is somewhat broken here. *)
......@@ -828,24 +818,34 @@ Proof.
- 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_bi_bupd `{BiBUpd PROP} : BiBUpd monPredI :=
{| bi_bupd_mixin := monPred_bupd_mixin |}.
Lemma monPred_at_bupd `{BUpdFacts PROP} i P : (|==> P) i ⊣⊢ |==> P i.
Lemma monPred_at_bupd `{BiBUpd 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} :
Global Instance bupd_absolute `{BiBUpd 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⎤.
Lemma monPred_bupd_embed `{BiBUpd 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.
End bi_facts.
Section sbi_facts.
Context {I : biIndex} {PROP : sbi}.
Local Notation monPred := (monPred I PROP).
Local Notation monPredSI := (monPredSI I PROP).
Implicit Types i : I.
Implicit Types P Q : monPred.
Global Instance monPred_at_timeless P i : Timeless P → Timeless (P i).
Proof. move => [] /(_ i). unfold Timeless. by unseal. Qed.
......@@ -865,16 +865,15 @@ Qed.
Global Instance monPred_sbi_embedding : SbiEmbedding PROP monPredSI.
Proof. split; try apply _; by unseal. Qed.
Global Instance monPred_fupd_facts `{FUpdFacts PROP} : FUpdFacts monPredSI.
Lemma monPred_fupd_mixin `{BiFUpd PROP} : BiFUpdMixin monPredSI monPred_fupd.
Proof.
split; first apply _; unseal; unfold monPred_fupd_def, monPred_upclosed.
split; unseal; unfold monPred_fupd_def, monPred_upclosed.
(* Note: Notation is somewhat broken here. *)
- intros E1 E2 n P Q HPQ. split=>/= i. by repeat f_equiv.
- intros E1 E2 P HE12. split=>/= i.
do 2 setoid_rewrite bi.pure_impl_forall. do 2 apply bi.forall_intro=>?.
rewrite (fupd_intro_mask E1 E2 (P i)) //. f_equiv.
do 2 apply bi.forall_intro=>?. do 2 f_equiv. by etrans.
- intros E P. split=>/= i. by setoid_rewrite bupd_fupd.
- intros E1 E2 P. split=>/= i. etrans; [apply bi.equiv_entails, bi.except_0_forall|].
do 2 f_equiv. rewrite bi.pure_impl_forall bi.except_0_forall. do 2 f_equiv.
by apply except_0_fupd.
......@@ -893,15 +892,21 @@ Proof.
- intros E P ?. split=>/= i. setoid_rewrite bi.pure_impl_forall.
do 2 setoid_rewrite bi.later_forall. do 4 f_equiv. apply later_fupd_plain, _.
Qed.
Global Instance monPred_bi_fupd `{BiFUpd PROP} : BiFUpd monPredSI :=
{| bi_fupd_mixin := monPred_fupd_mixin |}.
Global Instance monPred_bi_bupd_fupd `{BiBUpdFUpd PROP} : BiBUpdFUpd monPredSI.
Proof.
rewrite /BiBUpdFUpd; unseal; unfold monPred_fupd_def, monPred_upclosed.
intros E P. split=>/= i. by setoid_rewrite bupd_fupd.
Qed.
(** Unfolding lemmas *)
Lemma monPred_at_internal_eq {A : ofeT} i (a b : A) :
@monPred_at I PROP (a ≡ b) i ⊣⊢ a ≡ b.
Proof. by apply monPred_at_embed. Qed.
Lemma monPred_at_later i P : (▷ P) i ⊣⊢ ▷ P i.
Proof. by unseal. Qed.
Lemma monPred_at_fupd `{FUpdFacts PROP} i E1 E2 P :
Lemma monPred_at_fupd `{BiFUpd PROP} i E1 E2 P :
(|={E1,E2}=> P) i ⊣⊢ |={E1,E2}=> P i.
Proof.
unseal. setoid_rewrite bi.pure_impl_forall. apply bi.equiv_spec; split.
......@@ -911,7 +916,7 @@ Qed.
Lemma monPred_at_except_0 i P : (◇ P) i ⊣⊢ ◇ P i.
Proof. by unseal. Qed.
Lemma monPred_fupd_embed `{FUpdFacts PROP} E1 E2 (P : PROP) :
Lemma monPred_fupd_embed `{BiFUpd PROP} E1 E2 (P : PROP) :
⎡|={E1,E2}=> P⎤ ⊣⊢ fupd E1 E2 (PROP:=monPred) ⎡P⎤.
Proof.
unseal. split=>i /=. setoid_rewrite bi.pure_impl_forall. apply bi.equiv_spec; split.
......@@ -929,7 +934,6 @@ Proof.
Qed.
(** Absolute *)
Global Instance internal_eq_absolute {A : ofeT} (x y : A) :
@Absolute I PROP (x ≡ y)%I.
Proof. intros ??. by unseal. Qed.
......@@ -941,8 +945,7 @@ Proof. induction n; apply _. Qed.
Global Instance except0_absolute P `{!Absolute P} : Absolute (◇ P)%I.
Proof. rewrite /sbi_except_0. apply _. Qed.
Global Instance fupd_absolute E1 E2 P `{!Absolute P} `{FUpdFacts PROP} :
Global Instance fupd_absolute E1 E2 P `{!Absolute P} `{BiFUpd PROP} :
Absolute (|={E1,E2}=> P)%I.
Proof. intros ??. by rewrite !monPred_at_fupd absolute_at. Qed.
End sbi_facts.
theories/bi/updates.v
View file @ 6cad0bb1
From stdpp Require Import coPset.
From iris.bi Require Import interface derived_laws big_op.
(* We first define operational type classes for the notations, and then later
bundle these operational type classes with the laws. *)
Class BUpd (PROP : Type) : Type := bupd : PROP → PROP.
Instance : Params (@bupd) 2.
Hint Mode BUpd ! : typeclass_instances.
......@@ -35,7 +37,6 @@ Notation "P ={ E }=∗ Q" := (P -∗ |={E}=> Q)
(at level 99, E at level 50, Q at level 200, only parsing) : stdpp_scope.
(** Fancy updates that take a step. *)
Notation "|={ E1 , E2 }▷=> Q" := (|={E1,E2}=> (▷ |={E2,E1}=> Q))%I
(at level 99, E1, E2 at level 50, Q at level 200,
format "|={ E1 , E2 }▷=> Q") : bi_scope.
......@@ -49,26 +50,102 @@ 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 : sbi) `{BUpd PROP} : Prop :=
{ bupd_ne :> NonExpansive bupd;
bupd_intro (P : PROP) : P ==∗ P;
bupd_mono (P Q : PROP) : (P ⊢ Q) → (|==> P) ==∗ Q;
bupd_trans (P : PROP) : (|==> |==> P) ==∗ P;
bupd_frame_r (P R : PROP) : (|==> P) ∗ R ==∗ P ∗ R;
bupd_plainly (P : PROP) : (|==> bi_plainly P) -∗ P }.
Hint Mode BUpdFacts ! - : typeclass_instances.
(** Bundled versions *)
Record BiBUpdMixin (PROP : bi) `(BUpd PROP) := {
bi_bupd_mixin_bupd_ne : NonExpansive bupd;
bi_bupd_mixin_bupd_intro (P : PROP) : P ==∗ P;
bi_bupd_mixin_bupd_mono (P Q : PROP) : (P ⊢ Q) → (|==> P) ==∗ Q;
bi_bupd_mixin_bupd_trans (P : PROP) : (|==> |==> P) ==∗ P;
bi_bupd_mixin_bupd_frame_r (P R : PROP) : (|==> P) ∗ R ==∗ P ∗ R;
bi_bupd_mixin_bupd_plainly (P : PROP) : (|==> bi_plainly P) -∗ P;
}.
Record BiFUpdMixin (PROP : sbi) `(FUpd PROP) := {
bi_fupd_mixin_fupd_ne E1 E2 : NonExpansive (fupd E1 E2);
bi_fupd_mixin_fupd_intro_mask E1 E2 (P : PROP) : E2 ⊆ E1 → P ⊢ |={E1,E2}=> |={E2,E1}=> P;
bi_fupd_mixin_except_0_fupd E1 E2 (P : PROP) : ◇ (|={E1,E2}=> P) ={E1,E2}=∗ P;
bi_fupd_mixin_fupd_mono E1 E2 (P Q : PROP) : (P ⊢ Q) → (|={E1,E2}=> P) ⊢ |={E1,E2}=> Q;
bi_fupd_mixin_fupd_trans E1 E2 E3 (P : PROP) : (|={E1,E2}=> |={E2,E3}=> P) ⊢ |={E1,E3}=> P;
bi_fupd_mixin_fupd_mask_frame_r' E1 E2 Ef (P : PROP) :
E1 ## Ef → (|={E1,E2}=> ⌜E2 ## Ef⌝ → P) ={E1 ∪ Ef,E2 ∪ Ef}=∗ P;
bi_fupd_mixin_fupd_frame_r E1 E2 (P Q : PROP) : (|={E1,E2}=> P) ∗ Q ={E1,E2}=∗ P ∗ Q;
bi_fupd_mixin_fupd_plain' E1 E2 E2' (P Q : PROP) `{!Plain P} :
E1 ⊆ E2 →
(Q ={E1, E2'}=∗ P) -∗ (|={E1, E2}=> Q) ={E1}=∗ (|={E1, E2}=> Q) ∗ P;
bi_fupd_mixin_later_fupd_plain E (P : PROP) `{!Plain P} : (▷ |={E}=> P) ={E}=∗ ▷ ◇ P;
}.
Class BiBUpd (PROP : bi) := {
bi_bupd_bupd :> BUpd PROP;
bi_bupd_mixin : BiBUpdMixin PROP bi_bupd_bupd;
}.
Hint Mode BiBUpd ! : typeclass_instances.
Arguments bi_bupd_bupd : simpl never.
Class BiFUpd (PROP : sbi) := {
bi_fupd_fupd :> FUpd PROP;
bi_fupd_mixin : BiFUpdMixin PROP bi_fupd_fupd;
}.
Hint Mode BiBUpd ! : typeclass_instances.
Arguments bi_fupd_fupd : simpl never.
Class BiBUpdFUpd (PROP : sbi) `{BiBUpd PROP, BiFUpd PROP} :=
bupd_fupd E (P : PROP) : (|==> P) ={E}=∗ P.
Section bupd_laws.
Context `{BiBUpd PROP}.
Implicit Types P : PROP.
Global Instance bupd_ne : NonExpansive (@bupd PROP _).
Proof. eapply bi_bupd_mixin_bupd_ne, bi_bupd_mixin. Qed.
Lemma bupd_intro P : P ==∗ P.
Proof. eapply bi_bupd_mixin_bupd_intro, bi_bupd_mixin. Qed.
Lemma bupd_mono (P Q : PROP) : (P ⊢ Q) → (|==> P) ==∗ Q.
Proof. eapply bi_bupd_mixin_bupd_mono, bi_bupd_mixin. Qed.
Lemma bupd_trans (P : PROP) : (|==> |==> P) ==∗ P.
Proof. eapply bi_bupd_mixin_bupd_trans, bi_bupd_mixin. Qed.
Lemma bupd_frame_r (P R : PROP) : (|==> P) ∗ R ==∗ P ∗ R.
Proof. eapply bi_bupd_mixin_bupd_frame_r, bi_bupd_mixin. Qed.
Lemma bupd_plainly (P : PROP) : (|==> bi_plainly P) -∗ P.
Proof. eapply bi_bupd_mixin_bupd_plainly, bi_bupd_mixin. Qed.
End bupd_laws.
Section fupd_laws.
Context `{BiFUpd PROP}.
Implicit Types P : PROP.
Global Instance fupd_ne E1 E2 : NonExpansive (@fupd PROP _ E1 E2).
Proof. eapply bi_fupd_mixin_fupd_ne, bi_fupd_mixin. Qed.
Lemma fupd_intro_mask E1 E2 (P : PROP) : E2 ⊆ E1 → P ⊢ |={E1,E2}=> |={E2,E1}=> P.
Proof. eapply bi_fupd_mixin_fupd_intro_mask, bi_fupd_mixin. Qed.
Lemma except_0_fupd E1 E2 (P : PROP) : ◇ (|={E1,E2}=> P) ={E1,E2}=∗ P.
Proof. eapply bi_fupd_mixin_except_0_fupd, bi_fupd_mixin. Qed.
Lemma fupd_mono E1 E2 (P Q : PROP) : (P ⊢ Q) → (|={E1,E2}=> P) ⊢ |={E1,E2}=> Q.
Proof. eapply bi_fupd_mixin_fupd_mono, bi_fupd_mixin. Qed.
Lemma fupd_trans E1 E2 E3 (P : PROP) : (|={E1,E2}=> |={E2,E3}=> P) ⊢ |={E1,E3}=> P.
Proof. eapply bi_fupd_mixin_fupd_trans, bi_fupd_mixin. Qed.
Lemma fupd_mask_frame_r' E1 E2 Ef (P : PROP) :
E1 ## Ef → (|={E1,E2}=> ⌜E2 ## Ef⌝ → P) ={E1 ∪ Ef,E2 ∪ Ef}=∗ P.
Proof. eapply bi_fupd_mixin_fupd_mask_frame_r', bi_fupd_mixin. Qed.
Lemma fupd_frame_r E1 E2 (P Q : PROP) : (|={E1,E2}=> P) ∗ Q ={E1,E2}=∗ P ∗ Q.
Proof. eapply bi_fupd_mixin_fupd_frame_r, bi_fupd_mixin. Qed.
Lemma fupd_plain' E1 E2 E2' (P Q : PROP) `{!Plain P} :
E1 ⊆ E2 →
(Q ={E1, E2'}=∗ P) -∗ (|={E1, E2}=> Q) ={E1}=∗ (|={E1, E2}=> Q) ∗ P.
Proof. eapply bi_fupd_mixin_fupd_plain'; eauto using bi_fupd_mixin. Qed.
Lemma later_fupd_plain E (P : PROP) `{!Plain P} : (▷ |={E}=> P) ={E}=∗ ▷ ◇ P.
Proof. eapply bi_fupd_mixin_later_fupd_plain; eauto using bi_fupd_mixin. Qed.
End fupd_laws.
Section bupd_derived.
Context `{BUpdFacts PROP}.
Implicit Types P Q R: PROP.
Context `{BiBUpd PROP}.
Implicit Types P Q R : PROP.
(* FIXME: Removing the `PROP:=` diverges. *)
Global Instance bupd_proper : Proper ((≡) ==> (≡)) (bupd (PROP:=PROP)) := ne_proper _.
Global Instance bupd_proper :
Proper ((≡) ==> (≡)) (bupd (PROP:=PROP)) := ne_proper _.
(** BUpd derived rules *)
Global Instance bupd_mono' : Proper ((⊢) ==> (⊢)) (bupd (PROP:=PROP)).
Proof. intros P Q; apply bupd_mono. Qed.
Global Instance bupd_flip_mono' : Proper (flip (⊢) ==> flip (⊢)) (bupd (PROP:=PROP)).
......@@ -88,44 +165,25 @@ Section bupd_derived.
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 : PROP) : E2 ⊆ E1 → P ⊢ |={E1,E2}=> |={E2,E1}=> P;
bupd_fupd E (P : PROP) : (|==> P) ={E}=∗ P;
except_0_fupd E1 E2 (P : PROP) : ◇ (|={E1,E2}=> P) ={E1,E2}=∗ P;
fupd_mono E1 E2 (P Q : PROP) : (P ⊢ Q) → (|={E1,E2}=> P) ⊢ |={E1,E2}=> Q;
fupd_trans E1 E2 E3 (P : PROP) : (|={E1,E2}=> |={E2,E3}=> P) ⊢ |={E1,E3}=> P;
fupd_mask_frame_r' E1 E2 Ef (P : PROP) :
E1 ## Ef → (|={E1,E2}=> ⌜E2 ## Ef⌝ → P) ={E1 ∪ Ef,E2 ∪ Ef}=∗ P;
fupd_frame_r E1 E2 (P Q : PROP) : (|={E1,E2}=> P) ∗ Q ={E1,E2}=∗ P ∗ Q;
fupd_plain' E1 E2 E2' (P Q : PROP) `{!Plain P} :
E1 ⊆ E2 →
(Q ={E1, E2'}=∗ P) -∗ (|={E1, E2}=> Q) ={E1}=∗ (|={E1, E2}=> Q) ∗ P;
later_fupd_plain E (P : PROP) `{!Plain P} : (▷ |={E}=> P) ={E}=∗ ▷ ◇ P }.
Hint Mode FUpdFacts ! - - : typeclass_instances.
Section bupd_derived_sbi.
Context {PROP : sbi} `{BiBUpd PROP}.
Implicit Types P Q R : PROP.
Lemma except_0_bupd P : ◇ (|==> 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.
End bupd_derived_sbi.
Section fupd_derived.
Context `{FUpdFacts PROP}.
Implicit Types P Q R: PROP.
Context `{BiFUpd PROP}.
Implicit Types P Q R : PROP.
Global Instance fupd_proper E1 E2 : Proper ((≡) ==> (≡)) (fupd (PROP:=PROP) E1 E2) := ne_proper _.
Global Instance fupd_proper E1 E2 :
Proper ((≡) ==> (≡)) (fupd (PROP:=PROP) E1 E2) := ne_proper _.
(** FUpd derived rules *)
Global Instance fupd_mono' E1 E2 : Proper ((⊢) ==> (⊢)) (fupd (PROP:=PROP) E1 E2).
Proof. intros P Q; apply fupd_mono. Qed.
Global Instance fupd_flip_mono' E1 E2 :
......@@ -133,7 +191,7 @@ Section fupd_derived.
Proof. intros P Q; apply fupd_mono. Qed.
Lemma fupd_intro E P : P ={E}=∗ P.
Proof. rewrite -bupd_fupd. apply bupd_intro. Qed.
Proof. by rewrite {1}(fupd_intro_mask E E P) // fupd_trans. Qed.
Lemma fupd_intro_mask' E1 E2 : E2 ⊆ E1 → (|={E1,E2}=> |={E2,E1}=> bi_emp (PROP:=PROP))%I.
Proof. exact: fupd_intro_mask. Qed.
Lemma fupd_except_0 E1 E2 P : (|={E1,E2}=> ◇ P) ={E1,E2}=∗ P.
......@@ -193,7 +251,6 @@ Section fupd_derived.
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.
......
theories/proofmode/class_instances.v
View file @ 6cad0bb1
......@@ -1103,10 +1103,10 @@ Global Instance from_assumption_except_0 p P Q :
FromAssumption p P Q → FromAssumption p P (◇ Q)%I.
Proof. rewrite /FromAssumption=>->. apply except_0_intro. Qed.
Global Instance from_assumption_bupd `{BUpdFacts PROP} p P Q :
Global Instance from_assumption_bupd `{BiBUpd PROP} p P Q :
FromAssumption p P Q → FromAssumption p P (|==> Q).
Proof. rewrite /FromAssumption=>->. apply bupd_intro. Qed.
Global Instance from_assumption_fupd `{FUpdFacts PROP} E p P Q :
Global Instance from_assumption_fupd `{BiBUpdFUpd PROP} E p P Q :
FromAssumption p P (|==> Q) → FromAssumption p P (|={E}=> Q)%I.
Proof. rewrite /FromAssumption=>->. apply bupd_fupd. Qed.
......@@ -1121,10 +1121,10 @@ Proof. rewrite /FromPure=> ->. apply laterN_intro. Qed.
Global Instance from_pure_except_0 a P φ : FromPure a P φ → FromPure a (◇ P) φ.
Proof. rewrite /FromPure=> ->. apply except_0_intro. Qed.
Global Instance from_pure_bupd `{BUpdFacts PROP} a P φ :
Global Instance from_pure_bupd `{BiBUpd PROP} a P φ :
FromPure a P φ → FromPure a (|==> P) φ.
Proof. rewrite /FromPure=> <-. apply bupd_intro. Qed.
Global Instance from_pure_fupd `{FUpdFacts PROP} a E P φ :
Global Instance from_pure_fupd `{BiFUpd PROP} a E P φ :
FromPure a P φ → FromPure a (|={E}=> P) φ.