The Coq mailing list

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

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