The Coq mailing list

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

Thank you Greg for your answer.

Vincent

2012/12/3 Greg Morrisett <greg AT eecs.harvard.edu>

The easiest thing is to use "dependent destruction" from the
Program library:

Require Import Program.

Inductive t2 : nat -> Prop :=
| A2 : t2 0
| B2 : t2 1.

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

  dependent destruction x ; auto.
Qed.

-Greg

On Dec 3, 2012, at 8:41 AM, Vincent BENAYOUN <benayoun.vincent AT gmail.com> wrote:

> 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.
>
>