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`

?

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 `core`

for `by`

/`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.
```

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`

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 `Hint Extern`

?

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)

augmenting `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:

augmenting

`done`

is 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`

.

`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: Mar 03 2024 at 15:01 UTC