The Coq mailing list

["Samuel E. Moelius III" <moelius AT cis.udel.edu>]

It appears that, at the prompt, ``induction 2'' invokes the following 
version of ``induction'' from page 176 of the 8.2 reference manual.

18. simple induction num
    This tactic behaves as intros until num; elim ident where ident is the
    name given by intros until num to the num-th non-dependent premise of
    the goal.

I don't know why the behavior is different in Ltac vs. at the prompt.

Also, I don't know why, at the prompt, Coq isn't insisting on the presence 
of ``simple''.

In any case, which did you intend: the standard ``induction term'' or 
``simple induction num'' as above?

Sam

Edsko de Vries wrote:
> Hi Sam,
>
> > If you change ``integer'' to ``constr'' in the definition of my_induction, 
> > then you no longer get the error.
>
> Yes, the error disappears, and it seems to work, but appearances are deceiving
> I think. Here's a slightly extended example:
>
> Tactic Notation "my_induction" constr(n) :=
>   induction n.
>
> Inductive even : nat -> Prop :=
>   | even_zero : even 0
>   | even_succ : forall n, even n -> even (S (S n)).
>
> Inductive weird : nat -> Prop :=
>   | weird_0 : weird 0
>   | weird_1 : weird 1
>   | weird_2 : weird 2
>   | weird_3 : weird 3.
>
> Lemma foo : forall (n:nat), even n -> weird n -> True.
> Proof.
>
> Now, 
>
>   induction 2.
>
> will do induction on 'weird n' (and give 4 subgoals). my_induction 2 however
> will do induction on 'even n' (it seems its completely ignoring the argument);
> Thomas's "solution" does the same (induction on 'even n').
>
> Edsko
>
> --------------------------------------------------------
> Bug reports: http://logical.saclay.inria.fr/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>           http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club