The Coq mailing list

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

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