The Coq mailing list

[Jean-Francois Monin <jean-francois.monin AT univ-grenoble-alpes.fr>]

Hi,

The trick explained by D. Larchey-Wendling in this talk
at TYPES'2019 could be an option. It works on mutual
recursive finctiosn as well.

Jean-Francois

On Tue, Apr 16, 2019 at 10:41:03AM +0200, Pierre Courtieu wrote:
> 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]