I'm starting to use hint database, and I'm wonder if we can use them with things like
//. I know the
auto using foodb, but can I do something for
done/by to use a db that is not
This topic was moved here from #Coq users > Hint databases by Karl Palmskog
I think hint databases for finishers in MathComp is typically frowned upon, since it means they become unstable, but I'm sure it has been tried. I'm almost certain that augmenting
done is considered a bad idea in general.
It's actually used in mathcomp proper, for instance https://github.com/math-comp/math-comp/blob/master/mathcomp/algebra/ssrnum.v#L1409
but indeed the feature should be used carefully.
Piggybacking on this question, I would like to add a hint to
core but it's not working as expected. Feel free to tell me this is a bad idea. But in case it isn't (I think it should be fine), is there a way to do it?
From mathcomp Require Import all_ssreflect. From Coq Require Import ZArith Uint63. Definition nat_of_uint (n : int) : nat := match Uint63.to_Z n with | Zpos p => locked (nat_of_pos p) | _ => 0 end. Lemma nat_of_uint1 : nat_of_uint 1 = 1. Proof. by rewrite /nat_of_uint /= -lock. Qed. #[export] Hint Resolve nat_of_uint1 : core. Goal nat_of_uint 1 < 2. Proof. Fail by . by rewrite nat_of_uint1. Qed.
Not sure this is what you want, but it works:
Lemma nat_of_uint1 x : nat_of_uint 1 < x.+2. Proof. by rewrite /nat_of_uint /= -lock. Qed. #[export] Hint Resolve nat_of_uint1 : core. Goal nat_of_uint 1 < 2. Proof. by . Qed.
Goal was only an example. I have many
nat_of_uint 1 sprinkled around and wanted to avoid constantly rewriting with
Hint resolve doesn't take rewriting hints, only Hint Rewrite and autorewrite does (but it's not a great tactic)...
One can also add "rewrite foo" as an 0-cost hint extern
Cool, that teaches
auto to solve the
Goal :) Not
by  though, I guess it isn't affected by
Iirc, done uses trivial, which is affected by cheap enough hints
But I don't think trivial chains hints! And I think it's on purpose.
(but I use stdpp's done much more often so I could be wrong, "Print Ltac done" knows better)
done is in my opinion opening a can of worms
because you expect
done’s behavior to be consistent wherever the statement can be stated, I guess?
at the very least, I agree that importing a library should have limited and documented effects on global state; “hints in existing DBs” isn’t it. I’d be more lenient with “leaf formalizations”
(even if Karl disagrees with the concept)
I'm biased to consider the maintenance cost of tactic choices. If you use the same
done everywhere, it will typically break very consistently, allowing you to fix your proofs straightforwardly
sure, if you are doing some throwaway leaf formalization, go nuts...
I guess it would be more reasonable to have it be a local hint, which probably would be enough for my purposes anyway.
Karl Palmskog said:
doneis in my opinion opening a can of worms
Maybe, but there are certain things I found very useful to add in the past. The most useful is arguably to add the RHS simplifications for boolean operators (
rewrite !(andbT,andbF,orbT,orbF)), which makes
done more robust regarding the order of conjunctions and disjunctions. Another - possibly more controversial due to the nondeterminism in evar instantiations it causes - is using
eassumption in place of
done is designed to be overridden, so that you can plug in your own notion of triviality. IIRC in MC there are a few files where it is (locally) overridden: https://github.com/math-comp/math-comp/blob/ec8eaf48eb1e257ac2024edfb2eed2b96d4b4ec0/mathcomp/algebra/ssralg.v#L3551-L3562
yes, local overrides can make sense, if they are at least telegraphed...
All things considered, it's nice that just shadowing done is enough, since we don't have a proper alternative.
Last updated: Feb 08 2023 at 04:04 UTC