The Coq mailing list

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

2012/11/26 AUGER Cédric 
<sedrikov AT gmail.com>:
> Le Mon, 26 Nov 2012 14:50:02 +0100,
> Pierre Courtieu 
> <pierre.courtieu AT gmail.com>
>  a écrit :
>
>> Hi Cédric, can you give an example where "induction t" does what you
>> want (t being a non variable term) and "remember x as t ; induction x"
>> doesn't?
> I guess you mean "remember t as x ; induction x."

Yes

> Almost everywhere, I never want to have my environments polluted by
> needless equalities. Plus the generated proof term will be horrible,
> and it has an impact on performances when doing big developpements.

As my proposition is to "remember" only for non variable terms, I understand
that you often use "induction t" with a non variable t. This is interesting, 
why
do you need that so often? I never do.

>> Actually if you really want to just apply the induction principle,
>> then "elim" is probably better because "induction" does a lot of other
>> things anyway (what I propose is just doing a bit more for induction).
>
> A LOT of other things? Well beside generalizing all hypothesis relying
> on the pattern on which induction is done, and then reintroducing them
> in the environment, I do not see what this 'lot' is.

I mean this. On each subgoal, the hypothesis are re-introduced at their
previous place. On big proofs (lots of cases + big environment) this is a bit
expensive and introduces extra beta redexes.

> I have never used
> elim, since I never understood really what it is used for. 'case' and
> 'destruct' do all what I need when dealing with non recursive stuff.
> With recursion, I either use 'fix' (when I want full control, or when I
> use 'Unset Elimination Schemes.') or induction (after having carefuly
> selected what I want to be generalized).

elim x is exaclty "pattern x; apply foo_ind.". It does not generate any name,
it does not generalize any hypothesis (you will need to generalize/intro by
yourself as for case).

OK fix is even lighter...

Anyway I just saw the documentation of the experimental tactic
"dependent induction"
(http://coq.inria.fr/coq/refman/Reference-Manual011.html#@tactic97) which
seems to do exactly what I proposed.

P.