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)
@vlj try case: leqP
or case: (leqP m n)
.
@Kazuhiko Sakaguchi thanks ! it works better indeed.
For trichotomy, you may use ltngtP
.
there was a zify implementation for mathcomp nat and integer on a github repo is it still around ?
There is mczify
which was recently moved to the math-comp organization: https://github.com/math-comp/mczify
it's on opam ? this is nice !
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.
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 set0Pn
could be made implicit).
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
.
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.)
you could always try our tool (e.g., in VsCoq) and see what it suggests: https://github.com/EngineeringSoftware/roosterize
This looks very cool! Does it really require Coq 8.10.2?
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
I'm using MathComp 1.13 features, but I can probably tweak things around enough to make use of it
@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.
Maybe worth moving to coq-community then?
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.
Isn't it possible to just dump a pre-trained model and ship that?
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
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.
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.
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.
I'm sure some parts (getting suggestions online in a Coq development) could/should be ported to Emilio's PyCoq
Last updated: Oct 13 2024 at 01:02 UTC