The Coq mailing list

[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.