coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] hello coq users

From: Hugo Herbelin <Hugo.Herbelin AT inria.fr>
To: Jonas Oberhauser <s9joober AT gmail.com>
Cc: coq-club AT inria.fr, zerosum42 AT gmail.com
Subject: Re: [Coq-Club] hello coq users
Date: Fri, 23 Jan 2015 17:05:16 +0100

Hi,

BTW, there is also a (unfortunately not so nice) syntax for
"reverting" on the fly:

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

Lemma l : forall a b c n, P n a b c.
Proof.
intros a b c n. induction n in a, b, c |- *.
- apply baseCase.
- ...

Hugo

On Tue, Jan 20, 2015 at 02:01:21AM +0100, Jonas Oberhauser wrote:
> Am 18.01.2015 um 19:48 schrieb Andrei Borac:
> >Ah sorry folks, it seems making other variables "arbitrary" is indeed
> >the default in Coq,
>
> It is not. Try this on for size:
>
> Goal forall a b n c, ....
> induction n.
>
>
> What will happen is that a and b will be fixed, while c will stay
> generalized.
> Coq will fix the variables until the one that you mention, from left
> to right, and keep the ones after it generalized.
>
> hope that helps,
>
> jonas

[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