Coq: Defining Vernacular to avoid duplication

Question

I'm currently working on proofs where I find myself writing code like this over and over again:

Lemma eq_T: forall (x y : T), {x = y} + {x <> y}
  with eq_trait: forall (x y : trait), {x = y} + {x <> y}
  with eq_pi: forall (x y : pi), {x = y} + {x <> y}.
  Proof.
    decide equality; auto with ott_coq_equality arith.
    decide equality; auto with ott_coq_equality arith.
    decide equality; auto with ott_coq_equality arith.        
  Defined

Hint Resolve eq_T : ott_coq_equality.
Hint Resolve eq_trait : ott_coq_equality.
Hint Resolve eq_pi : ott_coq_equality.

That is, I have some number of mutually inductive types, and I simultaneously derive equality for all of them.

What I'd like to do is have some sort of macro, where I can write

MutualDeriveEquality T, pi, trait

and it will mechanically generate the above commands, so that I can use this for various groups of mutually inductive types.

I'm not very knowledgeable on LTac, but I'm not certain that it would apply here, since I'm not just automating the generation of proof terms, but the definition of values in vernacular. (I could be totally wrong though).

What I'm wondering is, is there a way to define a "vernacular macro" that can automate this? Or is this something that can be done with LTac? Or is the only way to write a Coq plugin in OCaml?

Yves Yves · Accepted Answer · 2018-07-05T07:22:12

You are right that Ltac is not adapted for this task. For now, there is no way to automate this kind of task in Coq, but some tools are being developed for this. See for example Template Coq or Coq-Elpi. Most of these tools are in pre-release state.

As an alternative, I would suggest generating your own .v files from a more abstract description of the types, writing the file generator in the language of your choice.

Coq: Defining Vernacular to avoid duplication

1 Answers