Skip to content
GitLab
Commit c6bf752e authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan
Browse files

Type classes for fancy updates and basic updates.

parent 91cbff6b
Hide whitespace changes
Inline Side-by-side
theories/base_logic/derived.v
View file @ c6bf752e
......@@ -58,9 +58,10 @@ Proof.
Qed.
(** * Derived rules *)
Global Instance bupd_mono' : Proper ((⊢) ==> (⊢)) (@uPred_bupd M).
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 (⊢)) (@uPred_bupd M).
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.
......@@ -77,7 +78,7 @@ Proof.
Qed.
Lemma except_0_bupd P : ◇ (|==> P) ⊢ (|==> ◇ P).
Proof.
rewrite /sbi_except_0. apply or_elim; auto using bupd_mono, or_intro_r.
rewrite /sbi_except_0. apply or_elim; eauto using bupd_mono, or_intro_r.
by rewrite -bupd_intro -or_intro_l.
Qed.
......
theories/base_logic/lib/fancy_updates.v
View file @ c6bf752e
......@@ -7,15 +7,15 @@ Set Default Proof Using "Type".
Export invG.
Import uPred.
Program Definition fupd_def `{invG Σ}
(E1 E2 : coPset) (P : iProp Σ) : iProp Σ :=
(wsat ∗ ownE E1 ==∗ ◇ (wsat ∗ ownE E2 ∗ P))%I.
Definition fupd_aux : seal (@fupd_def). by eexists. Qed.
Definition fupd := unseal fupd_aux.
Definition fupd_eq : @fupd = @fupd_def := seal_eq fupd_aux.
Arguments fupd {_ _} _ _ _%I.
Class FUpd (A : Type) : Type := fupd : coPset → coPset → A → A.
Instance: Params (@fupd) 4.
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.
Notation "|={ E1 , E2 }=> Q" := (fupd E1 E2 Q)
(at level 99, E1, E2 at level 50, Q at level 200,
format "|={ E1 , E2 }=> Q") : bi_scope.
......@@ -38,54 +38,54 @@ Section fupd.
Context `{invG Σ}.
Implicit Types P Q : iProp Σ.
Global Instance fupd_ne E1 E2 : NonExpansive (@fupd Σ _ E1 E2).
Proof. rewrite fupd_eq. solve_proper. Qed.
Global Instance fupd_proper E1 E2 : Proper ((≡) ==> (≡)) (@fupd Σ _ E1 E2).
Global Instance fupd_ne E1 E2 : NonExpansive (fupd E1 E2).
Proof. rewrite uPred_fupd_eq. solve_proper. Qed.
Global Instance fupd_proper E1 E2 : Proper ((≡) ==> (≡)) (fupd E1 E2).
Proof. apply ne_proper, _. Qed.
Lemma fupd_intro_mask E1 E2 P : E2 ⊆ E1 → P ⊢ |={E1,E2}=> |={E2,E1}=> P.
Proof.
intros (E1''&->&?)%subseteq_disjoint_union_L.
rewrite fupd_eq /fupd_def ownE_op //.
rewrite uPred_fupd_eq /uPred_fupd_def ownE_op //.
by iIntros "$ ($ & $ & HE) !> !> [$ $] !> !>" .
Qed.
Lemma except_0_fupd E1 E2 P : ◇ (|={E1,E2}=> P) ={E1,E2}=∗ P.
Proof. rewrite fupd_eq. iIntros ">H [Hw HE]". iApply "H"; by iFrame. Qed.
Proof. rewrite uPred_fupd_eq. iIntros ">H [Hw HE]". iApply "H"; by iFrame. Qed.
Lemma bupd_fupd E P : (|==> P) ={E}=∗ P.
Proof. rewrite fupd_eq /fupd_def. by iIntros ">? [$ $] !> !>". Qed.
Proof. rewrite uPred_fupd_eq. by iIntros ">? [$ $] !> !>". Qed.
Lemma fupd_mono E1 E2 P Q : (P ⊢ Q) → (|={E1,E2}=> P) ⊢ |={E1,E2}=> Q.
Proof.
rewrite fupd_eq /fupd_def. iIntros (HPQ) "HP HwE".
rewrite -HPQ. by iApply "HP".
rewrite uPred_fupd_eq. iIntros (HPQ) "HP HwE". rewrite -HPQ. by iApply "HP".
Qed.
Lemma fupd_trans E1 E2 E3 P : (|={E1,E2}=> |={E2,E3}=> P) ⊢ |={E1,E3}=> P.
Proof.
rewrite fupd_eq /fupd_def. iIntros "HP HwE".
rewrite uPred_fupd_eq. iIntros "HP HwE".
iMod ("HP" with "HwE") as ">(Hw & HE & HP)". iApply "HP"; by iFrame.
Qed.
Lemma fupd_mask_frame_r' E1 E2 Ef P :
E1 ## Ef → (|={E1,E2}=> ⌜E2 ## Ef⌝ → P) ={E1 ∪ Ef,E2 ∪ Ef}=∗ P.
Proof.
intros. rewrite fupd_eq /fupd_def ownE_op //. iIntros "Hvs (Hw & HE1 &HEf)".
intros. rewrite uPred_fupd_eq /uPred_fupd_def ownE_op //.
iIntros "Hvs (Hw & HE1 &HEf)".
iMod ("Hvs" with "[Hw HE1]") as ">($ & HE2 & HP)"; first by iFrame.
iDestruct (ownE_op' with "[HE2 HEf]") as "[? $]"; first by iFrame.
iIntros "!> !>". by iApply "HP".
Qed.
Lemma fupd_frame_r E1 E2 P Q : (|={E1,E2}=> P) ∗ Q ={E1,E2}=∗ P ∗ Q.
Proof. rewrite fupd_eq /fupd_def. by iIntros "[HwP $]". Qed.
Proof. rewrite uPred_fupd_eq /uPred_fupd_def. by iIntros "[HwP $]". Qed.
Lemma fupd_plain' E1 E2 E2' P Q `{!Plain P} :
E1 ⊆ E2 →
(Q ={E1, E2'}=∗ P) -∗ (|={E1, E2}=> Q) ={E1}=∗ (|={E1, E2}=> Q) ∗ P.
Proof.
iIntros ((E3&->&HE)%subseteq_disjoint_union_L) "HQP HQ".
rewrite fupd_eq /fupd_def ownE_op //. iIntros "H".
rewrite uPred_fupd_eq /uPred_fupd_def ownE_op //. iIntros "H".
iMod ("HQ" with "H") as ">(Hws & [HE1 HE3] & HQ)"; iModIntro.
iAssert (◇ P)%I as "#HP".
{ by iMod ("HQP" with "HQ [$]") as "(_ & _ & HP)". }
......@@ -94,16 +94,16 @@ Qed.
Lemma later_fupd_plain E P `{!Plain P} : (▷ |={E}=> P) ={E}=∗ ▷ ◇ P.
Proof.
rewrite fupd_eq /fupd_def. iIntros "HP [Hw HE]".
rewrite uPred_fupd_eq /uPred_fupd_def. iIntros "HP [Hw HE]".
iAssert (▷ ◇ P)%I with "[-]" as "#$"; last by iFrame.
iNext. by iMod ("HP" with "[$]") as "(_ & _ & HP)".
Qed.
(** * Derived rules *)
Global Instance fupd_mono' E1 E2 : Proper ((⊢) ==> (⊢)) (@fupd Σ _ E1 E2).
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).
Proper (flip (⊢) ==> flip (⊢)) (fupd E1 E2).
Proof. intros P Q; apply fupd_mono. Qed.
Lemma fupd_intro E P : P ={E}=∗ P.
......
theories/base_logic/lib/invariants.v
View file @ c6bf752e
......@@ -45,7 +45,7 @@ Qed.
Lemma inv_alloc N E P : ▷ P ={E}=∗ inv N P.
Proof.
rewrite inv_eq /inv_def fupd_eq /fupd_def. iIntros "HP [Hw $]".
rewrite inv_eq /inv_def uPred_fupd_eq. iIntros "HP [Hw $]".
iMod (ownI_alloc (∈ (↑N : coPset)) P with "[$HP $Hw]")
as (i ?) "[$ ?]"; auto using fresh_inv_name.
Qed.
......@@ -53,7 +53,7 @@ Qed.
Lemma inv_alloc_open N E P :
↑N ⊆ E → (|={E, E∖↑N}=> inv N P ∗ (▷P ={E∖↑N, E}=∗ True))%I.
Proof.
rewrite inv_eq /inv_def fupd_eq /fupd_def. iIntros (Sub) "[Hw HE]".
rewrite inv_eq /inv_def uPred_fupd_eq. iIntros (Sub) "[Hw HE]".
iMod (ownI_alloc_open (∈ (↑N : coPset)) P with "Hw")
as (i ?) "(Hw & #Hi & HD)"; auto using fresh_inv_name.
iAssert (ownE {[i]} ∗ ownE (↑ N ∖ {[i]}) ∗ ownE (E ∖ ↑ N))%I
......@@ -72,7 +72,7 @@ Qed.
Lemma inv_open E N P :
↑N ⊆ E → inv N P ={E,E∖↑N}=∗ ▷ P ∗ (▷ P ={E∖↑N,E}=∗ True).
Proof.
rewrite inv_eq /inv_def fupd_eq /fupd_def; iDestruct 1 as (i) "[Hi #HiP]".
rewrite inv_eq /inv_def uPred_fupd_eq /uPred_fupd_def; iDestruct 1 as (i) "[Hi #HiP]".
iDestruct "Hi" as % ?%elem_of_subseteq_singleton.
rewrite {1 4}(union_difference_L (↑ N) E) // ownE_op; last set_solver.
rewrite {1 5}(union_difference_L {[ i ]} (↑ N)) // ownE_op; last set_solver.
......
theories/base_logic/upred.v
View file @ c6bf752e
......@@ -317,6 +317,8 @@ Definition uPred_cmra_valid {M A} := unseal uPred_cmra_valid_aux M A.
Definition uPred_cmra_valid_eq :
@uPred_cmra_valid = @uPred_cmra_valid_def := seal_eq uPred_cmra_valid_aux.
Class BUpd (A : Type) : Type := bupd : A → A.
Program Definition uPred_bupd_def {M} (Q : uPred M) : uPred M :=
{| uPred_holds n x := ∀ k yf,
k ≤ n → ✓{k} (x ⋅ yf) → ∃ x', ✓{k} (x' ⋅ yf) ∧ Q k x' |}.
......@@ -328,16 +330,17 @@ Next Obligation.
apply uPred_mono with x'; eauto using cmra_includedN_l.
Qed.
Next Obligation. naive_solver. Qed.
Definition uPred_bupd_aux : seal (@uPred_bupd_def). by eexists. Qed.
Definition uPred_bupd {M} := unseal uPred_bupd_aux M.
Definition uPred_bupd_eq : @uPred_bupd = @uPred_bupd_def := seal_eq uPred_bupd_aux.
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_eq {M} :
@bupd _ uPred_bupd = @uPred_bupd_def M := seal_eq uPred_bupd_aux.
Module uPred_unseal.
Definition unseal_eqs :=
(uPred_pure_eq, uPred_and_eq, uPred_or_eq, uPred_impl_eq, uPred_forall_eq,
uPred_exist_eq, uPred_internal_eq_eq, uPred_sep_eq, uPred_wand_eq,
uPred_plainly_eq, uPred_persistently_eq, uPred_later_eq, uPred_ownM_eq,
uPred_cmra_valid_eq, uPred_bupd_eq).
uPred_cmra_valid_eq, @uPred_bupd_eq).
Ltac unseal := (* Coq unfold is used to circumvent bug #5699 in rewrite /foo *)
unfold bi_emp; simpl;
unfold uPred_emp, bi_pure, bi_and, bi_or, bi_impl, bi_forall, bi_exist,
......@@ -566,7 +569,7 @@ Coercion uPred_valid {M} : uPred M → Prop := bi_valid.
(* Latest notation *)
Notation "✓ x" := (uPred_cmra_valid x) (at level 20) : bi_scope.
Notation "|==> Q" := (uPred_bupd Q)
Notation "|==> Q" := (bupd Q)
(at level 99, Q at level 200, format "|==> Q") : bi_scope.
Notation "P ==∗ Q" := (P ⊢ |==> Q)
(at level 99, Q at level 200, only parsing) : stdpp_scope.
......@@ -599,14 +602,15 @@ Qed.
Global Instance cmra_valid_proper {A : cmraT} :
Proper ((≡) ==> (⊣⊢)) (@uPred_cmra_valid M A) := ne_proper _.
Global Instance bupd_ne : NonExpansive (@uPred_bupd M).
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 ((≡) ==> (≡)) (@uPred_bupd M) := ne_proper _.
Global Instance bupd_proper :
Proper ((≡) ==> (≡)) (@bupd _ (@uPred_bupd M)) := ne_proper _.
(** BI instances *)
......
theories/program_logic/adequacy.v
View file @ c6bf752e
......@@ -73,7 +73,7 @@ Lemma wp_step e1 σ1 e2 σ2 efs Φ :
world σ1 ∗ WP e1 {{ Φ }} ==∗ ▷ |==> ◇ (world σ2 ∗ WP e2 {{ Φ }} ∗ wptp efs).
Proof.
rewrite {1}wp_unfold /wp_pre. iIntros (?) "[(Hw & HE & Hσ) H]".
rewrite (val_stuck e1 σ1 e2 σ2 efs) // fupd_eq /fupd_def.
rewrite (val_stuck e1 σ1 e2 σ2 efs) // uPred_fupd_eq.
iMod ("H" $! σ1 with "Hσ [Hw HE]") as ">(Hw & HE & _ & H)"; first by iFrame.
iModIntro; iNext.
iMod ("H" $! e2 σ2 efs with "[%] [$Hw $HE]") as ">($ & $ & $ & $)"; auto.
......@@ -125,7 +125,7 @@ Lemma wptp_result n e1 t1 v2 t2 σ1 σ2 φ :
Proof.
intros. rewrite wptp_steps // laterN_later. apply: bupd_iter_laterN_mono.
iDestruct 1 as (e2 t2' ?) "((Hw & HE & _) & H & _)"; simplify_eq.
iDestruct (wp_value_inv with "H") as "H". rewrite fupd_eq /fupd_def.
iDestruct (wp_value_inv with "H") as "H". rewrite uPred_fupd_eq.
iMod ("H" with "[Hw HE]") as ">(_ & _ & $)"; iFrame; auto.
Qed.
......@@ -133,8 +133,8 @@ Lemma wp_safe e σ Φ :
world σ -∗ WP e {{ Φ }} ==∗ ▷ ⌜is_Some (to_val e) ∨ reducible e σ⌝.
Proof.
rewrite wp_unfold /wp_pre. iIntros "(Hw&HE&Hσ) H".
destruct (to_val e) as [v|] eqn:?; [eauto 10|].
rewrite fupd_eq. iMod ("H" with "Hσ [-]") as ">(?&?&%&?)"; eauto 10 with iFrame.
destruct (to_val e) as [v|] eqn:?; [eauto 10|]. rewrite uPred_fupd_eq.
iMod ("H" with "Hσ [-]") as ">(?&?&%&?)"; eauto 10 with iFrame.
Qed.
Lemma wptp_safe n e1 e2 t1 t2 σ1 σ2 Φ :
......@@ -157,7 +157,7 @@ Proof.
intros ?. rewrite wptp_steps // bupd_iter_frame_l laterN_later.
apply: bupd_iter_laterN_mono.
iIntros "[Hback H]"; iDestruct "H" as (e2' t2' ->) "[(Hw&HE&Hσ) _]".
rewrite fupd_eq.
rewrite uPred_fupd_eq.
iMod ("Hback" with "Hσ [$Hw $HE]") as "> (_ & _ & $)"; auto.
Qed.
End adequacy.
......@@ -172,14 +172,14 @@ Proof.
intros Hwp; split.
- intros t2 σ2 v2 [n ?]%rtc_nsteps.
eapply (soundness (M:=iResUR Σ) _ (S (S n))).
iMod wsat_alloc as (Hinv) "[Hw HE]".
rewrite fupd_eq in Hwp; iMod (Hwp with "[$Hw $HE]") as ">(Hw & HE & Hwp)".
iMod wsat_alloc as (Hinv) "[Hw HE]". specialize (Hwp _).
rewrite uPred_fupd_eq in Hwp; iMod (Hwp with "[$Hw $HE]") as ">(Hw & HE & Hwp)".
iDestruct "Hwp" as (Istate) "[HI Hwp]".
iApply (@wptp_result _ _ (IrisG _ _ Hinv Istate)); eauto with iFrame.
- intros t2 σ2 e2 [n ?]%rtc_nsteps ?.
eapply (soundness (M:=iResUR Σ) _ (S (S n))).
iMod wsat_alloc as (Hinv) "[Hw HE]".
rewrite fupd_eq in Hwp; iMod (Hwp with "[$Hw $HE]") as ">(Hw & HE & Hwp)".
iMod wsat_alloc as (Hinv) "[Hw HE]". specialize (Hwp _).
rewrite uPred_fupd_eq in Hwp; iMod (Hwp with "[$Hw $HE]") as ">(Hw & HE & Hwp)".
iDestruct "Hwp" as (Istate) "[HI Hwp]".
iApply (@wptp_safe _ _ (IrisG _ _ Hinv Istate)); eauto with iFrame.
Qed.
......@@ -194,8 +194,8 @@ Theorem wp_invariance Σ Λ `{invPreG Σ} e σ1 t2 σ2 φ :
Proof.
intros Hwp [n ?]%rtc_nsteps.
eapply (soundness (M:=iResUR Σ) _ (S (S n))).
iMod wsat_alloc as (Hinv) "[Hw HE]".
rewrite {1}fupd_eq in Hwp; iMod (Hwp with "[$Hw $HE]") as ">(Hw & HE & Hwp)".
iMod wsat_alloc as (Hinv) "[Hw HE]". specialize (Hwp _).
rewrite {1}uPred_fupd_eq in Hwp; iMod (Hwp with "[$Hw $HE]") as ">(Hw & HE & Hwp)".
iDestruct "Hwp" as (Istate) "(HIstate & Hwp & Hclose)".
iApply (@wptp_invariance _ _ (IrisG _ _ Hinv Istate)); eauto with iFrame.
Qed.
Supports Markdown
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