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
Splitting into subfunctions can be useful, especially if those subfunctions represent meaningful concepts which could support a theory.
Thanks! I'll try this
Last updated: Oct 13 2024 at 01:02 UTC