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: Jun 24 2024 at 01:01 UTC