Set theory notation with whitespaces and curly braces in Coq

user_4944714 0
Viewed 255

I'd like to have standard notation like "x ∈ { x }" in Coq. But there are problems:

1) Curly braces has special meaning in Coq, so the following happens:

Notation " x ∈ y " :=(tin x y) (at level 50).
Notation " { x } ":=(Sing x).
Check fun x => (x ∈ { x }).
(*error: Unknown interpretation for notation "_ ∈ { _ }". *)

How to define this notation correctly?

2) If the first problem cannot be solved, there is another. (Here I decided to use the additional symbol '`' in the notation.)

Notation " { x }` ":=(Sing x).
Check fun x => (x ∈ { x }`).
(* fun x : Ens => x ∈ {x }` *)

Now I should

a) either add a whitespace after the first curly brace or

b) delete the unintentional white space after the last x letter.

How can I do these actions?

coq
1 Answers

You can get your notation to work by adding a notation for tin x (Sing y) in addition to the other notations. There's something odd about curly braces in the parser due to several overlapping notations; see https://github.com/coq/coq/pull/6743 for some discussion.

You can fix whitespace printing quite generally by using Coq's format modifier for a notation (see the manual on printing notations). Alternately, using two spaces within your notation will force Coq to print a space there (as in your second example, it seems like sometimes decides to print one anyway, in which case you have to resort to a custom format).

Here are all of the solutions above implemented for your example:

Axiom Ens : Set.
Axiom tin : Ens -> Ens -> Prop.
Axiom Sing : Ens -> Ens.

Section FixingBraceNotation.
  Notation "x  ∈  y" := (tin x y) (at level 50).
  (* Note: the level on the following modifier is already set for this
  notation and so is redundant, but it needs to be reproduced exactly if
  you add a format modifier (you can overwrite the notation but not the
  parsing levels). *)
  Notation "{ x }" := (Sing x) (at level 0, x at level 99).
  Notation "x  ∈  { y }" := (tin x (Sing y)) (at level 50).
  Check fun x => (x ∈ { x }).
  Check fun x => {x}.
End FixingBraceNotation.

Section RemovingWhitespace.
  Notation "x  ∈  y" := (tin x y) (at level 50).
  Notation "{ x }`" := (Sing x) (at level 0, format "{ x }`").
  Check fun x => (x ∈ { x }`).
End RemovingWhitespace.

Section AddingWhitespace.
  Notation "x  ∈  y" := (tin x y) (at level 50).
  Notation "{  x  }`" := (Sing x) (at level 0).
  Check fun x => (x ∈ {x}`).
End AddingWhitespace.
user_40845670
Related