Stream: math-comp users

Topic: Hint databases for finishing tactic


view this post on Zulip 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 ?

view this post on Zulip Notification Bot (Nov 10 2021 at 10:32):

This topic was moved here from #Coq users > Hint databases by Karl Palmskog

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Enrico Tassi (Dec 13 2021 at 18:07):

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.

view this post on Zulip Ana de Almeida Borges (Dec 13 2021 at 18:15):

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

view this post on Zulip 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)...

view this post on Zulip Paolo Giarrusso (Dec 13 2021 at 18:26):

One can also add "rewrite foo" as an 0-cost hint extern

view this post on Zulip 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?

view this post on Zulip Paolo Giarrusso (Dec 13 2021 at 18:34):

Iirc, done uses trivial, which is affected by cheap enough hints

view this post on Zulip Paolo Giarrusso (Dec 13 2021 at 18:35):

But I don't think trivial chains hints! And I think it's on purpose.

view this post on Zulip 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)

view this post on Zulip Karl Palmskog (Dec 13 2021 at 18:42):

augmenting done is in my opinion opening a can of worms

view this post on Zulip 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?

view this post on Zulip 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”

view this post on Zulip Paolo Giarrusso (Dec 13 2021 at 19:05):

(even if Karl disagrees with the concept)

view this post on Zulip 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

view this post on Zulip Karl Palmskog (Dec 13 2021 at 20:18):

sure, if you are doing some throwaway leaf formalization, go nuts...

view this post on Zulip 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.

view this post on Zulip Christian Doczkal (Dec 14 2021 at 08:33):

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.

view this post on Zulip 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

view this post on Zulip Karl Palmskog (Dec 14 2021 at 13:35):

yes, local overrides can make sense, if they are at least telegraphed...

view this post on Zulip 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