The Coq mailing list

[Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>]

Well, the problem is as explained in the error message: it produces a type error.

First note that induction x eqn:e can be broken down into remember x eqn:e; induction x.

Rewriting your file as

Inductive bbb : nat -> Prop :=
| BBB : bbb 0.

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

Before the induction step we have the following goal:

n : nat
HHH : bbb n
b : bbb n
toto : b = HHH
______________________________________(1/1)
n = 0

Now, doing induction on HHH tries to create the term:

fun n' : nat => forall b : bbb n', b = HHH -> n' = 0

The "fun n' =>" part is to be able to substitute n with the correct value for the required constructor. It also puts toto back as an implication (you can do it with: revert toto). The problem here is obvious: b has type bbb n' and HHH has type bbb n which are different, hence b=HHH isn't well-typed. And the tactic fails.

Instead you can do  elim HHH, which works like induction HHH but without doing any revert. But of course, in that case, your remembered equation will be useless.

On 28 November 2012 11:55, Vincent BENAYOUN <benayoun.vincent AT gmail.com> wrote:

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.