The Coq mailing list

[Jean-Christophe Filliatre <Jean-Christophe.Filliatre AT lri.fr>]

Thery Laurent writes:
 > 
 > if having a clean extraction is important, the usual trick to get 
 > simplification back is to use rewriting.
 > 
 > For this, one way to go is to first define a predicate R with the idea
 > that  n R m means m = f(n), and shows that it is injective.

It is indeed a nice solution and it gives the expected extraction, namely:

======================================================================
let rec f x =
  match eq_nat_dec x (S O) with
    | Left -> O
    | Right ->
        (match even_odd_dec x with
           | Left -> f (plus x (S O))
           | Right -> f (minus x (S (S (S O)))))
======================================================================

However  you get  exactly the  same extraction  from a  direct  use of
well_founded_induction, since there is an obvious variant for function
f:

======================================================================
Require Omega.
Require Export Even.
Require Export Peano_dec.
Require Export Wf_nat.

Definition variant (n:nat) : nat := if even_odd_dec n then n+2 else n.

Definition f : nat -> nat.
refine 
  (well_founded_induction (well_founded_ltof _ variant) (fun _ => nat) 
    (fun x frec => if eq_nat_dec x 1 then 0
                   else if even_odd_dec x then frec (x+1) _
                   else frec (x-3) _));
unfold variant,ltof; 
case (even_odd_dec x); 
case (even_odd_dec (x+1)); 
case (even_odd_dec (x-3));
intuition;
try solve [elim (not_even_and_odd (x+1)); auto with arith];
(assert (x=0 \/ x=1 \/ x=2 \/ x >= 3); [ omega | intuition ]);
subst; inversion_clear o.
inversion_clear H; inversion_clear H0.
Defined.
======================================================================

Note the use of the `refine' tactic which is precisely given the
expected program, as a reminiscence of the Program tactic.

Hope this helps,
-- 
Jean-Christophe