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

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

2 голосов
/ 02 апреля 2020

Рассмотрим рефлексивное транзитивное замыкание отношения: 

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?

1 Ответ

1 голос
/ 02 апреля 2020

Вы действительно можете использовать систему обозначений 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. Вы можете использовать только этот обобщенный c нотация в сочетании со специальной для сокращения. 

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