From 8b46e26e67bd96c2014c73d00aacc59d2e4e9340 Mon Sep 17 00:00:00 2001 From: "Paolo G. Giarrusso" Date: Wed, 17 Mar 2021 00:00:16 +0100 Subject: [PATCH 1/5] Scopes for bi_car Robbert pointed out this should fix the scopes for derived_laws. --- iris/bi/interface.v | 1 + 1 file changed, 1 insertion(+) diff --git a/iris/bi/interface.v b/iris/bi/interface.v index 5447c68ed..70851cb0f 100644 --- a/iris/bi/interface.v +++ b/iris/bi/interface.v @@ -182,6 +182,7 @@ Structure bi := Bi { bi_bi_later_mixin : BiLaterMixin bi_entails bi_pure bi_or bi_impl bi_forall bi_exist bi_sep bi_persistently bi_later; }. +Bind Scope bi_scope with bi_car. Coercion bi_ofeO (PROP : bi) : ofe := Ofe PROP (bi_ofe_mixin PROP). Canonical Structure bi_ofeO. -- GitLab From 9b2bc83c044880f4818c1f0e2d0c4cbbec31c4d9 Mon Sep 17 00:00:00 2001 From: "Paolo G. Giarrusso" Date: Wed, 17 Mar 2021 00:15:17 +0100 Subject: [PATCH 2/5] (Controversial) remove some %I which are now implied --- iris/base_logic/algebra.v | 2 +- iris/base_logic/bi.v | 2 +- iris/base_logic/derived.v | 2 +- iris/bi/interface.v | 20 ++++++++++---------- 4 files changed, 13 insertions(+), 13 deletions(-) diff --git a/iris/base_logic/algebra.v b/iris/base_logic/algebra.v index ab1bea0d8..a86c5aeda 100644 --- a/iris/base_logic/algebra.v +++ b/iris/base_logic/algebra.v @@ -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. diff --git a/iris/base_logic/bi.v b/iris/base_logic/bi.v index 77be327e6..a16db04da 100644 --- a/iris/base_logic/bi.v +++ b/iris/base_logic/bi.v @@ -176,7 +176,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). Global Instance ownM_ne : NonExpansive (@uPred_ownM M) := uPred_primitive.ownM_ne. diff --git a/iris/base_logic/derived.v b/iris/base_logic/derived.v index b81a3b475..0dbfae8d2 100644 --- a/iris/base_logic/derived.v +++ b/iris/base_logic/derived.v @@ -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 *) diff --git a/iris/bi/interface.v b/iris/bi/interface.v index 70851cb0f..b7cd208de 100644 --- a/iris/bi/interface.v +++ b/iris/bi/interface.v @@ -205,25 +205,25 @@ Global Instance: Params (@bi_later) 1 := {}. Global Arguments bi_car : simpl never. Global Arguments bi_dist : simpl never. Global Arguments bi_equiv : simpl never. -Global Arguments bi_entails {PROP} _%I _%I : simpl never, rename. +Global Arguments bi_entails {PROP} _ _ : simpl never, rename. Global Arguments bi_emp {PROP} : simpl never, rename. Global Arguments bi_pure {PROP} _%stdpp : simpl never, rename. -Global Arguments bi_and {PROP} _%I _%I : simpl never, rename. -Global Arguments bi_or {PROP} _%I _%I : simpl never, rename. -Global Arguments bi_impl {PROP} _%I _%I : simpl never, rename. +Global Arguments bi_and {PROP} _ _ : simpl never, rename. +Global Arguments bi_or {PROP} _ _ : simpl never, rename. +Global Arguments bi_impl {PROP} _ _ : simpl never, rename. Global Arguments bi_forall {PROP _} _%I : simpl never, rename. Global Arguments bi_exist {PROP _} _%I : simpl never, rename. -Global Arguments bi_sep {PROP} _%I _%I : simpl never, rename. -Global Arguments bi_wand {PROP} _%I _%I : simpl never, rename. -Global Arguments bi_persistently {PROP} _%I : simpl never, rename. -Global Arguments bi_later {PROP} _%I : simpl never, rename. +Global Arguments bi_sep {PROP} _ _ : simpl never, rename. +Global Arguments bi_wand {PROP} _ _ : simpl never, rename. +Global Arguments bi_persistently {PROP} _ : simpl never, rename. +Global Arguments bi_later {PROP} _ : simpl never, rename. Global Hint Extern 0 (bi_entails _ _) => reflexivity : core. Global Instance bi_rewrite_relation (PROP : bi) : RewriteRelation (@bi_entails PROP) := {}. Global Instance bi_inhabited {PROP : bi} : Inhabited PROP := populate (bi_pure True). -Notation "P ⊢ Q" := (bi_entails P%I Q%I) : stdpp_scope. -Notation "P '⊢@{' PROP } Q" := (bi_entails (PROP:=PROP) P%I Q%I) (only parsing) : stdpp_scope. +Notation "P ⊢ Q" := (bi_entails P Q) : stdpp_scope. +Notation "P '⊢@{' PROP } Q" := (bi_entails (PROP:=PROP) P Q) (only parsing) : stdpp_scope. Notation "(⊢)" := bi_entails (only parsing) : stdpp_scope. Notation "'(⊢@{' PROP } )" := (bi_entails (PROP:=PROP)) (only parsing) : stdpp_scope. -- GitLab From 2dd7fd215c94a001a37502122723b611021600b1 Mon Sep 17 00:00:00 2001 From: "Paolo G. Giarrusso" Date: Wed, 17 Mar 2021 00:15:37 +0100 Subject: [PATCH 3/5] Remove %I which was implied before --- iris/base_logic/upred.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/iris/base_logic/upred.v b/iris/base_logic/upred.v index a369af8d7..d2b54213a 100644 --- a/iris/base_logic/upred.v +++ b/iris/base_logic/upred.v @@ -115,7 +115,7 @@ Record uPred (M : ucmra) : Type := UPred { this way. *) Local Coercion uPred_holds : uPred >-> Funclass. Bind Scope bi_scope with uPred. -Global Arguments uPred_holds {_} _%I _ _ : simpl never. +Global Arguments uPred_holds {_} _ _ _ : simpl never. Add Printing Constructor uPred. Global Instance: Params (@uPred_holds) 3 := {}. -- GitLab From 6747de6ec24368f381bdfc48f889b30a9781fda7 Mon Sep 17 00:00:00 2001 From: "Paolo G. Giarrusso" Date: Wed, 17 Mar 2021 00:15:50 +0100 Subject: [PATCH 4/5] Add non-implied %I for big ops --- iris/bi/big_op.v | 10 ++++++++-- 1 file changed, 8 insertions(+), 2 deletions(-) diff --git a/iris/bi/big_op.v b/iris/bi/big_op.v index b2c883411..376184753 100644 --- a/iris/bi/big_op.v +++ b/iris/bi/big_op.v @@ -6,6 +6,12 @@ From iris.prelude Require Import options. Import interface.bi derived_laws.bi derived_laws_later.bi. (** Notations for unary variants *) +(* Change the scope locally, to have it inherited globally by the notations. *) +Local Arguments big_opL {M} o {_ A} _%I !_ /. +Local Arguments big_opS {M} o {_ A _ _} _%I _. +Local Arguments big_opM {M} o {_ K _ _ A} _%I _. +Local Arguments big_opMS {M} o {_ A _ _} _%I _. + Notation "'[∗' 'list]' k ↦ x ∈ l , P" := (big_opL bi_sep (λ k x, P) l) : bi_scope. Notation "'[∗' 'list]' x ∈ l , P" := @@ -44,7 +50,7 @@ Fixpoint big_sepL2 {PROP : bi} {A B} | _, _ => False end%I. Global Instance: Params (@big_sepL2) 3 := {}. -Global Arguments big_sepL2 {PROP A B} _ !_ !_ /. +Global Arguments big_sepL2 {PROP} {A B}%type_scope _%I (!_ !_)%list_scope /. Typeclasses Opaque big_sepL2. Notation "'[∗' 'list]' k ↦ x1 ; x2 ∈ l1 ; l2 , P" := (big_sepL2 (λ k x1 x2, P) l1 l2) : bi_scope. @@ -57,7 +63,7 @@ Definition big_sepM2_def {PROP : bi} `{Countable K} {A B} [∗ map] k ↦ xy ∈ map_zip m1 m2, Φ k xy.1 xy.2)%I. Definition big_sepM2_aux : seal (@big_sepM2_def). Proof. by eexists. Qed. Definition big_sepM2 := big_sepM2_aux.(unseal). -Global Arguments big_sepM2 {PROP K _ _ A B} _ _ _. +Global Arguments big_sepM2 {PROP} {K}%type_scope {_ _} {A B}%type_scope _%I _ _. Definition big_sepM2_eq : @big_sepM2 = _ := big_sepM2_aux.(seal_eq). Global Instance: Params (@big_sepM2) 6 := {}. Notation "'[∗' 'map]' k ↦ x1 ; x2 ∈ m1 ; m2 , P" := -- GitLab From 4706753719c23a2cddcb51bbd16fe1f27b326d64 Mon Sep 17 00:00:00 2001 From: "Paolo G. Giarrusso" Date: Wed, 17 Mar 2021 10:18:37 +0100 Subject: [PATCH 5/5] WIP drop implied %E --- iris/bi/weakestpre.v | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/iris/bi/weakestpre.v b/iris/bi/weakestpre.v index 3bcc9cfe9..b2d99f698 100644 --- a/iris/bi/weakestpre.v +++ b/iris/bi/weakestpre.v @@ -41,15 +41,15 @@ Global Instance: Params (@twp) 7 := {}. (** Notations for partial weakest preconditions *) (** Notations without binder -- only parsing because they overlap with the notations with binder. *) -Notation "'WP' e @ s ; E {{ Φ } }" := (wp s E e%E Φ) +Notation "'WP' e @ s ; E {{ Φ } }" := (wp s E e Φ) (at level 20, e, Φ at level 200, only parsing) : bi_scope. -Notation "'WP' e @ E {{ Φ } }" := (wp NotStuck E e%E Φ) +Notation "'WP' e @ E {{ Φ } }" := (wp NotStuck E e Φ) (at level 20, e, Φ at level 200, only parsing) : bi_scope. -Notation "'WP' e @ E ? {{ Φ } }" := (wp MaybeStuck E e%E Φ) +Notation "'WP' e @ E ? {{ Φ } }" := (wp MaybeStuck E e Φ) (at level 20, e, Φ at level 200, only parsing) : bi_scope. -Notation "'WP' e {{ Φ } }" := (wp NotStuck ⊤ e%E Φ) +Notation "'WP' e {{ Φ } }" := (wp NotStuck ⊤ e Φ) (at level 20, e, Φ at level 200, only parsing) : bi_scope. -Notation "'WP' e ? {{ Φ } }" := (wp MaybeStuck ⊤ e%E Φ) +Notation "'WP' e ? {{ Φ } }" := (wp MaybeStuck ⊤ e Φ) (at level 20, e, Φ at level 200, only parsing) : bi_scope. (** Notations with binder. The indentation for the inner format block is chosen -- GitLab