The Coq mailing list

[Jonas Oberhauser <s9joober AT gmail.com>]

Am 25.11.2012 13:53, schrieb Gert Smolka:
> I wonder why functional induction doesn't work even for
> simple examples like gcd (see below).  Would the Equations
> plugin perform any better?
> - 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 y :
>    x=y -> gcd (x,y) = x.
>
> Proof.
>    functional induction (gcd(x,y)).
>    - (* Already the first case is unprovable *)

Hello Mr Smolka,

Here the proof. Your lemma is a corollary. It would've been a nice 
surprise if coq remembered in the induction that x and y are the two 
compontents of the tuple that we "do induction over", but alas it doesn't.

Definition pi1 {X Y} (p : X * Y) := let (x,_) := p in x.
Definition pi2 {X Y} (p : X * Y) := let (_,y) := p in y.

Lemma gcd_ref p :
  pi1 p = pi2 p -> gcd p = pi1 p.

Proof.
  functional induction (gcd p).

auto.
auto.
simpl. intros de. exfalso ; omega.
auto.
simpl. intros de. exfalso ; omega.
Qed.

Kind regards,

jonas