Обозначение теории множеств с пробелами и фигурными скобками в Coq - PullRequest
Новая
       13

Обозначение теории множеств с пробелами и фигурными скобками в Coq

0 голосов
/ 03 ноября 2018

Я хотел бы иметь стандартную запись, такую ​​как «x ∈ {x}» в Coq. Но есть проблемы:

1) Фигурные скобки имеют особое значение в Coq, поэтому происходит следующее: 

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

Как правильно определить это обозначение?

2) Если первая проблема не может быть решена, есть другая. (Здесь я решил использовать дополнительный символ «` »в обозначениях.) 

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

Теперь я должен

a) либо добавьте пробел после первой фигурной скобки, либо

b) удалить непреднамеренный пробел после последней буквы x.

Как я могу сделать эти действия?

1 Ответ

0 голосов
/ 03 ноября 2018

Вы можете заставить свою нотацию работать, добавив нотацию для tin x (Sing y) в дополнение к другим нотациям. Что-то странное в фигурных скобках в парсере из-за нескольких перекрывающихся обозначений; см. https://github.com/coq/coq/pull/6743 для обсуждения.

Вы можете исправить печать пробельных символов в целом, используя модификатор Coq format для обозначения (см. Руководство по печати обозначений ). В качестве альтернативы, использование двух пробелов в нотации заставит Coq напечатать там пробел (как во втором примере, иногда кажется, что иногда все равно приходится печатать один, и в этом случае вам приходится прибегать к пользовательскому формату).

Вот все вышеперечисленные решения, реализованные для вашего примера: 

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.
...