Commit 1a77ae7e authored by Robbert Krebbers's avatar Robbert Krebbers

Disambiguate Haskell-style notations for partially operators.

For example, change `(!! i)` into `(.!! x)` so that `!!` can also be used as
a prefix, as done in VST for example.

This closes issue #42.

I have used the `sed` script below. This script took care of nearly all uses
apart from a few occurrences where a space was missing, e.g. `(,foo)`. In
this case, `coqc` will just fail, allowing one to patch up things manually.

The script is slightly too eager on Iris developments, where it also replaces
`($ ...)` introduction patterns. When porting Iris developments you thus may
want to remove the line for `$`.

```
sed '
s/(= /(.= /g;
s/ =)/ =.)/g;
s/(≠ /(.≠ /g;
s/ ≠)/ ≠.)/g;
s/(≡ /(.≡ /g;
s/ ≡)/ ≡.)/g;
s/(≢ /(.≢ /g;
s/ ≢)/ ≢.)/g;
s/(∧ /(.∧ /g;
s/ ∧)/ ∧.)/g;
s/(∨ /(.∨ /g;
s/ ∨)/ ∨.)/g;
s/( /(. /g;
s/ )/ .)/g;
s/(→ /(.→ /g;
s/ →)/ →.)/g;
s/($ /(.$ /g;
s/(∘ /(.∘ /g;
s/ ∘)/ ∘.)/g;
s/(, /(., /g;
s/ ,)/ ,.)/g;
s/(∘ /(.∘ /g;
s/ ∘)/ ∘.)/g;
s/(∪ /(.∪ /g;
s/ ∪)/ ∪.)/g;
s/(⊎ /(.⊎ /g;
s/ ⊎)/ ⊎.)/g;
s/(∩ /(.∩ /g;
s/ ∩)/ ∩.)/g;
s/(∖ /(.∖ /g;
s/ ∖)/ ∖.)/g;
s/(⊆ /(.⊆ /g;
s/ ⊆)/ ⊆.)/g;
s/(⊈ /(.⊈ /g;
s/ ⊈)/ ⊈.)/g;
s/(⊂ /(.⊂ /g;
s/ ⊂)/ ⊂.)/g;
s/(⊄ /(.⊄ /g;
s/ ⊄)/ ⊄.)/g;
s/(∈ /(.∈ /g;
s/ ∈)/ ∈.)/g;
s/(∉ /(.∉ /g;
s/ ∉)/ ∉.)/g;
s/(≫= /(.≫= /g;
s/ ≫=)/ ≫=.)/g;
s/(!! /(.!! /g;
s/ !!)/ !!.)/g;
s/(⊑ /(.⊑ /g;
s/ ⊑)/ ⊑.)/g;
s/(⊓ /(.⊓ /g;
s/ ⊓)/ ⊓.)/g;
s/(⊔ /(.⊔ /g;
s/ ⊔)/ ⊔.)/g;
s/(:: /(.:: /g;
s/ ::)/ ::.)/g;
s/(++ /(.++ /g;
s/ ++)/ ++.)/g;
s/(≡ₚ /(.≡ₚ /g;
s/ ≡ₚ)/ ≡ₚ.)/g;
s/(≢ₚ /(.≢ₚ /g;
s/ ≢ₚ)/ ≢ₚ.)/g;
s/(::: /(.::: /g;
s/ :::)/ :::.)/g;
s/(+++ /(.+++ /g;
s/ +++)/ +++.)/g;
' -i $(find -name "*.v")
```
parent c579b46c
...@@ -167,11 +167,11 @@ Notation "'False'" := False (format "False") : type_scope. ...@@ -167,11 +167,11 @@ Notation "'False'" := False (format "False") : type_scope.
(** * Equality *) (** * Equality *)
(** Introduce some Haskell style like notations. *) (** Introduce some Haskell style like notations. *)
Notation "(=)" := eq (only parsing) : stdpp_scope. Notation "(=)" := eq (only parsing) : stdpp_scope.
Notation "( x =)" := (eq x) (only parsing) : stdpp_scope. Notation "( x =.)" := (eq x) (only parsing) : stdpp_scope.
Notation "(= x )" := (λ y, eq y x) (only parsing) : stdpp_scope. Notation "(.= x )" := (λ y, eq y x) (only parsing) : stdpp_scope.
Notation "(≠)" := (λ x y, x y) (only parsing) : stdpp_scope. Notation "(≠)" := (λ x y, x y) (only parsing) : stdpp_scope.
Notation "( x ≠)" := (λ y, x y) (only parsing) : stdpp_scope. Notation "( x ≠.)" := (λ y, x y) (only parsing) : stdpp_scope.
Notation "(≠ x )" := (λ y, y x) (only parsing) : stdpp_scope. Notation "(.≠ x )" := (λ y, y x) (only parsing) : stdpp_scope.
Infix "=@{ A }" := (@eq A) Infix "=@{ A }" := (@eq A)
(at level 70, only parsing, no associativity) : stdpp_scope. (at level 70, only parsing, no associativity) : stdpp_scope.
...@@ -199,12 +199,12 @@ Infix "≡@{ A }" := (@equiv A _) ...@@ -199,12 +199,12 @@ Infix "≡@{ A }" := (@equiv A _)
(at level 70, only parsing, no associativity) : stdpp_scope. (at level 70, only parsing, no associativity) : stdpp_scope.
Notation "(≡)" := equiv (only parsing) : stdpp_scope. Notation "(≡)" := equiv (only parsing) : stdpp_scope.
Notation "( X ≡)" := (equiv X) (only parsing) : stdpp_scope. Notation "( X ≡.)" := (equiv X) (only parsing) : stdpp_scope.
Notation "(≡ X )" := (λ Y, Y X) (only parsing) : stdpp_scope. Notation "(.≡ X )" := (λ Y, Y X) (only parsing) : stdpp_scope.
Notation "(≢)" := (λ X Y, ¬X Y) (only parsing) : stdpp_scope. Notation "(≢)" := (λ X Y, ¬X Y) (only parsing) : stdpp_scope.
Notation "X ≢ Y":= (¬X Y) (at level 70, no associativity) : stdpp_scope. Notation "X ≢ Y":= (¬X Y) (at level 70, no associativity) : stdpp_scope.
Notation "( X ≢)" := (λ Y, X Y) (only parsing) : stdpp_scope. Notation "( X ≢.)" := (λ Y, X Y) (only parsing) : stdpp_scope.
Notation "(≢ X )" := (λ Y, Y X) (only parsing) : stdpp_scope. Notation "(.≢ X )" := (λ Y, Y X) (only parsing) : stdpp_scope.
Notation "(≡@{ A } )" := (@equiv A _) (only parsing) : stdpp_scope. Notation "(≡@{ A } )" := (@equiv A _) (only parsing) : stdpp_scope.
Notation "(≢@{ A } )" := (λ X Y, ¬X @{A} Y) (only parsing) : stdpp_scope. Notation "(≢@{ A } )" := (λ X Y, ¬X @{A} Y) (only parsing) : stdpp_scope.
...@@ -295,8 +295,8 @@ Hint Mode ProofIrrel ! : typeclass_instances. ...@@ -295,8 +295,8 @@ Hint Mode ProofIrrel ! : typeclass_instances.
(** ** Common properties *) (** ** Common properties *)
(** These operational type classes allow us to refer to common mathematical (** These operational type classes allow us to refer to common mathematical
properties in a generic way. For example, for injectivity of [(k ++)] it properties in a generic way. For example, for injectivity of [(k ++.)] it
allows us to write [inj (k ++)] instead of [app_inv_head k]. *) allows us to write [inj (k ++.)] instead of [app_inv_head k]. *)
Class Inj {A B} (R : relation A) (S : relation B) (f : A B) : Prop := Class Inj {A B} (R : relation A) (S : relation B) (f : A B) : Prop :=
inj x y : S (f x) (f y) R x y. inj x y : S (f x) (f y) R x y.
Class Inj2 {A B C} (R1 : relation A) (R2 : relation B) Class Inj2 {A B C} (R1 : relation A) (R2 : relation B)
...@@ -414,16 +414,16 @@ Class TotalOrder {A} (R : relation A) : Prop := { ...@@ -414,16 +414,16 @@ Class TotalOrder {A} (R : relation A) : Prop := {
(** * Logic *) (** * Logic *)
Notation "(∧)" := and (only parsing) : stdpp_scope. Notation "(∧)" := and (only parsing) : stdpp_scope.
Notation "( A ∧)" := (and A) (only parsing) : stdpp_scope. Notation "( A ∧.)" := (and A) (only parsing) : stdpp_scope.
Notation "(∧ B )" := (λ A, A B) (only parsing) : stdpp_scope. Notation "(.∧ B )" := (λ A, A B) (only parsing) : stdpp_scope.
Notation "(∨)" := or (only parsing) : stdpp_scope. Notation "(∨)" := or (only parsing) : stdpp_scope.
Notation "( A ∨)" := (or A) (only parsing) : stdpp_scope. Notation "( A ∨.)" := (or A) (only parsing) : stdpp_scope.
Notation "(∨ B )" := (λ A, A B) (only parsing) : stdpp_scope. Notation "(.∨ B )" := (λ A, A B) (only parsing) : stdpp_scope.
Notation "(↔)" := iff (only parsing) : stdpp_scope. Notation "(↔)" := iff (only parsing) : stdpp_scope.
Notation "( A ↔)" := (iff A) (only parsing) : stdpp_scope. Notation "( A ↔.)" := (iff A) (only parsing) : stdpp_scope.
Notation "(↔ B )" := (λ A, A B) (only parsing) : stdpp_scope. Notation "(.↔ B )" := (λ A, A B) (only parsing) : stdpp_scope.
Hint Extern 0 (_ _) => reflexivity : core. Hint Extern 0 (_ _) => reflexivity : core.
Hint Extern 0 (_ _) => symmetry; assumption : core. Hint Extern 0 (_ _) => symmetry; assumption : core.
...@@ -488,18 +488,18 @@ Proof. unfold impl. red; intuition. Qed. ...@@ -488,18 +488,18 @@ Proof. unfold impl. red; intuition. Qed.
(** * Common data types *) (** * Common data types *)
(** ** Functions *) (** ** Functions *)
Notation "(→)" := (λ A B, A B) (only parsing) : stdpp_scope. Notation "(→)" := (λ A B, A B) (only parsing) : stdpp_scope.
Notation "( A →)" := (λ B, A B) (only parsing) : stdpp_scope. Notation "( A →.)" := (λ B, A B) (only parsing) : stdpp_scope.
Notation "(→ B )" := (λ A, A B) (only parsing) : stdpp_scope. Notation "(.→ B )" := (λ A, A B) (only parsing) : stdpp_scope.
Notation "t $ r" := (t r) Notation "t $ r" := (t r)
(at level 65, right associativity, only parsing) : stdpp_scope. (at level 65, right associativity, only parsing) : stdpp_scope.
Notation "($)" := (λ f x, f x) (only parsing) : stdpp_scope. Notation "($)" := (λ f x, f x) (only parsing) : stdpp_scope.
Notation "($ x )" := (λ f, f x) (only parsing) : stdpp_scope. Notation "(.$ x )" := (λ f, f x) (only parsing) : stdpp_scope.
Infix "∘" := compose : stdpp_scope. Infix "∘" := compose : stdpp_scope.
Notation "(∘)" := compose (only parsing) : stdpp_scope. Notation "(∘)" := compose (only parsing) : stdpp_scope.
Notation "( f ∘)" := (compose f) (only parsing) : stdpp_scope. Notation "( f ∘.)" := (compose f) (only parsing) : stdpp_scope.
Notation "(∘ f )" := (λ g, compose g f) (only parsing) : stdpp_scope. Notation "(.∘ f )" := (λ g, compose g f) (only parsing) : stdpp_scope.
Instance impl_inhabited {A} `{Inhabited B} : Inhabited (A B) := Instance impl_inhabited {A} `{Inhabited B} : Inhabited (A B) :=
populate (λ _, inhabitant). populate (λ _, inhabitant).
...@@ -599,8 +599,8 @@ Instance Empty_set_leibniz : LeibnizEquiv Empty_set. ...@@ -599,8 +599,8 @@ Instance Empty_set_leibniz : LeibnizEquiv Empty_set.
Proof. intros [] []; reflexivity. Qed. Proof. intros [] []; reflexivity. Qed.
(** ** Products *) (** ** Products *)
Notation "( x ,)" := (pair x) (only parsing) : stdpp_scope. Notation "( x ,.)" := (pair x) (only parsing) : stdpp_scope.
Notation "(, y )" := (λ x, (x,y)) (only parsing) : stdpp_scope. Notation "(., y )" := (λ x, (x,y)) (only parsing) : stdpp_scope.
Notation "p .1" := (fst p) (at level 2, left associativity, format "p .1"). Notation "p .1" := (fst p) (at level 2, left associativity, format "p .1").
Notation "p .2" := (snd p) (at level 2, left associativity, format "p .2"). Notation "p .2" := (snd p) (at level 2, left associativity, format "p .2").
...@@ -786,8 +786,8 @@ Hint Mode Union ! : typeclass_instances. ...@@ -786,8 +786,8 @@ Hint Mode Union ! : typeclass_instances.
Instance: Params (@union) 2 := {}. Instance: Params (@union) 2 := {}.
Infix "∪" := union (at level 50, left associativity) : stdpp_scope. Infix "∪" := union (at level 50, left associativity) : stdpp_scope.
Notation "(∪)" := union (only parsing) : stdpp_scope. Notation "(∪)" := union (only parsing) : stdpp_scope.
Notation "( x ∪)" := (union x) (only parsing) : stdpp_scope. Notation "( x ∪.)" := (union x) (only parsing) : stdpp_scope.
Notation "(∪ x )" := (λ y, union y x) (only parsing) : stdpp_scope. Notation "(.∪ x )" := (λ y, union y x) (only parsing) : stdpp_scope.
Infix "∪*" := (zip_with ()) (at level 50, left associativity) : stdpp_scope. Infix "∪*" := (zip_with ()) (at level 50, left associativity) : stdpp_scope.
Notation "(∪*)" := (zip_with ()) (only parsing) : stdpp_scope. Notation "(∪*)" := (zip_with ()) (only parsing) : stdpp_scope.
Infix "∪**" := (zip_with (zip_with ())) Infix "∪**" := (zip_with (zip_with ()))
...@@ -804,24 +804,24 @@ Hint Mode DisjUnion ! : typeclass_instances. ...@@ -804,24 +804,24 @@ Hint Mode DisjUnion ! : typeclass_instances.
Instance: Params (@disj_union) 2 := {}. Instance: Params (@disj_union) 2 := {}.
Infix "⊎" := disj_union (at level 50, left associativity) : stdpp_scope. Infix "⊎" := disj_union (at level 50, left associativity) : stdpp_scope.
Notation "(⊎)" := disj_union (only parsing) : stdpp_scope. Notation "(⊎)" := disj_union (only parsing) : stdpp_scope.
Notation "( x ⊎)" := (disj_union x) (only parsing) : stdpp_scope. Notation "( x ⊎.)" := (disj_union x) (only parsing) : stdpp_scope.
Notation "(⊎ x )" := (λ y, disj_union y x) (only parsing) : stdpp_scope. Notation "(.⊎ x )" := (λ y, disj_union y x) (only parsing) : stdpp_scope.
Class Intersection A := intersection: A A A. Class Intersection A := intersection: A A A.
Hint Mode Intersection ! : typeclass_instances. Hint Mode Intersection ! : typeclass_instances.
Instance: Params (@intersection) 2 := {}. Instance: Params (@intersection) 2 := {}.
Infix "∩" := intersection (at level 40) : stdpp_scope. Infix "∩" := intersection (at level 40) : stdpp_scope.
Notation "(∩)" := intersection (only parsing) : stdpp_scope. Notation "(∩)" := intersection (only parsing) : stdpp_scope.
Notation "( x ∩)" := (intersection x) (only parsing) : stdpp_scope. Notation "( x ∩.)" := (intersection x) (only parsing) : stdpp_scope.
Notation "(∩ x )" := (λ y, intersection y x) (only parsing) : stdpp_scope. Notation "(.∩ x )" := (λ y, intersection y x) (only parsing) : stdpp_scope.
Class Difference A := difference: A A A. Class Difference A := difference: A A A.
Hint Mode Difference ! : typeclass_instances. Hint Mode Difference ! : typeclass_instances.
Instance: Params (@difference) 2 := {}. Instance: Params (@difference) 2 := {}.
Infix "∖" := difference (at level 40, left associativity) : stdpp_scope. Infix "∖" := difference (at level 40, left associativity) : stdpp_scope.
Notation "(∖)" := difference (only parsing) : stdpp_scope. Notation "(∖)" := difference (only parsing) : stdpp_scope.
Notation "( x ∖)" := (difference x) (only parsing) : stdpp_scope. Notation "( x ∖.)" := (difference x) (only parsing) : stdpp_scope.
Notation "(∖ x )" := (λ y, difference y x) (only parsing) : stdpp_scope. Notation "(.∖ x )" := (λ y, difference y x) (only parsing) : stdpp_scope.
Infix "∖*" := (zip_with ()) (at level 40, left associativity) : stdpp_scope. Infix "∖*" := (zip_with ()) (at level 40, left associativity) : stdpp_scope.
Notation "(∖*)" := (zip_with ()) (only parsing) : stdpp_scope. Notation "(∖*)" := (zip_with ()) (only parsing) : stdpp_scope.
Infix "∖**" := (zip_with (zip_with ())) Infix "∖**" := (zip_with (zip_with ()))
...@@ -846,12 +846,12 @@ Hint Mode SubsetEq ! : typeclass_instances. ...@@ -846,12 +846,12 @@ Hint Mode SubsetEq ! : typeclass_instances.
Instance: Params (@subseteq) 2 := {}. Instance: Params (@subseteq) 2 := {}.
Infix "⊆" := subseteq (at level 70) : stdpp_scope. Infix "⊆" := subseteq (at level 70) : stdpp_scope.
Notation "(⊆)" := subseteq (only parsing) : stdpp_scope. Notation "(⊆)" := subseteq (only parsing) : stdpp_scope.
Notation "( X ⊆)" := (subseteq X) (only parsing) : stdpp_scope. Notation "( X ⊆.)" := (subseteq X) (only parsing) : stdpp_scope.
Notation "(⊆ X )" := (λ Y, Y X) (only parsing) : stdpp_scope. Notation "(.⊆ X )" := (λ Y, Y X) (only parsing) : stdpp_scope.
Notation "X ⊈ Y" := (¬X Y) (at level 70) : stdpp_scope. Notation "X ⊈ Y" := (¬X Y) (at level 70) : stdpp_scope.
Notation "(⊈)" := (λ X Y, X Y) (only parsing) : stdpp_scope. Notation "(⊈)" := (λ X Y, X Y) (only parsing) : stdpp_scope.
Notation "( X ⊈)" := (λ Y, X Y) (only parsing) : stdpp_scope. Notation "( X ⊈.)" := (λ Y, X Y) (only parsing) : stdpp_scope.
Notation "(⊈ X )" := (λ Y, Y X) (only parsing) : stdpp_scope. Notation "(.⊈ X )" := (λ Y, Y X) (only parsing) : stdpp_scope.
Infix "⊆@{ A }" := (@subseteq A _) (at level 70, only parsing) : stdpp_scope. Infix "⊆@{ A }" := (@subseteq A _) (at level 70, only parsing) : stdpp_scope.
Notation "(⊆@{ A } )" := (@subseteq A _) (only parsing) : stdpp_scope. Notation "(⊆@{ A } )" := (@subseteq A _) (only parsing) : stdpp_scope.
...@@ -870,12 +870,12 @@ Hint Extern 0 (_ ⊆** _) => reflexivity : core. ...@@ -870,12 +870,12 @@ Hint Extern 0 (_ ⊆** _) => reflexivity : core.
Infix "⊂" := (strict ()) (at level 70) : stdpp_scope. Infix "⊂" := (strict ()) (at level 70) : stdpp_scope.
Notation "(⊂)" := (strict ()) (only parsing) : stdpp_scope. Notation "(⊂)" := (strict ()) (only parsing) : stdpp_scope.
Notation "( X ⊂)" := (strict () X) (only parsing) : stdpp_scope. Notation "( X ⊂.)" := (strict () X) (only parsing) : stdpp_scope.
Notation "(⊂ X )" := (λ Y, Y X) (only parsing) : stdpp_scope. Notation "(.⊂ X )" := (λ Y, Y X) (only parsing) : stdpp_scope.
Notation "X ⊄ Y" := (¬X Y) (at level 70) : stdpp_scope. Notation "X ⊄ Y" := (¬X Y) (at level 70) : stdpp_scope.
Notation "(⊄)" := (λ X Y, X Y) (only parsing) : stdpp_scope. Notation "(⊄)" := (λ X Y, X Y) (only parsing) : stdpp_scope.
Notation "( X ⊄)" := (λ Y, X Y) (only parsing) : stdpp_scope. Notation "( X ⊄.)" := (λ Y, X Y) (only parsing) : stdpp_scope.
Notation "(⊄ X )" := (λ Y, Y X) (only parsing) : stdpp_scope. Notation "(.⊄ X )" := (λ Y, Y X) (only parsing) : stdpp_scope.
Infix "⊂@{ A }" := (strict (@{A})) (at level 70, only parsing) : stdpp_scope. Infix "⊂@{ A }" := (strict (@{A})) (at level 70, only parsing) : stdpp_scope.
Notation "(⊂@{ A } )" := (strict (@{A})) (only parsing) : stdpp_scope. Notation "(⊂@{ A } )" := (strict (@{A})) (only parsing) : stdpp_scope.
...@@ -903,12 +903,12 @@ Hint Mode ElemOf - ! : typeclass_instances. ...@@ -903,12 +903,12 @@ Hint Mode ElemOf - ! : typeclass_instances.
Instance: Params (@elem_of) 3 := {}. Instance: Params (@elem_of) 3 := {}.
Infix "∈" := elem_of (at level 70) : stdpp_scope. Infix "∈" := elem_of (at level 70) : stdpp_scope.
Notation "(∈)" := elem_of (only parsing) : stdpp_scope. Notation "(∈)" := elem_of (only parsing) : stdpp_scope.
Notation "( x ∈)" := (elem_of x) (only parsing) : stdpp_scope. Notation "( x ∈.)" := (elem_of x) (only parsing) : stdpp_scope.
Notation "(∈ X )" := (λ x, elem_of x X) (only parsing) : stdpp_scope. Notation "(.∈ X )" := (λ x, elem_of x X) (only parsing) : stdpp_scope.
Notation "x ∉ X" := (¬x X) (at level 80) : stdpp_scope. Notation "x ∉ X" := (¬x X) (at level 80) : stdpp_scope.
Notation "(∉)" := (λ x X, x X) (only parsing) : stdpp_scope. Notation "(∉)" := (λ x X, x X) (only parsing) : stdpp_scope.
Notation "( x ∉)" := (λ X, x X) (only parsing) : stdpp_scope. Notation "( x ∉.)" := (λ X, x X) (only parsing) : stdpp_scope.
Notation "(∉ X )" := (λ x, x X) (only parsing) : stdpp_scope. Notation "(.∉ X )" := (λ x, x X) (only parsing) : stdpp_scope.
Infix "∈@{ B }" := (@elem_of _ B _) (at level 70, only parsing) : stdpp_scope. Infix "∈@{ B }" := (@elem_of _ B _) (at level 70, only parsing) : stdpp_scope.
Notation "(∈@{ B } )" := (@elem_of _ B _) (only parsing) : stdpp_scope. Notation "(∈@{ B } )" := (@elem_of _ B _) (only parsing) : stdpp_scope.
...@@ -1005,8 +1005,8 @@ Arguments omap {_ _ _ _} _ !_ / : assert. ...@@ -1005,8 +1005,8 @@ Arguments omap {_ _ _ _} _ !_ / : assert.
Instance: Params (@omap) 4 := {}. Instance: Params (@omap) 4 := {}.
Notation "m ≫= f" := (mbind f m) (at level 60, right associativity) : stdpp_scope. Notation "m ≫= f" := (mbind f m) (at level 60, right associativity) : stdpp_scope.
Notation "( m ≫=)" := (λ f, mbind f m) (only parsing) : stdpp_scope. Notation "( m ≫=.)" := (λ f, mbind f m) (only parsing) : stdpp_scope.
Notation "(≫= f )" := (mbind f) (only parsing) : stdpp_scope. Notation "(.≫= f )" := (mbind f) (only parsing) : stdpp_scope.
Notation "(≫=)" := (λ m f, mbind f m) (only parsing) : stdpp_scope. Notation "(≫=)" := (λ m f, mbind f m) (only parsing) : stdpp_scope.
Notation "x ← y ; z" := (y = (λ x : _, z)) Notation "x ← y ; z" := (y = (λ x : _, z))
...@@ -1043,8 +1043,8 @@ Hint Mode Lookup - - ! : typeclass_instances. ...@@ -1043,8 +1043,8 @@ Hint Mode Lookup - - ! : typeclass_instances.
Instance: Params (@lookup) 4 := {}. Instance: Params (@lookup) 4 := {}.
Notation "m !! i" := (lookup i m) (at level 20) : stdpp_scope. Notation "m !! i" := (lookup i m) (at level 20) : stdpp_scope.
Notation "(!!)" := lookup (only parsing) : stdpp_scope. Notation "(!!)" := lookup (only parsing) : stdpp_scope.
Notation "( m !!)" := (λ i, m !! i) (only parsing) : stdpp_scope. Notation "( m !!.)" := (λ i, m !! i) (only parsing) : stdpp_scope.
Notation "(!! i )" := (lookup i) (only parsing) : stdpp_scope. Notation "(.!! i )" := (lookup i) (only parsing) : stdpp_scope.
Arguments lookup _ _ _ _ !_ !_ / : simpl nomatch, assert. Arguments lookup _ _ _ _ !_ !_ / : simpl nomatch, assert.
(** The singleton map *) (** The singleton map *)
...@@ -1272,8 +1272,8 @@ Hint Mode SqSubsetEq ! : typeclass_instances. ...@@ -1272,8 +1272,8 @@ Hint Mode SqSubsetEq ! : typeclass_instances.
Instance: Params (@sqsubseteq) 2 := {}. Instance: Params (@sqsubseteq) 2 := {}.
Infix "⊑" := sqsubseteq (at level 70) : stdpp_scope. Infix "⊑" := sqsubseteq (at level 70) : stdpp_scope.
Notation "(⊑)" := sqsubseteq (only parsing) : stdpp_scope. Notation "(⊑)" := sqsubseteq (only parsing) : stdpp_scope.
Notation "( x ⊑)" := (sqsubseteq x) (only parsing) : stdpp_scope. Notation "( x ⊑.)" := (sqsubseteq x) (only parsing) : stdpp_scope.
Notation "(⊑ y )" := (λ x, sqsubseteq x y) (only parsing) : stdpp_scope. Notation "(.⊑ y )" := (λ x, sqsubseteq x y) (only parsing) : stdpp_scope.
Infix "⊑@{ A }" := (@sqsubseteq A _) (at level 70, only parsing) : stdpp_scope. Infix "⊑@{ A }" := (@sqsubseteq A _) (at level 70, only parsing) : stdpp_scope.
Notation "(⊑@{ A } )" := (@sqsubseteq A _) (only parsing) : stdpp_scope. Notation "(⊑@{ A } )" := (@sqsubseteq A _) (only parsing) : stdpp_scope.
...@@ -1287,16 +1287,16 @@ Hint Mode Meet ! : typeclass_instances. ...@@ -1287,16 +1287,16 @@ Hint Mode Meet ! : typeclass_instances.
Instance: Params (@meet) 2 := {}. Instance: Params (@meet) 2 := {}.
Infix "⊓" := meet (at level 40) : stdpp_scope. Infix "⊓" := meet (at level 40) : stdpp_scope.
Notation "(⊓)" := meet (only parsing) : stdpp_scope. Notation "(⊓)" := meet (only parsing) : stdpp_scope.
Notation "( x ⊓)" := (meet x) (only parsing) : stdpp_scope. Notation "( x ⊓.)" := (meet x) (only parsing) : stdpp_scope.
Notation "(⊓ y )" := (λ x, meet x y) (only parsing) : stdpp_scope. Notation "(.⊓ y )" := (λ x, meet x y) (only parsing) : stdpp_scope.
Class Join A := join: A A A. Class Join A := join: A A A.
Hint Mode Join ! : typeclass_instances. Hint Mode Join ! : typeclass_instances.
Instance: Params (@join) 2 := {}. Instance: Params (@join) 2 := {}.
Infix "⊔" := join (at level 50) : stdpp_scope. Infix "⊔" := join (at level 50) : stdpp_scope.
Notation "(⊔)" := join (only parsing) : stdpp_scope. Notation "(⊔)" := join (only parsing) : stdpp_scope.
Notation "( x ⊔)" := (join x) (only parsing) : stdpp_scope. Notation "( x ⊔.)" := (join x) (only parsing) : stdpp_scope.
Notation "(⊔ y )" := (λ x, join x y) (only parsing) : stdpp_scope. Notation "(.⊔ y )" := (λ x, join x y) (only parsing) : stdpp_scope.
Class Top A := top : A. Class Top A := top : A.
Hint Mode Top ! : typeclass_instances. Hint Mode Top ! : typeclass_instances.
......
...@@ -121,7 +121,7 @@ Instance map_difference `{Merge M} {A} : Difference (M A) := ...@@ -121,7 +121,7 @@ Instance map_difference `{Merge M} {A} : Difference (M A) :=
of the elements. Implemented by conversion to lists, so not very efficient. *) of the elements. Implemented by conversion to lists, so not very efficient. *)
Definition map_imap `{ A, Insert K A (M A), A, Empty (M A), Definition map_imap `{ A, Insert K A (M A), A, Empty (M A),
A, FinMapToList K A (M A)} {A B} (f : K A option B) (m : M A) : M B := A, FinMapToList K A (M A)} {A B} (f : K A option B) (m : M A) : M B :=
list_to_map (omap (λ ix, (fst ix,) <$> curry f ix) (map_to_list m)). list_to_map (omap (λ ix, (fst ix ,.) <$> curry f ix) (map_to_list m)).
(* The zip operation on maps combines two maps key-wise. The keys of resulting (* The zip operation on maps combines two maps key-wise. The keys of resulting
map correspond to the keys that are in both maps. *) map correspond to the keys that are in both maps. *)
...@@ -507,7 +507,7 @@ Lemma insert_empty {A} i (x : A) : <[i:=x]>(∅ : M A) = {[i := x]}. ...@@ -507,7 +507,7 @@ Lemma insert_empty {A} i (x : A) : <[i:=x]>(∅ : M A) = {[i := x]}.
Proof. done. Qed. Proof. done. Qed.
Lemma insert_non_empty {A} (m : M A) i x : <[i:=x]>m . Lemma insert_non_empty {A} (m : M A) i x : <[i:=x]>m .
Proof. Proof.
intros Hi%(f_equal (!! i)). by rewrite lookup_insert, lookup_empty in Hi. intros Hi%(f_equal (.!! i)). by rewrite lookup_insert, lookup_empty in Hi.
Qed. Qed.
Lemma insert_subseteq {A} (m : M A) i x : m !! i = None m <[i:=x]>m. Lemma insert_subseteq {A} (m : M A) i x : m !! i = None m <[i:=x]>m.
...@@ -575,7 +575,7 @@ Lemma lookup_singleton_ne {A} i j (x : A) : ...@@ -575,7 +575,7 @@ Lemma lookup_singleton_ne {A} i j (x : A) :
Proof. by rewrite lookup_singleton_None. Qed. Proof. by rewrite lookup_singleton_None. Qed.
Lemma map_non_empty_singleton {A} i (x : A) : {[i := x]} ( : M A). Lemma map_non_empty_singleton {A} i (x : A) : {[i := x]} ( : M A).
Proof. Proof.
intros Hix. apply (f_equal (!! i)) in Hix. intros Hix. apply (f_equal (.!! i)) in Hix.
by rewrite lookup_empty, lookup_singleton in Hix. by rewrite lookup_empty, lookup_singleton in Hix.
Qed. Qed.
Lemma insert_singleton {A} i (x y : A) : <[i:=y]>({[i := x]} : M A) = {[i := y]}. Lemma insert_singleton {A} i (x y : A) : <[i:=y]>({[i := x]} : M A) = {[i := y]}.
...@@ -1619,7 +1619,7 @@ Lemma lookup_union_None {A} (m1 m2 : M A) i : ...@@ -1619,7 +1619,7 @@ Lemma lookup_union_None {A} (m1 m2 : M A) i :
Proof. rewrite lookup_union. destruct (m1 !! i), (m2 !! i); naive_solver. Qed. Proof. rewrite lookup_union. destruct (m1 !! i), (m2 !! i); naive_solver. Qed.
Lemma map_positive_l {A} (m1 m2 : M A) : m1 m2 = m1 = . Lemma map_positive_l {A} (m1 m2 : M A) : m1 m2 = m1 = .
Proof. Proof.
intros Hm. apply map_empty. intros i. apply (f_equal (!! i)) in Hm. intros Hm. apply map_empty. intros i. apply (f_equal (.!! i)) in Hm.
rewrite lookup_empty, lookup_union_None in Hm; tauto. rewrite lookup_empty, lookup_union_None in Hm; tauto.
Qed. Qed.
Lemma map_positive_l_alt {A} (m1 m2 : M A) : m1 m1 m2 . Lemma map_positive_l_alt {A} (m1 m2 : M A) : m1 m1 m2 .
......
...@@ -18,15 +18,15 @@ Definition card A `{Finite A} := length (enum A). ...@@ -18,15 +18,15 @@ Definition card A `{Finite A} := length (enum A).
Program Definition finite_countable `{Finite A} : Countable A := {| Program Definition finite_countable `{Finite A} : Countable A := {|
encode := λ x, encode := λ x,
Pos.of_nat $ S $ default 0 $ fst <$> list_find (x =) (enum A); Pos.of_nat $ S $ default 0 $ fst <$> list_find (x =.) (enum A);
decode := λ p, enum A !! pred (Pos.to_nat p) decode := λ p, enum A !! pred (Pos.to_nat p)
|}. |}.
Arguments Pos.of_nat : simpl never. Arguments Pos.of_nat : simpl never.
Next Obligation. Next Obligation.
intros ?? [xs Hxs HA] x; unfold encode, decode; simpl. intros ?? [xs Hxs HA] x; unfold encode, decode; simpl.
destruct (list_find_elem_of (x =) xs x) as [[i y] Hi]; auto. destruct (list_find_elem_of (x =.) xs x) as [[i y] Hi]; auto.
rewrite Nat2Pos.id by done; simpl; rewrite Hi; simpl. rewrite Nat2Pos.id by done; simpl; rewrite Hi; simpl.
destruct (list_find_Some (x =) xs i y); naive_solver. destruct (list_find_Some (x =.) xs i y); naive_solver.
Qed. Qed.
Hint Immediate finite_countable : typeclass_instances. Hint Immediate finite_countable : typeclass_instances.
...@@ -38,7 +38,7 @@ Proof. ...@@ -38,7 +38,7 @@ Proof.
destruct finA as [xs Hxs HA]; unfold encode_nat, encode, card; simpl. destruct finA as [xs Hxs HA]; unfold encode_nat, encode, card; simpl.
rewrite Nat2Pos.id by done; simpl. rewrite Nat2Pos.id by done; simpl.
destruct (list_find _ xs) as [[i y]|] eqn:?; simpl. destruct (list_find _ xs) as [[i y]|] eqn:?; simpl.
- destruct (list_find_Some (x =) xs i y); eauto using lookup_lt_Some. - destruct (list_find_Some (x =.) xs i y); eauto using lookup_lt_Some.
- destruct xs; simpl. exfalso; eapply not_elem_of_nil, (HA x). lia. - destruct xs; simpl. exfalso; eapply not_elem_of_nil, (HA x). lia.
Qed. Qed.
Lemma encode_decode A `{finA: Finite A} i : Lemma encode_decode A `{finA: Finite A} i :
...@@ -48,8 +48,8 @@ Proof. ...@@ -48,8 +48,8 @@ Proof.
unfold encode_nat, decode_nat, encode, decode, card; simpl. unfold encode_nat, decode_nat, encode, decode, card; simpl.
intros Hi. apply lookup_lt_is_Some in Hi. destruct Hi as [x Hx]. intros Hi. apply lookup_lt_is_Some in Hi. destruct Hi as [x Hx].
exists x. rewrite !Nat2Pos.id by done; simpl. exists x. rewrite !Nat2Pos.id by done; simpl.
destruct (list_find_elem_of (x =) xs x) as [[j y] Hj]; auto. destruct (list_find_elem_of (x =.) xs x) as [[j y] Hj]; auto.
destruct (list_find_Some (x =) xs j y) as [? ->]; auto. destruct (list_find_Some (x =.) xs j y) as [? ->]; auto.
rewrite Hj; csimpl; eauto using NoDup_lookup. rewrite Hj; csimpl; eauto using NoDup_lookup.
Qed. Qed.
Lemma find_Some `{finA: Finite A} P `{ x, Decision (P x)} (x : A) : Lemma find_Some `{finA: Finite A} P `{ x, Decision (P x)} (x : A) :
...@@ -282,7 +282,7 @@ Lemma sum_card `{Finite A, Finite B} : card (A + B) = card A + card B. ...@@ -282,7 +282,7 @@ Lemma sum_card `{Finite A, Finite B} : card (A + B) = card A + card B.
Proof. unfold card. simpl. by rewrite app_length, !fmap_length. Qed. Proof. unfold card. simpl. by rewrite app_length, !fmap_length. Qed.
Program Instance prod_finite `{Finite A, Finite B} : Finite (A * B)%type := Program Instance prod_finite `{Finite A, Finite B} : Finite (A * B)%type :=
{| enum := foldr (λ x, (pair x <$> enum B ++)) [] (enum A) |}. {| enum := foldr (λ x, (pair x <$> enum B ++.)) [] (enum A) |}.
Next Obligation. Next Obligation.
intros ??????. induction (NoDup_enum A) as [|x xs Hx Hxs IH]; simpl. intros ??????. induction (NoDup_enum A) as [|x xs Hx Hxs IH]; simpl.
{ constructor. } { constructor. }
...@@ -312,7 +312,7 @@ Definition list_enum {A} (l : list A) : ∀ n, list { l : list A | length l = n ...@@ -312,7 +312,7 @@ Definition list_enum {A} (l : list A) : ∀ n, list { l : list A | length l = n
fix go n := fix go n :=
match n with match n with
| 0 => [[]eq_refl] | 0 => [[]eq_refl]
| S n => foldr (λ x, (sig_map (x ::) (λ _ H, f_equal S H) <$> (go n) ++)) [] l | S n => foldr (λ x, (sig_map (x ::.) (λ _ H, f_equal S H) <$> (go n) ++.)) [] l
end. end.
Program Instance list_finite `{Finite A} n : Finite { l : list A | length l = n } := Program Instance list_finite `{Finite A} n : Finite { l : list A | length l = n } :=
......
...@@ -73,7 +73,7 @@ Instance gmap_merge `{Countable K} : Merge (gmap K) := λ A B C f m1 m2, ...@@ -73,7 +73,7 @@ Instance gmap_merge `{Countable K} : Merge (gmap K) := λ A B C f m1 m2,
(bool_decide_unpack _ Hm1) (bool_decide_unpack _ Hm2))). (bool_decide_unpack _ Hm1) (bool_decide_unpack _ Hm2))).
Instance gmap_to_list `{Countable K} {A} : FinMapToList K A (gmap K A) := λ m, Instance gmap_to_list `{Countable K} {A} : FinMapToList K A (gmap K A) := λ m,
let (m,_) := m in omap (λ ix : positive * A, let (m,_) := m in omap (λ ix : positive * A,
let (i,x) := ix in (,x) <$> decode i) (map_to_list m). let (i,x) := ix in (., x) <$> decode i) (map_to_list m).
(** * Instantiation of the finite map interface *) (** * Instantiation of the finite map interface *)
Instance gmap_finmap `{Countable K} : FinMap K (gmap K). Instance gmap_finmap `{Countable K} : FinMap K (gmap K).
...@@ -139,12 +139,12 @@ Section curry_uncurry. ...@@ -139,12 +139,12 @@ Section curry_uncurry.
(* FIXME: the type annotations `option (gmap K2 A)` are silly. Maybe these are (* FIXME: the type annotations `option (gmap K2 A)` are silly. Maybe these are
a consequence of Coq bug #5735 *) a consequence of Coq bug #5735 *)
Lemma lookup_gmap_curry (m : gmap K1 (gmap K2 A)) i j : Lemma lookup_gmap_curry (m : gmap K1 (gmap K2 A)) i j :
gmap_curry m !! (i,j) = (m !! i : option (gmap K2 A)) = (!! j).