The Coq mailing list

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