14

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?

Anton Trunov
  • 15,074
  • 2
  • 23
  • 43
LogicChains
  • 4,332
  • 2
  • 18
  • 27
  • 2
    Incidentally, the [Coq v8.7 roadmap](https://github.com/coq/roadmaps/blob/master/text/roadmap-8.7.md#implementation-cleanups) says their implementations are going to be merged. – Anton Trunov Jun 17 '17 at 15:35
  • 4
    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. – ejgallego Jun 17 '17 at 15:38

1 Answers1

6

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.
Joachim Breitner
  • 25,395
  • 6
  • 78
  • 139