The Coq mailing list

[Matthieu Sozeau <mattam AT mattam.org>]

Le 28 janv. 10 à 14:53, Guillaume Allais a écrit :

> Hi Flavio,
>
> I think that your definitions are a bit too complicated for what you  
> want to do. I took the second one and let Coq infer the measure  
> (when the measure is simple, it works well).
>
> Here is the code :
>
> __________________________________
>
> Fixpoint quotient (a b: nat) : nat := match a with
>    | 0 => 0
>    | S n => match b with
>               | 0 => 0
>               | S m => if (le_gt_dec m n) then S (quotient (n - m)  
> (S m)) else 0
> end
> end.

The system does not really infer a measure, it just checks a syntactic
guardness condition for each argument in turn. In this case it relies
on the fact that [minus] was cleverly defined as:

Fixpoint minus (n m : nat) :=
  match n with
    | 0 => n (* note n not 0 here *)
    | S k => match m with 0 => n (* n not (S k) here *)
               | S l => minus' k l
             end
  end.

If you change [n] to [0] or [n] to [S k] in these branches then the
syntactic check will be helpless when checking the definition of
quotient.

> In addition, from the Coq documentation, I couldn't find a difference
> between the constructions "Function" and "Program Fixpoint". Is there
> any conceptual difference between them?

Function is designed to generate a fixpoint equation and the inductive
graph of the function, whereas Program mainly provides support for  
defining
the function. There is a theory to work with the generated well-founded
fixpoints in Program.Wf though.

Hope this clarifies things a bit,
-- Matthieu