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。这在伊莎贝尔身上当然是可能的。在库克有干净的方法吗？

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

---

你可以用符号做很多事情。以下内容也适用。

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