The Coq mailing list

[Robbert Krebbers <mailinglists AT robbertkrebbers.nl>]

The reason that this fails is because Coq uses the non-dependent 
induction principle for inductive propositions by default. In this case, 
it uses:

  Check bbb_ind.
  (* bbb_ind
     : forall P : nat -> Prop, P 0 -> forall n : nat, bbb n -> P n *)


However, in order to make "induction term eqn:naming_intro_pattern" 
work, we need the dependent induction principle, which can be generated 
as follows.

  Scheme bbb_ind_dep := Induction for bbb Sort Prop.
  Check bbb_ind_dep.
  (* bbb_ind_dep
     : forall P : forall n : nat, bbb n -> Prop,
       P 0 BBB -> forall (n : nat) (b : bbb n), P n b *)

Using this induction principle, your proof works just fine:

Lemma bbb_theorem :
  forall (n:nat), bbb n -> n = 0.
Proof.
  intros n HHH.
  induction HHH eqn:toto using bbb_ind_dep.
  reflexivity.
Qed.

On 11/28/2012 11:55 AM, Vincent BENAYOUN wrote:
> Hi all,
>
> I need to use the tactic "induction term eqn:naming_intro_pattern" in
> some of my proofs but I get an error message.
> Here is a simplified version of my problem.
>
>
> If I remove "eqn:toto" from the following proof it works perfectly.
> But why does it fail with "eqn:toto" ???
>
> Inductive bbb : nat -> Prop :=
> | BBB : bbb 0.
>
> Lemma bbb_theorem :
>    forall (n:nat), bbb n -> n = 0.
> Proof.
>    intros n HHH.
>    induction HHH eqn:toto.
>    reflexivity.
> Qed.
>
> Thanks,
> Vincent