Commit 0ca74ec7 by Robbert Krebbers

### Remove useless scopes. Thanks to !674.

parent 0ca7041d
 ... ... @@ -10,7 +10,7 @@ Section upred. Context {M : ucmra}. (* Force implicit argument M *) Notation "P ⊢ Q" := (bi_entails (PROP:=uPredI M) P%I Q%I). Notation "P ⊢ Q" := (bi_entails (PROP:=uPredI M) P Q). Notation "P ⊣⊢ Q" := (equiv (A:=uPredI M) P%I Q%I). Lemma prod_validI {A B : cmra} (x : A * B) : ✓ x ⊣⊢ ✓ x.1 ∧ ✓ x.2. ... ... @@ -146,7 +146,7 @@ Section view. Qed. Lemma view_both_dfrac_validI_2 (relI : uPred M) dq a b : (∀ n (x : M), relI n x → rel n a b) → ⌜✓dq⌝%Qp ∧ relI ⊢ ✓ (●V{dq} a ⋅ ◯V b : view rel). ⌜✓dq⌝ ∧ relI ⊢ ✓ (●V{dq} a ⋅ ◯V b : view rel). Proof. intros Hrel. uPred.unseal. split=> n x _ /=. rewrite /uPred_holds /= view_both_dfrac_validN. by move=> [? /Hrel]. ... ...
 ... ... @@ -8,7 +8,7 @@ Set Default Proof Using "Type*". (** This file contains an alternative version of basic updates, that is expression in terms of just the plain modality [■]. *) Definition bupd_alt `{BiPlainly PROP} (P : PROP) : PROP := (∀ R, (P -∗ ■ R) -∗ ■ R)%I. ∀ R, (P -∗ ■ R) -∗ ■ R. (** This definition is stated for any BI with a plain modality. The above definition is akin to the continuation monad, where one should think of [■ R] ... ...
 ... ... @@ -15,7 +15,7 @@ Implicit Types P Q : uPred M. Implicit Types A : Type. (* Force implicit argument M *) Notation "P ⊢ Q" := (bi_entails (PROP:=uPredI M) P%I Q%I). Notation "P ⊢ Q" := (bi_entails (PROP:=uPredI M) P Q). Notation "P ⊣⊢ Q" := (equiv (A:=uPredI M) P%I Q%I). (** Propers *) ... ... @@ -24,7 +24,7 @@ Global Instance cmra_valid_proper {A : cmra} : Proper ((≡) ==> (⊣⊢)) (@uPred_cmra_valid M A) := ne_proper _. (** Own and valid derived *) Lemma persistently_cmra_valid_1 {A : cmra} (a : A) : ✓ a ⊢ (✓ a : uPred M). Lemma persistently_cmra_valid_1 {A : cmra} (a : A) : ✓ a ⊢@{uPredI M} (✓ a). Proof. by rewrite {1}plainly_cmra_valid_1 plainly_elim_persistently. Qed. Lemma intuitionistically_ownM (a : M) : CoreId a → □ uPred_ownM a ⊣⊢ uPred_ownM a. Proof. ... ...
 ... ... @@ -292,7 +292,7 @@ Proof. - iMod (slice_delete_full with "Hslice1 Hbox") as (P1) "(HQ1 & Heq1 & Hbox)"; try done. iMod (slice_delete_full with "Hslice2 Hbox") as (P2) "(HQ2 & Heq2 & Hbox)"; first done. { by simplify_map_eq. } iMod (slice_insert_full _ _ _ _ (Q1 ∗ Q2)%I with "[\$HQ1 \$HQ2] Hbox") iMod (slice_insert_full _ _ _ _ (Q1 ∗ Q2) with "[\$HQ1 \$HQ2] Hbox") as (γ ?) "[#Hslice Hbox]"; first done. iExists γ. iIntros "{\$% \$#} !>". iNext. iApply (internal_eq_rewrite_contractive _ _ (box _ _) with "[Heq1 Heq2] Hbox"). ... ...
 ... ... @@ -53,9 +53,9 @@ Section definitions. Context `{!invG Σ, !gen_heapG L V Σ, gG: !inv_heapG L V Σ}. Definition inv_heap_inv_P : iProp Σ := (∃ h : gmap L (V * (V -d> PropO)), own (inv_heap_name gG) (● to_inv_heap h) ∗ [∗ map] l ↦ p ∈ h, ⌜p.2 p.1⌝ ∗ l ↦ p.1)%I. ∃ h : gmap L (V * (V -d> PropO)), own (inv_heap_name gG) (● to_inv_heap h) ∗ [∗ map] l ↦ p ∈ h, ⌜p.2 p.1⌝ ∗ l ↦ p.1. Definition inv_heap_inv : iProp Σ := inv inv_heapN inv_heap_inv_P. ... ...
 ... ... @@ -22,8 +22,8 @@ Section defs. own p (CoPset E, GSet ∅). Definition na_inv (p : na_inv_pool_name) (N : namespace) (P : iProp Σ) : iProp Σ := (∃ i, ⌜i ∈ (↑N:coPset)⌝ ∧ inv N (P ∗ own p (CoPset ∅, GSet {[i]}) ∨ na_own p {[i]}))%I. ∃ i, ⌜i ∈ (↑N:coPset)⌝ ∧ inv N (P ∗ own p (CoPset ∅, GSet {[i]}) ∨ na_own p {[i]}). End defs. Global Instance: Params (@na_inv) 3 := {}. ... ...
 ... ... @@ -43,8 +43,8 @@ Section definitions. map_Forall (λ p vs, vs = proph_list_resolves pvs p) R. Definition proph_map_interp pvs (ps : gset P) : iProp Σ := (∃ R, ⌜proph_resolves_in_list R pvs ∧ dom (gset _) R ⊆ ps⌝ ∗ ghost_map_auth (proph_map_name pG) 1 R)%I. ∃ R, ⌜proph_resolves_in_list R pvs ∧ dom (gset _) R ⊆ ps⌝ ∗ ghost_map_auth (proph_map_name pG) 1 R. Definition proph_def (p : P) (vs : list V) : iProp Σ := p ↪[proph_map_name pG] vs. ... ...
 ... ... @@ -35,7 +35,6 @@ Definition invariant_unfold {Σ} (P : iProp Σ) : later (iProp Σ) := Next P. Definition ownI `{!invG Σ} (i : positive) (P : iProp Σ) : iProp Σ := own invariant_name (gmap_view_frag i DfracDiscarded (invariant_unfold P)). Global Arguments ownI {_ _} _ _%I. Typeclasses Opaque ownI. Global Instance: Params (@invariant_unfold) 1 := {}. Global Instance: Params (@ownI) 3 := {}. ... ...
 ... ... @@ -718,7 +718,7 @@ Section sep_list2. Lemma big_sepL2_later_1 `{BiAffine PROP} Φ l1 l2 : (▷ [∗ list] k↦y1;y2 ∈ l1;l2, Φ k y1 y2) ⊢ ◇ [∗ list] k↦y1;y2 ∈ l1;l2, ▷ Φ k y1 y2. Proof. rewrite !big_sepL2_alt later_and big_sepL_later (timeless ⌜ _ ⌝%I). rewrite !big_sepL2_alt later_and big_sepL_later (timeless ⌜ _ ⌝). rewrite except_0_and. auto using and_mono, except_0_intro. Qed. ... ... @@ -1189,7 +1189,7 @@ Section map. □ (∀ k x, ⌜m !! k = Some x⌝ → Φ k x) ⊢ [∗ map] k↦x ∈ m, Φ k x. Proof. revert Φ. induction m as [|i x m ? IH] using map_ind=> Φ. { by rewrite (affine (□ _)%I) big_sepM_empty. } { by rewrite (affine (□ _)) big_sepM_empty. } rewrite big_sepM_insert // intuitionistically_sep_dup. f_equiv. - rewrite (forall_elim i) (forall_elim x) lookup_insert. by rewrite pure_True // True_impl intuitionistically_elim. ... ... @@ -1597,11 +1597,11 @@ Section map2. ⊣⊢ ([∗ map] k↦y1;y2 ∈ m1;m2, Φ k y1 y2) ∗ ([∗ map] k↦y1;y2 ∈ m1;m2, Ψ k y1 y2). Proof. rewrite big_sepM2_eq /big_sepM2_def. rewrite -{1}(and_idem ⌜∀ k : K, is_Some (m1 !! k) ↔ is_Some (m2 !! k)⌝%I). rewrite -and_assoc. rewrite -{1}(idemp bi_and ⌜∀ k : K, is_Some (m1 !! k) ↔ is_Some (m2 !! k)⌝%I). rewrite -assoc. rewrite !persistent_and_affinely_sep_l /=. rewrite -sep_assoc. apply sep_proper=>//. rewrite sep_assoc (sep_comm _ ( _)%I) -sep_assoc. rewrite -assoc. apply sep_proper=>//. rewrite assoc (comm _ _ ( _)%I) -assoc. apply sep_proper=>//. apply big_sepM_sep. Qed. ... ... @@ -1694,7 +1694,7 @@ Section map2. (▷ [∗ map] k↦x1;x2 ∈ m1;m2, Φ k x1 x2) ⊢ ◇ ([∗ map] k↦x1;x2 ∈ m1;m2, ▷ Φ k x1 x2). Proof. rewrite big_sepM2_eq /big_sepM2_def later_and (timeless ⌜_⌝%I). rewrite big_sepM2_eq /big_sepM2_def later_and (timeless ⌜_⌝). rewrite big_sepM_later except_0_and. auto using and_mono_r, except_0_intro. Qed. ... ... @@ -1702,7 +1702,7 @@ Section map2. ([∗ map] k↦x1;x2 ∈ m1;m2, ▷ Φ k x1 x2) ⊢ ▷ [∗ map] k↦x1;x2 ∈ m1;m2, Φ k x1 x2. Proof. rewrite big_sepM2_eq /big_sepM2_def later_and -(later_intro ⌜_⌝%I). rewrite big_sepM2_eq /big_sepM2_def later_and -(later_intro ⌜_⌝). apply and_mono_r. by rewrite big_opM_commute. Qed. ... ... @@ -1904,7 +1904,7 @@ Section gset. □ (∀ x, ⌜x ∈ X⌝ → Φ x) ⊢ [∗ set] x ∈ X, Φ x. Proof. revert Φ. induction X as [|x X ? IH] using set_ind_L=> Φ. { by rewrite (affine (□ _)%I) big_sepS_empty. } { by rewrite (affine (□ _)) big_sepS_empty. } rewrite intuitionistically_sep_dup big_sepS_insert //. f_equiv. - rewrite (forall_elim x) pure_True ?True_impl; last set_solver. by rewrite intuitionistically_elim. ... ... @@ -2100,7 +2100,7 @@ Section gmultiset. □ (∀ x, ⌜x ∈ X⌝ → Φ x) ⊢ [∗ mset] x ∈ X, Φ x. Proof. revert Φ. induction X as [|x X IH] using gmultiset_ind=> Φ. { by rewrite (affine (□ _)%I) big_sepMS_empty. } { by rewrite (affine (□ _)) big_sepMS_empty. } rewrite intuitionistically_sep_dup big_sepMS_disj_union. rewrite big_sepMS_singleton. f_equiv. - rewrite (forall_elim x) pure_True ?True_impl; last multiset_solver. ... ...
 ... ... @@ -2,13 +2,13 @@ From iris.algebra Require Import monoid. From iris.bi Require Export interface. From iris.prelude Require Import options. Definition bi_iff {PROP : bi} (P Q : PROP) : PROP := ((P → Q) ∧ (Q → P))%I. Definition bi_iff {PROP : bi} (P Q : PROP) : PROP := (P → Q) ∧ (Q → P). Global Arguments bi_iff {_} _%I _%I : simpl never. Global Instance: Params (@bi_iff) 1 := {}. Infix "↔" := bi_iff : bi_scope. Definition bi_wand_iff {PROP : bi} (P Q : PROP) : PROP := ((P -∗ Q) ∧ (Q -∗ P))%I. (P -∗ Q) ∧ (Q -∗ P). Global Arguments bi_wand_iff {_} _%I _%I : simpl never. Global Instance: Params (@bi_wand_iff) 1 := {}. Infix "∗-∗" := bi_wand_iff : bi_scope. ... ... @@ -19,7 +19,7 @@ Global Arguments persistent {_} _%I {_}. Global Hint Mode Persistent + ! : typeclass_instances. Global Instance: Params (@Persistent) 1 := {}. Definition bi_affinely {PROP : bi} (P : PROP) : PROP := (emp ∧ P)%I. Definition bi_affinely {PROP : bi} (P : PROP) : PROP := emp ∧ P. Global Arguments bi_affinely {_} _%I : simpl never. Global Instance: Params (@bi_affinely) 1 := {}. Typeclasses Opaque bi_affinely. ... ... @@ -38,7 +38,7 @@ Class BiPositive (PROP : bi) := bi_positive (P Q : PROP) : (P ∗ Q) ⊢ P ∗ Q. Global Hint Mode BiPositive ! : typeclass_instances. Definition bi_absorbingly {PROP : bi} (P : PROP) : PROP := (True ∗ P)%I. Definition bi_absorbingly {PROP : bi} (P : PROP) : PROP := True ∗ P. Global Arguments bi_absorbingly {_} _%I : simpl never. Global Instance: Params (@bi_absorbingly) 1 := {}. Typeclasses Opaque bi_absorbingly. ... ... @@ -88,13 +88,13 @@ Fixpoint bi_laterN {PROP : bi} (n : nat) (P : PROP) : PROP := match n with | O => P | S n' => ▷ ▷^n' P end%I end where "▷^ n P" := (bi_laterN n P) : bi_scope. Global Arguments bi_laterN {_} !_%nat_scope _%I. Global Instance: Params (@bi_laterN) 2 := {}. Notation "▷? p P" := (bi_laterN (Nat.b2n p) P) : bi_scope. Definition bi_except_0 {PROP : bi} (P : PROP) : PROP := (▷ False ∨ P)%I. Definition bi_except_0 {PROP : bi} (P : PROP) : PROP := ▷ False ∨ P. Global Arguments bi_except_0 {_} _%I : simpl never. Notation "◇ P" := (bi_except_0 P) : bi_scope. Global Instance: Params (@bi_except_0) 1 := {}. ... ... @@ -112,7 +112,7 @@ Global Instance: Params (@Timeless) 1 := {}. Definition bi_wandM {PROP : bi} (mP : option PROP) (Q : PROP) : PROP := match mP with | None => Q | Some P => (P -∗ Q)%I | Some P => P -∗ Q end. Global Arguments bi_wandM {_} !_%I _%I /. Notation "mP -∗? Q" := (bi_wandM mP Q) ... ...
 ... ... @@ -607,7 +607,7 @@ Lemma pure_wand_forall φ P `{!Absorbing P} : (⌜φ⌝ -∗ P) ⊣⊢ (∀ _ : Proof. apply (anti_symm _). - apply forall_intro=> Hφ. rewrite -(pure_intro φ emp%I) // emp_wand //. rewrite -(pure_intro φ emp) // emp_wand //. - apply wand_intro_l, wand_elim_l', pure_elim'=> Hφ. apply wand_intro_l. rewrite (forall_elim Hφ) comm. by apply absorbing. Qed. ... ... @@ -794,7 +794,7 @@ Section bi_affine. Context `{BiAffine PROP}. Global Instance bi_affine_absorbing P : Absorbing P | 0. Proof. by rewrite /Absorbing /bi_absorbingly (affine True%I) left_id. Qed. Proof. by rewrite /Absorbing /bi_absorbingly (affine True) left_id. Qed. Global Instance bi_affine_positive : BiPositive PROP. Proof. intros P Q. by rewrite !affine_affinely. Qed. ... ... @@ -929,7 +929,7 @@ Qed. Lemma persistently_and_sep_l_1 P Q : P ∧ Q ⊢ P ∗ Q. Proof. by rewrite -{1}(emp_sep Q%I) persistently_and_sep_assoc and_elim_l. by rewrite -{1}(emp_sep Q) persistently_and_sep_assoc and_elim_l. Qed. Lemma persistently_and_sep_r_1 P Q : P ∧ Q ⊢ P ∗ Q. Proof. by rewrite !(comm _ P) persistently_and_sep_l_1. Qed. ... ... @@ -937,7 +937,7 @@ Proof. by rewrite !(comm _ P) persistently_and_sep_l_1. Qed. Lemma persistently_and_sep P Q : (P ∧ Q) ⊢ (P ∗ Q). Proof. rewrite persistently_and. rewrite -{1}persistently_idemp -persistently_and -{1}(emp_sep Q%I). rewrite -{1}persistently_idemp -persistently_and -{1}(emp_sep Q). by rewrite persistently_and_sep_assoc (comm bi_and) persistently_and_emp_elim. Qed. ... ... @@ -990,7 +990,7 @@ Proof. intros; rewrite -persistently_and_sep_r_1; auto. Qed. Lemma persistently_impl_wand_2 P Q : (P -∗ Q) ⊢ (P → Q). Proof. apply persistently_intro', impl_intro_r. rewrite -{2}(emp_sep P%I) persistently_and_sep_assoc. rewrite -{2}(emp_sep P) persistently_and_sep_assoc. by rewrite (comm bi_and) persistently_and_emp_elim wand_elim_l. Qed. ... ...
 ... ... @@ -111,7 +111,7 @@ Lemma löb `{!BiLöb PROP} P : (▷ P → P) ⊢ P. Proof. apply entails_impl_True, löb_weak. apply impl_intro_r. rewrite -{2}(idemp (∧) (▷ P → P))%I. rewrite {2}(later_intro (▷ P → P))%I. rewrite {2}(later_intro (▷ P → P)). rewrite later_impl. rewrite assoc impl_elim_l. rewrite impl_elim_r. done. ... ... @@ -131,7 +131,7 @@ Proof. assert (Q ⊣⊢ (▷ Q → P)) as HQ by (exact: fixpoint_unfold). intros HP. rewrite -HP. assert (▷ Q ⊢ P) as HQP. { rewrite -HP. rewrite -(idemp (∧) (▷ Q))%I {2}(later_intro (▷ Q))%I. { rewrite -HP. rewrite -(idemp (∧) (▷ Q))%I {2}(later_intro (▷ Q)). by rewrite {1}HQ {1}later_impl impl_elim_l. } rewrite -HQP HQ -2!later_intro. apply (entails_impl_True _ P). done. ... ... @@ -139,15 +139,15 @@ Qed. Lemma löb_wand_intuitionistically `{!BiLöb PROP} P : □ (□ ▷ P -∗ P) ⊢ P. Proof. rewrite -{3}(intuitionistically_elim P) -(löb (□ P)%I). apply impl_intro_l. rewrite -{3}(intuitionistically_elim P) -(löb (□ P)). apply impl_intro_l. rewrite {1}intuitionistically_into_persistently_1 later_persistently. rewrite persistently_and_intuitionistically_sep_l. rewrite -{1}(intuitionistically_idemp (▷ P)%I) intuitionistically_sep_2. rewrite -{1}(intuitionistically_idemp (▷ P)) intuitionistically_sep_2. by rewrite wand_elim_r. Qed. Lemma löb_wand `{!BiLöb PROP} P : □ (▷ P -∗ P) ⊢ P. Proof. by rewrite -(intuitionistically_elim (▷ P)%I) löb_wand_intuitionistically. by rewrite -(intuitionistically_elim (▷ P)) löb_wand_intuitionistically. Qed. (** The proof of the right-to-left direction relies on the BI being affine. It ... ... @@ -322,7 +322,7 @@ Proof. by rewrite {1}(except_0_intro Q) except_0_sep. Qed. Lemma later_affinely_1 `{!Timeless (PROP:=PROP) emp} P : ▷ P ⊢ ◇ ▷ P. Proof. rewrite /bi_affinely later_and (timeless emp%I) except_0_and. rewrite /bi_affinely later_and (timeless emp) except_0_and. by apply and_mono, except_0_intro. Qed. ... ...
 ... ... @@ -21,9 +21,8 @@ Section definition. (** atomic_acc as the "introduction form" of atomic updates: An accessor that can be aborted back to [P]. *) Definition atomic_acc Eo Ei α P β Φ : PROP := (|={Eo, Ei}=> ∃.. x, α x ∗ ((α x ={Ei, Eo}=∗ P) ∧ (∀.. y, β x y ={Ei, Eo}=∗ Φ x y)) )%I. |={Eo, Ei}=> ∃.. x, α x ∗ ((α x ={Ei, Eo}=∗ P) ∧ (∀.. y, β x y ={Ei, Eo}=∗ Φ x y)). Lemma atomic_acc_wand Eo Ei α P1 P2 β Φ1 Φ2 : ((P1 -∗ P2) ∧ (∀.. x y, Φ1 x y -∗ Φ2 x y)) -∗ ... ...
 ... ... @@ -9,7 +9,7 @@ Import bi. Definition coreP `{!BiPlainly PROP} (P : PROP) : PROP := (* TODO: Looks like we want notation for affinely-plainly; that lets us avoid using conjunction/implication here. *) (∀ Q : PROP, ■ (Q -∗ Q) -∗ ■ (P -∗ Q) -∗ Q)%I. ∀ Q : PROP, ■ (Q -∗ Q) -∗ ■ (P -∗ Q) -∗ Q. Global Instance: Params (@coreP) 1 := {}. Typeclasses Opaque coreP. ... ...