The Coq mailing list

[dehlinge AT dpt-info.u-strasbg.fr]

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

>
>
> Dear Christophe,
>
> You wrote,
>> 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
>
>
> It looks much simpler just to use the structure of this particular
> function which is very simple.
>
> If n is even then n+1 is odd and from f n = f (n+1) =f ((n +1) -3) = f
> (n-2)  by induction on n we get that (f n)
> should be  equal for all even n. Denote this value by a.
> Next,  if n >1 and n is odd then n-3 is even and f n = f (n-3) =a.
> So that  definition of the function could be as follows
> f n = 0       if n=1
> f n = a       if n >1
> where a is arbitrary constant to be specified.
>
> Regards,
> Jevgenijs Sallinens.
>
>