The Coq mailing list

[Julien Forest <julien.forest AT ensiie.fr>]

Hi,
Jonas gave you a way to make the proof but I will try to make something
for that king of problems (probably by mimicking the following proof) : 

Lemma gcd_ref x y :
  x=y -> gcd (x,y) = x.

Proof.
  (* Changing the first argument of gcd as a unique argument p and 
     keeping track of the value *)
  set(p:=(x,y)) in *.
  generalize (eq_refl p);unfold p at 2.
  clearbody p.
  revert x y.
  functional induction (gcd p);
(* Removing the reférences to p *)
  intros a b H; injection H;clear H;do 2 intro;subst. 
(* Jonas's proof *)
  auto.
auto.
simpl. intros de. exfalso ; omega.
auto.
simpl. intros de. exfalso ; omega.
Qed.

Kind regards, 
Julien

On Sun, 25 Nov 2012 14:29:47 +0100
Jonas Oberhauser 
<s9joober AT gmail.com>
 wrote:

> 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