Search code examples
coqtotality

What's the difference between Program Fixpoint and Function in Coq?

They seem to serve similar purposes. The one difference I've noticed so far is that while Program Fixpoint will accept a compound measure like {measure (length l1 + length l2) }, Function seems to reject this and will only allow {measure length l1}.

Is Program Fixpoint strictly more powerful than Function, or are they better suited for different use cases?

Solution

  • This may not be a complete list, but it is what I have found so far:

    • As you already mentioned, Program Fixpoint allows the measure to look at more than one argument.
    • Function creates a foo_equation lemma that can be used to rewrite calls to foo with its RHS. Very useful to avoid problems like Coq simpl for Program Fixpoint.
    • In some (simple?) cases, Function can define a foo_ind lemma to perform induction along the structure of recursive calls of foo. Again, very useful to prove things about foo without effectively repeating the termination argument in the proof.
    • Program Fixpoint can be tricked into supporting nested recursion, see https://stackoverflow.com/a/46859452/946226. This is also why Program Fixpoint can define the Ackermann function when Function cannot.