induction using always names the induction hypotheses based on the type of the term being examined, while a plain
induction sometimes gives it a short name (at least when doing induction over a variable). Is there any way to change the default name, or will I need as
as clause at every use?
I tried to suggest a name in the definition of the induction lemma by using an unnecessary forall to bind the induction hypothesis, but that didn't help. (I suspect Coq doesn't remember the name if you write a not-actually-dependent parameter with forall rather than
This may be overkill but you can have a look at my librarie LibHyps (https://github.com/Matafou/LibHyps, installable with opam). It defines a generic customizable auto naming scheme, together with a tactical (default syntax is an exclamation point before any tactic which renames any "new" hypothesis after the tactic. Customization is done by means of ltac functions.
Once installed try the demo file https://github.com/Matafou/LibHyps/blob/master/LibHyps/LibHypsDemo.v.
Last updated: Jan 27 2023 at 02:04 UTC