The Coq mailing list

[Matthieu Sozeau <matthieu.sozeau AT gmail.com>]

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.