The Coq mailing list

[Merlin Göttlinger <megoettlinger AT gmail.com>]

Hi,

recurse is only a fold which accumulates the resulting failure (list eqn) together and passes the new free_nominal context along.

It's type already ensures that the measure decreases on the arguments rule_transform is called with. Otherwise the function wouldn't typecheck due to Program not unfolding higher order functions in its body if I'm not mistaken.

I will try inlining that by unrolling the fold and see if Functional Scheme is then happier with it.

Thanks for your help!

Cheers,

Merlin

Joachim Breitner <mail AT joachim-breitner.de> schrieb am Mo., 5. März 2018 um 15:37 Uhr:

Hi,

this looks like nested recursion through a function called [recurse].
It might work if you eta-expand the argument to [rule_transform] in
[recurse], and give [recurse] a more helpful type that promises to only
pass smaller things to it..

But a simpler way of testing if that helps is to inline the definition
of recurse. You can do so in a

  let recurse := … in

_in the body_ of the definition of [recurse].

See https://stackoverflow.com/a/46859452/946226 for how I tackle nested
recursion with Program Fixpoint.

cheers,
Joachim


Am Montag, den 05.03.2018, 12:59 +0000 schrieb Merlin Göttlinger:
> Hi,
>
> to give the complete definition in a self contained way I would have to include many many files, but here is the fixpoint definition if that helps: https://gist.github.com/mgttlinger/6b37299dac61b07348b4feddc6e1d375
> The EnvT it returns is basically (nat -> nat) * failure (list eqn) where failure is a sum where the left and right type are the same. "fail:" and "succ:" are notations for the sum injections.
> The free_nominals parameter is a stream (nat -> nat) of fresh "names" in the context the function is called from, which is modified when names are used in recursive calls.
>
> It doesn't involve dependent types (or at least not in an obvious way) but the term that Program generates is packed full of existT and proofs (given that the function generates over 200 obligations) and is 12k lines long...
>
> Cheers,
> Merlin
>
>
> Pierre Courtieu <pierre.courtieu AT gmail.com> schrieb am Mo., 5. März 2018 um 12:52 Uhr:
> > Hi
> > Usually well founded induction (using the same  well founded relation than the one used for your function) is the way to go.
> >
> > If your function has dependent types this is indeed not covered by Function. Can you give your definition?
> >
> > Best regards
> > Pierre
> >
> > Le lun. 5 mars 2018 à 10:05, Merlin Göttlinger <megoettlinger AT gmail.com> a écrit :
> > > Hi all,
> > >
> > > I have a complicated Program Fixpoint that gets folded over a list of inputs and involves a state monad (allowing the function to choose fresh variable names during its processing of the input syntax). The initial state for that is calculated from the input list. (The resulting state after the fold is discarded)
> > >
> > > Now I want to prove that this transformation is actually correct with respect to a notion of equivalence I defined, but I find myself in the situation that induction over the input list doesn't work because the generated IH is not usable (if the input list has one element more, the free variable names also change) and also proving that this Program Fixpoint is correct w.r.t. my equivalence doesn't work by "normal" induction for the same reason.
> > >
> > > What is the way to go here?
> > >
> > > I heard about functional induction but Functional Scheme isn't able to process my fixpoint and after computing for a few seconds fails with Error: Cannot define graph(s) for rule_transform_func
> > >
> > > I heard about well-founded induction. If that is the way to go, is there a way to reuse that information that Program must have generated in an elegant way?
> > >
> > > Cheers,
> > > Merlin
> > >
--
Joachim “nomeata” Breitner
  mail AT joachim-breitner.de
  https://www.joachim-breitner.de/