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`

.

Please contribute here your examples of goals for which the output of `Search`

is frustratingly lost.

`Search algC GRing.mul`

should find`mulC_rect`

(by pattern matching modulo CS)

`Search (_%:~R + _%:~R)`

should find`raddfD`

and/or`rmorphD`

(by pattern matching modulo CS)

`Search ((_ + _) + _)`

should find`addrA`

(with either a global or local (to`addrA`

) directive to indicate`associative`

should be transparent for search)

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

I know this is in the math-comp stream, but ideally Search should also cover typeclasses…

I though that the new coq search could list, say, only tc instances. But maybe it was proposed and not implemented in the end?

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!

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

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.

(parts of the _implementation_ differ)

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)

and thanks @Assia Mahboubi for the hospitality and for raising the topic :-).

This topic was moved here from #math-comp users > Towards a CEP for improving Search by Cyril Cohen

@_**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

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 :)

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.

that could simplify life for end-users, but it shouldn't be required IMHO — the GUI should be a frontend.

(It doesn't mean the frontend needs to output a `Search`

command, as long as the features aren't tied to a single editor)

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

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`

?

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.

and even `Search concl:(x ∈ enum A).`

isn't better...

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: Jun 18 2024 at 09:02 UTC