The Coq mailing list

[Yves Bertot <Yves.Bertot AT sophia.inria.fr>]

> 
> Oops ! Forgot the recursive calls...
> 
> The actual function I'm interested in is :
>       f n = 0         if n=1
>       f n = f (n+1)   if n is even
>       f n = f (n-3)   if n is odd
> 
> 

One of the functions that you use in the proof of WFL must be opaque.
This is often the case and in practice, I believe that you cannot reduce
well-founded recursive function to simple values.

I don't really know the answer of your question, but I have a comment
that may useful.  I don't know how to reduce the value f 1 to 0, but I 
know a way to prove that the result is 0.  Thus, I suggest you proceed 
by rewriting rather than by reduction.

If you want to prove that the function has a given value for a given
input, I think you should proceed by rewriting.  You should use
Fix_eq, and reason by well-founded induction over the order that was
used to define your function.  The rest of this message is a valid Coq 
script for coq-8.0.

Set Implicit Arguments.
Require Export Arith.
Require Export Even.
Require Export Peano_dec.
Require Export Wf_nat.

(* creating a well-founded relation between the argument value of a
recursive call and the original value*)

Inductive l : nat -> nat -> Prop :=
          L : forall n : nat, (even n)->(l (S n) n)
        | L2 : forall n : nat, n<>1->(odd n)->(l (n-3) n).


(* The script you gave for the proof of WFL seems to be wrong, but
   it not important. *)

Parameter WFL : well_founded l.

Definition f : nat->nat := Fix WFL (fun _ => nat)
        (fun (x:nat) (rec:(forall y : nat, l y x -> nat)) =>
                match (eq_nat_dec x 1) with
                  (left _) => 0
                | (right neqx1) =>
                        (match (even_odd_dec x) with
                          (left e) => rec _ (L e)
                        | (right o) => rec _ (L2 neqx1 o)
                        end)
                end).



Theorem f_is_constant_0 : forall n, f n = 0.
intros n; elim n using (well_founded_ind WFL); 
clear n; intros n Hrec.
rewrite Fix_eq.
(* This part of the proof is always systematic.  In the paper that
Antonia Balaa and I published in TPHOLS'2000, we argue that this proof 
can be done automatically, we had a prototype implementation, but it
became obsolete with the version changes in Coq. *)
2: intros x f0 g Heq; case (eq_nat_dec x 1);trivial.
2: intros Hneq; case (even_odd_dec x); trivial.
(* end of the systematic part. *)

(* At this step, you can reason on the computation performed in the
function, using the induction hypothesis Hrec to gather information about
recursive calls. When using this induction hypothesis, you need to
show again that the arguments of recursive calls are predecessors of
the initial argument for the relation l. *)

case (eq_nat_dec n 1); trivial.
intros Hneq; case (even_odd_dec n).
intros Heven; apply Hrec.
apply L;assumption.
intros Hodd; apply Hrec.
apply L2;assumption.
Qed.

I hope this helps.

  Yves