Stream: Ltac2

Topic: pi quantifier

Michael Soegtrop (Nov 16 2022 at 15:05):

Elpi provides a pi quantifier which allows to easily move under binders. With this it is e.g. easy to write a tactic which recurses over a term producing a modified term, e.g. a term which is fully computed in certain subterms and otherwise left untouched.

I am not sure how I would do this (fully compute certain sub terms of a term) best in Ltac2. Should I construct the modified term as kind and use Constr.make? Is this efficient if done recursively? Higher level methods don't seem to work, e.g. it doesn't seem to be possible to bind the bound term of a forall with match!.

Jason Gross (Nov 16 2022 at 16:44):

Are you talking about https://github.com/coq/coq/issues/16421?

Short answer: Yes, you need to use Constr.Unsafe.kind and Constr.Unsafe.make and be very careful about doing reduction on terms with unbound Vars/Rels. Or if you're willing to pay a superlinear cost in the number of binders you can use Constr.in_context. Or implement a multi-binder version of this (I thought I had an open issue for this but apparently not.)

Long answer:
After spending some time rewriting reification in Ltac2, I've been coming to the view that Ltac2 does not expose an adequately performant API for dealing with binders. (cc @Pierre-Marie Pédrot ) In particular, I think there needs to be a distinction between tactics that need to take place in a goal (such as intro) and tactics that need a valid context/evar map but no goal (such as cbv delta, simpl, and Constr.type). (And of course there are the constructs that don't need either, like match, function application, fun, (), etc.)

There are two ways, currently, to recurse under binders: one is to use Constr.Unsafe.kind and deal with ill-scoped terms. This is fine for things like Constr.make, but not for things like Constr.type. The other is to use Constr.in_context, which is for constructing constrs and is very slow because every binder you recurse under allocates a new evar for the goal and this incurs (last I checked) linear overhead.

There should also be a way to recurse under binders in a way that modifies the current context/evar map in O(1) and sets it up so that there are no goals under focus (a la Ltac2 Eval). This should allow things like match! to work right. (It might be nice to be able to match over the hypotheses without matching over the goal here, but that's not required.)

Gaëtan Gilbert (Nov 16 2022 at 16:48):

In particular, I think there needs to be a distinction between tactics that need to take place in a goal (such as intro) and tactics that need a valid context/evar map but no goal (such as cbv delta, simpl, and Constr.type)

maybe we should expose functions which take an explicit context instead of the goal context?

There should also be a way to recurse under binders in a way that modifies the current context/evar map in O(1) and sets it up so that there are no goals under focus (a la Ltac2 Eval).

That's not possible because of renaming isn't it? and there is no current context without a goal

Jason Gross (Nov 16 2022 at 16:49):

https://github.com/coq/coq/issues/16352

Jason Gross (Nov 16 2022 at 16:51):

In particular, I think there needs to be a distinction between tactics that need to take place in a goal (such as intro) and tactics that need a valid context/evar map but no goal (such as cbv delta, simpl, and Constr.type)

maybe we should expose functions which take an explicit context instead of the goal context?

That would also work well. I'd be fine with having a layer of tactics that take things explicitly, and have the monadic layer built on top of that. (Not sure how to expose this in the types, though, which seems desirable?) But I suspect there's a reason that @Pierre-Marie Pédrot built Ltac2 around assuming there's a goal around, rather than having a lower level of tactics that don't assume a goal, though?

Jason Gross (Nov 16 2022 at 16:54):

There should also be a way to recurse under binders in a way that modifies the current context/evar map in O(1) and sets it up so that there are no goals under focus (a la Ltac2 Eval).

That's not possible because of renaming isn't it? and there is no current context without a goal

What does renaming have to do with it? Just have the context should just store a hash map of the currently used identifiers and have the tactic error if the name you give is already in use. (O(log(n)) in the size of the context is also fine, if need be.)

Gaëtan Gilbert (Nov 16 2022 at 16:54):

Not sure how to expose this in the types, though, which seems desirable?

Ltac2 Type named_context. (* + APIs to treat it as a list of decls etc *)

Ltac2 @ external goal_context : unit -> named_context := ...
Ltac2 @ external type_in_context : named_context -> constr -> constr := ...

?

Jason Gross (Nov 16 2022 at 17:05):

Yes, that seems good, and I'd be quite happy to see a PR merged adding named_context, ability to push, pop, get list of things, etc, the full API.

I'm saying that it might be nice to have type-level information about which tactics need to happen in a goal and which ones work in Ltac2 Eval or w/e. (Any maybe more generally for tactics that require focusing vs not.) But maybe exposing this in the types and also having polymorphism over it is too ambitious.

Michael Soegtrop (Nov 16 2022 at 17:08):

@Jason Gross : did you look into the performance of Elpi's pi x\ decl x X T => and pi x\ def x X T V => constructs?

See (https://github.com/VeriNum/vcfloat/pull/7/files) for an example (a simple elpi tactic which runs cbv only under applications of a given head symbol).

@Enrico Tassi : can you say something on the question if these constructs are O(1) in the number of binders processed?

Jason Gross (Nov 16 2022 at 17:08):

No, I haven't managed to test out Elpi. How's the performance?

Michael Soegtrop (Nov 16 2022 at 17:11):

For the things I managed to write in both Ltac2 and Elpi it is about the same, maybe Elpi is a few 10% faster. It is hard to measure because even on largish terms both run in the one digit ms area per call. And I didn't manage to write larger things with equivalent functionality in both.

Michael Soegtrop (Nov 16 2022 at 17:14):

What I can say is that especially this kind of stuff is much less obscure in Elpi. But I guess one should have a bit of Prolog experience - otherwise the relational style of writing programs is a bit weird (I did write Prolog for a while).

Enrico Tassi (Nov 16 2022 at 21:24):

Michael Soegtrop said:

Jason Gross : did you look into the performance of Elpi's pi x\ decl x X T => and pi x\ def x X T V => constructs?

See (https://github.com/VeriNum/vcfloat/pull/7/files) for an example (a simple elpi tactic which runs cbv only under applications of a given head symbol).

Enrico Tassi : can you say something on the question if these constructs are O(1) in the number of binders processed?

About the complexity of crossing a binder, in Elpi it is made of

• match over a term, eg the rule's head is foo (fun _ Ty F), this is linear in the size of the pattern if the variables are linear
• run pi x\, constant
• substitute x for the bound variable in F, eg writing F x, very likely constant in practice (that is the main new idea in Elpi, based on De Bruijn levels and a language fragment called $L_\lambda^{\beta_0}$ which occurs often in practice)
• assume bar x via =>, this is indexing 2 integers (bar and x) on two patricia trees, likely log(n)

But, to be honest there are other operations which are not necessarily constant time, because Elpi is a quite naive prolog interpreter after all.
You can start to see them if you map a spine of fun nodes of size 150 or so. Below that you should have no visible problem according to my experience.

In a language like ML there are two ways I know to cross binders in an educated way:

• in the language, like MLTS and Mtac2, which have something like pi built in
• in the API, a la bindlib, which forces you to follow roughly the same discipline often phrased "no such a thing as a free variable"

Neither give you something like =>, and this is the reason why I wanted Elpi to be rule based. If the language is not, then one has to encode the context (eg a list you pass around) or code open recursion (you don't call self directly, but via a first class dispatcher one can override).
I'd advocate an API like bindlib for Ltac2, at least for the user which does not care about perf too much, but wants to get the job done with no headaches.

Nice to hear Elpi is on par with Ltac2 on your measurements. IMO there is no actual reason for it to be true, e.g. crossing the language boundary is much faster in Ltac2 since terms don't need to be converted... well, apparently you don't do that too often. But the languages are so different that the only thing one can really do is to run a wall clock, IMO.

Michael Soegtrop (Nov 18 2022 at 08:48):

Some concluding remarks on this: I sat down and wrote Ltac2 functions which recurse over a term, does reductions in specific parts of the term, puts the result together again and change the goal with it. This is all based on the Constr.Unsafe interface.

Up to now I used the Constr.Unsafe interface a lot to analyse terms (reification), but I was a bit scared away to use it for constructing terms - mostly by the name and the prospect of slowness of additional type checking when putting unsafe terms together again. When doing reification I constructed terms using constr: which is natural and easy, but using it for traversing and partially modifying a term seems to be impossible.

Now while the code is lengthy (compared to Elpi) it is not complicated - I didn't have to do anything special. Constr.Unsafe.make and Constr.Binder.make seems to work in all cases (not yet tested too much). I guess this is because the term is convertible with the original one (I just do computation). I honestly did not really expect that I can mess around with the constr argument of a binder of a Unsafe.Prod and put it together again with Constr.Binder.make and Constr.Unsafe.make. But apparently it just works.

What is still unclear to me is what overhead Constr.Binder.make and Constr.Unsafe.make have. In the end I use the term created this way with change and it just works. When is the type checking of the term done? When I call change? Are the make operations essentially O(1)?

In summary I would say the API works for me, just the documentation isn't sufficient to come to this conclusion without actually trying it.

Michael Soegtrop (Nov 18 2022 at 08:52):

@Enrico Tassi : FYI : the symbol table management part works just splendidly in Elpi (as far as I can tell Ltac2 has no APIs for this yet), but with term traversal I ended up in "Not yet implemented" issues around mutual recursives and it is very hard to debug. As far as I can tell the cbv tactic does throw an error if a mutual recusive function is in the term - I think on return and not on entry. So I moved back to Ltac2 for this part. Cherry picking ...

Enrico Tassi (Nov 18 2022 at 09:08):

Right, mutual fixpoints are not supported. I guess it fails if the result still contains a mutual fix. If the mutual fix is not to be passed back to elpi, it should not fail.

Michael Soegtrop (Nov 18 2022 at 09:18):

Yes, this is what I figured from the effects I see. The issue is that it is hard to debug - I probably would have to add another symbol to the delta list, but without looking at the resulting term I can't tell which. The functions are generally not visible in the original term I pass in - it needs to be expanded quite deep to make them visible. And I have about 1000 symbols in my explicit delta lists.

But maybe we should continue the details in the Elpi thread. I posted the conclusion here to give some hint on the question when to use Ltac2 and when to use Elpi.

Pierre-Marie Pédrot (Nov 18 2022 at 10:57):

@Michael Soegtrop the make operations are essentially O(1), barring things like array and list conversions. If you use the unsafe API, no type checking is performed ever, so it is your duty to ensure that the generated terms are OK.

Michael Soegtrop (Nov 18 2022 at 11:00):

Thanks for the confirmation - this is all not so clear. So if I understand this right in my case (just doing computations) I can do an explicit type check at the end during testing and remove it later and leave it to Qed to find any remaining bugs?

Pierre-Marie Pédrot (Nov 18 2022 at 11:01):

I'd recommend keeping the typing operation at the end, except if you really do simple things. It's easy to break typing by missing e.g. universe constraints and those are a hell to debug.

Pierre-Marie Pédrot (Nov 18 2022 at 11:02):

Except if your computations are reduction-only, maybe. Those can never create new constraints.

Janno (Nov 18 2022 at 11:16):

Binder.make does retyping for relevance, doesn't it? Maybe that got fixed since 8.16

Pierre-Marie Pédrot (Nov 18 2022 at 11:18):

Yes, but 8.17 introduced an unsafe_make variant that's constant time.

Michael Soegtrop (Nov 18 2022 at 12:02):

Pierre-Marie Pédrot said:

I'd recommend keeping the typing operation at the end, except if you really do simple things. It's easy to break typing by missing e.g. universe constraints and those are a hell to debug.

Did you mean you would not recommend keeping the typing to the end? Otherwise I don't understand the "except" part.

Currently I only do cbv in parts of the term and put it together again. Of course one can mess up this as well (swap variables of the same type, ...) but I guess one would find such blunders quickly. In general I would try to find a compromise between frequency of typing, complexity of the code and speed requirements. It might be an option to enable explicit typing only for debug purposes and leave it to Qed otherwise.

Pierre-Marie Pédrot (Nov 18 2022 at 12:04):

My claim is that, as a general rule of thumb, when you use unsafe primitives, you should perform typing when you're outside of the unsafe block.

Pierre-Marie Pédrot (Nov 18 2022 at 12:04):

This will catch errors early, instead of getting weird anomalies later on.

Pierre-Marie Pédrot (Nov 18 2022 at 12:05):

Assuming you know what you're doing, then no typing is fine. But this is the exception.

Gaëtan Gilbert (Nov 18 2022 at 12:07):

when you produce terms in an unsafe way you need to keep in your head the proof that the term is well typed
there is no tool support for this
it is especially easy to miss universe constraints while reasoning, typically "f takes a type as argument, x is a type, so f x is well typed" but it should have been "f takes Typeu, x is Typev, so I need to add v<=u"

Michael Soegtrop (Nov 18 2022 at 12:09):

Oh OK - I read "I'd recommend keeping the typing operation at the end" as "do typing only at the end (vs in the middle of the construction as well)" - which is a bit strange together with the "except for simpel terms". But you meant "do not remove typing in the end"!

Michael Soegtrop (Nov 22 2022 at 14:44):

One more update on this: my "limited reduction" function now ran into the case of a dependent product - something like forall (A:Type) (a:A), a=a. Do I see it correctly that it is impossible to use Constr.Binder.make to recreate the inner binder because as discussed above it will type check the term which I guess is impossible since the type A is sort of a dangling reference in the sub term? And I guess unsafe_make is there to fix this?

Gaëtan Gilbert (Nov 22 2022 at 14:47):

yes
note that binder.make doesn't do full typechecking, just retyping, but in this case it changes nothing

Jason Gross (Nov 22 2022 at 22:22):

You can run Constr.Binder.make on something like A : Type or (I think this works, but not sure) match A return Type with x => x end to get retyping to not inspect the unbound variable

Michael Soegtrop (Nov 23 2022 at 07:23):

@Jason Gross : Sorry I can't quite follow your hint. To clarify: I am having issues with calling Constr.Binder.make on (a : A), not on (A : Type).

Gaëtan Gilbert (Nov 23 2022 at 10:29):

I think the idea is to do Binder.make "a" (mkCast (A, Type)) (slightly pseudocode)

Gaëtan Gilbert (Nov 23 2022 at 10:30):

of course it means you get a slightly different term with an extra cast
and you used unsafe for mkcast so no reason not to use binder.unsafe_make instead

Michael Soegtrop (Nov 23 2022 at 11:05):

I see. So I would end up with forall (A : Type) (a : (A:Type)), a=a instead of forall (A:Type) (a:A), a=a - makes sense.

Binder.unsafe_makedoesn't exist in 8.16 - I hope I can live without this trick until 8.17 is out. Currently it looks like I don't need to modify the type of binders.

Last updated: Oct 08 2024 at 16:02 UTC