(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
.
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).
As far as extendable tactics go, there is also smpl.
So would it be possible to create a custom tactic like auto
?
The usual strategy would be to define a hint database rduce
, and a tactic Ltac rduce := autorewrite with rduce.
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
Ah, right. Thanks ^^
Meven Lennon-Bertrand said:
The usual strategy would be to define a hint database
rduce
, and a tacticLtac rduce := autorewrite with rduce.
Do we also have something like this but for, for example, refine (subst_app _ _ _ _ @ _).
instead of rewrites?
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))
I mean the command can be repeated to add for instance rewrite other_thing
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.
Then smpl
sounds like a good idea in the case of Ltac. Thanks!
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!
@Gaëtan Gilbert Is it possible to use Ltac2
with refine
? Because it seems to throw syntax errors?
cf https://github.com/coq/coq/issues/13806 https://github.com/coq/coq/issues/18522
Thanks! That helps
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.
Not as nice as a real rewrite db though.
Ah, right. Thanks!
For now, I implemented it as a mutable Ltac2
tactic.
You might want to have a look at Elpi - a prolog based tactic language for Coq. Advanced databases are inherent to Elpi.
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.
still correct
see also https://github.com/coq/coq/pull/17482 I guess
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