The Coq mailing list

[Morgan Sinclaire <morgansinclaire AT boisestate.edu>]

Summary: I've received the error message "Only structural decreasing is supported for a non-Program Fixpoint", I have little clue what it means, and googling this message turned up no actual results. In particular I don't get what it means exactly by "structural decreasing" and "non-Program".

~~~

I have defined a Type called "ptree", which is an infinitary tree with a certain complicated structure, and I'm defining a function (which I'll just call F) that takes in a (P : ptree) as well as some simpler inputs, and returns a ptree. Abstracting away some other details, the definitions look roughly like this:

Inductive ptree : Type :=
| node : nat -> ptree
| cons : nat -> ptree -> ptree
[...]
.

 

Fixpoint F (P : ptree) [...] : ptree :=
match P with
| node n => P
| cons n P' => cons n (F (F P'))
[...]
end.

Now, when I define F like this, I get the familiar "Cannot guess decreasing argument of fix" because of the double application of F. If I change "F (F P')" to "F P'" then the issue goes away, so on some level Coq recognizes that P gets simpler at each stage. However, when I try to tell Coq this by changing the first line to:

Fixpoint F (P : ptree) [...] {measure P} : ptree :=

Then I instead get the error message:

Only structural decreasing is supported for a non-Program Fixpoint

And I don't understand what this means, or how to tell Coq to recognize that P is simplifying, just like in the case where we have the single application F P' instead.

(I believe I know of a way to avoid this double application of F in my situation, but that workaround is tedious, and besides I'm quite interested in understanding what's going on here).