Vincent Siles (Nov 10 2021 at 10:30): Vincent Siles (Nov 10 2021 at 10:30):I'm starting to use hint database, and I'm wonder if we can use them with things like by, done or //. I know the auto using foodb, but can I do something for done/by to use a db that is not core ?
Notification Bot (Nov 10 2021 at 10:32):This topic was moved here from #Coq users > Hint databases by Karl Palmskog
Karl Palmskog (Nov 10 2021 at 10:33):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 core for by/done is considered a bad idea in general.
Pierre Roux (Nov 10 2021 at 10:55):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.
Ana de Almeida Borges (Dec 13 2021 at 17:55):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.
No, my Goal was only an example. I have many nat_of_uint 1 sprinkled around and wanted to avoid constantly rewriting with nat_of_uint1
Paolo Giarrusso (Dec 13 2021 at 18:24):Hint resolve doesn't take rewriting hints, only Hint Rewrite and autorewrite does (but it's not a great tactic)...
Paolo Giarrusso (Dec 13 2021 at 18:26):One can also add "rewrite foo" as an 0-cost hint extern
Ana de Almeida Borges (Dec 13 2021 at 18:30):Cool, that teaches auto to solve the Goal :) Not by [] though, I guess it isn't affected by Hint Extern?
Paolo Giarrusso (Dec 13 2021 at 18:34):Iirc, done uses trivial, which is affected by cheap enough hints
Paolo Giarrusso (Dec 13 2021 at 18:35):But I don't think trivial chains hints! And I think it's on purpose.
Paolo Giarrusso (Dec 13 2021 at 18:36):(but I use stdpp's done much more often so I could be wrong, "Print Ltac done" knows better)
Karl Palmskog (Dec 13 2021 at 18:42):augmenting done is in my opinion opening a can of worms
Paolo Giarrusso (Dec 13 2021 at 19:00):because you expect done’s behavior to be consistent wherever the statement can be stated, I guess?
Paolo Giarrusso (Dec 13 2021 at 19:05):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”
Paolo Giarrusso (Dec 13 2021 at 19:05):(even if Karl disagrees with the concept)
Karl Palmskog (Dec 13 2021 at 20:18):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
Karl Palmskog (Dec 13 2021 at 20:18):sure, if you are doing some throwaway leaf formalization, go nuts...
Ana de Almeida Borges (Dec 13 2021 at 21:47):I guess it would be more reasonable to have it be a local hint, which probably would be enough for my purposes anyway.
Christian Doczkal (Dec 14 2021 at 08:33):Karl Palmskog said:
augmenting
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 assumption.
Enrico Tassi (Dec 14 2021 at 12:32):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
Karl Palmskog (Dec 14 2021 at 13:35):yes, local overrides can make sense, if they are at least telegraphed...
Paolo Giarrusso (Dec 14 2021 at 14:16):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