coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Gert Smolka <smolka AT ps.uni-saarland.de>
- To: "coq-club AT inria.fr" <coq-club AT inria.fr>
- Cc: Pierre Courtieu <pierre.courtieu AT gmail.com>
- Subject: Re: [Coq-Club] functional induction, Equations plugin
- Date: Mon, 26 Nov 2012 12:29:25 +0100
Doing remember and the subsequent inversion automatically
would certainly spare us a lot of tedium. I don't like the current
setting where induction automatically generalizes over
non-variables.
Gert
On Nov 26, 2012, at 11:29 , Pierre Courtieu
<pierre.courtieu AT gmail.com>
wrote:
> Indeed, functional induction is similar to induction (it *is* a call
> to induction actually): it mostly works on variables. We could modify
> functional induction (and induction actually) to always do a
> "remember" when applied to non variable terms. I wonder if this would
> break some strange usage of induction.
>
> Has anyone ever user successfully "induction X" where X is something
> else than a variable?
>
> Best regards,
> Pierre
>
> 2012/11/25 Gert Smolka
> <smolka AT ps.uni-saarland.de>:
>> Thank you so much Jonas and Julien for
>> opening my eyes. I shall try to remember
>> to use remember when doing induction,
>> see my favorite solution below. Gert
>>
>> Require Import Recdef Omega.
>>
>> Definition gcd_order (p : nat * nat) : nat := let (x,y) := p in x+y.
>>
>> Function gcd (p : nat * nat) {measure gcd_order p} : nat :=
>> match p with
>> | (0,_) => 0
>> | (_,0) => 0
>> | (x,y) => match gt_eq_gt_dec x y with
>> | inleft (left _) => gcd (x, y-x)
>> | inleft (right _) => x
>> | inright xgty => gcd (x-y, y)
>> end
>> end.
>> - unfold gcd_order ; intros ; omega.
>> - unfold gcd_order ; intros ; omega.
>> Defined.
>>
>> Lemma gcd_ref x :
>> gcd (x,x) = x.
>>
>> Proof.
>> remember (x,x) as p.
>> functional induction (gcd p) ; inversion Heqp ; omega.
>> Qed.
- [Coq-Club] functional induction, Equations plugin, Gert Smolka, 11/25/2012
- Re: [Coq-Club] functional induction, Equations plugin, Jonas Oberhauser, 11/25/2012
- Re: [Coq-Club] functional induction, Equations plugin, Jonas Oberhauser, 11/25/2012
- Re: [Coq-Club] functional induction, Equations plugin, Julien Forest, 11/25/2012
- Re: [Coq-Club] functional induction, Equations plugin, Gert Smolka, 11/25/2012
- Re: [Coq-Club] functional induction, Equations plugin, Matthieu Sozeau, 11/25/2012
- Re: [Coq-Club] functional induction, Equations plugin, Jonas Oberhauser, 11/25/2012
- Message not available
- Re: [Coq-Club] functional induction, Equations plugin, Gert Smolka, 11/26/2012
- Re: [Coq-Club] functional induction, Equations plugin, AUGER Cédric, 11/26/2012
- Re: [Coq-Club] functional induction, Equations plugin, Pierre Courtieu, 11/26/2012
- Re: [Coq-Club] functional induction, Equations plugin, AUGER Cédric, 11/26/2012
- Re: [Coq-Club] functional induction, Equations plugin, Pierre Courtieu, 11/26/2012
- Re: [Coq-Club] functional induction, Equations plugin, Pierre Courtieu, 11/27/2012
- Re: [Coq-Club] functional induction, Equations plugin, AUGER Cédric, 11/26/2012
- Re: [Coq-Club] functional induction, Equations plugin, Gert Smolka, 11/26/2012
- Re: [Coq-Club] functional induction, Equations plugin, Matthieu Sozeau, 11/25/2012
- Re: [Coq-Club] functional induction, Equations plugin, Gert Smolka, 11/25/2012
- Re: [Coq-Club] functional induction, Equations plugin, Julien Forest, 11/25/2012
Archive powered by MHonArc 2.6.18.