Stream: Coq users

Topic: Recursive function with deep pattern matching


view this post on Zulip Jad Hamza (Nov 07 2020 at 08:05):

Hello,

I have a function f (n: nat) (input: Input): Output (a type-checker where Input is the input of the type-checking algorithm and Output is the derivation when it exists), defined using a Fixpoint (on n) by pattern matching on input using deep patterns. The definition is accepted quickly enough (5 secs), but then I cannot do any proof on it. The nested patterns are desugared into nested patterns with around 1300 lines.

For a lemma of the form forall n input, P (f n input) -> Q input, I'd like to do intros; destruct n; simpl in * to simply unfold the definition of the recursive function (I expect this is a delta reduction for f, then a fix reduction to unfold the fix and then beta reductions to substitute the n and input into the body of the function. I was able to do cbv delta in * (succeeds in a few seconds), but cbv fix in * or lazy fix in * doesn't finish in minutes, so I assume the issue is there. I guess unfolding the fix is very expensive, because it involves substituting the recursive calls of f with fix itself (30 calls * 1300 lines?). But in the end I don't want to substitute the 1300 lines, but rather the constant name f.

I'm thinking of some workarounds but I'm not sure what's best here:
1) If there is a quick workaround that allows me to quickly do the unfolding that would be great (maybe using special flags)
2) Split each case into its own "case handler" function, that given an input, generates the inputs for the recursive calls, and specify how to merge the results; then f can combine all of these in a parametric way, so that each function stays small. This is tedious but that should probably work
3) Define an inductive structure InputCase which has as many cases as inputs, and then define f by recursion on this structure. But I'm not sure how to do the recursive calls (maybe which a function from Input to InputCase, but that function will again be large because of the nested functions; at least it won't be recursive). I remember reading a Coq documentation page about setting this up but I can't find it anymore, does anyone have a link please?

Edit: I found this: https://sympa.inria.fr/sympa/arc/coq-club/2020-06/msg00126.html Unfortunately I can't try the trick with Function right now because it doesn't support notations, but I may try later. I also tried Equations but it seems too slow to accept the definition at with only 5-10 cases

view this post on Zulip Paolo Giarrusso (Nov 07 2020 at 11:21):

Splitting into subfunctions can be useful, especially if those subfunctions represent meaningful concepts which could support a theory.

view this post on Zulip Jad Hamza (Nov 07 2020 at 12:25):

Thanks! I'll try this


Last updated: Jan 28 2023 at 07:30 UTC