coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Robbert Krebbers <mailinglists AT robbertkrebbers.nl>
- To: Vincent BENAYOUN <benayoun.vincent AT gmail.com>
- Cc: coq-club AT inria.fr
- Subject: Re: [Coq-Club] Unable to do "induction ... eqn:.."
- Date: Sat, 08 Dec 2012 13:48:12 +0100
The reason that this fails is because Coq uses the non-dependent induction principle for inductive propositions by default. In this case, it uses:
Check bbb_ind.
(* bbb_ind
: forall P : nat -> Prop, P 0 -> forall n : nat, bbb n -> P n *)
However, in order to make "induction term eqn:naming_intro_pattern" work, we need the dependent induction principle, which can be generated as follows.
Scheme bbb_ind_dep := Induction for bbb Sort Prop.
Check bbb_ind_dep.
(* bbb_ind_dep
: forall P : forall n : nat, bbb n -> Prop,
P 0 BBB -> forall (n : nat) (b : bbb n), P n b *)
Using this induction principle, your proof works just fine:
Lemma bbb_theorem :
forall (n:nat), bbb n -> n = 0.
Proof.
intros n HHH.
induction HHH eqn:toto using bbb_ind_dep.
reflexivity.
Qed.
On 11/28/2012 11:55 AM, Vincent BENAYOUN wrote:
Hi all,
I need to use the tactic "induction term eqn:naming_intro_pattern" in
some of my proofs but I get an error message.
Here is a simplified version of my problem.
If I remove "eqn:toto" from the following proof it works perfectly.
But why does it fail with "eqn:toto" ???
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.
Thanks,
Vincent
- 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.