Coq中自反传递关闭的注释

Question

考虑关系的自反传递关闭：

Inductive star {A : Type} (r : A -> A -> Prop) : A -> A -> Prop :=
| star_refl x : star r x x
| star_step x y z : r x y -> star r y z -> star r x z

如何在Coq中给出符号，以便我可以写x-> * y，也许添加下标来表示关系-> __ r。在伊莎贝尔，这当然是可能的。在Coq中有一种干净的方法吗？

Answer 1

您确实可以为此使用Coq的符号系统：

Notation "x '[' R ']*' y" := (star R x y) (at level 20).

Goal
  forall A (x y z : A) R,
    x [R]* y ->
    y [R]* z ->
    x [R]* z.

您可以尝试使用其他符号，该示例明确提到了R。您只能将此通用表示法与特殊表示法结合使用以进行简化。

Section Terms.

  Context (term : Type).
  Context (red : term -> term -> Prop).
  Notation "x → y" := (red x y) (at level 0).

  Notation "x →* y" := (x [red]* y) (at level 19).

  Goal forall x y, x → y -> x →* y.
  Abort.

End Terms.

还请注意，您可以做一些花哨的事情，并使用定义中已经存在的符号。

Reserved Notation "x '[' R ']*' y" (at level 20).

Inductive star {A : Type} (r : A -> A -> Prop) : A -> A -> Prop :=
| star_refl x : x [r]* x
| star_step x y z : r x y -> y [r]* z -> x [r]* z

where "x '[' R ']*' y" := (star R x y).