Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Unable to do "induction ... eqn:.."

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Unable to do "induction ... eqn:.."


Chronological Thread 
  • 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



Archive powered by MHonArc 2.6.18.

Top of Page