Commit 7ccbb8cd authored by Joseph Tassarotti's avatar Joseph Tassarotti

Use explicit names in some scripts, re-organize fupd plainly derived laws,...

Use explicit names in some scripts, re-organize fupd plainly derived laws, adjust wsat import/export.
parent 334b689e
...@@ -50,7 +50,7 @@ Proof. ...@@ -50,7 +50,7 @@ Proof.
iNext. by iMod ("HP" with "[$]") as "(_ & _ & HP)". iNext. by iMod ("HP" with "[$]") as "(_ & _ & HP)".
Qed. Qed.
Lemma fupd_plain_soundness `{invPreG Σ} E (P: iPropSI Σ) `{!Plain P}: Lemma fupd_plain_soundness `{invPreG Σ} E (P: iProp Σ) `{!Plain P}:
( `{Hinv: invG Σ}, (|={, E}=> P)%I) ( P)%I. ( `{Hinv: invG Σ}, (|={, E}=> P)%I) ( P)%I.
Proof. Proof.
iIntros (Hfupd). iMod wsat_alloc as (Hinv) "[Hw HE]". iIntros (Hfupd). iMod wsat_alloc as (Hinv) "[Hw HE]".
...@@ -68,7 +68,7 @@ Proof. ...@@ -68,7 +68,7 @@ Proof.
eapply (fupd_plain_soundness ); first by apply _. eapply (fupd_plain_soundness ); first by apply _.
intros Hinv. rewrite -/sbi_laterN. intros Hinv. rewrite -/sbi_laterN.
iPoseProof (Hiter Hinv) as "H". iPoseProof (Hiter Hinv) as "H".
destruct n. destruct n as [|n].
- rewrite //=. iPoseProof (fupd_plain_strong with "H") as "H'". - rewrite //=. iPoseProof (fupd_plain_strong with "H") as "H'".
do 2 iMod "H'"; iModIntro; auto. do 2 iMod "H'"; iModIntro; auto.
- iPoseProof (step_fupdN_mono _ _ _ _ (|={}=> ⌜φ⌝)%I with "H") as "H'". - iPoseProof (step_fupdN_mono _ _ _ _ (|={}=> ⌜φ⌝)%I with "H") as "H'".
......
...@@ -13,23 +13,24 @@ Module invG. ...@@ -13,23 +13,24 @@ Module invG.
enabled_name : gname; enabled_name : gname;
disabled_name : gname; disabled_name : gname;
}. }.
End invG.
Import invG.
Definition invΣ : gFunctors := Definition invΣ : gFunctors :=
#[GFunctor (authRF (gmapURF positive (agreeRF (laterCF idCF)))); #[GFunctor (authRF (gmapURF positive (agreeRF (laterCF idCF))));
GFunctor coPset_disjUR; GFunctor coPset_disjUR;
GFunctor (gset_disjUR positive)]. GFunctor (gset_disjUR positive)].
Class invPreG (Σ : gFunctors) : Set := WsatPreG { Class invPreG (Σ : gFunctors) : Set := WsatPreG {
inv_inPreG :> inG Σ (authR (gmapUR positive (agreeR (laterC (iPreProp Σ))))); inv_inPreG :> inG Σ (authR (gmapUR positive (agreeR (laterC (iPreProp Σ)))));
enabled_inPreG :> inG Σ coPset_disjR; enabled_inPreG :> inG Σ coPset_disjR;
disabled_inPreG :> inG Σ (gset_disjR positive); disabled_inPreG :> inG Σ (gset_disjR positive);
}. }.
Instance subG_invΣ {Σ} : subG invΣ Σ invPreG Σ. Instance subG_invΣ {Σ} : subG invΣ Σ invPreG Σ.
Proof. solve_inG. Qed. Proof. solve_inG. Qed.
End invG.
Import invG.
Definition invariant_unfold {Σ} (P : iProp Σ) : agree (later (iPreProp Σ)) := Definition invariant_unfold {Σ} (P : iProp Σ) : agree (later (iPreProp Σ)) :=
to_agree (Next (iProp_unfold P)). to_agree (Next (iProp_unfold P)).
Definition ownI `{invG Σ} (i : positive) (P : iProp Σ) : iProp Σ := Definition ownI `{invG Σ} (i : positive) (P : iProp Σ) : iProp Σ :=
......
...@@ -272,38 +272,6 @@ Section fupd_derived. ...@@ -272,38 +272,6 @@ Section fupd_derived.
intros P1 P2 HP Q1 Q2 HQ. by rewrite HP HQ -fupd_sep. intros P1 P2 HP Q1 Q2 HQ. by rewrite HP HQ -fupd_sep.
Qed. Qed.
Lemma fupd_plain_weak `{BiPlainly PROP, !BiFUpdPlainly PROP} E P Q `{!Plain P}:
(Q ={E}= P) - Q ={E}= Q P.
Proof. by rewrite {1}(plain P) fupd_plainly_weak. Qed.
Lemma later_fupd_plain `{BiPlainly PROP, !BiFUpdPlainly PROP} p E1 E2 P `{!Plain P} :
(?p |={E1, E2}=> P) ={E1}= ?p P.
Proof. by rewrite {1}(plain P) later_fupd_plainly. Qed.
Lemma fupd_plain_strong `{BiPlainly PROP, !BiFUpdPlainly PROP} E1 E2 P `{!Plain P} :
(|={E1, E2}=> P) ={E1}= P.
Proof. by apply (later_fupd_plain false). Qed.
Lemma fupd_plain' `{BiPlainly PROP, !BiFUpdPlainly PROP} E1 E2 E2' P Q `{!Plain P} :
E1 E2
(Q ={E1, E2'}= P) - (|={E1, E2}=> Q) ={E1}= (|={E1, E2}=> Q) P.
Proof.
intros (E3&->&HE)%subseteq_disjoint_union_L.
apply wand_intro_l. rewrite fupd_frame_r.
rewrite fupd_plain_strong fupd_except_0 fupd_plain_weak wand_elim_r.
rewrite (fupd_mask_mono E1 (E1 E3)); last by set_solver+.
rewrite fupd_trans -(fupd_trans E1 (E1 E3) E1).
apply fupd_mono. rewrite -fupd_frame_r.
apply sep_mono; auto. apply fupd_intro_mask; set_solver+.
Qed.
Lemma fupd_plain `{BiPlainly PROP, !BiFUpdPlainly PROP} 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 wand_intro_l.
by rewrite wand_elim_r -fupd_intro.
Qed.
(** Fancy updates that take a step derived rules. *) (** Fancy updates that take a step derived rules. *)
Lemma step_fupd_wand E1 E2 E3 P Q : (|={E1,E2,E3}=> P) - (P - Q) - |={E1,E2,E3}=> Q. Lemma step_fupd_wand E1 E2 E3 P Q : (|={E1,E2,E3}=> P) - (P - Q) - |={E1,E2,E3}=> Q.
Proof. Proof.
...@@ -345,13 +313,6 @@ Section fupd_derived. ...@@ -345,13 +313,6 @@ Section fupd_derived.
by apply later_mono, fupd_mono. by apply later_mono, fupd_mono.
Qed. Qed.
Lemma step_fupd_plain `{BiPlainly PROP, !BiFUpdPlainly PROP} E P `{!Plain P} :
(|={E, }=> P) ={E}= P.
Proof.
specialize (later_fupd_plain true E P) => //= ->.
rewrite fupd_trans fupd_plain_strong. apply fupd_mono, except_0_later.
Qed.
Lemma step_fupd_fupd E P: Lemma step_fupd_fupd E P:
(|={E, }=> P) (|={E, }=> |={E}=> P). (|={E, }=> P) (|={E, }=> |={E}=> P).
Proof. Proof.
...@@ -380,15 +341,58 @@ Section fupd_derived. ...@@ -380,15 +341,58 @@ Section fupd_derived.
rewrite step_fupd_frame_l IH //=. rewrite step_fupd_frame_l IH //=.
Qed. Qed.
Lemma step_fupdN_plain `{BiPlainly PROP, !BiFUpdPlainly PROP} E n P `{!Plain P}: Section fupd_plainly_derived.
(|={E, }=>^n P) ={E}= ^n P. Context `{BiPlainly PROP, !BiFUpdPlainly PROP}.
Proof.
induction n as [| n]. Lemma fupd_plain_weak E P Q `{!Plain P}:
- rewrite -fupd_intro. apply except_0_intro. (Q ={E}= P) - Q ={E}= Q P.
- rewrite Nat_iter_S step_fupd_fupd IHn ?fupd_trans step_fupd_plain. Proof. by rewrite {1}(plain P) fupd_plainly_weak. Qed.
apply fupd_mono. destruct n; simpl.
* by rewrite except_0_idemp. Lemma later_fupd_plain p E1 E2 P `{!Plain P} :
* by rewrite except_0_later. (?p |={E1, E2}=> P) ={E1}= ?p P.
Qed. Proof. by rewrite {1}(plain P) later_fupd_plainly. Qed.
Lemma fupd_plain_strong E1 E2 P `{!Plain P} :
(|={E1, E2}=> P) ={E1}= P.
Proof. by apply (later_fupd_plain false). 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.
intros (E3&->&HE)%subseteq_disjoint_union_L.
apply wand_intro_l. rewrite fupd_frame_r.
rewrite fupd_plain_strong fupd_except_0 fupd_plain_weak wand_elim_r.
rewrite (fupd_mask_mono E1 (E1 E3)); last by set_solver+.
rewrite fupd_trans -(fupd_trans E1 (E1 E3) E1).
apply fupd_mono. rewrite -fupd_frame_r.
apply sep_mono; auto. apply fupd_intro_mask; set_solver+.
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 wand_intro_l.
by rewrite wand_elim_r -fupd_intro.
Qed.
Lemma step_fupd_plain E P `{!Plain P} :
(|={E, }=> P) ={E}= P.
Proof.
specialize (later_fupd_plain true E P) => //= ->.
rewrite fupd_trans fupd_plain_strong. apply fupd_mono, except_0_later.
Qed.
Lemma step_fupdN_plain E n P `{!Plain P}:
(|={E, }=>^n P) ={E}= ^n P.
Proof.
induction n as [|n IH].
- rewrite -fupd_intro. apply except_0_intro.
- rewrite Nat_iter_S step_fupd_fupd IH ?fupd_trans step_fupd_plain.
apply fupd_mono. destruct n; simpl.
* by rewrite except_0_idemp.
* by rewrite except_0_later.
Qed.
End fupd_plainly_derived.
End fupd_derived. End fupd_derived.
From stdpp Require Import namespaces. From stdpp Require Import namespaces.
From iris.program_logic Require Export weakestpre. From iris.program_logic Require Export weakestpre.
From iris.algebra Require Import gmap auth agree gset coPset. From iris.algebra Require Import gmap auth agree gset coPset.
From iris.base_logic.lib Require Export wsat. From iris.base_logic.lib Require Import wsat.
From iris.proofmode Require Import tactics. From iris.proofmode Require Import tactics.
Set Default Proof Using "Type". Set Default Proof Using "Type".
Import uPred. Import uPred.
......
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