coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] hello coq users

From: Anders Lundstedt <anders AT anderslundstedt.se>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: Re: [Coq-Club] hello coq users
Date: Sun, 18 Jan 2015 08:24:56 +0100

In your case you can also just keep a b c in the goal when doing induction on
n.

Parameter P : nat -> nat -> nat -> nat -> Prop.
Axiom baseCase : forall a b c, P 0 a b c.

Lemma l : forall n a b c, P n a b c.
Proof.
intros n a b c. induction n.
- apply baseCase.
- (* now not in induction hypothesis *) Restart.
intro n. induction n.
- apply baseCase.
- (* now more general induction hypothesis *)

[Coq-Club] hello coq users, Andrei Borac, 01/18/2015
- Re: [Coq-Club] hello coq users, Andrew Hirsch, 01/18/2015
  - Re: [Coq-Club] hello coq users, Anders Lundstedt, 01/18/2015
  - Re: [Coq-Club] hello coq users, Cedric Auger, 01/18/2015
    - Re: [Coq-Club] hello coq users, Randy Pollack, 01/18/2015
      - Re: [Coq-Club] hello coq users, Andrei Borac, 01/18/2015
        
        Re: [Coq-Club] hello coq users, Jonas Oberhauser, 01/20/2015
        
        Re: [Coq-Club] hello coq users, Hugo Herbelin, 01/23/2015