Janno (Dec 01 2020 at 11:20): 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?
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.
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)
Janno (Dec 01 2020 at 11:31):This is a good point! Sadly all my proofs by reflection deal with binders.
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.
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.
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.
Pierre-Marie Pédrot (Dec 01 2020 at 11:40):Can't you hack that with a non-recursive coinductive record or something?
Janno (Dec 01 2020 at 11:40):I think in the case of parameters
What do you mean by "parameters"?
Fabian Kunze (Dec 01 2020 at 11:41):Can you generalize over the "large" term before running vm-compute?
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
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.
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 ?
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.
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.
Pierre-Marie Pédrot (Dec 01 2020 at 11:45):Or a projection, for the primitive flavour.
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.
Pierre-Marie Pédrot (Dec 01 2020 at 11:46):I have to look deeper at that though to convince myself.
Janno (Dec 01 2020 at 11:46):Hm, sounds sketchy but also tempting. I'll play around with it a bit.
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.
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.
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 *)
It seems a bit too simple to be the solution. But it is a coinductive value not surrounded by a match.
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
Pierre-Marie Pédrot (Dec 01 2020 at 11:53):Because vm_compute will reduce the cofix arguments as well.
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 *)
maybe the trick doesn't apply to vm_compute :confused:
Janno (Dec 01 2020 at 11:58):Does it apply to some other reduction strategy?
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
Pierre-Marie Pédrot (Dec 01 2020 at 11:59):But that's the same as a thunk.
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
Janno (Dec 01 2020 at 12:01):Does Coq offer weak cbv as a reduction strategy?
Pierre-Marie Pédrot (Dec 01 2020 at 12:02):Probably not from the user-facing commands.
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
Pierre-Marie Pédrot (Dec 01 2020 at 12:06):Indeed. It'd be harder for vm/native though.
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: Jun 10 2023 at 23:01 UTC