Stream: Coq users

Topic: Custom reduction


view this post on Zulip James Wood (Sep 13 2022 at 14:25):

I've written a recursive function, and I want to just have a look at what output it produces for an example input (closed term). The output has quite a complex inductive type, containing record types, function types, &c. I find that Eval cbv, Eval vm_compute, &c take more time than I can wait for, and Eval cbn, Eval simpl, &c don't normalise as deeply as I would like. Is there some sort of middle ground, where I can reduce the whole term to WHNF and then reduce each of the arguments of the resulting head constructor to WHNF, or something like that? Being able to do so with some amount of interactivity would be nice.

view this post on Zulip Michael Soegtrop (Sep 13 2022 at 15:44):

This is odd. If you apply a function to a closed term, Eval vm_compute and even Eval cbv should be reasonably fast.

I see two possibilities:

You can analyze the run time for increasing term complexity with Time Eval cbv ... and analyse the asymptotic behavior of your code.

In case I need to do deep reductions on terms with variables, I usually use an explicit delta symbol list with cbv, say cbv delta [sym1 sym2 sym3 ...] beta iota zeta.. The symbol list can be lengthy - I am working on Ltac2 functions to manage symbol lists, say all symbols from module X, but this is not yet ready.

view this post on Zulip James Wood (Sep 13 2022 at 15:58):

I think what slows it down is that, deep down, there are two bijections (represented as two functions and two proofs) in the output which I don't really care about seeing, but are very big (even just the functions are big match expressions, which I think were ultimately generated by Equations). So maybe this suggests that limiting delta-reductions will give me a good enough result.

view this post on Zulip Michael Soegtrop (Sep 13 2022 at 16:06):

OK, to get fast you should separate computational stuff from proofs. cbv honors the opaqueness of proofs, but afaik vm compute and native compute don't, so this can get quite ugly. In general you should write a function without any proof content and prove something about this function.

view this post on Zulip James Wood (Sep 13 2022 at 16:12):

The functions in the bijections are computational, it just happens that I don't want to see them in their entirety.

view this post on Zulip Michael Soegtrop (Sep 13 2022 at 16:16):

Please note that Equations also comes with dedicated simplification functions for the functions it creates (which are opaque by default afair, so cbv wouldn't expand them). Maybe this opaqueness of Equations defined functions is your problem. You can fix this by either using Equations simplifier or by making them transparent - otherwice cbv won't expand them.

view this post on Zulip Michael Soegtrop (Sep 13 2022 at 16:20):

Such unexpanded functions can lead to arbitrary term blow up.

view this post on Zulip Paolo Giarrusso (Sep 14 2022 at 14:12):

cbv honors the opaqueness of proofs, but afaik vm compute and native compute don't, so this can get quite ugly.

You're right about Opaque, but they all honor Qed, which is the right way to make proofs opaque.

view this post on Zulip Paolo Giarrusso (Sep 14 2022 at 14:14):

@James Wood it might be appropriate to "seal" those functions — using coq-elpi's mlock commands (or the ssreflect pattern by hand) — or project out the relevant parts from the output

view this post on Zulip Paolo Giarrusso (Sep 14 2022 at 14:15):

the problem with sealing, of course, is that it'd made those functions non-computational, which might not be appropriate.

view this post on Zulip James Wood (Sep 14 2022 at 14:18):

To address the easy parts: I'm not projecting out the relevant parts because they're underneath inductive constructors. I know there are tricks I can do to get around that, but it takes effort. I'm starting to think, though, that this is the lowest effort I can achieve.

view this post on Zulip Michael Soegtrop (Sep 14 2022 at 14:35):

@Paolo Giarrusso : thanks, interesting, I didn't know that - I assumed Qed just sets the strategy. But what does Qed do then technically? Do definitions have something like an "original opaqueness"?

view this post on Zulip Paolo Giarrusso (Sep 14 2022 at 14:37):

Yes, there is an original opacity: Qed produces something closer to an axiom, because the name is not definitionally equal to the body.

view this post on Zulip Paolo Giarrusso (Sep 14 2022 at 14:37):

Moreover, Opaque cannot replicate this behavior, because existing terms could become ill-typed.

view this post on Zulip Paolo Giarrusso (Sep 14 2022 at 14:39):

Ssreflect's module sealing uses the only point to make things opaque "a bit later": module sealing.

view this post on Zulip Paolo Giarrusso (Sep 14 2022 at 14:41):

https://github.com/LPCIC/coq-elpi/blob/master/apps/locker/README.md#example-of-mlock is a good summary of the pattern, if that helps


Last updated: Jan 31 2023 at 13:02 UTC