Consider the reflexive transitive closure of a relation:
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.
How can I give notation in Coq so that I can write x ->* y, perhaps adding a subscript to represent the relation ->__r. This is certainly possible in Isabelle. Is there a clean way of doing it in Coq?
You can indeed use the notation system of Coq for this:
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.
There are other notations that you can try, this an example explicitly mentioning the R. You can only use this generic notation in combination with a special one for reduction.
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.
Also note that you can do something fancy and use the notation already in the definition.
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).
You can do a lot of things with notations. The following also works.
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.