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

Question

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?

Hinds

Incidentally, the Coq v8.7 roadmap says their implementations are going to be merged. – Parker

This is a good question, I recommend going to Coq's gitter if you need a detailed answer as the people knowledgeable about it don't read SO AFAIK; the implementation of Function and Program were done by different persons and in different contexts so indeed their set of features is not strictly a subset of the other. There are plans to merge both on them in a new "Equations" plugin, but that won't happen in 8.7, even if a lot of progress has been made. That being said, I think that you would usually better off with Program if you care about compatibility with future Coq releases. – Roy

Answer 1

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://mcmap.net/q/901900/-nested-recursion-and-program-fixpoint-or-function. This is also why Program Fixpoint can define the Ackermann function when Function cannot.

Dovetail

It also seems impossible to define the Ackermann function with Function, but Program Fixpoint can do it. – Parker

Thanks, added that to the answer. – Dovetail