为何基于已有Notation定义的Coq符号显示不符合预期？

问题原因 #

你定义的x ∪ y属于语法层面的缩写，本质是∪ {x, y}的展开式，而非直接绑定到一个独立的常量或公理。Coq的默认打印策略会优先显示表达式的底层结构，而非语法缩写——只有当符号直接关联到原始的常量（比如你后来定义的build_two_union公理）时，打印才会保留缩写形式。

简单来说：你的二元并集符号仅负责把x ∪ y解析成∪ {x, y}，但打印时Coq不会自动把∪ {x, y}反过来还原成x ∪ y，除非你明确配置打印规则。

解决方案 #

方案1：直接定义二元并集公理（推荐） #

像你发现的那样，为二元并集单独定义公理，让符号直接绑定到这个原始常量，打印时就会保留x ∪ y的形式：

Section Test.
  Variable set:Type.
  Variable In : set -> set -> Prop.
  Notation "x ∈ y" := (In y x) (at level 50).

  Structure class φ := {
    class_base :> set;
    class_row : forall x, x ∈ class_base <-> φ x;
  }.

  Axiom build_union : forall F, class (fun x => exists Y, x ∈ Y /\ Y ∈ F).
  Notation "∪ F" := (build_union F) (at level 50).

  Axiom build_non_ordered_pair_set : forall x y, class (fun w => w = x \/ w = y).
  Notation "{ x , y }" := (build_non_ordered_pair_set x y) (at level 45).

  -- 直接定义二元并集公理
  Axiom build_two_union : forall x y, class (fun z => exists Y, z ∈ Y /\ Y ∈ {x, y}).
  Notation "x ∪ y" := (build_two_union x y) (at level 50, left associativity).

  Variable F x y:set.

  Check x ∪ y. -- 现在会显示 x ∪ y
End Test.

方案2：强制打印语法缩写 #

如果不想新增公理，可以通过调整符号定义和打印选项，让Coq在打印时还原缩写：

Section Test.
  Variable set:Type.
  Variable In : set -> set -> Prop.
  Notation "x ∈ y" := (In y x) (at level 50).

  Structure class φ := {
    class_base :> set;
    class_row : forall x, x ∈ class_base <-> φ x;
  }.

  Axiom build_union : forall F, class (fun x => exists Y, x ∈ Y /\ Y ∈ F).
  Notation "∪ F" := (build_union F) (at level 50).

  Axiom build_non_ordered_pair_set : forall x y, class (fun w => w = x \/ w = y).
  Notation "{ x , y }" := (build_non_ordered_pair_set x y) (at level 45).

  -- 定义符号时指定作用域，同时开启打印符号选项
  Notation "x ∪ y" := (∪ {x, y}) (at level 50, left associativity) : set_scope.
  Delimit Scope set_scope with set.
  Set Printing Notations. -- 强制打印已定义的符号缩写

  Variable F x y:set.

  Check (x ∪ y)%set. -- 显示 x ∪ y
End Test.

需要用作用域限定符（%set）明确指定使用自定义符号规则，同时开启Set Printing Notations让Coq优先使用你的缩写符号打印。

内容的提问来源于stack exchange，提问作者Ryuta Ito