The Coq mailing list

[Christian Doczkal <christian.doczkal AT ens-lyon.fr>]

Hi, 

The "non-Program Fixpoint" refers the to distinction between the normal 
"Fixpoint" command (which is mostly a nice syntactic wrapper around the "fix" 
construct in the term language of Coq) and the "Program Fixpoint" command, 
which is quite different and described here:

https://coq.inria.fr/refman/addendum/program.html?highlight=program%20fixpoint#program-fixpoint

In particular, "Fixpoint" only handles structural recursion, i.e., recursive 
calls only on proper subterms of the decreasing argument. 

Unless I'm missing something, in your example the termination of F depends on 
F being non-increasing with respect to some measure also satisfying [measure 
P < measure cons n P]. The second condition is required for the inner call, 
and the first for the subsequent outer call. If you can define such a 
measure, maybe you can use Program Fixpoint or the Equations plugin to define 
your functions. I'm not sure how well they handle nested recursion though.

Best,
Christian

On 7/11/19 11:46 PM, Morgan Sinclaire wrote:
> 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).

Attachment: signature.asc
Description: OpenPGP digital signature