The Coq mailing list

[Jonas Oberhauser <s9joober AT gmail.com>]

Am 25.11.2012 18:23, schrieb Matthieu Sozeau:
> Hi,
>
>    indeed Equations would remember the pair:
>
> Equations gcd (p : nat * nat) : nat :=
> gcd p by rec p gcd_rel :=
> gcd (pair 0 _) := 0 ;
> gcd (pair _ 0) := 0 ;
> gcd (pair x y) with gt_eq_gt_dec x y := {
>    | inleft (left p) := gcd (x, y - x) ;
>    | inleft (right p) := x ;
>    | inright xgty := gcd (x - y, y) }.
>
> Lemma gcd_ref x : gcd (x,x) = x.
> Proof.
>    funelim (gcd (x, x)); now (try (exfalso; omega)).
> Qed.
>
> -- Matthieu
>
> On 25 nov. 2012, at 12:03, Gert Smolka 
> <smolka AT ps.uni-saarland.de>
>  wrote:
>
> > 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.

Neat!

jonas