Stream: CUDW 2020

Topic: WG: vm_compute support for proof by partial reflection


view this post on Zulip Janno (Dec 01 2020 at 11:20):

(I hope it is okay to just start a new topic for WG proposals. Let me know if I should so something else) I often deal with proofs that make use of reflection but with the added difficulty that reified terms contain subterms that must not be reduced (both because the result will be visible to the user but also because they may be huge terms). As far as I can tell I cannot use vm_compute in this scenario because there is no control over what gets reduced. I was wondering if there was a way to change that. I vaguely remember somebody telling me that some of the infrastructure might already exist but I might be getting this mixed up with native_compute. Is anyone else interested in this?

view this post on Zulip Fabian Kunze (Dec 01 2020 at 11:26):

You know of the technique to have an list env : list reflectionDomainof "atomic" terms that works as "environment" and, instead of an arbitrary "constant (x:reflectionDomain)" constructor, have an "constant (index:Fin.t (length env))" to refere to those things in the environment?

This of course does not work in all use cases, for example, with binders inside the reflectionDomain it gets very hairy.

view this post on Zulip Fabian Kunze (Dec 01 2020 at 11:28):

The added bonus is that one can make use of syntactic equality of non-reflected constants. (I think this trick is from CPDT)

view this post on Zulip Janno (Dec 01 2020 at 11:31):

This is a good point! Sadly all my proofs by reflection deal with binders.

view this post on Zulip Janno (Dec 01 2020 at 11:32):

Apart from that I fear tracking the environment might add quite a bit of complexity to longer-running reflective tactics where new terms are introduced (via TC search, for example). But I haven't worked with this approach so maybe I am overestimating the complexity.

view this post on Zulip Janno (Dec 01 2020 at 11:34):

This is a good point! Sadly all my proofs by reflection deal with binders.

To clarify: by this I mean that the types of terms in the environment are not uniform. They live under different binders.

view this post on Zulip Fabian Kunze (Dec 01 2020 at 11:39):

I think in the case of parameters, one could use a heterogenous list, as the typing can still be "guaranteed" in the constant constructor.
But yes, this is certainly not the most easy way to do it, if it even works. some way to lock subterms for vm_compute would be a lot easier.

view this post on Zulip Pierre-Marie Pédrot (Dec 01 2020 at 11:40):

Can't you hack that with a non-recursive coinductive record or something?

view this post on Zulip Janno (Dec 01 2020 at 11:40):

I think in the case of parameters

What do you mean by "parameters"?

view this post on Zulip Fabian Kunze (Dec 01 2020 at 11:41):

Can you generalize over the "large" term before running vm-compute?

view this post on Zulip Fabian Kunze (Dec 01 2020 at 11:41):

I mean that if the type of the constant-atom to reflect depends on parameters, like the values of binders above

view this post on Zulip Janno (Dec 01 2020 at 11:43):

My terms usually depend on nested telescopes of some form. It might still work to find a well-typed representation for the environment but it sounds much, much more complicated than stopping vm_compute from reducing certain terms or maybe just reducing a given list of terms.

view this post on Zulip Janno (Dec 01 2020 at 11:43):

Can't you hack that with a non-recursive coinductive record or something?

Can you elaborate, @Pierre-Marie Pédrot ?

view this post on Zulip Pierre-Marie Pédrot (Dec 01 2020 at 11:44):

I think I have already seen some clever use of coinductive types to block reduction.

view this post on Zulip Pierre-Marie Pédrot (Dec 01 2020 at 11:44):

Because they have this weird rule that prevents reducing if you're not inside a match.

view this post on Zulip Pierre-Marie Pédrot (Dec 01 2020 at 11:45):

Or a projection, for the primitive flavour.

view this post on Zulip Pierre-Marie Pédrot (Dec 01 2020 at 11:46):

By wrapping a big value inside a coinductive record, I believe you can get something that looks like a thunk but doesn't allow strong reduction.

view this post on Zulip Pierre-Marie Pédrot (Dec 01 2020 at 11:46):

I have to look deeper at that though to convince myself.

view this post on Zulip Janno (Dec 01 2020 at 11:46):

Hm, sounds sketchy but also tempting. I'll play around with it a bit.

view this post on Zulip Janno (Dec 01 2020 at 11:49):

Can you generalize over the "large" term before running vm-compute?

In my current use case I operate on terms that do not actually appear in the current goal. The tactic builds a large proof term with intermediate steps which are never reflected in the state of the proof engine. That means generalizing at the end (when the proof term is given to the proof engine) could work and would help Qed, I suppose. But the intermediate steps would also benefit from vm_compute to perform simplification and other operations on the reified terms. I am not sure if I could easily make use of generalize for those intermediate steps.

view this post on Zulip Matthieu Sozeau (Dec 01 2020 at 11:51):

Pierre-Marie Pédrot said:

By wrapping a big value inside a coinductive record, I believe you can get something that looks like a thunk but doesn't allow strong reduction.

For sure that is used a lot in Agda to prevent computations, so it should apply to Coq as well.

view this post on Zulip Janno (Dec 01 2020 at 11:52):

I think I don't understand the trick yet. Should this work?

CoInductive stop {X} : Type := { go : X }.
Eval vm_compute in {| go := 1 + 1 |}. (* go := 2 *)

view this post on Zulip Janno (Dec 01 2020 at 11:52):

It seems a bit too simple to be the solution. But it is a coinductive value not surrounded by a match.

view this post on Zulip Pierre-Marie Pédrot (Dec 01 2020 at 11:53):

You probably have to throw a cofix somewhere, although now I don't see how to do that in any way that will satisfy your requirements

view this post on Zulip Pierre-Marie Pédrot (Dec 01 2020 at 11:53):

Because vm_compute will reduce the cofix arguments as well.

view this post on Zulip Janno (Dec 01 2020 at 11:55):

I am sure this is also not what you mean but I thought I'd try it anyway:

Eval vm_compute in (cofix go (u : unit) := {| go := 1 + 1 |}) tt. (* (cofix Fcofix (x : unit) : stop := {| go := 2 |}) tt *)

view this post on Zulip Pierre-Marie Pédrot (Dec 01 2020 at 11:56):

maybe the trick doesn't apply to vm_compute :confused:

view this post on Zulip Janno (Dec 01 2020 at 11:58):

Does it apply to some other reduction strategy?

view this post on Zulip Pierre-Marie Pédrot (Dec 01 2020 at 11:59):

Clearly if you're in weak cbv, you won't compute under a cofix blox

view this post on Zulip Pierre-Marie Pédrot (Dec 01 2020 at 11:59):

But that's the same as a thunk.

view this post on Zulip Pierre-Marie Pédrot (Dec 01 2020 at 12:00):

The difference is that the result is cached so that you effectively implement call-by-need instead of call-by-name

view this post on Zulip Janno (Dec 01 2020 at 12:01):

Does Coq offer weak cbv as a reduction strategy?

view this post on Zulip Pierre-Marie Pédrot (Dec 01 2020 at 12:02):

Probably not from the user-facing commands.

view this post on Zulip Matthieu Sozeau (Dec 01 2020 at 12:05):

weak cbv is something I've wished for a few times, it should not be hard to make it available

view this post on Zulip Pierre-Marie Pédrot (Dec 01 2020 at 12:06):

Indeed. It'd be harder for vm/native though.

view this post on Zulip Janno (Dec 01 2020 at 12:29):

What about my original question of restricting vm_compute to certain terms? Or maybe support for a "do not cross" feature where reduction can be stopped from going under applications of certain terms? How hard would it be to implement these features?


Last updated: Oct 16 2021 at 07:02 UTC