Stream: Coq users

Topic: Towards a CEP for improving Search


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

view this post on Zulip Assia Mahboubi (Oct 20 2021 at 15:31):

Please contribute here your examples of goals for which the output of Search is frustratingly lost.

view this post on Zulip Cyril Cohen (Oct 20 2021 at 15:47):

view this post on Zulip Cyril Cohen (Oct 20 2021 at 16:12):

view this post on Zulip Cyril Cohen (Oct 20 2021 at 16:16):

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

view this post on Zulip Paolo Giarrusso (Oct 21 2021 at 01:15):

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

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

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

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

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

view this post on Zulip Paolo Giarrusso (Oct 21 2021 at 07:22):

(parts of the _implementation_ differ)

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

view this post on Zulip Paolo Giarrusso (Oct 21 2021 at 07:29):

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

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

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

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

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

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

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

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

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

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

view this post on Zulip Paolo Giarrusso (Nov 30 2021 at 20:44):

and even Search concl:(x ∈ enum A). isn't better...

view this post on Zulip 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: Jan 29 2023 at 01:02 UTC