Commit 568f6b7a by Robbert Krebbers

### Use notation |==> instead of |=r=> for basic update modality.

parent 1b85d654
 ... @@ -23,8 +23,8 @@ Notation "P =n=★ Q" := (P -★ |=n=> Q)%I ... @@ -23,8 +23,8 @@ Notation "P =n=★ Q" := (P -★ |=n=> Q)%I (at level 99, Q at level 200, format "P =n=★ Q") : uPred_scope. (at level 99, Q at level 200, format "P =n=★ Q") : uPred_scope. (* Our goal is to prove that: (* Our goal is to prove that: (1) |=n=> has (nearly) all the properties of the |=r=> modality that are used in Iris (1) |=n=> has (nearly) all the properties of the |==> modality that are used in Iris (2) If our meta-logic is classical, then |=n=> and |=r=> are equivalent (2) If our meta-logic is classical, then |=n=> and |==> are equivalent *) *) Section bupd_nnupd. Section bupd_nnupd. ... @@ -264,7 +264,7 @@ Qed. ... @@ -264,7 +264,7 @@ Qed. direction from bupd to nnupd is similar to the proof of direction from bupd to nnupd is similar to the proof of nnupd_ownM_updateP *) nnupd_ownM_updateP *) Lemma bupd_nnupd P: (|=r=> P) ⊢ |=n=> P. Lemma bupd_nnupd P: (|==> P) ⊢ |=n=> P. Proof. Proof. split. rewrite /uPred_nnupd. repeat uPred.unseal. intros n x ? Hbupd a. split. rewrite /uPred_nnupd. repeat uPred.unseal. intros n x ? Hbupd a. red; rewrite //= => n' yf ??. red; rewrite //= => n' yf ??. ... @@ -282,7 +282,7 @@ Qed. ... @@ -282,7 +282,7 @@ Qed. (* However, the other direction seems to need a classical axiom: *) (* However, the other direction seems to need a classical axiom: *) Section classical. Section classical. Context (not_all_not_ex: ∀ (P : M → Prop), ¬ (∀ n : M, ¬ P n) → ∃ n : M, P n). Context (not_all_not_ex: ∀ (P : M → Prop), ¬ (∀ n : M, ¬ P n) → ∃ n : M, P n). Lemma nnupd_bupd P: (|=n=> P) ⊢ (|=r=> P). Lemma nnupd_bupd P: (|=n=> P) ⊢ (|==> P). Proof. Proof. rewrite /uPred_nnupd. rewrite /uPred_nnupd. split. uPred.unseal; red; rewrite //=. split. uPred.unseal; red; rewrite //=. ... @@ -373,8 +373,8 @@ Qed. ... @@ -373,8 +373,8 @@ Qed. (* Open question: (* Open question: Do the basic properties of the |=r=> modality (bupd_intro, bupd_mono, rvs_trans, rvs_frame_r, Do the basic properties of the |==> modality (bupd_intro, bupd_mono, rvs_trans, rvs_frame_r, bupd_ownM_updateP, and adequacy) uniquely characterize |=r=>? bupd_ownM_updateP, and adequacy) uniquely characterize |==>? *) *) End bupd_nnupd. End bupd_nnupd.
 ... @@ -310,12 +310,12 @@ Notation "▷ P" := (uPred_later P) ... @@ -310,12 +310,12 @@ Notation "▷ P" := (uPred_later P) (at level 20, right associativity) : uPred_scope. (at level 20, right associativity) : uPred_scope. Infix "≡" := uPred_eq : uPred_scope. Infix "≡" := uPred_eq : uPred_scope. Notation "✓ x" := (uPred_cmra_valid x) (at level 20) : uPred_scope. Notation "✓ x" := (uPred_cmra_valid x) (at level 20) : uPred_scope. Notation "|=r=> Q" := (uPred_bupd Q) Notation "|==> Q" := (uPred_bupd Q) (at level 99, Q at level 200, format "|=r=> Q") : uPred_scope. (at level 99, Q at level 200, format "|==> Q") : uPred_scope. Notation "P =r=> Q" := (P ⊢ |=r=> Q) Notation "P ==★ Q" := (P ⊢ |==> Q) (at level 99, Q at level 200, only parsing) : C_scope. (at level 99, Q at level 200, only parsing) : C_scope. Notation "P =r=★ Q" := (P -★ |=r=> Q)%I Notation "P ==★ Q" := (P -★ |==> Q)%I (at level 99, Q at level 200, format "P =r=★ Q") : uPred_scope. (at level 99, Q at level 200, format "P ==★ Q") : uPred_scope. Definition uPred_iff {M} (P Q : uPred M) : uPred M := ((P → Q) ∧ (Q → P))%I. Definition uPred_iff {M} (P Q : uPred M) : uPred M := ((P → Q) ∧ (Q → P))%I. Instance: Params (@uPred_iff) 1. Instance: Params (@uPred_iff) 1. ... @@ -1283,20 +1283,20 @@ Lemma always_cmra_valid {A : cmraT} (a : A) : □ ✓ a ⊣⊢ ✓ a. ... @@ -1283,20 +1283,20 @@ Lemma always_cmra_valid {A : cmraT} (a : A) : □ ✓ a ⊣⊢ ✓ a. Qed. Qed. (* Basic update modality *) (* Basic update modality *) Lemma bupd_intro P : P =r=> P. Lemma bupd_intro P : P ==★ P. Proof. Proof. unseal. split=> n x ? HP k yf ?; exists x; split; first done. unseal. split=> n x ? HP k yf ?; exists x; split; first done. apply uPred_closed with n; eauto using cmra_validN_op_l. apply uPred_closed with n; eauto using cmra_validN_op_l. Qed. Qed. Lemma bupd_mono P Q : (P ⊢ Q) → (|=r=> P) =r=> Q. Lemma bupd_mono P Q : (P ⊢ Q) → (|==> P) ==★ Q. Proof. Proof. unseal. intros HPQ; split=> n x ? HP k yf ??. unseal. intros HPQ; split=> n x ? HP k yf ??. destruct (HP k yf) as (x'&?&?); eauto. destruct (HP k yf) as (x'&?&?); eauto. exists x'; split; eauto using uPred_in_entails, cmra_validN_op_l. exists x'; split; eauto using uPred_in_entails, cmra_validN_op_l. Qed. Qed. Lemma bupd_trans P : (|=r=> |=r=> P) =r=> P. Lemma bupd_trans P : (|==> |==> P) ==★ P. Proof. unseal; split; naive_solver. Qed. Proof. unseal; split; naive_solver. Qed. Lemma bupd_frame_r P R : (|=r=> P) ★ R =r=> P ★ R. Lemma bupd_frame_r P R : (|==> P) ★ R ==★ P ★ R. Proof. Proof. unseal; split; intros n x ? (x1&x2&Hx&HP&?) k yf ??. unseal; split; intros n x ? (x1&x2&Hx&HP&?) k yf ??. destruct (HP k (x2 ⋅ yf)) as (x'&?&?); eauto. destruct (HP k (x2 ⋅ yf)) as (x'&?&?); eauto. ... @@ -1306,7 +1306,7 @@ Proof. ... @@ -1306,7 +1306,7 @@ Proof. apply uPred_closed with n; eauto 3 using cmra_validN_op_l, cmra_validN_op_r. apply uPred_closed with n; eauto 3 using cmra_validN_op_l, cmra_validN_op_r. Qed. Qed. Lemma bupd_ownM_updateP x (Φ : M → Prop) : Lemma bupd_ownM_updateP x (Φ : M → Prop) : x ~~>: Φ → uPred_ownM x =r=> ∃ y, ■ Φ y ∧ uPred_ownM y. x ~~>: Φ → uPred_ownM x ==★ ∃ y, ■ Φ y ∧ uPred_ownM y. Proof. Proof. unseal=> Hup; split=> n x2 ? [x3 Hx] k yf ??. unseal=> Hup; split=> n x2 ? [x3 Hx] k yf ??. destruct (Hup k (Some (x3 ⋅ yf))) as (y&?&?); simpl in *. destruct (Hup k (Some (x3 ⋅ yf))) as (y&?&?); simpl in *. ... @@ -1320,20 +1320,20 @@ Global Instance bupd_mono' : Proper ((⊢) ==> (⊢)) (@uPred_bupd M). ... @@ -1320,20 +1320,20 @@ Global Instance bupd_mono' : Proper ((⊢) ==> (⊢)) (@uPred_bupd M). Proof. intros P Q; apply bupd_mono. Qed. 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 (⊢)) (@uPred_bupd M). Proof. intros P Q; apply bupd_mono. Qed. Proof. intros P Q; apply bupd_mono. Qed. Lemma bupd_frame_l R Q : (R ★ |=r=> Q) =r=> R ★ Q. Lemma bupd_frame_l R Q : (R ★ |==> Q) ==★ R ★ Q. Proof. rewrite !(comm _ R); apply bupd_frame_r. Qed. Proof. rewrite !(comm _ R); apply bupd_frame_r. Qed. Lemma bupd_wand_l P Q : (P -★ Q) ★ (|=r=> P) =r=> Q. Lemma bupd_wand_l P Q : (P -★ Q) ★ (|==> P) ==★ Q. Proof. by rewrite bupd_frame_l wand_elim_l. Qed. Proof. by rewrite bupd_frame_l wand_elim_l. Qed. Lemma bupd_wand_r P Q : (|=r=> P) ★ (P -★ Q) =r=> Q. Lemma bupd_wand_r P Q : (|==> P) ★ (P -★ Q) ==★ Q. Proof. by rewrite bupd_frame_r wand_elim_r. Qed. Proof. by rewrite bupd_frame_r wand_elim_r. Qed. Lemma bupd_sep P Q : (|=r=> P) ★ (|=r=> Q) =r=> P ★ Q. Lemma bupd_sep P Q : (|==> P) ★ (|==> Q) ==★ P ★ Q. Proof. by rewrite bupd_frame_r bupd_frame_l bupd_trans. Qed. Proof. by rewrite bupd_frame_r bupd_frame_l bupd_trans. Qed. Lemma bupd_ownM_update x y : x ~~> y → uPred_ownM x ⊢ |=r=> uPred_ownM y. Lemma bupd_ownM_update x y : x ~~> y → uPred_ownM x ⊢ |==> uPred_ownM y. Proof. Proof. intros; rewrite (bupd_ownM_updateP _ (y =)); last by apply cmra_update_updateP. intros; rewrite (bupd_ownM_updateP _ (y =)); last by apply cmra_update_updateP. by apply bupd_mono, exist_elim=> y'; apply pure_elim_l=> ->. by apply bupd_mono, exist_elim=> y'; apply pure_elim_l=> ->. Qed. Qed. Lemma except_last_bupd P : ◇ (|=r=> P) ⊢ (|=r=> ◇ P). Lemma except_last_bupd P : ◇ (|==> P) ⊢ (|==> ◇ P). Proof. Proof. rewrite /uPred_except_last. apply or_elim; auto using bupd_mono. rewrite /uPred_except_last. apply or_elim; auto using bupd_mono. by rewrite -bupd_intro -or_intro_l. by rewrite -bupd_intro -or_intro_l. ... @@ -1490,9 +1490,9 @@ Lemma always_entails_r P Q `{!PersistentP Q} : (P ⊢ Q) → P ⊢ P ★ Q. ... @@ -1490,9 +1490,9 @@ Lemma always_entails_r P Q `{!PersistentP Q} : (P ⊢ Q) → P ⊢ P ★ Q. Proof. by rewrite -(always_always Q); apply always_entails_r'. Qed. Proof. by rewrite -(always_always Q); apply always_entails_r'. Qed. (** Consistency and adequancy statements *) (** Consistency and adequancy statements *) Lemma adequacy φ n : (True ⊢ Nat.iter n (λ P, |=r=> ▷ P) (■ φ)) → φ. Lemma adequacy φ n : (True ⊢ Nat.iter n (λ P, |==> ▷ P) (■ φ)) → φ. Proof. Proof. cut (∀ x, ✓{n} x → Nat.iter n (λ P, |=r=> ▷ P)%I (■ φ)%I n x → φ). cut (∀ x, ✓{n} x → Nat.iter n (λ P, |==> ▷ P)%I (■ φ)%I n x → φ). { intros help H. eapply (help ∅); eauto using ucmra_unit_validN. { intros help H. eapply (help ∅); eauto using ucmra_unit_validN. eapply H; try unseal; eauto using ucmra_unit_validN. } eapply H; try unseal; eauto using ucmra_unit_validN. } unseal. induction n as [|n IH]=> x Hx Hupd; auto. unseal. induction n as [|n IH]=> x Hx Hupd; auto. ... @@ -1500,7 +1500,7 @@ Proof. ... @@ -1500,7 +1500,7 @@ Proof. eapply IH with x'; eauto using cmra_validN_S, cmra_validN_op_l. eapply IH with x'; eauto using cmra_validN_S, cmra_validN_op_l. Qed. Qed. Corollary consistency_modal n : ¬ (True ⊢ Nat.iter n (λ P, |=r=> ▷ P) False). Corollary consistency_modal n : ¬ (True ⊢ Nat.iter n (λ P, |==> ▷ P) False). Proof. exact (adequacy False n). Qed. Proof. exact (adequacy False n). Qed. Corollary consistency : ¬ (True ⊢ False). Corollary consistency : ¬ (True ⊢ False). ... ...
 ... @@ -162,7 +162,7 @@ Proof. ... @@ -162,7 +162,7 @@ Proof. Qed. Qed. Lemma recv_split E l P1 P2 : Lemma recv_split E l P1 P2 : nclose N ⊆ E → recv l (P1 ★ P2) ={E}=> recv l P1 ★ recv l P2. nclose N ⊆ E → recv l (P1 ★ P2) ={E}=★ recv l P1 ★ recv l P2. Proof. Proof. rename P1 into R1; rename P2 into R2. rewrite {1}/recv /barrier_ctx. rename P1 into R1; rename P2 into R2. rewrite {1}/recv /barrier_ctx. iIntros (?). iDestruct 1 as (γ P Q i) "(#(%&Hh&Hsts)&Hγ&#HQ&HQR)". iIntros (?). iDestruct 1 as (γ P Q i) "(#(%&Hh&Hsts)&Hγ&#HQ&HQR)". ... ...
 ... @@ -23,7 +23,7 @@ Proof. ... @@ -23,7 +23,7 @@ Proof. - iIntros (P) "#? !# _". iApply (newbarrier_spec _ P); eauto. - iIntros (P) "#? !# _". iApply (newbarrier_spec _ P); eauto. - iIntros (l P) "!# [Hl HP]". by iApply signal_spec; iFrame "Hl HP". - iIntros (l P) "!# [Hl HP]". by iApply signal_spec; iFrame "Hl HP". - iIntros (l P) "!# Hl". iApply wait_spec; iFrame "Hl"; eauto. - iIntros (l P) "!# Hl". iApply wait_spec; iFrame "Hl"; eauto. - intros; by apply recv_split. - iIntros (l P Q) "!#". by iApply recv_split. - apply recv_weaken. - apply recv_weaken. Qed. Qed. End spec. End spec.
 ... @@ -40,7 +40,7 @@ Notation wptp t := ([★ list] ef ∈ t, WP ef {{ _, True }})%I. ... @@ -40,7 +40,7 @@ Notation wptp t := ([★ list] ef ∈ t, WP ef {{ _, True }})%I. Lemma wp_step e1 σ1 e2 σ2 efs Φ : Lemma wp_step e1 σ1 e2 σ2 efs Φ : prim_step e1 σ1 e2 σ2 efs → prim_step e1 σ1 e2 σ2 efs → world σ1 ★ WP e1 {{ Φ }} =r=> ▷ |=r=> ◇ (world σ2 ★ WP e2 {{ Φ }} ★ wptp efs). world σ1 ★ WP e1 {{ Φ }} ==★ ▷ |==> ◇ (world σ2 ★ WP e2 {{ Φ }} ★ wptp efs). Proof. Proof. rewrite {1}wp_unfold /wp_pre. iIntros (Hstep) "[(Hw & HE & Hσ) [H|[_ H]]]". rewrite {1}wp_unfold /wp_pre. iIntros (Hstep) "[(Hw & HE & Hσ) [H|[_ H]]]". { iDestruct "H" as (v) "[% _]". apply val_stuck in Hstep; simplify_eq. } { iDestruct "H" as (v) "[% _]". apply val_stuck in Hstep; simplify_eq. } ... @@ -54,7 +54,7 @@ Qed. ... @@ -54,7 +54,7 @@ Qed. Lemma wptp_step e1 t1 t2 σ1 σ2 Φ : Lemma wptp_step e1 t1 t2 σ1 σ2 Φ : step (e1 :: t1,σ1) (t2, σ2) → step (e1 :: t1,σ1) (t2, σ2) → world σ1 ★ WP e1 {{ Φ }} ★ wptp t1 world σ1 ★ WP e1 {{ Φ }} ★ wptp t1 =r=> ∃ e2 t2', t2 = e2 :: t2' ★ ▷ |=r=> ◇ (world σ2 ★ WP e2 {{ Φ }} ★ wptp t2'). ==★ ∃ e2 t2', t2 = e2 :: t2' ★ ▷ |==> ◇ (world σ2 ★ WP e2 {{ Φ }} ★ wptp t2'). Proof. Proof. iIntros (Hstep) "(HW & He & Ht)". iIntros (Hstep) "(HW & He & Ht)". destruct Hstep as [e1' σ1' e2' σ2' efs [|? t1'] t2' ?? Hstep]; simplify_eq/=. destruct Hstep as [e1' σ1' e2' σ2' efs [|? t1'] t2' ?? Hstep]; simplify_eq/=. ... @@ -69,7 +69,7 @@ Qed. ... @@ -69,7 +69,7 @@ Qed. Lemma wptp_steps n e1 t1 t2 σ1 σ2 Φ : Lemma wptp_steps n e1 t1 t2 σ1 σ2 Φ : nsteps step n (e1 :: t1, σ1) (t2, σ2) → nsteps step n (e1 :: t1, σ1) (t2, σ2) → world σ1 ★ WP e1 {{ Φ }} ★ wptp t1 ⊢ world σ1 ★ WP e1 {{ Φ }} ★ wptp t1 ⊢ Nat.iter (S n) (λ P, |=r=> ▷ P) (∃ e2 t2', Nat.iter (S n) (λ P, |==> ▷ P) (∃ e2 t2', t2 = e2 :: t2' ★ world σ2 ★ WP e2 {{ Φ }} ★ wptp t2'). t2 = e2 :: t2' ★ world σ2 ★ WP e2 {{ Φ }} ★ wptp t2'). Proof. Proof. revert e1 t1 t2 σ1 σ2; simpl; induction n as [|n IH]=> e1 t1 t2 σ1 σ2 /=. revert e1 t1 t2 σ1 σ2; simpl; induction n as [|n IH]=> e1 t1 t2 σ1 σ2 /=. ... @@ -79,11 +79,11 @@ Proof. ... @@ -79,11 +79,11 @@ Proof. iUpdIntro; iNext; iUpd "H" as ">?". by iApply IH. iUpdIntro; iNext; iUpd "H" as ">?". by iApply IH. Qed. Qed. Instance bupd_iter_mono n : Proper ((⊢) ==> (⊢)) (Nat.iter n (λ P, |=r=> ▷ P)%I). Instance bupd_iter_mono n : Proper ((⊢) ==> (⊢)) (Nat.iter n (λ P, |==> ▷ P)%I). Proof. intros P Q HP. induction n; simpl; do 2?f_equiv; auto. Qed. Proof. intros P Q HP. induction n; simpl; do 2?f_equiv; auto. Qed. Lemma bupd_iter_frame_l n R Q : Lemma bupd_iter_frame_l n R Q : R ★ Nat.iter n (λ P, |=r=> ▷ P) Q ⊢ Nat.iter n (λ P, |=r=> ▷ P) (R ★ Q). R ★ Nat.iter n (λ P, |==> ▷ P) Q ⊢ Nat.iter n (λ P, |==> ▷ P) (R ★ Q). Proof. Proof. induction n as [|n IH]; simpl; [done|]. induction n as [|n IH]; simpl; [done|]. by rewrite bupd_frame_l {1}(later_intro R) -later_sep IH. by rewrite bupd_frame_l {1}(later_intro R) -later_sep IH. ... @@ -92,7 +92,7 @@ Qed. ... @@ -92,7 +92,7 @@ Qed. Lemma wptp_result n e1 t1 v2 t2 σ1 σ2 φ : Lemma wptp_result n e1 t1 v2 t2 σ1 σ2 φ : nsteps step n (e1 :: t1, σ1) (of_val v2 :: t2, σ2) → nsteps step n (e1 :: t1, σ1) (of_val v2 :: t2, σ2) → world σ1 ★ WP e1 {{ v, ■ φ v }} ★ wptp t1 ⊢ world σ1 ★ WP e1 {{ v, ■ φ v }} ★ wptp t1 ⊢ Nat.iter (S (S n)) (λ P, |=r=> ▷ P) (■ φ v2). Nat.iter (S (S n)) (λ P, |==> ▷ P) (■ φ v2). Proof. Proof. intros. rewrite wptp_steps //. intros. rewrite wptp_steps //. rewrite (Nat_iter_S_r (S n)). apply bupd_iter_mono. rewrite (Nat_iter_S_r (S n)). apply bupd_iter_mono. ... @@ -102,7 +102,7 @@ Proof. ... @@ -102,7 +102,7 @@ Proof. Qed. Qed. Lemma wp_safe e σ Φ : Lemma wp_safe e σ Φ : world σ ★ WP e {{ Φ }} =r=> ▷ ■ (is_Some (to_val e) ∨ reducible e σ). world σ ★ WP e {{ Φ }} ==★ ▷ ■ (is_Some (to_val e) ∨ reducible e σ). Proof. Proof. rewrite wp_unfold /wp_pre. iIntros "[(Hw&HE&Hσ) [H|[_ H]]]". rewrite wp_unfold /wp_pre. iIntros "[(Hw&HE&Hσ) [H|[_ H]]]". { iDestruct "H" as (v) "[% _]"; eauto 10. } { iDestruct "H" as (v) "[% _]"; eauto 10. } ... @@ -113,7 +113,7 @@ Qed. ... @@ -113,7 +113,7 @@ Qed. Lemma wptp_safe n e1 e2 t1 t2 σ1 σ2 Φ : Lemma wptp_safe n e1 e2 t1 t2 σ1 σ2 Φ : nsteps step n (e1 :: t1, σ1) (t2, σ2) → e2 ∈ t2 → nsteps step n (e1 :: t1, σ1) (t2, σ2) → e2 ∈ t2 → world σ1 ★ WP e1 {{ Φ }} ★ wptp t1 ⊢ world σ1 ★ WP e1 {{ Φ }} ★ wptp t1 ⊢ Nat.iter (S (S n)) (λ P, |=r=> ▷ P) (■ (is_Some (to_val e2) ∨ reducible e2 σ2)). Nat.iter (S (S n)) (λ P, |==> ▷ P) (■ (is_Some (to_val e2) ∨ reducible e2 σ2)). Proof. Proof. intros ? He2. rewrite wptp_steps //; rewrite (Nat_iter_S_r (S n)). apply bupd_iter_mono. intros ? He2. rewrite wptp_steps //; rewrite (Nat_iter_S_r (S n)). apply bupd_iter_mono. iDestruct 1 as (e2' t2') "(% & Hw & H & Htp)"; simplify_eq. iDestruct 1 as (e2' t2') "(% & Hw & H & Htp)"; simplify_eq. ... @@ -123,9 +123,9 @@ Qed. ... @@ -123,9 +123,9 @@ Qed. Lemma wptp_invariance n e1 e2 t1 t2 σ1 σ2 I φ Φ : Lemma wptp_invariance n e1 e2 t1 t2 σ1 σ2 I φ Φ : nsteps step n (e1 :: t1, σ1) (t2, σ2) → nsteps step n (e1 :: t1, σ1) (t2, σ2) → (I ={⊤,∅}=> ∃ σ', ownP σ' ∧ ■ φ σ') → (I ={⊤,∅}=★ ∃ σ', ownP σ' ∧ ■ φ σ') → I ★ world σ1 ★ WP e1 {{ Φ }} ★ wptp t1 ⊢ I ★ world σ1 ★ WP e1 {{ Φ }} ★ wptp t1 ⊢ Nat.iter (S (S n)) (λ P, |=r=> ▷ P) (■ φ σ2). Nat.iter (S (S n)) (λ P, |==> ▷ P) (■ φ σ2). Proof. Proof. intros ? HI. rewrite wptp_steps //. intros ? HI. rewrite wptp_steps //. rewrite (Nat_iter_S_r (S n)) bupd_iter_frame_l. apply bupd_iter_mono. rewrite (Nat_iter_S_r (S n)) bupd_iter_frame_l. apply bupd_iter_mono. ... @@ -156,8 +156,8 @@ Proof. ... @@ -156,8 +156,8 @@ Proof. Qed. Qed. Theorem wp_invariance Σ `{irisPreG Λ Σ} e σ1 t2 σ2 I φ Φ : Theorem wp_invariance Σ `{irisPreG Λ Σ} e σ1 t2 σ2 I φ Φ : (∀ `{irisG Λ Σ}, ownP σ1 ={⊤}=> I ★ WP e {{ Φ }}) → (∀ `{irisG Λ Σ}, ownP σ1 ={⊤}=★ I ★ WP e {{ Φ }}) → (∀ `{irisG Λ Σ}, I ={⊤,∅}=> ∃ σ', ownP σ' ∧ ■ φ σ') → (∀ `{irisG Λ Σ}, I ={⊤,∅}=★ ∃ σ', ownP σ' ∧ ■ φ σ') → rtc step ([e], σ1) (t2, σ2) → rtc step ([e], σ1) (t2, σ2) → φ σ2. φ σ2. Proof. Proof. ... ...
 ... @@ -91,7 +91,7 @@ Section auth. ... @@ -91,7 +91,7 @@ Section auth. Proof. intros a1 a2. apply auth_own_mono. Qed. Proof. intros a1 a2. apply auth_own_mono. Qed. Lemma auth_alloc_strong N E t (G : gset gname) : Lemma auth_alloc_strong N E t (G : gset gname) : ✓ (f t) → ▷ φ t ={E}=> ∃ γ, ■ (γ ∉ G) ∧ auth_ctx γ N f φ ∧ auth_own γ (f t). ✓ (f t) → ▷ φ t ={E}=★ ∃ γ, ■ (γ ∉ G) ∧ auth_ctx γ N f φ ∧ auth_own γ (f t). Proof. Proof. iIntros (?) "Hφ". rewrite /auth_own /auth_ctx. iIntros (?) "Hφ". rewrite /auth_own /auth_ctx. iUpd (own_alloc_strong (Auth (Excl' (f t)) (f t)) G) as (γ) "[% Hγ]"; first done. iUpd (own_alloc_strong (Auth (Excl' (f t)) (f t)) G) as (γ) "[% Hγ]"; first done. ... @@ -102,17 +102,17 @@ Section auth. ... @@ -102,17 +102,17 @@ Section auth. Qed. Qed. Lemma auth_alloc N E t : Lemma auth_alloc N E t : ✓ (f t) → ▷ φ t ={E}=> ∃ γ, auth_ctx γ N f φ ∧ auth_own γ (f t). ✓ (f t) → ▷ φ t ={E}=★ ∃ γ, auth_ctx γ N f φ ∧ auth_own γ (f t). Proof. Proof. iIntros (?) "Hφ". iIntros (?) "Hφ". iUpd (auth_alloc_strong N E t ∅ with "Hφ") as (γ) "[_ ?]"; eauto. iUpd (auth_alloc_strong N E t ∅ with "Hφ") as (γ) "[_ ?]"; eauto. Qed. Qed. Lemma auth_empty γ : True =r=> auth_own γ ∅. Lemma auth_empty γ : True ==★ auth_own γ ∅. Proof. by rewrite /auth_own -own_empty. Qed. Proof. by rewrite /auth_own -own_empty. Qed. Lemma auth_acc E γ a : Lemma auth_acc E γ a : ▷ auth_inv γ f φ ★ auth_own γ a ={E}=> ∃ t, ▷ auth_inv γ f φ ★ auth_own γ a ={E}=★ ∃ t, ■ (a ≼ f t) ★ ▷ φ t ★ ∀ u b, ■ (a ≼ f t) ★ ▷ φ t ★ ∀ u b, ■ ((f t, a) ~l~> (f u, b)) ★ ▷ φ u ={E}=★ ▷ auth_inv γ f φ ★ auth_own γ b. ■ ((f t, a) ~l~> (f u, b)) ★ ▷ φ u ={E}=★ ▷ auth_inv γ f φ ★ auth_own γ b. Proof. Proof. ... @@ -128,7 +128,7 @@ Section auth. ... @@ -128,7 +128,7 @@ Section auth. Lemma auth_open E N γ a : Lemma auth_open E N γ a : nclose N ⊆ E → nclose N ⊆ E → auth_ctx γ N f φ ★ auth_own γ a ={E,E∖N}=> ∃ t, auth_ctx γ N f φ ★ auth_own γ a ={E,E∖N}=★ ∃ t, ■ (a ≼ f t) ★ ▷ φ t ★ ∀ u b, ■ (a ≼ f t) ★ ▷ φ t ★ ∀ u b, ■ ((f t, a) ~l~> (f u, b)) ★ ▷ φ u ={E∖N,E}=★ auth_own γ b. ■ ((f t, a) ~l~> (f u, b)) ★ ▷ φ u ={E∖N,E}=★ auth_own γ b. Proof. Proof. ... ...
 ... @@ -63,7 +63,7 @@ Qed. ... @@ -63,7 +63,7 @@ Qed. Lemma box_own_auth_update γ b1 b2 b3 : Lemma box_own_auth_update γ b1 b2 b3 : box_own_auth γ (● Excl' b1) ★ box_own_auth γ (◯ Excl' b2) box_own_auth γ (● Excl' b1) ★ box_own_auth γ (◯ Excl' b2) =r=> box_own_auth γ (● Excl' b3) ★ box_own_auth γ (◯ Excl' b3). ==★ box_own_auth γ (● Excl' b3) ★ box_own_auth γ (◯ Excl' b3). Proof. Proof. rewrite /box_own_auth -!own_op. apply own_update, prod_update; last done. rewrite /box_own_auth -!own_op. apply own_update, prod_update; last done. by apply auth_update, option_local_update, exclusive_local_update. by apply auth_update, option_local_update, exclusive_local_update. ... @@ -86,7 +86,7 @@ Proof. ... @@ -86,7 +86,7 @@ Proof. Qed. Qed. Lemma box_insert f P Q : Lemma box_insert f P Q : ▷ box N f P ={N}=> ∃ γ, f !! γ = None ★ ▷ box N f P ={N}=★ ∃ γ, f !! γ = None ★ slice N γ Q ★ ▷ box N (<[γ:=false]> f) (Q ★ P). slice N γ Q ★ ▷ box N (<[γ:=false]> f) (Q ★ P). Proof. Proof. iDestruct 1 as (Φ) "[#HeqP Hf]". iDestruct 1 as (Φ) "[#HeqP Hf]". ... @@ -106,7 +106,7 @@ Qed. ... @@ -106,7 +106,7 @@ Qed. Lemma box_delete f P Q γ : Lemma box_delete f P Q γ : f !! γ = Some false → f !! γ = Some false → slice N γ Q ★ ▷ box N f P ={N}=> ∃ P', slice N γ Q ★ ▷ box N f P ={N}=★ ∃ P', ▷ ▷ (P ≡ (Q ★ P')) ★ ▷ box N (delete γ f) P'. ▷ ▷ (P ≡ (Q ★ P')) ★ ▷ box N (delete γ f) P'. Proof. Proof. iIntros (?) "[#Hinv H]"; iDestruct "H" as (Φ) "[#HeqP Hf]". iIntros (?) "[#Hinv H]"; iDestruct "H" as (Φ) "[#HeqP Hf]". ... @@ -125,7 +125,7 @@ Qed. ... @@ -125,7 +125,7 @@ Qed. Lemma box_fill f γ P Q : Lemma box_fill f γ P Q : f !! γ = Some false → f !! γ = Some false → slice N γ Q ★ ▷ Q ★ ▷ box N f P ={N}=> ▷ box N (<[γ:=true]> f) P. slice N γ Q ★ ▷ Q ★ ▷ box N f P ={N}=★ ▷ box N (<[γ:=true]> f) P. Proof. Proof. iIntros (?) "(#Hinv & HQ & H)"; iDestruct "H" as (Φ) "[#HeqP Hf]". iIntros (?) "(#Hinv & HQ & H)"; iDestruct "H" as (Φ) "[#HeqP Hf]". iInv N as (b') "(>Hγ & #HγQ & _)" "Hclose". iInv N as (b') "(>Hγ & #HγQ & _)" "Hclose". ... @@ -143,7 +143,7 @@ Qed. ... @@ -143,7 +143,7 @@ Qed. Lemma box_empty f P Q γ : Lemma box_empty f P Q γ : f !! γ = Some true → f !! γ = Some true → slice N γ Q ★ ▷ box N f P ={N}=> ▷ Q ★ ▷ box N (<[γ:=false]> f) P. slice N γ Q ★ ▷ box N f P ={N}=★ ▷ Q ★ ▷ box N (<[γ:=false]> f) P. Proof. Proof. iIntros (?) "[#Hinv H]"; iDestruct "H" as (Φ) "[#HeqP Hf]". iIntros (?) "[#Hinv H]"; iDestruct "H" as (Φ) "[#HeqP Hf]". iInv N as (b) "(>Hγ & #HγQ & HQ)" "Hclose". iInv N as (b) "(>Hγ & #HγQ & HQ)" "Hclose". ... @@ -160,7 +160,7 @@ Proof. ... @@ -160,7 +160,7 @@ Proof. iFrame; eauto. iFrame; eauto. Qed. Qed. Lemma box_fill_all f P Q : box N f P ★ ▷ P ={N}=> box N (const true <\$> f) P. Lemma box_fill_all f P Q : box N f P ★ ▷ P ={N}=★ box N (const true <\$> f) P. Proof. Proof. iIntros "[H HP]"; iDestruct "H" as (Φ) "[#HeqP Hf]". iIntros "[H HP]"; iDestruct "H" as (Φ) "[#HeqP Hf]". iExists Φ; iSplitR; first by rewrite big_sepM_fmap. iExists Φ; iSplitR; first by rewrite big_sepM_fmap. ... @@ -176,7 +176,7 @@ Qed. ... @@ -176,7 +176,7 @@ Qed. Lemma box_empty_all f P Q : Lemma box_empty_all f P Q : map_Forall (λ _, (true =)) f → map_Forall (λ _, (true =)) f → box N f P ={N}=> ▷ P ★ box N (const false <\$> f) P. box N f P ={N}=★ ▷ P ★ box N (const false <\$> f) P. Proof. Proof.