The Coq mailing list

[Vincent BENAYOUN <benayoun.vincent AT gmail.com>]

Thank you very much for your answer.

I understand the error message but I still can't find a way to solve my problem.

Thanks to your explanations, I managed to explain more precisely my problem as follow.

For the following Lemma, I would like to prove it by induction but I can't because of the type error. Well, a can give a proof term.

Inductive t : nat -> Prop :=

| A : t 0.

Lemma toto : forall (x:t 0), x = A.

Proof.

  intro x.

  apply(match x with | A => eq_refl end).

Qed.

But since there are many cases, I don't know how to prove the Lemma. The following Coq script fails with a type error.

Inductive t2 : nat -> Prop :=

| A2 : t2 0

| B2 : t2 1.

Lemma toto2 : forall (x:t2 0), x = A2.

Proof.

  intros x.

  eapply(match x with | A2 => eq_refl | B2 => _ end).

Qed.

I should prove False in the second branch of the pattern-matching but I don't know how !

Is there a way to prove such a Lemma ?

Thanks in advance,

Vincent

2012/11/29 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.