Assia Mahboubi (Oct 20 2021 at 15:30): Assia Mahboubi (Oct 20 2021 at 15:30):Although the Search command has improved a lot, it is still super hard to find the right lemma in mathcomp, specially when the relevant lemmas are generic, in the sense of involving canonical instances. I am thinking of bigops, morphisms, etc. This topic aims at collecting feature wishes and suggestions, so as to hopefully be able to design a principled improved version of Search.
Assia Mahboubi (Oct 20 2021 at 15:31):Please contribute here your examples of goals for which the output of Search is frustratingly lost.
Cyril Cohen (Oct 20 2021 at 15:47):Search algC GRing.mul should find mulC_rect (by pattern matching modulo CS) Cyril Cohen (Oct 20 2021 at 16:12):Search (_%:~R + _%:~R) should find raddfD and/or rmorphD (by pattern matching modulo CS) Cyril Cohen (Oct 20 2021 at 16:16):Search ((_ + _) + _) should find addrA (with either a global or local (to addrA) directive to indicate associative should be transparent for search) Enrico Tassi (Oct 20 2021 at 18:24):Any bigop lemmas where the pattern is too specific, eg you write \sum or you omit the filter and get xpredT which kills all conditional lemmas
Paolo Giarrusso (Oct 21 2021 at 01:15):I know this is in the math-comp stream, but ideally Search should also cover typeclasses…
Enrico Tassi (Oct 21 2021 at 07:04):I though that the new coq search could list, say, only tc instances. But maybe it was proposed and not implemented in the end?
Assia Mahboubi (Oct 21 2021 at 07:17):Paolo Giarrusso said:
I know this is in the math-comp stream, but ideally Search should also cover typeclasses…
Sure, please do not refrain from describing the support you miss for TC!
Théo Zimmermann (Oct 21 2021 at 07:20):Enrico Tassi said:
I though that the new coq search could list, say, only tc instances. But maybe it was proposed and not implemented in the end?
Yes, it can: https://coq.inria.fr/refman/proof-engine/vernacular-commands.html#grammar-token-logical_kind
Paolo Giarrusso (Oct 21 2021 at 07:21):That can also find canonical instances, but that’s not enough…
I mean that @Cyril Cohen’s questions translate to typeclasses, even if the implementation is completely different. E.g. Search ((_ + _) + _) should find assoc, if we have the following (from stdpp) in scope:
Class Assoc {A} (R : relation A) (f : A → A → A) : Prop :=
assoc x y z : R (f x (f y z)) (f (f x y) z).
Instance Assoc eq Nat.add. Proof. … Qed.
basically, what users of that would like is “Search” modulo TC search.
Paolo Giarrusso (Oct 21 2021 at 07:22):(parts of the _implementation_ differ)
Paolo Giarrusso (Oct 21 2021 at 07:25):similarly, most of the stdpp theory of finite sets is TC-polymorphic over classes such as:
Class FinSet A C `{ElemOf A C, Empty C, Singleton A C, Union C,
Intersection C, Difference C, Elements A C, EqDecision A} : Prop := {
fin_set_set :> Set_ A C;
elem_of_elements (X : C) x : x ∈ elements X ↔ x ∈ X;
NoDup_elements (X : C) : NoDup (elements X)
}.
(and I’m sure math-classes has similar questions)
Paolo Giarrusso (Oct 21 2021 at 07:29):and thanks @Assia Mahboubi for the hospitality and for raising the topic :-).
Notification Bot (Oct 22 2021 at 09:27):This topic was moved here from #math-comp users > Towards a CEP for improving Search by Cyril Cohen
Cyril Cohen (Oct 22 2021 at 09:28):@_Notification Bot|100006 said:
This topic was moved here from #math-comp users > Towards a CEP for improving Search by Cyril Cohen
Moved here by request of @Assia Mahboubi
Vincent Siles (Oct 26 2021 at 11:39):Noob user of stdpp and Search: I recently had trouble to find map_to_list and list_to_map cause I was doing Search (list (_ * _) -> gmap _ _) instead of Search (list (_ * _) -> _). I found working with Search and type classes to be tricky :)
Jim Fehrle (Nov 30 2021 at 19:58):It may be considerably easier to use Search through an IDE GUI dialog box rather than through a somewhat complex command syntax. Option settings could more-easily be reused, such as included/excluded modules. A well-designed dialog is more likely to be understood without having to read the manual. Perhaps that can be considered in the CEP.
Paolo Giarrusso (Nov 30 2021 at 20:01):that could simplify life for end-users, but it shouldn't be required IMHO — the GUI should be a frontend.
Paolo Giarrusso (Nov 30 2021 at 20:01):(It doesn't mean the frontend needs to output a Search command, as long as the features aren't tied to a single editor)
Paolo Giarrusso (Nov 30 2021 at 20:02):FWIW, most of the examples here seem about making Search (signature) be smarter in matching signature with the lemma, so better GUIs (while valuable) _might_ be somewhat orthogonal...
Paolo Giarrusso (Nov 30 2021 at 20:41):General Q: Is there a way to ask Search x to find lemmas that can be _instantiated_ to apply to x — basically, a step of eauto — instead of lemmas that are instances of x?
Paolo Giarrusso (Nov 30 2021 at 20:43):for instance, if I have a lemma elem_of_enum : ∀ {Finite A} x, x ∈ enum A in scope, Search (x ∈ enum A). won't find anything because it's too specific; I must manually figure out what to throw away and come up with Search (?x ∈ enum ?A)`. In other cases, there are many more choices in where to place holes.
Paolo Giarrusso (Nov 30 2021 at 20:44):and even Search concl:(x ∈ enum A). isn't better...
Jim Fehrle (Nov 30 2021 at 21:31):How about something like letting the user highlight a subexpression in the context in the GUI and have Coq return all lemmas that can unify with it, automatically picking up the type information associated with it? (not trivial to do, but maybe rather easy to use, even for beginners)
Last updated: Sep 30 2023 at 06:01 UTC