Stream: Coq users

Topic: "Dynamic dispatch" in Ltac(2)


view this post on Zulip Arnoud van der Leer (Mar 14 2024 at 09:42):

(For my thesis) I am currently working with an axiomatized version of the lambda calculus with explicit substitution. I.e. I have a set and a couple of axioms that this set has constructors "var", "abs", "app" and "subst".
Now, propagating "subst" through a term is a pain, because it takes a lot of rewrites: "rewrite subst_abs, subst_subst, subst_app, subst_var, subst_var" etc.
Of course, I can create a tactic that repeatedly tries to determine which rewrite to use.
However, now I am building new combinators like compose, pair, curry etc.
So here is my question: would it be possible to create a "list" or "database" lst of applicable tactics (mostly consisting of rewrite ... or refine ...), to which we can separately add new tactics for new combinators along the way. And can we create a tactic rduce that tries to apply the tactics that are currently in lst to the current goal? Note that we would also want to use rduce to prove things about our new combinators, which yields new tactics that we add to lst.

view this post on Zulip Meven Lennon-Bertrand (Mar 14 2024 at 09:46):

The auto tactic can be extended by hint databases, which you can extend as you go with new lemmas to use. If you want to do rewriting only, then autorewrite might also be doing the job more cleanly (it has been designed for the kind of cases you encounter).

view this post on Zulip Meven Lennon-Bertrand (Mar 14 2024 at 09:47):

As far as extendable tactics go, there is also smpl.

view this post on Zulip Arnoud van der Leer (Mar 14 2024 at 09:50):

So would it be possible to create a custom tactic like auto?

view this post on Zulip Meven Lennon-Bertrand (Mar 14 2024 at 09:52):

The usual strategy would be to define a hint database rduce, and a tactic Ltac rduce := autorewrite with rduce.

view this post on Zulip Gaëtan Gilbert (Mar 14 2024 at 09:56):

It's possible to accumulate using a mutable ltac2, eg

Ltac2 mutable rduce () := ().

Ltac2 Set rduce as rduce0 := fun () => Control.plus (fun () => rewrite some_thing) (fun _ => rduce0 ()).
(* etc *)

not sure how well it works though, especially note that repeating Import of a module which does the Set will add duplicate entries

view this post on Zulip Arnoud van der Leer (Mar 14 2024 at 10:06):

Ah, right. Thanks ^^

view this post on Zulip Arnoud van der Leer (Mar 14 2024 at 10:07):

Meven Lennon-Bertrand said:

The usual strategy would be to define a hint database rduce, and a tactic Ltac rduce := autorewrite with rduce.

Do we also have something like this but for, for example, refine (subst_app _ _ _ _ @ _). instead of rewrites?

view this post on Zulip Arnoud van der Leer (Mar 14 2024 at 10:09):

Gaëtan Gilbert said:

It's possible to accumulate using a mutable ltac2, eg

Ltac2 mutable rduce () := ().

Ltac2 Set rduce as rduce0 := fun () => Control.plus (fun () => rewrite some_thing) (fun _ => rduce0 ()).
(* etc *)

not sure how well it works though, especially note that repeating Import of a module which does the Set will add duplicate entries

Can you elaborate a bit on the "etc"? (I am still not very much acquainted with Ltac(2))

view this post on Zulip Gaëtan Gilbert (Mar 14 2024 at 10:09):

I mean the command can be repeated to add for instance rewrite other_thing

view this post on Zulip Meven Lennon-Bertrand (Mar 14 2024 at 10:15):

Arnoud van der Leer said:

Do we also have something like this but for, for example, refine (subst_app _ _ _ _ @ _). instead of rewrites?

This is trickier: autorewrite only supports rewriting lemmas. You can try and use auto, possibly with a Hint Extern, but the issue is that auto by default either succeeds or leaves the goal unchanged. So if you merely want to simplify the goal, you'd either have to craft something with shelve/unshelve, or use smpl which will simply apply all tactics from an (extensible) list until none of them applies any more.

view this post on Zulip Arnoud van der Leer (Mar 14 2024 at 10:41):

Then smpl sounds like a good idea in the case of Ltac. Thanks!

view this post on Zulip Arnoud van der Leer (Mar 14 2024 at 10:51):

Gaëtan Gilbert said:

I mean the command can be repeated to add for instance rewrite other_thing

Oooh, now I see. I viewed this on mobile, and did not see beyond the fun (). But on my laptop it makes sense. Thank you!

view this post on Zulip Arnoud van der Leer (Mar 14 2024 at 11:56):

@Gaëtan Gilbert Is it possible to use Ltac2 with refine? Because it seems to throw syntax errors?

view this post on Zulip Gaëtan Gilbert (Mar 14 2024 at 11:59):

cf https://github.com/coq/coq/issues/13806 https://github.com/coq/coq/issues/18522

view this post on Zulip Arnoud van der Leer (Mar 14 2024 at 22:25):

Thanks! That helps

view this post on Zulip Pierre Courtieu (Mar 15 2024 at 08:20):

It is probably better with ltac2 but you can also do it in ltac by redefining your tactic.

Ltac rduce:= idtac.

Ltac rd1 := match goal with .... end
Ltac rduce::= rd2.
...
Ltac rd2 := match goal with ... | _=>rd1 end
Ltac rduce::= rd2.

view this post on Zulip Pierre Courtieu (Mar 15 2024 at 08:20):

Not as nice as a real rewrite db though.

view this post on Zulip Arnoud van der Leer (Mar 15 2024 at 08:26):

Ah, right. Thanks!

For now, I implemented it as a mutable Ltac2 tactic.

view this post on Zulip Michael Soegtrop (Mar 15 2024 at 08:28):

You might want to have a look at Elpi - a prolog based tactic language for Coq. Advanced databases are inherent to Elpi.

view this post on Zulip Michael Soegtrop (Mar 15 2024 at 08:30):

In my experience mutable Ltac2 tactics don't scale very well for databases, because (at least at the time I tried it last), one could not assign an evaluated Ltac2 term to a mutable Ltac2 definition. This means that the construction of the database has to be redone each time you use it. Depending on how the construction is done, this might be feasible or not - in my case it wasn't.

view this post on Zulip Gaëtan Gilbert (Mar 15 2024 at 08:35):

still correct
see also https://github.com/coq/coq/pull/17482 I guess

view this post on Zulip Michael Soegtrop (Mar 15 2024 at 08:46):

A small side note: since I do quite a bit of Elpi advertising, I wanted to emphasise that I really like Ltac2 as well - it is a very well designed language and a dramatic improvement over Ltac1. Many of the things I do would be entirely unmaintainable with Ltac instead of Ltac2. It is just so that Elpi is also a very well designed tactic language and it is less known. In many cases the two don't give each other much, but there are cases where Elpi has clear advantages and cases where Ltac2 has clear advantages. Database based automation is IMHO the domain where Elpi is quite a bit stronger than Ltac2. This is the kind of task Prolog was made for. auto is kind of a poor man's Prolog - Elpi is the real thing.


Last updated: Oct 13 2024 at 01:02 UTC