The Coq mailing list

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

Hi,

that trick with the Program Fixpoint for the proofs seems pretty useful as it effectively does well founded induction but without requiring me to prove well foundedness by hand.

Thank you all for your help!

Cheers,

Merlin

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

Hi,

Am Montag, den 05.03.2018, 14:59 +0000 schrieb Merlin Göttlinger:
> 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.

Ah, so Program Fixpoint defines it all right and you can prove all
obligations, but you are stuck proving something about the function? In
that case, ignore me, I misread your problem.

Here is an idiom I use when verifying Program Fixpoint functions is to
use Program Fixpoint for the proofs, i.e.

Program Fixpoint rule_transform_lemma
  `{UInverse opu} `{BInverse opb} (p : pro)
   (free_nominals : Stream nat) (ed : eqn)
  {measure (complexity p ed)} :
  Some_P (rule_Transform p free_nominals ed) := _ .
Next Obligation.
 (* now you can invoke rule_transform_lemma conveniently on all
 smaller arguments, in particular the arguments of the recursive
 calls to rule_transform in its definition *)

Again, I am not sure if this is really related to your problem. If not,
ignore me :-)

Joachim


> 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/
--
Joachim Breitner
  mail AT joachim-breitner.de
  http://www.joachim-breitner.de/