The Coq mailing list

[Pierre Courtieu <pierre.courtieu AT gmail.com>]

Le mer. 16 mai 2018 à 18:31, Joachim Breitner <mail AT joachim-breitner.de> a écrit :

> 3) the shape of this "functional scheme" is probably not accepted by
> "induction ... using foo_ind". Does it? Or do you have to apply the
> principle by hand?

Right now I use

    revert e captured.
    apply go_ind.

in my lemma (e and captured are the actual parameters to my function
go); changing that to

    induction e, captured using go_ind.

gives me “Cannot recognize an induction scheme.”. So far I am happy
with apply; how would I have to change the lemma so that [induction]
works,

The presence of (f x) (à la functional scheme) and WellFormed (à la inductive type) simultaneously in the principle is not supported currently by induction/elim . This could be a feature wish I guess.

and what would I gain from it?

Induction has a few features that make it a bit more shiny than basic standard apply. For instance it supports “as”, it performs substitution in hyps, it names induction hyps differently etc. See the documentation of induction. Nothing crucial but still useful most of the time.

P

Cheers,
Joachim

--
Joachim Breitner
  mail AT joachim-breitner.de
  http://www.joachim-breitner.de/