在Coq中使用空格和花括号设置理论符号

问题描述

我想在Coq中使用标准符号 x∈{x}。
但是存在问题：

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

1）花括号在Coq中具有特殊含义，因此会发生以下情况：

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）如果第一个问题无法解决，那么还有另一个问题。 （这里我决定在符号中使用附加符号'`'。）

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 }` *)

现在，我应该

a）在第一个花括号之后添加空格，或者

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

b）删除无意最后一个x字母后的空白。

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

我该怎么做？

推荐答案

您可以得到通过添加 tin x（Sing y）的符号，可以使用其他符号。由于几个重叠的符号，解析器中的花括号有些奇怪；参见讨论。

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.

您可以通过使用Coq的 format 修饰符来更一般地解决空白打印问题（请参见）。或者，在符号中使用两个空格将强制Coq在此处打印一个空格（如第二个示例中所示，有时似乎还是决定打印一个空格，在这种情况下，您必须诉诸自定义格式）。

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.

这篇关于在Coq中使用空格和花括号设置理论符号的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持！