coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Vincent BENAYOUN <benayoun.vincent AT gmail.com>
- To: Greg Morrisett <greg AT eecs.harvard.edu>
- Cc: Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>, Coq Club <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] Unable to do "induction ... eqn:.."
- Date: Thu, 6 Dec 2012 12:29:37 +0100
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.
dependent destruction x ; auto.
Inductive t2 : nat -> Prop :=
| A2 : t2 0
| B2 : t2 1.
Lemma toto2 : forall (x:t2 0), x = A2.
Proof.
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.
>
>
- Re: [Coq-Club] Unable to do "induction ... eqn:..", Vincent BENAYOUN, 12/03/2012
- Re: [Coq-Club] Unable to do "induction ... eqn:..", Greg Morrisett, 12/03/2012
- Re: [Coq-Club] Unable to do "induction ... eqn:..", Vincent BENAYOUN, 12/06/2012
- Re: [Coq-Club] Unable to do "induction ... eqn:..", Robbert Krebbers, 12/08/2012
- Re: [Coq-Club] Unable to do "induction ... eqn:..", Vincent BENAYOUN, 12/06/2012
- <Possible follow-up(s)>
- Re: [Coq-Club] Unable to do "induction ... eqn:..", Robbert Krebbers, 12/08/2012
- Re: [Coq-Club] Unable to do "induction ... eqn:..", Greg Morrisett, 12/03/2012
Archive powered by MHonArc 2.6.18.