I am trying to implement a tactic that uses small hint databases to solve simple arithmetic problems:
Ltac pattern_matching_rewriter :=
match goal with
|[ |- context[0] ] => solve[auto with nocore zero_rewriters]
|[ |- context[1] ] => solve[auto with nocore one_rewriters]
|[ |- context[- _] ] => solve[auto with nocore opp_rewriters]
|[ |- context[Rabs _] ] => solve[auto with nocore abs_rewriters]
|[ |- context[R_dist _] ] => solve[auto with nocore abs_rewriters]
|[ |- context[_²] ] => solve[auto with nocore sqr_rewriters]
|[ |- context[exp _] ] => solve[auto with nocore exp_rewriters]
|[ |- context[_ + _]] => solve[auto with nocore plus]
|[ |- context[_ - _]] => solve[auto with nocore minus]
|[ |- context[_ * _]] => solve[auto with nocore mult]
| _ => first[solve[timeout 5 auto with nocore rewriters] | idtac "Finding a proof takes too long. Try taking a smaller step."]
end.
So for example, whenever the goal contains an exponential, I want to use the exp_rewriters database. However, sometimes, my goal contains an exponential and a square. In that case I would like to use both the exp_rewriters as well as the abs_rewriters databases , without using all of the others (the rewriters database contains all databases).
Is there a possibility to do that, without hardcoding every possible combination?
Do lia or nia not solve your problem, even in the latest Coq version? At least lia is extensible IIUC, maybe that helps better?
I can’t answer your exact question, but here’s my closest idea. One can make the hints themselves match against the context using Hint Extern — so hints in zero_rewriters could be instead be written along these lines:
This is oversimplified — Hint Resolve foo isn’t just Hint Extern prio => apply foo, it also guards the Hint Extern with a pattern. I recommend checking out the docs for Hint Extern (hoping they’re clear enough).
If those hints are rewrite hints (but not sure how they work with auto, except if they’re hint extern), maybe autorewrite or rewrite_strat or https://github.com/mit-plv/rewriter (described in this draft) might help (low-confidence suggestion)?
There are definitely easier ways to prove the stuff that I want to do with the databases, but I am not looking for a ‘fast’ or ‘easy’ proving tool. With this distinction in databases I am trying to implement a more controlled automation.
This is an interesting solution, so thanks for the suggestion! However, I am afraid it does not solve my problem. If I now use auto with rewriters it still searches through all hints in that database, but I would like to call auto with a smaller database in the first place.
So perhaps I phrased my problem wrong - in my current implementation, and in the suggested one, the database is quite large. This slows down the application of the tactic enormously, and I would like to avoid that.
Consider the statement Rabs (Rabs (ln (exp a)) = Rabs a. The tactic auto with rewriters solves this problem, but it does so very slowly. The better alternative is to use auto with exp_rewriters abs_rewriters, which solves the statement very quickly. Only, I am expclitely looking for one tactic that takes care of determining which databases auto needs (based on the different contexts).
I am indeed using Hint Extern, in combination with the rewrite tactic. I’ll take a look into the reference, but I think that point 1 applies here as well.
I see — so it’s crucial to check the context only once, not once per hint.
You just want to build a list of database names, and then pass that list to auto (as you had asked), which should be easy, but isn’t in Ltac1.
Ltac2 might be better at this, but I don’t know if all the needed ingredients are there.@ppedrot, does Ltac2 let you pass a program-generated list of databases to auto?
The type given to auto in the Ltac2 sources seem to indicate that you can pass a list of database names as third parameter, and you should be able to combine it with the pattern matching features.
Edit: Here is a self contained version using Ltac2 (I probably have misused the Hint databases and Hint Resolve command, proof automation in Coq is something that I still have to learn)
From Ltac2 Require Import Ltac2 Ident.
Create HintDb base.
Create HintDb zero_rewriters.
Create HintDb one_rewriters.
Hint Resolve eq_refl : base.
Hint Resolve f_equal_nat : base.
Hint Resolve f_equal2_nat : base.
Hint Resolve plus_n_O : zero_rewriters.
Hint Resolve plus_O_n : zero_rewriters.
Hint Resolve mult_n_O : zero_rewriters.
Axiom mult_n_1 : forall n, n = n * 1.
Axiom mult_1_n : forall n, n = 1 * n.
Hint Resolve mult_n_1 : one_rewriters.
Hint Resolve mult_1_n : one_rewriters.
Goal forall n (f : nat -> nat), f n = f (n + 0).
Proof.
solve[ auto with nocore base zero_rewriters ].
Qed.
Goal forall m n, n + m = (n + 0) + m.
Proof. solve[ auto with nocore base zero_rewriters ]. Qed.
Ltac2 unwrap_cons x l :=
match x with
| None => l
| Some y => y :: l
end.
Ltac2 collect_db () :=
let l :=
unwrap_cons (of_string "nocore") (unwrap_cons (of_string "base") [])
in
let l := match! goal with
| [ |- context [0] ] => unwrap_cons (of_string "zero_rewriters") l
| [ |- _ ] => l
end
in
let l := match! goal with
| [ |- context [1] ] => unwrap_cons (of_string "one_rewriters") l
| [ |- _ ] => l
end
in
l.
Ltac2 Notation myauto :=
let l := collect_db () in
solve[ auto0 None None (Some (Some l)) ].
Goal forall n (f : nat -> nat), f n = f n.
Proof.
Ltac2 Eval (collect_db ()).
myauto.
Defined.
Goal forall n m, n + m = (n + 0) + m.
Proof.
Ltac2 Eval (collect_db ()).
myauto.
Defined.
Goal forall n m, n + m = (n + 0) + 1 * m.
Proof.
Ltac2 Eval (collect_db ()).
myauto.
Defined.