The Coq mailing list

[Venanzio Capretta <Venanzio.Capretta AT mathstat.uottawa.ca>]

Dear Christophe,
 since your function is not structurally recursive, it is not 
guaranteed to terminate by its syntactic form. You have to prove 
termination. When you define it, it may well be partial. Unfortunately, 
Coq doesn't directly handle partial functions. Ana Bove and I developed 
a way to represent partial functions by characterizing their domain by 
an inductive predicate. In the case of your function, you would do this:

Inductive Dom: nat -> Set :=
 dom0 : (Dom O)
| dom_even : (n:nat)(even n) -> (Dom (plus n (1))) -> (Dom n)
| dom_odd : (n:nat)(odd n) -> (Dom (minus n (3))) -> (Dom n).

Fixpoint ff [n:nat; h:(Dom n)]: nat :=
Cases h of
 dom0 => O
| (dom_even n p h1) => (ff (plus n (1)) h1)
| (dom_odd n p h1) => (ff (minus n (3)) h1)
end.

In this case, the function can be proved to be total, that is, the 
domain predicate is always true:

Lemma all_Dom: (n:nat)(Dom n).
Proof.
(* easy *)
Defined.

Then you can remove the proof of the domain predicate from your function:

Definition f: nat -> nat:=
[n](ff n (all_Dom n)).

If you want to know more, you can find the following articles on my web 
page (http://www.science.uottawa.ca/~vcapr396/):

Nested General Recursion and Partiality in Type Theory (in TPHOLs 2001)
Modelling General Recursion in Type Theory
Recursive Functions with Higher Order Domains

Cheers,
 Venanzio



dehlinge AT dpt-info.u-strasbg.fr
 wrote:

> Dear Jevgenijs,
>
> actually, if n is odd then f n = f (n-3) = f (n-3+1) = f (n-2) = ... =
> f(n-4) = ... = f(n-6) = ... = f 1 = 0
> and if n is even, f n = f (n+1) = 0 (as n+1 is odd)
> So this function always yields 0.
> I probably should have stressed that point more, but what I really am
> insterested in is why what I have done so far does not work, and not
> finding any implementation for this function.
> f is just an arbitrary very simple example of a function that does not
> have a decreasing argument. What I'm trying to do is to find an easy,
> direct and generic way to circumvent the decreasing argument constraint,
> expressing such a function in Coq without fundamentally altering the
> algorithm it implements. This is why I tried Fix, which seems to be made
> for this purpose, although not very convenient and intuitive to use.
> Thus I don't want to perform any simplifications that would be specific to
> f, such as replacing it with fun _ => 0, as this is a completely different
> way to compute 0 from n. In other words, I'd like to build f in such a way
> that Extraction f yields something like:
> let rec f n =
>  if (eq_nat_dec n (S O))
>  then O
>  else if (even_odd_dec n)
>  then f (S n)
>  else f (minus n (S (S (S O))))
> I hope this clears things up a little.
> Regards,
>
> Christophe
>