Commit 4a1a97b5 by Ralf Jung

### fix scopes for big-ops

parent 730f24ec
 ... ... @@ -7,29 +7,29 @@ Import interface.bi derived_laws.bi derived_laws_later.bi. (** Notations for unary variants *) Notation "'[∗' 'list]' k ↦ x ∈ l , P" := (big_opL bi_sep (λ k x, P) l) : bi_scope. (big_opL bi_sep (λ k x, P%I) l) : bi_scope. Notation "'[∗' 'list]' x ∈ l , P" := (big_opL bi_sep (λ _ x, P) l) : bi_scope. Notation "'[∗]' Ps" := (big_opL bi_sep (λ _ x, x) Ps) : bi_scope. (big_opL bi_sep (λ _ x, P%I) l) : bi_scope. Notation "'[∗]' Ps" := (big_opL bi_sep (λ _ x, x) Ps%I) : bi_scope. Notation "'[∧' 'list]' k ↦ x ∈ l , P" := (big_opL bi_and (λ k x, P) l) : bi_scope. (big_opL bi_and (λ k x, P%I) l) : bi_scope. Notation "'[∧' 'list]' x ∈ l , P" := (big_opL bi_and (λ _ x, P) l) : bi_scope. Notation "'[∧]' Ps" := (big_opL bi_and (λ _ x, x) Ps) : bi_scope. (big_opL bi_and (λ _ x, P%I) l) : bi_scope. Notation "'[∧]' Ps" := (big_opL bi_and (λ _ x, x) Ps%I) : bi_scope. Notation "'[∨' 'list]' k ↦ x ∈ l , P" := (big_opL bi_or (λ k x, P) l) : bi_scope. (big_opL bi_or (λ k x, P%I) l) : bi_scope. Notation "'[∨' 'list]' x ∈ l , P" := (big_opL bi_or (λ _ x, P) l) : bi_scope. Notation "'[∨]' Ps" := (big_opL bi_or (λ _ x, x) Ps) : bi_scope. (big_opL bi_or (λ _ x, P%I) l) : bi_scope. Notation "'[∨]' Ps" := (big_opL bi_or (λ _ x, x) Ps%I) : bi_scope. Notation "'[∗' 'map]' k ↦ x ∈ m , P" := (big_opM bi_sep (λ k x, P) m) : bi_scope. Notation "'[∗' 'map]' x ∈ m , P" := (big_opM bi_sep (λ _ x, P) m) : bi_scope. Notation "'[∗' 'map]' k ↦ x ∈ m , P" := (big_opM bi_sep (λ k x, P%I) m) : bi_scope. Notation "'[∗' 'map]' x ∈ m , P" := (big_opM bi_sep (λ _ x, P%I) m) : bi_scope. Notation "'[∗' 'set]' x ∈ X , P" := (big_opS bi_sep (λ x, P) X) : bi_scope. Notation "'[∗' 'set]' x ∈ X , P" := (big_opS bi_sep (λ x, P%I) X) : bi_scope. Notation "'[∗' 'mset]' x ∈ X , P" := (big_opMS bi_sep (λ x, P) X) : bi_scope. Notation "'[∗' 'mset]' x ∈ X , P" := (big_opMS bi_sep (λ x, P%I) X) : bi_scope. (** Definitions and notations for binary variants *) (** A version of the separating big operator that ranges over two lists. This ... ... @@ -47,9 +47,9 @@ Global Instance: Params (@big_sepL2) 3 := {}. Global Arguments big_sepL2 {PROP A B} _ !_ !_ /. Typeclasses Opaque big_sepL2. Notation "'[∗' 'list]' k ↦ x1 ; x2 ∈ l1 ; l2 , P" := (big_sepL2 (λ k x1 x2, P) l1 l2) : bi_scope. (big_sepL2 (λ k x1 x2, P%I) l1 l2) : bi_scope. Notation "'[∗' 'list]' x1 ; x2 ∈ l1 ; l2 , P" := (big_sepL2 (λ _ x1 x2, P) l1 l2) : bi_scope. (big_sepL2 (λ _ x1 x2, P%I) l1 l2) : bi_scope. Definition big_sepM2_def {PROP : bi} `{Countable K} {A B} (Φ : K → A → B → PROP) (m1 : gmap K A) (m2 : gmap K B) : PROP := ... ... @@ -61,9 +61,9 @@ Global Arguments big_sepM2 {PROP K _ _ A B} _ _ _. 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" := (big_sepM2 (λ k x1 x2, P) m1 m2) : bi_scope. (big_sepM2 (λ k x1 x2, P%I) m1 m2) : bi_scope. Notation "'[∗' 'map]' x1 ; x2 ∈ m1 ; m2 , P" := (big_sepM2 (λ _ x1 x2, P) m1 m2) : bi_scope. (big_sepM2 (λ _ x1 x2, P%I) m1 m2) : bi_scope. (** * Properties *) Section big_op. ... ...
 ... ... @@ -249,9 +249,9 @@ Infix "∗" := bi_sep : bi_scope. Notation "(∗)" := bi_sep (only parsing) : bi_scope. Notation "P -∗ Q" := (bi_wand P Q) : bi_scope. Notation "∀ x .. y , P" := (bi_forall (λ x, .. (bi_forall (λ y, P)) ..)%I) : bi_scope. (bi_forall (λ x, .. (bi_forall (λ y, P%I)) ..)) : bi_scope. Notation "∃ x .. y , P" := (bi_exist (λ x, .. (bi_exist (λ y, P)) ..)%I) : bi_scope. (bi_exist (λ x, .. (bi_exist (λ y, P%I)) ..)) : bi_scope. Notation "'' P" := (bi_persistently P) : bi_scope. Notation "▷ P" := (bi_later P) : bi_scope. ... ...
 ... ... @@ -15,6 +15,16 @@ Section base_logic_tests. Definition use_plainly_uPred (n : nat) : uPred M := ■ |==> ∃ m : nat , ⌜ n = 2 ⌝. (* Test scopes inside big-ops *) Definition big_op_scope_1 (xs : list nat) : uPred M := [∗ list] _ ↦ x ∈ xs, True. Definition big_op_scope_2 (xs : list nat) : uPred M := [∗ list] x; y ∈ xs; xs, True. Definition big_op_scope_3 (m : gmap nat nat) : uPred M := [∗ map] _ ↦ x ∈ m, True. Definition big_op_scope_4 (m : gmap nat nat) : uPred M := [∗ map] x; y ∈ m; m, True. Lemma test_random_stuff (P1 P2 P3 : nat → uPred M) : ⊢ ∀ (x y : nat) a b, x ≡ y → ... ...
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!