Stream: math-comp users

Topic: naming convention

vlj (Sep 21 2020 at 11:31):

Hi, I'm looking for decidable unequality for srrnat (ie "m <= n" || "m > n"). The closest lemma I found is leq_total. For others types with decidable unequality, is "total" the keyword used for such lemma, or is there a more precise lemma ? (leq_total is "m<=n" || "n <= m" so there is equality shared between cases)

Kazuhiko Sakaguchi (Sep 21 2020 at 11:38):

@vlj try case: leqP or case: (leqP m n).

vlj (Sep 21 2020 at 11:39):

@Kazuhiko Sakaguchi thanks ! it works better indeed.

Kazuhiko Sakaguchi (Sep 21 2020 at 11:41):

For trichotomy, you may use ltngtP.

vlj (Sep 22 2020 at 08:47):

there was a zify implementation for mathcomp nat and integer on a github repo is it still around ?

Christian Doczkal (Sep 22 2020 at 09:17):

There is mczify which was recently moved to the math-comp organization: https://github.com/math-comp/mczify

vlj (Sep 22 2020 at 09:18):

it's on opam ? this is nice !

vlj (Oct 02 2020 at 15:56):

Is setDset0 the correct name for the type (Y `\` X) != set0 <-> exists2 a : T, Y a & ~ X a.? I don't know if I should add a E at the end, because it's a lemma that can eliminate goal of the form Y\X != set 0.

Christian Doczkal (Oct 03 2020 at 18:02):

I don't think this merits a lemma, because this is just the chaining of set0Pn and setDP. That is, if you have AB0 : A :\: B != set0 you can eliminate it using have [x /setDP [x_A xNB]] := set0Pn _ AB0. (I suppose the A argument of set0Pncould be made implicit).

Christian Doczkal (Oct 03 2020 at 18:04):

But if you really want this as a lemma, I guess the statement should be
reflect (exists2 a : T, a \in Y & a \notin X) (Y `\` X != set0)
and the natural name would likely be setD0Pn.

Ana de Almeida Borges (Nov 14 2021 at 15:27):

I would like your opinion on how to name the following kind of lemma:

P x -> foo x -> foo (bar x)

and

Q x -> foo (bar x) -> foo x

I originally named the first one foo_bar, and had the impulse to name the second one bar_foo, but I don't think I would come up with that name in the absence of the first lemma, and furthermore I think I will easily forget which I named in which way.

In my particular use-case, the P x and Q x assumptions are obviously needed and I was not expecting to include a reference to them in the names. (And I don't want to, since I don't have a nice name for either of them.)

Karl Palmskog (Nov 14 2021 at 15:28):

you could always try our tool (e.g., in VsCoq) and see what it suggests: https://github.com/EngineeringSoftware/roosterize

Ana de Almeida Borges (Nov 14 2021 at 15:34):

This looks very cool! Does it really require Coq 8.10.2?

Karl Palmskog (Nov 14 2021 at 15:35):

unfortunately yes due to being mostly a paper artifact. But in my experience, a MathComp project that breaks compatibility with Coq 8.10 or 8.11 is doing something exotic

Ana de Almeida Borges (Nov 14 2021 at 15:37):

I'm using MathComp 1.13 features, but I can probably tweak things around enough to make use of it

Christian Doczkal (Nov 14 2021 at 17:42):

@Karl Palmskog , note that mathcomp-1.13.0 dropped support for Coq-8.10. IIRC, the reason for this is that this allowed us to finally use the deprecated attribute of Coq in favor of the old and fragile mathcomp notation trickery. So maybe the time has come to update your tool.

Théo Zimmermann (Nov 14 2021 at 19:19):

Maybe worth moving to coq-community then?

Karl Palmskog (Nov 15 2021 at 08:51):

there are two significant hurdles: (1) maintaining the Python parts, which use PyTorch and requires machine learning knowledge and (2) curating Coq datasets and training on them. Neither are my specialty, and not at all easy to find a drop-in maintainer for that.

Théo Zimmermann (Nov 15 2021 at 11:26):

Isn't it possible to just dump a pre-trained model and ship that?

Karl Palmskog (Nov 15 2021 at 11:27):

that's what we currently do, but the performance will not be very good unless you train on relevant code, and at this point I think the changes are many in MathComp between 1.9 (current dump) and 1.13

Karl Palmskog (Nov 15 2021 at 11:29):

this is the research dilemma in action: all the novelty of the tooling has been "consumed", what is left is an engineering problem. I think we could basically use "whatever MathComp projects are in the Coq Platform" to train on, but I don't have the funding or skills to do this development by myself.

When we started out, the Coq Platform was not around and most projects didn't build well together on a particular Coq, so this was part of the contribution, and it went into the projects themselves, the Coq opam archive and the platform scripts. All the Coq stuff on serialization has been incorporated into SerAPI.

Théo Zimmermann (Nov 15 2021 at 11:48):

Let's at least open an issue in the manifesto repo about roosterize and what are the required skills to maintain it. I think that nowadays it's more and more likely to see students coming who understand both Coq and PyTorch.

Karl Palmskog (Nov 15 2021 at 11:52):

OK, that's fine by me, but please ping in @pengyunie and @gliga, in the GitHub issue, since they wrote nearly all the Python code. I'm not sure what their current plans are regarding Roosterize.

Karl Palmskog (Nov 15 2021 at 11:53):

I'm sure some parts (getting suggestions online in a Coq development) could/should be ported to Emilio's PyCoq

Last updated: Apr 20 2024 at 02:40 UTC