Consider the following fixpoint:
Require Import Coq.Lists.List.
Import ListNotations.
Inductive my_type: Type:=
| Left: my_type
| Right: my_type
.
Fixpoint decrease (which: my_type) (left right: list my_type) : list my_type :=
match which with
| Left =>
match left with
| [] => []
| a::tl => decrease a tl right
end
| Right =>
match right with
| [] => []
| a::tl => decrease a left tl
end
end.
Coq rejects the following fixpoint because it can not guess the decreasing fixpoint (sometimes the left
list looses its head, sometimes it is the right
one).
This answer shows that one can solve this by using a Program Fixpoint
and specifying a {measure ((length left)+(length right))}
.
My questions are:
- What is the difference between a regular
Fixpoint
and aProgram Fixpoint
? - Is it possible to explicit the decreasing argument in a regular
Fixpoint
? - What is the
Next Obligation
goal ?
The
Fixpoint
command in Coq constructs a recursive function using Coq's primitivefix
, which checks for structural recursion to ensure termination. This is the only recursion in Coq, and all other techniques ultimately desugar to afix
of some sort.Program Fixpoint
is a feature of Program, which allows writing definitions in a slightly extended language that are then compiled into Coq definitions.Program Fixpoint
accepts any recursive function, generates an appropriate proof obligation that shows the function terminates (by decreasing some measure of its arguments on each recursive subcall), and then packages up the definition and termination proof into a Coq definition that structurally decreases an argument. If that sounds magical it basically is, but CPDT gives a good explanation of how to do this kind of encoding.Yes, you can add a
{struct arg}
annotation to explicitly specify which argument is structurally decreasing:Fixpoint decrease (which: my_type) (left right: list my_type) {struct right} : list my_type
. This doesn't help for your example, since your function doesn't in general structurally decrease either argument. All primitivefix
constructs have astruct
annotation, but Coq can usually infer it automatically when you write aFixpoint
. For example, here'sNat.add
:You get two types of goals from
Next Obligation
withProgram Fixpoint
: first that each subcall has a smaller argument (usingmeasure
, "smaller" is defined using < on nats), and second, that the "smaller" relation is well-founded; this is, it has no infinitely descending sequences of smaller and smaller objects. I'm not sure whyProgram Fixpoint
doesn't do this automatically forNat.lt
, given that it should know the relevant theorem. Note thatProgram
has more features than just more general recursion, so it can generate other goals related to those features as well, depending on the definition you write.