The Coq mailing list

[Pierre Courtieu <pierre.courtieu AT gmail.com>]

Hi,

In general Function does not deal well with higher order except in
very simple cases. However in your case you are hitting a limit of
inductive scheme generation of coq itself if i understand well.

Function generates the graph of foo (Print R_foo) correctly imho, but
the induction scheme of R_foo does not have the recursion hypothesis
you want either.

I suppose you can give a try to the Equation plugin (but higher order
may lead to axioms?) or prove you scheme by hand.


Le mar. 16 avr. 2019 à 09:13, John Wiegley 
<johnw AT newartisans.com>
 a écrit :
> ...
> Function foo' (h : Higher) : Higher :=
>   match h with
>   | Ctor f => Ctor (fun x => foo' (f x))
>   | Neg x => Rec (bar' x)
>   | Rec x => Rec (foo' x)
>   end
> with
>   bar' (h : Higher) : Higher :=
>   match h with
>   | Ctor f => Ctor (fun x => bar' (f x))
>   | Neg x => Rec (foo' x)
>   | Rec x => Rec (bar' x)
>   end.
>
> (** Why does it now fail to build the graph?

This time you hit a limtation of Function itself with higher order.

Hope this helps,
Pierre

>     Warning: Cannot define graph(s) for foo', bar'
>     [funind-cannot-define-graph,funind]