Follow

Once upon a time, I didn’t know how to use `Hint` commands. Now, I find myself in a position where I convinced myself I *need* them every now and then.

By the way, I ran into an… interesting problem yesterday and I don’t really know how to deal with it.

I have a typeclass of the form C (f : a -> b) : Prop := { pred : forall (x : a), P (f x) }, and I have a function g : c -> a -> b such that I can prove that forall x, C (g x) -> False, so basically, I would like a way to tell Coq to trust me on this one, and just cut the search and backtrack if it finds itself in a situation where it searches for such goal.

Not surprisingly, I was able to greatly improve the performance of the typeclass instance search just by using typeclass priorities.

Instance my_instance : C|10 := ...

Here, 10 is the priority of the instance (otherwise decided by based on the number of variables the instance needs).

Coq uses instances with a low priority number first, so by setting a high number to instances less likely to succeed, I was able to cut my build time from ~33s to ~8s on my work laptop.

\o/

@lthms Arf, je ne les utilise jamais. Ça sert à diriger la recherche de la tactique auto, c'est bien cela ? Est-ce que tu aurais un lien vers un bon tutoriel ? ☺️

@MartinShadok Je m’en sers surtout pour guider à la truelle la recherche d’instances pour les typeclasses.

Pour ce qui est de tutoriels, malheureusement non. J’ai surtout appris par essai/erreur/recherche d’exemples sur GitHub. Ceci étant dit, le manuel est pas trop mal détaillé sur ces points.

Faudrait que j’écrive un tutoriel comme ça, ça serait pas mal…

@lthms Tiens ? C'est marrant : sur une tactique je trouvais ça normal de mettre des heuristiques, mais sur une recherche d'instance ça me titille un peu. Est-ce que la recherche reste déterministe ?

@MartinShadok Coq ne choisit pas ses hints au hasard, du coup ça doit le rester (de toute façon, la lib standard utilise des hints pour guider l’inférence de certaines typeclasses de ce que j’ai vu, notamment Proper)

@lthms C'est vrai 😊
Ça rend le mécanisme de classes de type assez magie noire pour ceux qui ne connaissent pas trop, par contre 😕 Je veux bien croire que ça aide pour les structures mathématiques complexes en math.

@MartinShadok après il l’est déjà pas mal en vrai :p d’ailleurs c’est pas vraiment un bon nom typeclasses vu que tu peux les paramétrer par des termes

Sign in to participate in the conversation
Mastodon

Server run by the main developers of the project 🐘 It is not focused on any particular niche interest - everyone is welcome as long as you follow our code of conduct!