В чем разница между точкой фиксации программы и функцией в Coq?

Question

Кажется, они служат схожим целям. Единственное различие, которое я заметил, заключается в том, что пока Program Fixpoint примет сложную меру, как {measure (length l1 + length l2) }, Function кажется, отвергнуть это и позволит только {measure length l1},

Является Program Fixpoint строго сильнее, чем Functionили они лучше подходят для разных вариантов использования?

Answer 1

Это может быть не полный список, но это то, что я нашел до сих пор:

• Как вы уже упоминали, Program Fixpoint позволяет меру взглянуть на более чем один аргумент.
• Function создает foo_equation лемма, которая может быть использована для переписывания вызовов foo с его RHS. Очень полезно, чтобы избежать проблем, таких как Coq упрощенный для программы Fixpoint.
• В некоторых (простых?) Случаях Function может определить foo_ind лемма для индукции вдоль структуры рекурсивных вызовов foo, Опять же, очень полезно доказать вещи о foo без эффективного повторения аргумента завершения в доказательстве.
• Program Fixpoint можно обмануть поддержку вложенной рекурсии, см. /questions/38599710/vlozhennaya-rekursiya-i-program-fixpoint-ilifunction/38599727#38599727. Это также почему Program Fixpoint может определить функцию Аккермана, когда Function не могу.