Stream: math-comp users

Topic: imported from gitter room math-comp/Lobby


view this post on Zulip Enrico Tassi (Dec 11 2018 at 18:20):

Hello everybody!

view this post on Zulip Anton Trunov (Dec 11 2018 at 18:21):

Hi! Thanks for creating the channel!

view this post on Zulip Cyril Cohen (Dec 11 2018 at 18:22):

Hi!

view this post on Zulip Cyril Cohen (Dec 11 2018 at 18:23):

I am not sure I did the right thing... I am not used to gitter... I created both math-comp/Lobby (no github integration) and math-comp/math-comp (with github integration). Shall I keep both or remove one? (And if so which one?)

view this post on Zulip Anton Trunov (Dec 11 2018 at 18:25):

Maybe @Emilio Jesús Gallego Arias could help with this.

view this post on Zulip Erik Martin-Dorel (Dec 11 2018 at 18:26):

Hi all! :)

view this post on Zulip Emilio Jesús Gallego Arias (Dec 11 2018 at 18:26):

Hi all!

view this post on Zulip Emilio Jesús Gallego Arias (Dec 11 2018 at 18:27):

I am not expert on Gitter, what I did for Coq was indeed to remove the Lobby, and have one chat room per repos, but could not be the best choice for math-comp

view this post on Zulip Florent Hivert (Dec 11 2018 at 18:53):

Hi There ! :-)

view this post on Zulip Karl Palmskog (Dec 12 2018 at 18:42):

so, is there an easy/idomatic way to use omega and similar tactics with ssrnat? or is the bottom line that it's the wrong thing to do?

view this post on Zulip Karl Palmskog (Dec 12 2018 at 18:44):

for example, the following seems very hacky: https://github.com/JetBrains/ot-coq/blob/master/Ssromega.v

view this post on Zulip Emilio Jesús Gallego Arias (Dec 12 2018 at 20:58):

There was more principled support at some point, but it's been some time I don't hear about that [I think it was on CoqPL]

view this post on Zulip Emilio Jesús Gallego Arias (Dec 12 2018 at 20:58):

anyways omega is almost removed from Coq, you are supposed to use lia et al.

view this post on Zulip Emilio Jesús Gallego Arias (Dec 12 2018 at 20:58):

https://github.com/coq/coq/issues/7872

view this post on Zulip Karl Palmskog (Dec 12 2018 at 21:40):

and lia et al. actually work with ssrnat?

view this post on Zulip Emilio Jesús Gallego Arias (Dec 12 2018 at 22:06):

I think it was the work of Nicolas Magaud "Transferring Arithmetic Decision Procedures (on Z) to Alternative Representations"

view this post on Zulip Emilio Jesús Gallego Arias (Dec 12 2018 at 22:07):

or maybe it was Frederic Besson?

view this post on Zulip Emilio Jesús Gallego Arias (Dec 12 2018 at 22:08):

I don't recall now

view this post on Zulip Emilio Jesús Gallego Arias (Dec 12 2018 at 22:08):

but there was work toward making things work

view this post on Zulip Karl Palmskog (Dec 12 2018 at 22:11):

ah, CoqPL '17: https://hal.inria.fr/hal-01518660/document

view this post on Zulip Karl Palmskog (Dec 12 2018 at 22:15):

does not seem to be maintained though: http://dpt-info.u-strasbg.fr/~magaud/SSR

view this post on Zulip Emilio Jesús Gallego Arias (Dec 12 2018 at 23:22):

yup is a pity

view this post on Zulip Emilio Jesús Gallego Arias (Dec 12 2018 at 23:22):

is there not already an issue in the math-comp tracker?

view this post on Zulip Reynald Affeldt (Dec 12 2018 at 23:35):

about omega > I have been using ssrnat and Coq's omega using the same trick (https://github.com/affeldt-aist/seplog/blob/master/lib/ssrnat_ext.v#L46-L81) as JetBrains for a long time, it turns out to be stable, so not that hacky (after all, it is only about switching view for the simple nat data structure).

view this post on Zulip Karl Palmskog (Dec 13 2018 at 00:13):

thanks, that's a bit more cohesive as a single tactic

view this post on Zulip Karl Palmskog (Dec 13 2018 at 00:14):

@affeldt-aist can I use that snippet without changing my project to GPLv3?

view this post on Zulip Reynald Affeldt (Dec 13 2018 at 01:00):

I am no specialist but I think that as long as you do not relicense the snippet itself that is ok

view this post on Zulip Karl Palmskog (Dec 13 2018 at 01:15):

I mean, there are two options here: (1) the snippet is small enough to be under fair use, or (2) any integration into a project will force the project to become GPLv3

view this post on Zulip Karl Palmskog (Dec 13 2018 at 01:16):

most of our projects use BSD/MIT, @affeldt-aist if you're the author, any chance I could get permission to relicense? (or could you relicense under LGPL at least?)

view this post on Zulip Reynald Affeldt (Dec 13 2018 at 01:29):

claiming fair use seems right to me: the snippet is small and that is the obvious(/only?) way to do it

view this post on Zulip Karl Palmskog (Dec 13 2018 at 01:32):

OK thanks

view this post on Zulip Emilio Jesús Gallego Arias (Dec 13 2018 at 01:33):

It'd be great if that snipped would find its way to the math-comp "extra" repos that we discussed in the first meeting.

view this post on Zulip Emilio Jesús Gallego Arias (Dec 13 2018 at 01:33):

as to avoid having N copies of it floating around

view this post on Zulip Karl Palmskog (Dec 13 2018 at 01:35):

is there any public repo like that yet? I think I have lemmas lying around that could fit there

view this post on Zulip Karl Palmskog (Dec 13 2018 at 01:36):

doing a PR there would feel like a lower threshold to pass than mathcomp proper

view this post on Zulip Reynald Affeldt (Dec 13 2018 at 01:49):

I don't think that such a repo exists yet (still, basic lemmas about nats and lists are still added from time to time to the basic mathcomp library).

view this post on Zulip Reynald Affeldt (Dec 13 2018 at 02:02):

https://github.com/math-comp/math-comp/issues/263

view this post on Zulip Laurent Théry (Gitter import) (Dec 13 2018 at 09:06):

As said in math-comp/math-comp#263

view this post on Zulip Laurent Théry (Gitter import) (Dec 13 2018 at 09:08):

There is a translation from ssr to Z provided by ppsimpl. To try it

opam install coq-ppsimpl

then
Require Import Lia.
Require Import PP.Ppsimplmathcomp.
From mathcomp Require Import all_ssreflect.

Goal forall m n, n + 2 * n <= 4 * n + 4 * m + 3.
move=> m n.
ppsimpl.
lia.

view this post on Zulip Cyril Cohen (Dec 13 2018 at 10:41):

Hi all! We might submit a math-comp workshop or tutorial proposal for ITP 2019. What do you think folks?

view this post on Zulip Reynald Affeldt (Dec 13 2018 at 12:32):

+1 :-)

view this post on Zulip Maxime Dénès (Dec 13 2018 at 12:32):

sounds like a great idea

view this post on Zulip Cyril Cohen (Dec 13 2018 at 13:08):

The idea is @Enrico Tassi'

view this post on Zulip Cyril Cohen (Dec 13 2018 at 13:10):

Should we rather do a workshop or a tutorial? I am more inclined to have a workshop. (At ITP 2016 there was a tutorial)

view this post on Zulip Karl Palmskog (Dec 13 2018 at 17:08):

+1 for workshop

view this post on Zulip Reynald Affeldt (Dec 14 2018 at 05:59):

no risk of conflict with the Coq workshop?

view this post on Zulip Cyril Cohen (Dec 14 2018 at 09:14):

@affeldt-aist I do not know, maybe we can ask for an absence of conflict

view this post on Zulip Reynald Affeldt (Dec 14 2018 at 12:09):

at least for the schedule, because I would like to attend both :-)

view this post on Zulip Karl Palmskog (Dec 14 2018 at 21:31):

for the Coq 8.9 beta, is it recommended to go with mathcomp 1.7.0 or current master?

view this post on Zulip Karl Palmskog (Dec 14 2018 at 21:32):

it seems that both work fine, but not sure what the high-level consequences are

view this post on Zulip Erik Martin-Dorel (Dec 15 2018 at 17:47):

@Karl Palmskog I was wondering the same thing, BTW the current spec of opam packages says: coq-mathcomp-ssreflect.1.7.0 (in coq-released) => "coq" {((>= "8.6" & < "8.9~") | (= "dev"))} and coq-mathcomp-ssreflect.dev (in coq-extra-dev) => "coq" {(>= "8.5" & < "8.9~") | (= "dev")}; if I'm not mistaken the spec in coq-released shouldn't not be modified to cope with Coq 8.9 before its stable release, while the spec in coq-extra-dev could be (?)

view this post on Zulip Karl Palmskog (Dec 15 2018 at 18:32):

@Erik Martin-Dorel it seems quite strange that the package inreleased should be compatible with dev - it could be taken as a guarantee that 1.7.0 should work with master in perpetuity

view this post on Zulip Karl Palmskog (Dec 15 2018 at 18:33):

also is a bit disconcerting that packages in released implicitly have ties to core-dev, which is arguably "experts only"

view this post on Zulip Karl Palmskog (Dec 15 2018 at 18:35):

I think the decision to change < "8.9~" to < "8.10~" in an existing package should be up to every project maintainer

view this post on Zulip Karl Palmskog (Dec 15 2018 at 18:36):

not sure mathcomp has a policy here?

view this post on Zulip Emilio Jesús Gallego Arias (Dec 15 2018 at 22:43):

The dev or dependency likely was added to overcome a limitation of coq-bench which uses opam, but also could be due to a limitation of opam and dev versions themselves.

view this post on Zulip Karl Palmskog (Dec 18 2018 at 23:38):

is there any specific rationale for always beginning with Require Import mathcomp.ssreflect.ssreflect. as a separate command?

view this post on Zulip Karl Palmskog (Dec 18 2018 at 23:39):

as compared to, say, From mathcomp Require Import ssreflect path fintype. and similar

view this post on Zulip Cyril Cohen (Dec 18 2018 at 23:39):

@Karl Palmskog this is for historical reasons (backward compat with Coq 8.6)

view this post on Zulip Cyril Cohen (Dec 18 2018 at 23:40):

please start with From mathcomp Require Import [...] directly from now on

view this post on Zulip Karl Palmskog (Dec 18 2018 at 23:40):

I see, thanks

view this post on Zulip Cyril Cohen (Dec 18 2018 at 23:40):

I often use From mathcomp Require Import all_ssreflect.

view this post on Zulip Karl Palmskog (Dec 18 2018 at 23:41):

and there's no reason to qualify like From mathcomp.ssreflect Require ..., right?

view this post on Zulip Karl Palmskog (Dec 18 2018 at 23:41):

since I believe all module/file names are guaranteed to be unique

view this post on Zulip Cyril Cohen (Dec 18 2018 at 23:41):

yes indeed

view this post on Zulip Karl Palmskog (Dec 18 2018 at 23:42):

:thumbsup:

view this post on Zulip Emilio Jesús Gallego Arias (Dec 19 2018 at 00:42):

Qualification doesn't exactly work like that and indeed could become a problem in the future; in fact it is a problem now [for more efficient builds] as correct dependencies for a module are not context-free, but need access to the whole filesystem exposed in the loadpath to do the search of the module.

view this post on Zulip Cyril Cohen (Dec 19 2018 at 14:41):

@Karl Palmskog hi, I am surprised that you picked finmap for your benchmark here https://users.ece.utexas.edu/~gligoric/papers/PalmskogETAL18piCoq.pdf, and why not the whole mathcomp library?

view this post on Zulip Karl Palmskog (Dec 19 2018 at 18:05):

@Cyril Cohen we needed something that had a history that worked during 8.5

view this post on Zulip Karl Palmskog (Dec 19 2018 at 18:06):

as far as I could tell most commits to mathcomp during the time window we considered (to enable selective checking with .vio) were not big additions/changes

view this post on Zulip Karl Palmskog (Dec 19 2018 at 18:07):

on the other hand, finmap appeared to be under much higher churn and we were able to get it working easily

view this post on Zulip Karl Palmskog (Dec 19 2018 at 18:17):

not getting things to build/compile is very common in empirical software research, cf. https://dibt.unimol.it/staff/fpalomba/documents/J3.pdf ("On average, only 38% of the change history of project systems is currently successfully compilable")

view this post on Zulip Karl Palmskog (Dec 19 2018 at 18:36):

ah, I now see that mathcomp for the time interval we considered probably would have compiled, so I think it was mostly due to the type of changes during the interval. Hope we get to revisit the project for a new study though.

view this post on Zulip Karl Palmskog (Dec 19 2018 at 18:37):

btw, the historic mathcomp versions seem to not be available anymore unless they have moved somewhere else: http://ssr.msr-inria.inria.fr/FTP/

view this post on Zulip Emilio Jesús Gallego Arias (Dec 20 2018 at 18:13):

@Karl Palmskog I have a git repos on math-comp released versions

view this post on Zulip Emilio Jesús Gallego Arias (Dec 20 2018 at 18:13):

for self study

view this post on Zulip Emilio Jesús Gallego Arias (Dec 20 2018 at 18:13):

starting in fact from 4 color to 1.6

view this post on Zulip Emilio Jesús Gallego Arias (Dec 20 2018 at 18:13):

I should publish it somehwere

view this post on Zulip Emilio Jesús Gallego Arias (Dec 20 2018 at 18:14):

let me know if you need a copy

view this post on Zulip Karl Palmskog (Dec 20 2018 at 19:49):

@Emilio Jesús Gallego Arias I don't think we need them right now, but making them public would be useful

view this post on Zulip Emilio Jesús Gallego Arias (Dec 20 2018 at 20:08):

Yeah I should ask the devs first tho

view this post on Zulip Karl Palmskog (Jan 03 2019 at 22:22):

thanks to Enrico, the full archive is back on GitHub: https://github.com/math-comp/math-comp/releases/tag/archive

view this post on Zulip Karl Palmskog (Jan 03 2019 at 22:37):

anyone know if the revision history before GitHub still exists? would be interesting for research purposes, e.g., computing process metrics such as how many lines were changed in a commit, regression proving times, etc.

view this post on Zulip Erik Martin-Dorel (Jan 18 2019 at 09:17):

Hi all, even if Coq 8.9.0 has not yet been released, IMHO it could be useful to bump both coq-mathcomp-ssreflect.dev and coq-mathcomp-ssreflect.1.7.0's required version of coq to {< "8.10~"} (so that (1) mathcomp's CI could be tested against Coq 8.9+beta1 from now on and (2) projects relying on 1.7.0 could smoothly switch to coq-8.9)... Do you agree? If it helps, I could propose a PR in opam-coq-archive.

view this post on Zulip Enrico Tassi (Jan 18 2019 at 11:10):

anyone know if the revision history before GitHub still exists?

I can access it, and I can give you a git-svn clone, but it was not public and is messy (eg contains also papers, schools material, ci scripts...). So please do not just post it online. I'll try to build the clone tonight (IIRC it was terribly slow, I'll let it run overnight) so that I can hand it to you tomorrow. Or I can send it to you later on if we don't manage to exchange the file.

view this post on Zulip Enrico Tassi (Jan 18 2019 at 11:21):

Oh, I've the git-svn export here on my laptop, so I can just give you the 150M zip to you @Karl Palmskog , just find me (I assume you are at POPL, or will be tomorrow)

view this post on Zulip Karl Palmskog (Jan 18 2019 at 19:06):

@Enrico Tassi great, hopefully we can sync during CoqPL

view this post on Zulip Karl Palmskog (Jan 25 2019 at 06:35):

I have many projects that use MathComp and extract code to OCaml. There are many quirks in this, which I believe others also face. To document quirks and ask for advice, would it be reasonable to open a MathComp GitHub issue? Or is that only for Coq side of things?

view this post on Zulip Karl Palmskog (Jan 25 2019 at 06:37):

ideally one would refine code away from some MathComp structures that behave strangely when extracted, but this is not all that easy to set up

view this post on Zulip Assia Mahboubi (Jan 28 2019 at 13:51):

Hi! I would like to work with 2 variable polynomials, more precisely to define a few concepts related to elliptic curves over Q. I tried to use the notations of polyXY but so far I am stuck with cumbersome notations. For instance, if b is a rational parameter, polynomial X + b Y is typeset 'X + b%:P%:P *'Y which does not look so nice. Polynomial X + 2Y is 'X + 2%:Q%:P%:P*Y which is hardly readable. Is there a better solution?

view this post on Zulip Cyril Cohen (Jan 28 2019 at 13:59):

Hi @Assia Mahboubi , for your second example, you could just write 'X + 2%:R * 'Y. For the first one, I know no easy way (i.e. two solutions: 1. switching to multivariate polynomials, 2. extending mathcomp with a specific bivariate polynomial type and making it a lmodType R, so that 'X + b *: 'Y would work)

view this post on Zulip Cyril Cohen (Jan 28 2019 at 14:01):

hi @Karl Palmskog, I know no better way than doing the CoqEAL way, ... I hope that is works better this year though.

view this post on Zulip Karl Palmskog (Jan 28 2019 at 14:02):

@Cyril Cohen I like the general setup and will try to use it, but there are some things like: how do I have my finType not keep a list of all members

view this post on Zulip Karl Palmskog (Jan 28 2019 at 14:02):

that seems like something a bit orthogonal to CoqEAL in itself

view this post on Zulip Cyril Cohen (Jan 28 2019 at 14:03):

@Karl Palmskog I am not sure I understand what you mean by "not keep a list of all members"

view this post on Zulip Karl Palmskog (Jan 28 2019 at 14:03):

basically, I had this fintype with a lot of members, but never used enum anywhere

view this post on Zulip Karl Palmskog (Jan 28 2019 at 14:04):

and I was seeing weird performance issues because the extracted code was populating the list of all members of the fintype every time I ran it

view this post on Zulip Karl Palmskog (Jan 28 2019 at 14:05):

so I short-circuited that out with an extraction directive

view this post on Zulip Karl Palmskog (Jan 28 2019 at 14:06):

specifically: Extract Inlined Constant fintype.ord_enum => "(fun _ -> [])".

view this post on Zulip Cyril Cohen (Jan 28 2019 at 14:08):

The principle of data refinements is that you replace a datatype with another, so if you never use enum, you don't get to extract it...

view this post on Zulip Karl Palmskog (Jan 28 2019 at 14:10):

right, so it helps having heuristics like: when you're using a finType and don't use enum, here's what you should replace it with during refinement...

view this post on Zulip Karl Palmskog (Jan 28 2019 at 14:16):

@Cyril Cohen hoping to get to explore CoqEAL soon, let me know if you want help to test/package, etc., for 8.9

view this post on Zulip Assia Mahboubi (Jan 28 2019 at 14:51):

@Cyril Cohen . As usual, the problem is not only the notation here, but the composition of embeddings. And 2%:R and 2%:P%:P are not convertible.

view this post on Zulip Assia Mahboubi (Jan 28 2019 at 15:08):

I think that making 1. work would be the best option (I guess that by multivariate polynomials you mean math-comp/multinomials?) But we have to work with @Florent Hivert and @Pierre-Yves Strub to finalize the Dagsthul discussion and merge it.

view this post on Zulip Cyril Cohen (Jan 28 2019 at 15:13):

@Assia Mahboubi, I agree

view this post on Zulip Cyril Cohen (Jan 28 2019 at 15:14):

@Karl Palmskog I will gladly ask for your help

view this post on Zulip Erik Martin-Dorel (Jan 28 2019 at 15:40):

FYI regarding option 2., Laurent Théry and I had developed some material in the TaMaDi/CoqHensel project (before polyXY.v was available in mathcomp) here: http://tamadi.gforge.inria.fr/CoqHensel/coqhensel-2.1.0-coqdoc/CoqHensel.bipoly.html (this theory is not subsumed by polyXY.v but there is obviously some overlap as it also relies onNotation bipoly := {poly {poly R}} for R : ringType or R : comRingType), anyway option 1. indeed seems a good choice

view this post on Zulip Assia Mahboubi (Jan 28 2019 at 15:52):

Many thanks for your answer @Erik Martin-Dorel ! By the way, is CoqHensel still maintained? This webpage refers to coq versions <= 8.4. Do you think that CoqHensel is a relevant test case for the multinomial library? If so would it be hard to resurrect it?

view this post on Zulip Erik Martin-Dorel (Jan 28 2019 at 16:11):

Hi @Assia Mahboubi! Indeed the last release of CoqHensel was for Coq 8.4, and I guess some parts of the library could/should be refactored to benefit from new features and support lemmas in mathcomp. I've just checked that the bipoly.v theory you might be interested (to write e.g. Check fun (b : rat) => 'X + b *:: 'Y.) still compiles with mathcomp.1.7.0 and coq.8.7, but CoqHensel does not only deal with bivariate polynomials, so I'd be very glad to "ressurect" CoqHensel soon (by proposing some mathcomp PR to integrate results that could be useful in general, and putting the other specialized results in a GitHub repo or so ...)

view this post on Zulip Assia Mahboubi (Jan 29 2019 at 15:10):

@Erik Martin-Dorel Good idea! PR complementing mathcomp are very welcome. Regarding bipoly, my impression is that multinomial would ideally subsume polyXY, and thus the right test would be to see whether CoqHensel can make use of multinomial to replace bipoly.

view this post on Zulip Emilio Jesús Gallego Arias (Jan 29 2019 at 18:59):

@Karl Palmskog wrt extraction indeed that also bothers me quite a log, for example in the verdilog proof, we had to do terrible hacks

view this post on Zulip Emilio Jesús Gallego Arias (Jan 29 2019 at 18:59):

so count with me to help in improving this

view this post on Zulip Pierre-Yves Strub (Jan 30 2019 at 12:51):

mathcomp -real-closed.dev does not compile with Coq 8.8.2?

view this post on Zulip Reynald Affeldt (Jan 31 2019 at 00:01):

related matter: with Coq 8.9.0, the git version of real-closed needs a few minor fixes https://github.com/math-comp/real-closed/pull/7/commits

view this post on Zulip Karl Palmskog (Feb 07 2019 at 16:22):

this is related to the discussion on extraction of mathcomp above (sadly, uses forks of Coq+MathComp): https://github.com/pi8027/efficient-finfun

view this post on Zulip Karl Palmskog (Feb 07 2019 at 16:23):

paper: https://doi.org/10.1007/978-3-319-90686-7_4

view this post on Zulip Karl Palmskog (Feb 07 2019 at 16:24):

I think I will at least copy some key extraction directives from that work

view this post on Zulip Kazuhiko Sakaguchi (Mar 22 2019 at 10:40):

@Karl Palmskog Hello. I'm the author of that paper. The structures in MathComp (eqType, finType, etc.) are defined as records which includes all the mixins of super classes. Generally, many of these mixins are useless in extracted code. I have tried to eliminate them by inlining, in the Sec 4.1 of my paper. It requires some changes on the extraction plugin and the current implementation is ad-hoc.

view this post on Zulip Karl Palmskog (Mar 22 2019 at 19:58):

@Kazuhiko Sakaguchi so are there parts of the inlining approach that can be used even without the modified plugin? Could the plugin be separated and packaged separately from the efficient-finfun development?

view this post on Zulip Karl Palmskog (Mar 22 2019 at 21:02):

@Kazuhiko Sakaguchi it may also be a good idea to build directly on reglang instead of patching: https://github.com/chdoc/coq-reglang (OPAM package: coq-reglang)

view this post on Zulip Kazuhiko Sakaguchi (Mar 25 2019 at 10:34):

@Karl Palmskog We wouldn't get a satisfactory result with MathComp+extraction without any modification because the extraction plugin cannot inline this:

let t := C t_1 ... t_n in (* C is a constructor *)
... (match t with ... end) ... .

My plugin could be packaged separately but I want to reimplement the extraction plugin in a more satisfactory way and contribute it to Coq. I have no enough time to do this now.

I have heard from @Christian Doczkal that he refined definitions in coq-reglang for proofs but might deoptimized them for execution. So I didn't try it yet.

view this post on Zulip Christian Doczkal (Mar 25 2019 at 11:58):

@Kazuhiko Sakaguchi , are you talking about the defintion of operations on finite automata? If so, the difference between the new coq-reglang and the CPP paper, besides quite a bit of general cleanup, is that the constructions for sequential composition and A* now yield NFAs with epsilon-transitions that are eliminated in a second step. This leads to a cleaner lemma statements, because one does not have to treat empty words separately. The old construction was essentially inlining a bit of on-the-fly epsilon-closure to avoid having to define epsilon-NFAs.

view this post on Zulip Kazuhiko Sakaguchi (Mar 25 2019 at 17:39):

@Christian Doczkal Yes. So you would use fingraph.connect to compute epsilon-closure. Using fingraph.dfs instead of it is better for the performance of the extracted code.

view this post on Zulip Karl Palmskog (Mar 25 2019 at 17:42):

if you already have a rel T, not sure how dfs would help over connect

view this post on Zulip Christian Doczkal (Mar 25 2019 at 17:42):

Isn't connect implemented using dfs? In any case, the old formalization does not compute epsilon-closure at all, because the "moral" epsilon-edges can only occur around the auxiliary state, and so no closure computation was/is required.

view this post on Zulip Karl Palmskog (Mar 25 2019 at 17:43):

yes, the only thing that happens in connect is that you turn a rel T into T -> seq T via rgraph before calling dfs

view this post on Zulip Kazuhiko Sakaguchi (Mar 25 2019 at 17:48):

https://github.com/math-comp/math-comp/blob/master/mathcomp/ssreflect/fingraph.v#L139
https://github.com/chdoc/coq-reglang/blob/master/theories/nfa.v#L57
[set q : T | connect ... p q] requires to compute the same dfs #|T| times.

view this post on Zulip Kazuhiko Sakaguchi (Mar 25 2019 at 17:54):

So let s := dfs (enfa_trans None) #|T| [::] x in [set q | q \in s] is better for computation.

view this post on Zulip Karl Palmskog (Mar 25 2019 at 18:12):

hmm, that should be possible to improve further

view this post on Zulip Karl Palmskog (Mar 25 2019 at 19:06):

@Kazuhiko Sakaguchi this is arguably just as wasteful, unless we know that this is a disjoint union: https://github.com/chdoc/coq-reglang/blob/master/theories/nfa.v#L66

view this post on Zulip Karl Palmskog (Mar 25 2019 at 19:07):

could be written in the seqworld using foldl

view this post on Zulip Karl Palmskog (Mar 25 2019 at 19:19):

the best solution is probably to do a full-scale CoqEAL-style refinement

view this post on Zulip Christian Doczkal (Mar 25 2019 at 19:22):

that's my thinking as well, although this is something I never looked at too closely. I'd expect there to be more places that cause similar inefficiencies and I'd like to avoid these things spreading all over the place. (What you do in your forks is your business, of course).

view this post on Zulip Karl Palmskog (Mar 25 2019 at 19:23):

oh, deleted the link with the redefinition by accident, here it is: https://github.com/palmskog/coq-reglang/commit/78339fe351b35f09c45d259fdec59b4c83a20102

view this post on Zulip Karl Palmskog (Mar 25 2019 at 19:23):

yeah that was just an experiment

view this post on Zulip Christian Doczkal (Mar 25 2019 at 19:24):

had already looked at it, that one doesn't look bad, but it does look a bit like opening Pandora's box. In any case, more on that maybe tomorrow, getting kind of late here ...

view this post on Zulip Kazuhiko Sakaguchi (Mar 25 2019 at 19:27):

That's nice. There would be many possible performance improvements, e.g., efficient subset construction producing only reachable states. > CoqEAL-style refinement

view this post on Zulip Karl Palmskog (Mar 25 2019 at 19:31):

in any case, almost the same optimizations showed up for me in another context, so some subset of us should likely be looking at this more closely

view this post on Zulip Karl Palmskog (Mar 25 2019 at 19:33):

specifically, I ad-hoc-refined dfs to use red-black trees: https://github.com/palmskog/chip/blob/bf75377c2a3b29793f5e0058c752cd6b3c708c48/core/dfs_set.v#L117-L119

view this post on Zulip Karl Palmskog (Mar 25 2019 at 19:34):

gave 10-30% speedups for sparse graphs

view this post on Zulip Karl Palmskog (Mar 25 2019 at 19:50):

hmm, I still have no intuition for when a mathcomp datatype should be a Variant vs. Inductive, shouldn't this be Variant: https://github.com/math-comp/math-comp/blob/master/mathcomp/ssreflect/fingraph.v#L72-L73

view this post on Zulip Kazuhiko Sakaguchi (Mar 25 2019 at 19:59):

@Karl Palmskog I think that should be Variant. We want to avoid generating elimination scheme for non-recursive data types. relevant discussion: https://github.com/coq/coq/pull/7536

view this post on Zulip Karl Palmskog (Mar 25 2019 at 20:08):

then likely all the following are wrong as well

algebra/vector.v:116:Inductive mixin_of (V : lmodType R) := Mixin dim & axiom_def dim (Phant V).
algebra/vector.v:1898:Inductive subvs_of : predArgType := Subvs u & u \in U.
algebra/finalg.v:428:Inductive unit_of (phR : phant R) := Unit (x : R) of x \is a GRing.unit.
algebra/matrix.v:211:Inductive matrix : predArgType := Matrix of {ffun 'I_m * 'I_n -> R}.
algebra/fraction.v:30:Inductive ratio := mkRatio { frac :> R * R; _ : frac.2 != 0 }.
ssreflect/seq.v:2818:Inductive all_iff_and (P Q : Prop) : Prop := AllIffConj of P & Q.
ssreflect/fintype.v:1582:Inductive ordinal : predArgType := Ordinal m of m < n.
ssreflect/finset.v:110:Inductive set_type : predArgType := FinSet of {ffun pred T}.
ssreflect/finfun.v:42:Inductive finfun_type : predArgType := Finfun of #|aT|.-tuple rT.
fingroup/fingroup.v:1744:Inductive subg_of : predArgType := Subg x & x \in G.
fingroup/presentation.v:109:Inductive env gT := Env of {set gT} & seq gT.

view this post on Zulip Kazuhiko Sakaguchi (Mar 26 2019 at 08:41):

@Karl Palmskog I'm not sure that they are bugs, but replacing them with Variants (and Records?) would be a good improvement. Can you send PR to fix it?

view this post on Zulip Karl Palmskog (Mar 27 2019 at 18:56):

@Christian Doczkal if you don't mind, I'll record the refinement ideas discussed with @Kazuhiko Sakaguchi as issues in the coq-reglang GitHub repo. It could be spun off into a new repo in the future.

view this post on Zulip Karl Palmskog (Mar 27 2019 at 18:58):

but I think one would really want the plugin from @Kazuhiko Sakaguchi for practical viability

view this post on Zulip Karl Palmskog (Mar 27 2019 at 18:59):

(also, I'll try to report the Variant issues to the mathcomp repo this weekend)

view this post on Zulip Christian Doczkal (Mar 28 2019 at 16:32):

@Karl Palmskog , sure, create any issues you like. I'd be very much interested to see how much one needs to refine in order to extract reasonable programs and whether one can do so without compromising too much as it comes to the "proof centered" definitions currently being used.

view this post on Zulip Karl Palmskog (Mar 28 2019 at 21:00):

my experience has been that one never wants to use the rel V representation of graphs in practice, only the V -> seq V one

view this post on Zulip Karl Palmskog (Mar 28 2019 at 21:01):

but I guess for some algorithms it may work out

view this post on Zulip Kazuhiko Sakaguchi (Apr 01 2019 at 11:05):

I have reimplemented the fintype equipped with indexing which is completely backward-compatible. If someone wants to use it, I will send PR.

view this post on Zulip Kazuhiko Sakaguchi (Apr 01 2019 at 11:26):

I got an idea about reimplementing the extraction plugin in a satisfactory way. I also have started to check the current issues of extraction. (I don't like to rebase my plugin repetitively, so I need to merge it into Coq.)

view this post on Zulip Karl Palmskog (Apr 01 2019 at 15:15):

@Kazuhiko Sakaguchi Coq devs are open to adding external plugins into their CI and provide PRs to fix them when they break

view this post on Zulip Karl Palmskog (Apr 01 2019 at 15:16):

but of course, it may still be nice to have it merged into Coq proper

view this post on Zulip Karl Palmskog (Apr 03 2019 at 04:14):

hmm, some developments sadly not getting proper mention here (panel background an issue?): https://blogs.scientificamerican.com/cross-check/okay-maybe-proofs-arent-dying-after-all/

view this post on Zulip Karl Palmskog (Apr 03 2019 at 04:15):

(followup to this apparently controversial 1993 article)

view this post on Zulip Assia Mahboubi (May 22 2019 at 11:39):

Hi. I am trying to update the real_closed library, which seems to break with the latest versions of its dependencies. I have an issue with l.498 of polyrcf.v. I have no idea how to fix this quickly. Any suggestion?

view this post on Zulip Enrico Tassi (May 22 2019 at 11:50):

@Assia Mahboubi I don't get what are doing exactly, but given the time my question is: does this problem affect the release?

view this post on Zulip Assia Mahboubi (May 22 2019 at 11:50):

no

view this post on Zulip Assia Mahboubi (May 22 2019 at 11:50):

at least, I do not think so.

view this post on Zulip Assia Mahboubi (May 22 2019 at 11:53):

The context is: I am trying to port my proof of Apéry theorem. And this library is in the dependencies. But I do not know it well enough to be able to make a diagnostic, here, and to understand whether the problem with this line comes from the changes in the treatment of order, or from the tactic language, or from something else.

view this post on Zulip Enrico Tassi (May 22 2019 at 11:56):

well, me neither ;-) sorry

view this post on Zulip Assia Mahboubi (May 22 2019 at 11:58):

sure, no worries. In fact I was hoping to get insight from @Kazuhiko Sakaguchi or @Cyril Cohen, who did similar ports recently if I understand correctly.

view this post on Zulip Kazuhiko Sakaguchi (May 22 2019 at 12:01):

@Assia Mahboubi Hello. Which version of mathcomp do you use? master?

view this post on Zulip Assia Mahboubi (May 22 2019 at 12:02):

Hello. mathcomp-1.8.

view this post on Zulip Kazuhiko Sakaguchi (May 22 2019 at 12:13):

Is homo_mono_in or ltr_hornerW undefined?

view this post on Zulip Assia Mahboubi (May 22 2019 at 12:16):

They are defined: ltr_hornerWis the lemme just above in the same file, and homo_mono_in is in ssrbool. But the script is broken (even with an apply) and I could not see how to fix it quickly. I thought may be you had similar issues when working on ordered structures.

view this post on Zulip Kazuhiko Sakaguchi (May 22 2019 at 12:21):

I have tried to fix real-closed recently but I didn't see the same problem here: https://github.com/math-comp/real-closed/pull/16/files

view this post on Zulip Assia Mahboubi (May 22 2019 at 12:26):

did you manage to compile polyrcf?

view this post on Zulip Assia Mahboubi (May 22 2019 at 12:29):

I forgot to say that I was trying to work with real-closed's master. I am trying now with version 1.01. It does not compile but the required changes start the same (adding a few /=, that you also have in your PR).

view this post on Zulip Kazuhiko Sakaguchi (May 22 2019 at 12:29):

With the experiment/order branch and the above change, polyrcf did compile (but may not compile now). Now I'm trying to reproduce your problem.

view this post on Zulip Assia Mahboubi (May 22 2019 at 12:31):

Many thanks!

view this post on Zulip Assia Mahboubi (May 22 2019 at 12:48):

Ok, I managed to fix polyrcf in real-closed's version 1.0.1.

view this post on Zulip Assia Mahboubi (May 22 2019 at 12:48):

But other files need fix.

view this post on Zulip Assia Mahboubi (May 22 2019 at 12:49):

I continue.

view this post on Zulip Kazuhiko Sakaguchi (May 22 2019 at 12:49):

Is this problem introduced by coq/coq#9995?

view this post on Zulip Kazuhiko Sakaguchi (May 22 2019 at 12:52):

OK.

view this post on Zulip Assia Mahboubi (May 22 2019 at 12:52):

if you really mean "introduced" then I do not think so, as I mathcomp-1.8 does not include that code if I understand correctly.

view this post on Zulip Assia Mahboubi (May 22 2019 at 12:53):

Does the PR solves known issues this could be an instance of?

view this post on Zulip Assia Mahboubi (May 22 2019 at 13:01):

A similar problem occurs, but later, at line 976 in realalg...

view this post on Zulip Kazuhiko Sakaguchi (May 22 2019 at 13:08):

@Assia Mahboubi Hmm. I don't understand what's happened. But this one may help you if still broken. https://github.com/math-comp/real-closed/pull/17

view this post on Zulip Assia Mahboubi (May 22 2019 at 13:36):

Many thanks, I thought this PR was too outdated to be relevant, but indeed it suggested the solution to my current issue.

view this post on Zulip Assia Mahboubi (May 22 2019 at 14:16):

@affeldt-aist @Kazuhiko Sakaguchi , thanks a lot, math-comp/real-closed#17 compiles out of the box, contrarily to what CI suggests (the problems seems to be only a docker issue)

view this post on Zulip Anton Trunov (May 22 2019 at 14:26):

Hi! I’m wondering what the release enumeration scheme for mathcomp is. I’m updating fcsl-pcm library for the 1.9.0 release and I need to change the version range for mathcomp in the opam file. Is this the correct way to do it or do I need to say < “2.0~"?

"coq-mathcomp-ssreflect" {(>= "1.9.0" & < "1.10~") | (= "dev")}

Thank you.

view this post on Zulip Karl Palmskog (May 22 2019 at 14:55):

@Anton Trunov maybe you can open a real GitHub issue about this, I will have the same problem for my packages

view this post on Zulip Anton Trunov (May 22 2019 at 14:57):

@Karl Palmskog I just found 1.10.0 in Milestones: https://github.com/math-comp/math-comp/milestones

view this post on Zulip Karl Palmskog (May 22 2019 at 15:08):

ah, good to know

view this post on Zulip Anton Trunov (May 22 2019 at 15:11):

On the other hand, it’s probably not a big deal, since I guess 1.10~ < 2.0~. So even if 1.10 release is skipped for some reason, we will still be on the safe side.

view this post on Zulip Kazuhiko Sakaguchi (May 27 2019 at 08:30):

Should we relocate the changelog file for new changes to CHANGELOG_UNRELEASED.md as like as #210? @Cyril Cohen @Enrico Tassi

view this post on Zulip Cyril Cohen (May 27 2019 at 08:33):

I think we decided that in https://github.com/math-comp/math-comp/wiki/Agenda-of-the-April-23rd-2019-meeting-9h30-to-12h30#avoiding-issues-with-changelog

view this post on Zulip Kazuhiko Sakaguchi (May 27 2019 at 08:35):

Now I see. Thanks.

view this post on Zulip Anton Trunov (May 29 2019 at 10:45):

Is there a way to restart CI? It looks like CI failed for PR #351 for some unrelated to the changes reasons

view this post on Zulip Karl Palmskog (Jun 05 2019 at 08:44):

@Cyril Cohen here is my attempted port of Elliptic Curves to Coq8.10+MC1.9.0 where I get stuck: https://github.com/palmskog/elliptic-curves-ssr/tree/dev-compatibility

view this post on Zulip Karl Palmskog (Jun 05 2019 at 08:47):

here is a list of projects we tried:

Projects we found a SHA for that works with Coq8.10+MC1.9.0 (sometimes by forking):
https://github.com/math-comp/math-comp
https://github.com/imdea-software/fcsl-pcm
https://github.com/DistributedComponents/disel
https://github.com/palmskog/coq-reglang
https://github.com/palmskog/comp-dec-pdl
https://github.com/math-comp/odd-order
https://github.com/math-comp/fourcolor
https://github.com/math-comp/finmap
https://github.com/math-comp/bigenough
https://github.com/math-comp/analysis
https://github.com/math-comp/real-closed
https://github.com/affeldt-aist/coq-robot
https://github.com/math-comp/multinomials

Projects with no known SHA that works with Coq8.10+MC1.9.0:
https://github.com/palmskog/elliptic-curves-ssr
https://github.com/affeldt-aist/infotheo
https://github.com/affeldt-aist/monae

view this post on Zulip Karl Palmskog (Jun 05 2019 at 08:49):

any tips about other large MathComp projects that (could) work with Coq8.10+MC1.9.0 are welcome (cc: @Kazuhiko Sakaguchi @Anton Trunov)

view this post on Zulip Karl Palmskog (Jun 05 2019 at 08:51):

the end goal here is to build a "snapshot" of high quality MathComp-related projects that can be analyzed, e.g., after serialization via SerAPI

view this post on Zulip Anton Trunov (Jun 05 2019 at 08:52):

@Karl Palmskog Does toychain work with MC1.9.0?

view this post on Zulip Karl Palmskog (Jun 05 2019 at 08:52):

oh right, I should check

view this post on Zulip Karl Palmskog (Jun 05 2019 at 08:53):

if not I guess I should port

view this post on Zulip Anton Trunov (Jun 05 2019 at 08:54):

Also, I recently ported coq-bits to work with MC1.9, here is the PR: https://github.com/artart78/coq-bits/pull/1

view this post on Zulip Assia Mahboubi (Jun 05 2019 at 08:55):

Hi @Karl Palmskog. You should definitively contact @Pierre-Yves Strub (pierre-yves@Pierre-Yves Strub.nu) regarding your attempted port.

view this post on Zulip Anton Trunov (Jun 05 2019 at 08:56):

@Karl Palmskog I think I’m gonna open a coq-community issue asking the authors to transfer ownership of coq-bits and coq-bitset.

view this post on Zulip Karl Palmskog (Jun 05 2019 at 08:59):

@Anton Trunov good idea, I was wondering what happened with those projects, but I think they would take some effort to port

view this post on Zulip Anton Trunov (Jun 05 2019 at 08:59):

coq-bits are done I think, and I’m working on coq-bitset now, hopefully it’ll be finished by the end of this week

view this post on Zulip Karl Palmskog (Jun 05 2019 at 09:00):

@Assia Mahboubi I will synchronize with Cyril first (we are both at the Coq users+dev workshop), and then I will probably email Pierre-Yves

view this post on Zulip Karl Palmskog (Jun 05 2019 at 09:01):

basically, we aren't looking to become maintainers but will be happy to contribute any and all changes upstream

view this post on Zulip Assia Mahboubi (Jun 05 2019 at 09:02):

Ok. Thanks for the context. I mentioned this because I think @Pierre-Yves Strub is still interested in (actively) maintaining this library alive.

view this post on Zulip Karl Palmskog (Jun 05 2019 at 09:02):

@Anton Trunov please point me to your coq-bits repo when it's available

view this post on Zulip Karl Palmskog (Jun 05 2019 at 09:04):

ah ok I missed the link

view this post on Zulip Emilio Jesús Gallego Arias (Jun 05 2019 at 10:04):

@Anton Trunov actually there is a fork for coq-bits https://github.com/ejgallego/ssrbit which indeed uses a different approach

view this post on Zulip Emilio Jesús Gallego Arias (Jun 05 2019 at 10:05):

it is a long story but the paper on the fork got stuck, depending on what you are trying to do ssrbit may work better for you

view this post on Zulip Emilio Jesús Gallego Arias (Jun 05 2019 at 10:05):

however it misses some lemmas

view this post on Zulip Emilio Jesús Gallego Arias (Jun 05 2019 at 10:06):

I am not sure Arthur is interested in the lib anymore, you should ask him of course

view this post on Zulip Anton Trunov (Jun 05 2019 at 10:07):

@Emilio Jesús Gallego Arias this looks interesting, thank you. It appears your fork uses some non-trivial dependencies. How hard do you think would it be to bring ssrbit up-to-date with the current Coq and MC versions?

view this post on Zulip Emilio Jesús Gallego Arias (Jun 05 2019 at 10:20):

I can do that next week

view this post on Zulip Emilio Jesús Gallego Arias (Jun 05 2019 at 10:21):

and we could discuss about the lib , if @Pierre-Yves Strub is interested, as to discuss what limitations, API needs, etc... it does have ; I'll check with Pierre-Evariste to see if he has time too

view this post on Zulip Emilio Jesús Gallego Arias (Jun 05 2019 at 10:24):

the old lib had a few issues due mainly to computing with proofs [which turns out was done in the original x86 fork], see for example https://github.com/artart78/coq-bits/blob/master/src/spec/operations.v#L21 so this is indeed using map_tuple not the subjacent map.

In ssrbit we did indeed implement the operations à la tuple, with operations over plain sequences, plus proofs

view this post on Zulip Emilio Jesús Gallego Arias (Jun 05 2019 at 10:25):

The main challenge of the bit library is indeed deciding which operations should be the basic ones, you have a rich theory of bit operators however most are definable in terms of each other

view this post on Zulip Emilio Jesús Gallego Arias (Jun 05 2019 at 10:25):

@Anton Trunov please open an issue in the ssrbits repos with what you need so Pierre-Evariste is in the loop and assign it to me, otherwise I'll slip

view this post on Zulip Anton Trunov (Jun 05 2019 at 10:27):

@Emilio Jesús Gallego Arias I basically need a library to implement “safe” arithmetics (with functions like add and so on signalling underflows/oferflows), reason about the correctness of implementation and extract the safe functions into OCaml.

view this post on Zulip Anton Trunov (Jun 05 2019 at 10:29):

The main challenge of the bit library is indeed deciding which operations should be the basic ones, you have a rich theory of bit operators however most are definable in terms of each other

I agree, lots of design space here

view this post on Zulip Anton Trunov (Jun 05 2019 at 10:32):

@Emilio Jesús Gallego Arias I opened the issue, but GitHub does not let me assing it to you :(

view this post on Zulip Emilio Jesús Gallego Arias (Jun 05 2019 at 10:38):

oh, let fix that

view this post on Zulip Emilio Jesús Gallego Arias (Jun 05 2019 at 10:39):

thanks!

view this post on Zulip Anton Trunov (Jun 05 2019 at 10:40):

thank you, I hope the library fits the use case I have

view this post on Zulip Karl Palmskog (Jun 05 2019 at 11:16):

OK thanks to @Cyril Cohen the port of Elliptic Curves to Coq 8.10 + MC 1.9.0 is now done, I will open a PR and email Pierre-Yves

view this post on Zulip Karl Palmskog (Jun 06 2019 at 08:06):

thanks @Pierre-Yves Strub for merging!

view this post on Zulip Karl Palmskog (Jun 07 2019 at 07:53):

@Kazuhiko Sakaguchi do you think one could/should write this functor in the "packaging mathematical structures" style? https://github.com/certichain/toychain/blob/master/Structures/Parameters.v

view this post on Zulip Karl Palmskog (Jun 07 2019 at 07:55):

it feels very non-idiomatic to mix the usual MathComp approach with functors, even though it's mostly for extraction purposes here

view this post on Zulip Kazuhiko Sakaguchi (Jun 07 2019 at 08:27):

@Karl Palmskog @affeldt-aist might have some experiences in defining classes of functors and their hierarchy.

view this post on Zulip Kazuhiko Sakaguchi (Jun 07 2019 at 08:35):

Ah, what I said is about functors like monads. Now I don't understand what Parameters.v does...

view this post on Zulip Cyril Cohen (Jun 07 2019 at 08:40):

@Karl Palmskog since you show only one module, "packaging mathematical structures" does not really make much sense yet, but sure you could prefer putting this in a record rather in a module.

view this post on Zulip Karl Palmskog (Jun 07 2019 at 09:29):

yeah I was thinking mainly of writing an idiomatic record type, there is also another functor: https://github.com/certichain/toychain/blob/master/Structures/Types.v

view this post on Zulip Karl Palmskog (Jun 07 2019 at 09:32):

@Kazuhiko Sakaguchi basically, whenever one thinks of "I have some structure that I want to instantiate in multiple ways" the default approach for many Coq users would be a module type/functor, but it seems to me one would almost never want to mix them with MathComp structures

view this post on Zulip Karl Palmskog (Jun 07 2019 at 09:35):

note that this is about the features used in the Coq development, not about encoding category theory in Coq

view this post on Zulip Karl Palmskog (Jun 19 2019 at 17:41):

@Cyril Cohen thanks for your work on the finmap library, we used it extensively in some recent work: https://github.com/runtimeverification/algorand-verification

view this post on Zulip Cyril Cohen (Jun 19 2019 at 19:53):

@Karl Palmskog thanks

view this post on Zulip Cyril Cohen (Jun 21 2019 at 17:53):

@Karl Palmskog please feel free to report bugs, make suggestions and pull requests. FYI, math-comp/finmap/finmap.v and math-comp/finmap/order.v are both going to be integrated to math-comp/math-comp as respectively math-comp/math-comp#259 and math-comp/math-comp#270 .

view this post on Zulip Karl Palmskog (Jun 21 2019 at 18:04):

@Cyril Cohen will do, one from the top of my head is that having to do Import Order.Theory Order.Syntax Order.Def. was not obvious to get access to the order-related notations and so on. But this may have already been fixed after 1.2.1?

view this post on Zulip Erik Martin-Dorel (Jun 25 2019 at 00:29):

Hi, when discussing with a colleague I realized that these two definitions below are not part of math-comp… Do you think they should be included? or they are too straightforward to be worth it.

Definition tuple_of_finfun :
  forall (T : Type) (n : nat), (T ^ n)%type -> n.-tuple T :=
  fun T n f => ecast i (i.-tuple T) (card_ord n) (fgraph f).

Definition finfun_of_tuple :
  forall (T : Type) (n : nat), n.-tuple T -> (T ^ n)%type :=
  fun T n t => Finfun (ecast i (i.-tuple T) (esym (card_ord n)) t).

view this post on Zulip Cyril Cohen (Jun 25 2019 at 08:50):

@Karl Palmskog Hi, I guess it is better documented (cf https://github.com/math-comp/finmap/blob/master/order.v#L10-L18) but is it what you expect as a "fix", or would you have liked something else?

view this post on Zulip Cyril Cohen (Jun 25 2019 at 08:56):

@Erik Martin-Dorel you should rather write them like this:

Definition tuple_of_finfun (T : Type) (n : nat) (f : T ^ n) : n.-tuple T :=
  [tuple f i | i < n].

Definition finfun_of_tuple (T : Type) (n : nat) (t : n.-tuple T) : (T ^ n) :=
  [ffun i => tnth t i].  (* alternatively  finfun (tnth t) *)

And then they are so obvious they can be inlined.

view this post on Zulip Erik Martin-Dorel (Jun 25 2019 at 09:20):

@Cyril Cohen OK thanks

view this post on Zulip Cyril Cohen (Jun 25 2019 at 09:28):

@Erik Martin-Dorel you might still want to submit

Section FinFunTuple.

Context {T : Type} {n : nat}.

Definition tuple_of_finfun (f : T ^ n) : n.-tuple T := [tuple f i | i < n].

Definition finfun_of_tuple (t : n.-tuple T) : (T ^ n) := [ffun i => tnth t i].

Lemma finfun_of_tupleK : cancel finfun_of_tuple tuple_of_finfun.
Proof.
by move=> t; apply: eq_from_tnth => i; rewrite tnth_map ffunE tnth_ord_tuple.
Qed.

Lemma tuple_of_finfunK : cancel tuple_of_finfun finfun_of_tuple.
Proof.
by move=> f; apply/ffunP => i; rewrite ffunE tnth_map tnth_ord_tuple.
Qed.

End FinFunTuple.

as a PR...

view this post on Zulip Karl Palmskog (Jun 25 2019 at 16:14):

@Cyril Cohen ah, those are good inline comments. Nevertheless, I'm probably going to define some local file like all_order.v that does Export Order.Def Order.Syntax Order.Theory., since I think that's what I nearly always want (and so I don't have to remember submodule names)

view this post on Zulip Karl Palmskog (Jun 28 2019 at 18:39):

@Anton Trunov since you're probably in a better position to do this than I am, can you try to convince Ilya to put the latest pdf and zip on https://ilyasergey.net/pnp/ ? (have tried a few times before)

view this post on Zulip Karl Palmskog (Jun 28 2019 at 18:40):

always good to be able to point people to up-to-date material conveniently, both for PnP and MCB

view this post on Zulip Anton Trunov (Jun 28 2019 at 23:04):

@Karl Palmskog sure, I’ll try that. I finally pushed the fixes to PnP I had on my drive for while. I’ll ask Ilya to update the pdf on his website after he merges those.

view this post on Zulip Karl Palmskog (Jun 28 2019 at 23:39):

:thumbsup:

view this post on Zulip Cyril Cohen (Jul 01 2019 at 14:44):

Dear math-comp users and developpers. Tomorrow I will migrate all math-comp channels to zulip.

view this post on Zulip Emilio Jesús Gallego Arias (Jul 01 2019 at 15:14):

Oh @Cyril Cohen I guess this was discussed in the last meetings, I'm sorry I was super busy

view this post on Zulip Emilio Jesús Gallego Arias (Jul 01 2019 at 15:14):

Sad to see the math-comp chat moving to a c̶l̶o̶s̶e̶d̶,̶ ̶n̶o̶n̶-̶f̶r̶e̶e̶ ̶p̶l̶a̶t̶f̶o̶r̶m̶ platform that requires registration

view this post on Zulip Emilio Jesús Gallego Arias (Jul 01 2019 at 15:16):

There was some discussion in the OCaml channels [slack] recently about whether threading etc... was useful, and surprisingly typical people there seem to find threads more confusing than non-threads

view this post on Zulip Emilio Jesús Gallego Arias (Jul 01 2019 at 15:17):

oh I stand corrected Zulip is open source, sorry, but indeed you need to register to be able to read / participate

view this post on Zulip Karl Palmskog (Jul 01 2019 at 15:20):

I think Zulip is the worst trade-off between chat and forum

view this post on Zulip Karl Palmskog (Jul 01 2019 at 15:21):

number of threads is typically gigantic, and keeping track of which ones are actually used seemed near impossible even after a few days of use

view this post on Zulip Emilio Jesús Gallego Arias (Jul 01 2019 at 15:25):

Yup, it's a kind of hybrid discourse; I kinda never grew on me. But really my main reason to be sad is that the number of discussions platforms I need to use is just out of control: Github / Gitlab / Mail / News / RSS / Discourse / various forums / facebook / twitter / Gitter / Zulip / Several slacks / discord ...

view this post on Zulip Emilio Jesús Gallego Arias (Jul 01 2019 at 15:26):

number of threads is typically gigantic, and keeping track of which ones are actually used seemed near impossible even after a few days of use

That's what happened in the OCamlabs slack, I thought people liked thread but like people who's busy and goes on and off claimed to be unable to follow the threads

view this post on Zulip Karl Palmskog (Jul 01 2019 at 15:27):

yeah the cognitive load was just terrible after a while

view this post on Zulip Karl Palmskog (Jul 01 2019 at 15:28):

if I want to say something, there's 10 threads it could fit in

view this post on Zulip Anton Trunov (Jul 01 2019 at 15:28):

you mean channels, right?

view this post on Zulip Karl Palmskog (Jul 01 2019 at 15:28):

whatever terminology they use

view this post on Zulip Anton Trunov (Jul 01 2019 at 15:29):

a constant headache to choose a Slack channel :)

view this post on Zulip Karl Palmskog (Jul 01 2019 at 15:29):

I mean, if you have one channel like ocaml in Slack, then people open 300+ threads in that channel

view this post on Zulip Karl Palmskog (Jul 01 2019 at 15:30):

that's basically Zulip

view this post on Zulip Emilio Jesús Gallego Arias (Jul 01 2019 at 15:30):

streams

view this post on Zulip Karl Palmskog (Jul 01 2019 at 15:32):

if someone prevented ad-hoc creation of new "streams" it might work

view this post on Zulip Karl Palmskog (Jul 01 2019 at 15:32):

but it looked to me like in practice every message had a new stream

view this post on Zulip Assia Mahboubi (Jul 02 2019 at 15:45):

@Karl Palmskog @Emilio Jesús Gallego Arias , thanks for the feedback on zulip. On the other hand, I

view this post on Zulip Assia Mahboubi (Jul 02 2019 at 15:46):

have gradually stopped using gitter, because nearly all the messages I can see in the lobby when I visit are out of my main area of expertise.

view this post on Zulip Assia Mahboubi (Jul 02 2019 at 15:47):

These days the topics most discussed are about the maintenance and technical dev issues. Not much the use of the libraries.

view this post on Zulip Assia Mahboubi (Jul 02 2019 at 15:48):

My feeling is that an outsider, specially a new user, might not feel at home in spite of the description (General discussion and questions...) in the header.

view this post on Zulip Assia Mahboubi (Jul 02 2019 at 15:50):

We concluded our discussion by betting that a classification mechanism of the discussions/threads/channels would help.

view this post on Zulip Assia Mahboubi (Jul 02 2019 at 15:53):

And the size of the mathcomp user community is way smaller than the one of Ocaml, and will remain so for a while I am afraid (I'd love to be wrong).

view this post on Zulip Emilio Jesús Gallego Arias (Jul 02 2019 at 16:23):

Indeed @Assia Mahboubi gitter is much more tailed to "live" discussion and it is hard to have any structure here. But I guess indeed the point Karl and I were making is that actually Discourse seems even better for structured discussion.

view this post on Zulip Karl Palmskog (Jul 02 2019 at 17:19):

I agree that MathComp Discourse could make a lot of sense

view this post on Zulip Karl Palmskog (Jul 02 2019 at 17:20):

in particular, I would like to see much more of: here is some proposed MathComp+SSReflect code, how could I make better use of library facilities

view this post on Zulip Karl Palmskog (Jul 02 2019 at 17:22):

I think it the tradeoff Discourse/Zulip could be between searchability and timeliness of response

view this post on Zulip Karl Palmskog (Jul 02 2019 at 17:23):

for example, I'm already using Coq Discourse pages as references for certain topics, but if someone doesn't know exactly what to ask, there is no way to get real-time feedback (easy questions-answer-refinement)

view this post on Zulip Anton Trunov (Jul 02 2019 at 20:19):

in particular, I would like to see much more of: here is some proposed MathComp+SSReflect code, how could I make better use of library facilities

@Karl Palmskog This sounds interesting to me. I’d happily join such channel or forum. For instance, we could ask someone to create a dedicated mathcomp category for such exchanges. WDYT?

view this post on Zulip Karl Palmskog (Jul 02 2019 at 21:00):

@Anton Trunov yes, we could just piggy-back on the Coq Discourse I guess

view this post on Zulip Karl Palmskog (Jul 02 2019 at 21:00):

ask Theo to create a MathComp/SSReflect category

view this post on Zulip Karl Palmskog (Jul 02 2019 at 21:04):

for example, I'm interested in just tracking MathComp-related projects as they show up on GitHub or similar

view this post on Zulip Karl Palmskog (Jul 02 2019 at 21:05):

I don't think Theo reads Gitter so often nowadays though, I think I will just email him

view this post on Zulip Cyril Cohen (Jul 02 2019 at 21:15):

ask Theo to create a MathComp/SSReflect category

@Karl Palmskog please do not do that....

view this post on Zulip Cyril Cohen (Jul 02 2019 at 21:18):

We decided to switch from gitter to zulip and I am about to remove math-comp gitter channel to avoid having too many forum/chat-like plateforms... Creating a category on Coq discourse would go against that

view this post on Zulip Karl Palmskog (Jul 02 2019 at 21:21):

@Cyril Cohen but is it searchable and viewable then for outside users?

view this post on Zulip Karl Palmskog (Jul 02 2019 at 21:21):

I think it's a lot to ask for someone to register just to get access to search functionality for finding answers to questions

view this post on Zulip Karl Palmskog (Jul 02 2019 at 21:22):

as per above, I regularly send Coq Discourse links to people

view this post on Zulip Cyril Cohen (Jul 02 2019 at 21:24):

Cyril Cohen but is it searchable and viewable then for outside users?

I don't know actually,... I did not think about that... what do you think @affeldt-aist @Assia Mahboubi @mkerjean @Enrico Tassi ?

view this post on Zulip Cyril Cohen (Jul 02 2019 at 21:25):

@Karl Palmskog anyway, please do not hurry in creating a new channel

view this post on Zulip Karl Palmskog (Jul 02 2019 at 21:25):

OK, understood

view this post on Zulip Emilio Jesús Gallego Arias (Jul 02 2019 at 22:23):

Also stackoverflow has a math-comp category and even if the volume is low I don't think zulip does substitute it

view this post on Zulip Karl Palmskog (Jul 02 2019 at 22:25):

StackOverflow has searchability but still terrible for new users IMO

view this post on Zulip Karl Palmskog (Jul 02 2019 at 22:26):

the admins there seem to be terrible, if you ask a "judgment question" it will be shut down - e.g., "what do you think about this piece of code"

view this post on Zulip Karl Palmskog (Jul 02 2019 at 22:34):

(another thing I don't like is how they reward quick-and-dirty answers and not detailed expert responses)

view this post on Zulip Anton Trunov (Jul 03 2019 at 07:13):

the admins there seem to be terrible, if you ask a "judgment question" it will be shut down - e.g., "what do you think about this piece of code"

I just remembered that Stackexchange platform has a special place for this use case https://codereview.stackexchange.com.

Code Review is a question and answer site for seeking peer review of your code.

view this post on Zulip Anton Trunov (Jul 03 2019 at 07:13):

CC @Karl Palmskog

view this post on Zulip Marie Kerjean (Jul 03 2019 at 07:42):

I thought the interest of Zulip was to manage a specific place where beginners feel welcome, as well a a place for developers. It does indeed not seem to be searchable for outside users. Anyway a mathcomp/ssreflect Discourse should feature susbsection for beginners, for ssreflect, for mathcomp libraries, for mathcomp-analysis libraries ... Discourse also seems to favour long argumented discussions while Zulip may be easier to use for chatting, and for beginners looking for quick advices.

view this post on Zulip Assia Mahboubi (Jul 03 2019 at 09:05):

We should specify the needs before committing to one (or more) technical tool. E.g. I suspect what @Karl Palmskog, @Emilio Jesús Gallego Arias, @Anton Trunov need is not the same as what beginner mathematicians need. And we need to care about both groups.

view this post on Zulip Anton Trunov (Jul 03 2019 at 09:09):

@affeldt-aist I’ve noticed that some wiki pages have been moved to https://math-comp.github.io. Does it mean that any new content should be added to https://github.com/math-comp/math-comp.github.io repository?

view this post on Zulip Assia Mahboubi (Jul 03 2019 at 09:17):

Personally, I am not sure yet about this move. But these days we are trying to improve the documentation and accessibility (in general) so things are moving. Any suggestion welcomed by the way.

view this post on Zulip Reynald Affeldt (Jul 03 2019 at 12:14):

@Anton Trunov @Assia Mahboubi It is really just a proposal to have an easy to maintain website with minimal effort. At this time, the contents is almost the same as the wiki (org file vs. md file). @Anton Trunov What do you think?

view this post on Zulip Reynald Affeldt (Jul 03 2019 at 12:16):

I can put back the org file back to the wiki, since github understands org as well.

view this post on Zulip Reynald Affeldt (Jul 03 2019 at 12:19):

@Cyril Cohen I don't known about Zulip enough :-(

view this post on Zulip Reynald Affeldt (Jul 03 2019 at 12:22):

@Karl Palmskog @Kazuhiko Sakaguchi Karl, Kazuhiko is maybe referring to https://staff.aist.go.jp/reynald.affeldt/documents/monae.pdf (Section 2.1)

view this post on Zulip Anton Trunov (Jul 03 2019 at 12:29):

@affeldt-aist On one hand, GitHub’s wiki might be easier to edit and maintain in general, on the other, it’s may not be flexible enough. E.g. long lists of interdisciplinary formalizations can benefit from tags and it seems that GitHub does not support tags even in org-files. Overall, I fully support the move provided we can have extra features not possible with the current solution.

view this post on Zulip Karl Palmskog (Jul 03 2019 at 12:40):

One more data point:

Much of the discussion surrounding Lean occurs in a Zulip chat room. Since this chatroom is only visible to registered users, we provide an openly accessible archive of the public discussions. This is useful for quick reference; for a better browsing interface, and to participate in the discussions, we strongly suggest joining the chat.

view this post on Zulip Karl Palmskog (Jul 03 2019 at 12:40):

from https://leanprover-community.github.io (note that archive is not searchable)

view this post on Zulip Karl Palmskog (Jul 03 2019 at 12:42):

I'm fine with Zulip as long as it doesn't rule out using something like Discourse as well (and I don't think Stack Overflow and its sister sites can fill the latter role)

view this post on Zulip Reynald Affeldt (Jul 03 2019 at 12:50):

@Anton Trunov I agree that tags would be nice.

view this post on Zulip Assia Mahboubi (Jul 03 2019 at 13:30):

What is a tag in this context? What solution would make them available?

view this post on Zulip Assia Mahboubi (Jul 03 2019 at 13:34):

If the list becomes part of the website, then edition can only be done by pushers. So how are people expected to contribute and add a reference to their paper?

view this post on Zulip Reynald Affeldt (Jul 03 2019 at 13:34):

Like keywords for papers (I guess). I don't know of any solution for a webpage (there are such DB-like facilities for org-files in emacs but I would be surprised that they transpose easily to generated html).

view this post on Zulip Reynald Affeldt (Jul 03 2019 at 13:37):

PR to the org-file are still possible, definitely a bit heavier than editing a wiki, still the wiki was not changing that much, so I am not sure either :-/

view this post on Zulip Assia Mahboubi (Jul 03 2019 at 13:38):

One option is to provide a contact email (e.g. mathcomp-dev) so that people can send pointers.

view this post on Zulip Assia Mahboubi (Jul 03 2019 at 13:39):

In any case we need to nominate a volunteer to take care of this list, if we want to keep it alive.

view this post on Zulip Reynald Affeldt (Jul 03 2019 at 13:39):

this might be just right enough given the volume of data and the frequency of changes

view this post on Zulip Anton Trunov (Jul 03 2019 at 13:40):

Like keywords for papers (I guess).

Yes, this is what I meant.

view this post on Zulip Anton Trunov (Jul 03 2019 at 13:40):

Or authors can just submit PRs to the website repostitory

view this post on Zulip Reynald Affeldt (Jul 03 2019 at 13:41):

just send an email with some predefined category, it will be a matter of copy-pasting a line in the org-file

view this post on Zulip Anton Trunov (Jul 03 2019 at 13:45):

what I like about having all those papers, tutorials, etc. in a repository is that one can subscribe to getting notifications about additions of new entries. afaik, wiki does not have this feature

view this post on Zulip Reynald Affeldt (Jul 03 2019 at 13:46):

again a good idea!

view this post on Zulip Anton Trunov (Jul 03 2019 at 13:51):

Let me expand a bit on this. GitHub has this feature called “watch releases only”, we could use it for additions of new entries or major corrections, so that everyone who wants to track that facet of mathcomp’s progress can subscribe without getting all the notifications about minor issues connected to the maintanence of the website. The website admin would have to tag each commit with a new paper or some other entry.

view this post on Zulip Anton Trunov (Jul 03 2019 at 13:52):

and thank you @affeldt-aist :)

view this post on Zulip Assia Mahboubi (Jul 03 2019 at 13:58):

Many thanks @Anton Trunov for this very nice suggestion (and its expanded version)! Let's try it.

view this post on Zulip Anton Trunov (Jul 03 2019 at 14:00):

Thank you, @Assia Mahboubi! Please don’t hesitate to get in touch with me if you need help with this

view this post on Zulip Assia Mahboubi (Jul 03 2019 at 14:00):

I will, thanks again.

view this post on Zulip Pierre-Yves Strub (Jul 03 2019 at 14:05):

I also do like Anton's suggestion.

view this post on Zulip Assia Mahboubi (Jul 03 2019 at 14:09):

Cool! Thanks for the feedback!

view this post on Zulip Karl Palmskog (Jul 03 2019 at 14:52):

@affeldt-aist any chance for a release or git tag of monae with "official" compatibility with MC 1.9.0, etc.?

view this post on Zulip Karl Palmskog (Jul 03 2019 at 14:53):

we are putting together a dataset for mining software repositories style research, and this would be helpful

view this post on Zulip Assia Mahboubi (Jul 03 2019 at 15:44):

I implemented @Anton Trunov 's proposal on top of @affeldt-aist 's orgification. I just pushed a new version of the publication list, with a (git) tag.

view this post on Zulip Karl Palmskog (Jul 03 2019 at 15:53):

@Assia Mahboubi could it be within the scope of the website to also list/track MathComp-related projects on GitHub (and similar platforms)?

view this post on Zulip Karl Palmskog (Jul 03 2019 at 15:54):

I think a common occurrence may be, I need a theory of X in MathComp, there may be a project but not necessarily a publication

view this post on Zulip Assia Mahboubi (Jul 03 2019 at 15:56):

Hi @Karl Palmskog . Indeed, this would be very good. We kind of hoped the Mathcomp organization would be a good start, but usage indicates it does not play that role well.

view this post on Zulip Assia Mahboubi (Jul 03 2019 at 15:58):

The main problem I see with such a list is that such list gets old and we would need manpower to maintain it. So I would rather advocate asking a question on a mailing list/forum for this kind of need.

view this post on Zulip Karl Palmskog (Jul 03 2019 at 16:11):

in my experience, repo URLs are very stable (and GitHub automatically redirects in case of a move). I also think mailing lists are terrible for tracking repos. @Anton Trunov what do you think, is this something that should live in some wiki?

view this post on Zulip Assia Mahboubi (Jul 03 2019 at 16:17):

Repos are stable, but the not the relevance of the library.

view this post on Zulip Assia Mahboubi (Jul 03 2019 at 16:19):

In the past, the Coq Contrib page has been used for similar purposes. But then it got outdated, and in my opinion the result was terrible for the image of Coq.

view this post on Zulip Assia Mahboubi (Jul 03 2019 at 16:20):

Hence my suggestion to use a forum. I fully agree with the limitations you point, but the advantage is that you increase the chances to get the relevant answer at the time of asking.

view this post on Zulip Anton Trunov (Jul 03 2019 at 16:33):

@Karl Palmskog I think Assia’s concerns are legit. I’ve seen people maintaining the so-called awesome lists. E.g. ocaml-community maintains awesome-ocaml list. We could create something like “awesome-mathcomp” list under coq-community, or awesome-coq with a section devoted to Mathcomp.

view this post on Zulip Anton Trunov (Jul 03 2019 at 16:34):

What do people think about this tentative suggestion?

view this post on Zulip Karl Palmskog (Jul 03 2019 at 16:39):

yeah it would definitely have to live under coq-community

view this post on Zulip Karl Palmskog (Jul 03 2019 at 16:40):

but as Theo would say, better then to do awesome-coq with MathComp section

view this post on Zulip Anton Trunov (Jul 03 2019 at 16:41):

but as Theo would say, better then to do awesome-coq with MathComp section

yep, my thinking exactly :)

view this post on Zulip Karl Palmskog (Jul 03 2019 at 16:42):

for example, this is what one should not have

view this post on Zulip Karl Palmskog (Jul 03 2019 at 16:42):

https://github.com/uhub/awesome-coq

view this post on Zulip Karl Palmskog (Jul 03 2019 at 16:42):

links almost completely devoid of information

view this post on Zulip Anton Trunov (Jul 03 2019 at 16:46):

I agree, I actually already tried experimenting with this. I have couple of unpublished attempts at compiling a useful list of Coq projects / resources / libraries. But I didn’t come to a conclusion on how to organize it best. I tried doing it either by topics (e.g. algebra, hardware, pl, etc.) or by resource type (library, book, paper, video, etc.). Tag support from GitHub would definitely help here.

view this post on Zulip Karl Palmskog (Jul 03 2019 at 16:47):

right, there are just too many limitations with flat lists

view this post on Zulip Karl Palmskog (Jul 03 2019 at 16:47):

for example, one could even tag with coq-8.8 if 8.8 is confirmed to work or similar

view this post on Zulip Anton Trunov (Jul 03 2019 at 16:47):

oh, that’s a great idea

view this post on Zulip Karl Palmskog (Jul 03 2019 at 16:48):

e.g., toychain would have tags: math-comp, ssreflect, blockchain, distributed-systems, fcsl-pcm, coq-8.8, coq-8.9, math-comp-1.9(?), ocaml

view this post on Zulip Karl Palmskog (Jul 03 2019 at 16:50):

if one could filter easily, having lots of tags would not be an issue, as for GitHub repos that look silly with 20+ tags

view this post on Zulip Anton Trunov (Jul 03 2019 at 16:54):

btw, I have a feeling that https://github.com/uhub/awesome-coq is just generated using coq tag on GitHub and sorted wrt the number of stars a project has.

view this post on Zulip Karl Palmskog (Jul 03 2019 at 16:56):

yeah I think you're right, which shows the problem with that approach

view this post on Zulip Karl Palmskog (Jul 03 2019 at 16:56):

not that one shouldn't look at stars

view this post on Zulip Anton Trunov (Jul 03 2019 at 16:56):

in principle, if there was an interface to coq’s opam archive allowing advanced filtering, we could have what we are looking for.

view this post on Zulip Karl Palmskog (Jul 03 2019 at 16:56):

I did code search of Coq code on GitHub searching for "ssreflect", and it was pretty terrible as well

view this post on Zulip Karl Palmskog (Jul 03 2019 at 16:57):

the problem is that only a fraction of projects do releases and even fewer put them as packages on the Coq OPAM archive

view this post on Zulip Karl Palmskog (Jul 03 2019 at 17:00):

some examples not locatable through OPAM: chdoc/comp-dec-pdl gstew5/games strub/elliptic-curves-ssr pi8027/lambda-calculus drouhling/LaSalle certichain/probchain

view this post on Zulip Karl Palmskog (Jul 03 2019 at 17:02):

I completely understand that not everyone feels that doing release+package is time well spent, but a major detriment to mining proofs

view this post on Zulip Anton Trunov (Jul 03 2019 at 17:06):

If there are no objections, we could create a list of project maintained and curated by the community.

view this post on Zulip Karl Palmskog (Jul 03 2019 at 17:07):

yeah I guess we can try to figure out tags as we go along

view this post on Zulip Anton Trunov (Jul 03 2019 at 17:07):

sure!

view this post on Zulip Karl Palmskog (Jul 03 2019 at 17:07):

can at least contribute my current MathComp list

view this post on Zulip Anton Trunov (Jul 03 2019 at 17:07):

that would be awesome!

view this post on Zulip Karl Palmskog (Jul 03 2019 at 17:11):

@Anton Trunov we at least have the following now: https://coq.inria.fr/opam/coq-packages.json

view this post on Zulip Anton Trunov (Jul 03 2019 at 17:18):

thanks for the pointer, that seems like a good start

view this post on Zulip Anton Trunov (Jul 03 2019 at 17:43):

I implemented Anton Trunov 's proposal on top of affeldt-aist 's orgification. I just pushed a new version of the publication list, with a (git) tag.

@Assia Mahboubi Awesome! Thank you. I subscribed to those releases.

view this post on Zulip Reynald Affeldt (Jul 04 2019 at 05:17):

@Karl Palmskog Here you are! :-) (and we still have to thank you for your PR last month)

view this post on Zulip Karl Palmskog (Jul 04 2019 at 16:27):

@affeldt-aist much appreciated, if all goes well we'll have some interesting stuff going back to the community soon after all help with compatibility/tagging/packaging

view this post on Zulip Karl Palmskog (Jul 04 2019 at 16:30):

by the way, our statistics indicates that infotheo is second in size after MathComp itself out of all MathComp-related projects, both in terms of Gallina LOC and SSRreflect LOC

view this post on Zulip Karl Palmskog (Jul 04 2019 at 16:34):

one interesting factoid is that the arguably most idiomatic projects (MathComp itself, fourcolor, finmap, odd-order) have a distinctly higher average number of Ltac tokens per SSReflect sentence than other projects in the MathComp org (15.77 toks/sentence vs. 12.13)

view this post on Zulip Anton Trunov (Jul 04 2019 at 16:42):

@Karl Palmskog thanks for sharing! Is the tooling you have used to extract those stats available publicly?

view this post on Zulip Karl Palmskog (Jul 04 2019 at 16:42):

well, we directly hook into Coq's implementation via SerAPI

view this post on Zulip Karl Palmskog (Jul 04 2019 at 16:43):

here is the recent extension for getting tokens out: https://github.com/ejgallego/coq-serapi/pull/161

view this post on Zulip Karl Palmskog (Aug 04 2019 at 16:38):

@affeldt-aist you probably want to enable the with-test clause in your CI, I can submit a PR for that if you want

view this post on Zulip Reynald Affeldt (Aug 04 2019 at 23:44):

If it takes you less than 2 minutes, I would be grateful, otherwise just point me to an example, I don't want to waste your time.

view this post on Zulip Karl Palmskog (Aug 05 2019 at 00:02):

@affeldt-aist OK, key option to opam install is -t, here's an example, let me know if something is unclear: https://github.com/lukaszcz/coqhammer/blob/coq8.10/coq-hammer.opam#L20 https://github.com/lukaszcz/coqhammer/blob/master/.travis.yml#L29

view this post on Zulip Reynald Affeldt (Aug 05 2019 at 13:13):

It seems that I could managed to do it. Thank you @Karl Palmskog !

view this post on Zulip Karl Palmskog (Aug 05 2019 at 15:03):

:thumbsup:

view this post on Zulip Karl Palmskog (Aug 13 2019 at 20:19):

this Let is never used inside its scope, and by definition is not accessible outside its section: https://github.com/math-comp/math-comp/blob/6be8fd5c67949a59bde7083e81401263986e7a4e/mathcomp/field/algC.v#L635

view this post on Zulip Karl Palmskog (Aug 13 2019 at 20:20):

does anyone know what purpose it serves, if any?

view this post on Zulip Karl Palmskog (Aug 13 2019 at 20:20):

e.g., should it be a regular Definition?

view this post on Zulip Emilio Jesús Gallego Arias (Aug 14 2019 at 17:55):

@Karl Palmskog obviously the authors are the best persons to answer that question, but my feeling about that let is that it just tries to mimic "regular" mathematical writing, as you would find in a paper "Corollary N: 2 != 0" , as a kind of "sanity checking" or demonstration purpose of the just proved lemmas.

view this post on Zulip Karl Palmskog (Aug 22 2019 at 06:15):

does anyone know if there is a particular reason why odd-order (and fourcolor) always has a newline after From mathcomp, while MathComp itself (seemingly) never does? We had thought it would be the same across these projects. (finmap seems to have a bit of both)

view this post on Zulip Cyril Cohen (Aug 22 2019 at 07:26):

does anyone know what purpose it serves, if any?

Let is a way of putting something in the context so that by [] finds it using assumption (you can see it as a more stable alternative to Hint Resolve. I guess that is why it is used here, so there is no point in making it a Definition and it might never be explicitly used.

view this post on Zulip Cyril Cohen (Aug 22 2019 at 07:28):

does anyone know if there is a particular reason why odd-order (and fourcolor) always has a newline after From mathcomp, while MathComp itself (seemingly) never does? We had thought it would be the same across these projects. (finmap seems to have a bit of both)

Historically Coq 8.6 (or 8.5 can't remember now) did not have the From ... Import syntax, so it we used to compensate by adding this syntax to the ssr plugin, however in order to make coqdoc work we had to remove them, in order to make the sed script as simple as possible I put all of the From mathcomp on a distinct line.

view this post on Zulip Karl Palmskog (Aug 22 2019 at 07:56):

thanks, explains a lot (context: we were training an auto-formatter on both mathcomp and odd-order and fourcolor, and got somewhat unstable results)

view this post on Zulip Karl Palmskog (Aug 22 2019 at 07:58):

@Cyril Cohen but the bottom line is that the one without newlines in MathComp is the preferred style now?

view this post on Zulip Karl Palmskog (Aug 22 2019 at 08:02):

very experimental results on learning-based auto-formatting where this came up are geneorously being reviewed by @Anton Trunov here: https://github.com/imdea-software/fcsl-pcm/pull/9

view this post on Zulip Cyril Cohen (Aug 23 2019 at 08:43):

Cyril Cohen but the bottom line is that the one without newlines in MathComp is the preferred style now?

yes

view this post on Zulip Karl Palmskog (Sep 06 2019 at 02:55):

this looks like it could be feasible in MathComp: https://www.cs.stanford.edu/~knuth/papers/huang.pdf

view this post on Zulip Karl Palmskog (Sep 06 2019 at 02:56):

cf. https://www.scottaaronson.com/blog/?p=4278

view this post on Zulip Florent Hivert (Sep 11 2019 at 15:25):

Hi there ! I got a very basic question: what's the most SSReflect idiomatic way to transform a goal (A -> B) -> A -> C into B -> C. I usually do a move=> H{}/H. But it seems very cryptic...

view this post on Zulip Pierre-Yves Strub (Sep 11 2019 at 15:26):

I do the same, and that’s a bit ugly, indeed

view this post on Zulip Florent Hivert (Sep 11 2019 at 17:19):

A grep "[^ ]{}/" **/*.v didn't find any similar trick in the whole mathcomp source... So I supposed there where a better trick...

view this post on Zulip Anton Trunov (Sep 11 2019 at 19:18):

@Florent Hivert @Pierre-Yves Strub This can be simulated using the new features in Coq 8.10 like so:

Ltac apply_top_to_next := let top := fresh in move=> top {}/top.
Notation "%_" := (ltac:( apply_top_to_next )).

Lemma foo A B C : (A -> B) -> A -> C.
Proof.
move=> /%_.
Abort.

This is described in the docs here: https://coq.github.io/doc/master/refman/proof-engine/ssreflect-proof-language.html#views

view this post on Zulip Anton Trunov (Sep 11 2019 at 19:21):

More suggestive notation for this would be much appreciated :)

view this post on Zulip Cyril Cohen (Sep 12 2019 at 13:11):

I am working on a PR to take advantage of 8.10 features and there, I suggested to name it "/apply" :laughing: https://github.com/math-comp/math-comp/blob/87e0c9f0ab76a57b796fea668858fbef15504c87/mathcomp/ssreflect/ssreflect.v#L174

view this post on Zulip Pierre-Yves Strub (Sep 12 2019 at 13:11):

Too long, too long ! (the name)

view this post on Zulip Cyril Cohen (Sep 12 2019 at 13:11):

And I forgot to clear it :)

view this post on Zulip Cyril Cohen (Sep 12 2019 at 13:12):

@Pierre-Yves Strub in the end I am not such an extremist

view this post on Zulip Anton Trunov (Sep 12 2019 at 13:20):

@Cyril Cohen wow! very nice, can’t wait to have those. I usually define duP lemma A -> A * A to imitate what your dup does

view this post on Zulip Cyril Cohen (Sep 12 2019 at 13:22):

@Anton Trunov feel free to comment or improve on https://github.com/math-comp/math-comp/pull/372

view this post on Zulip Anton Trunov (Sep 12 2019 at 13:31):

@Cyril Cohen Sure! it looks fantastic

view this post on Zulip Florent Hivert (Sep 12 2019 at 15:11):

Knowing the usual ssreflect syntax, my first attempt was to issue a /(_ _). I was disappointed It didn't word. In my mind, it was a merge of /H and /(_ H). This notation can be generalized to /(H _ _ _) which transform A -> B -> C -> D to (H A B C) -> Dor to /(_ H _ _) transforming A -> B -> C -> D to (A H B C) -> D. Maybe it is only me but all those seems very consistent. I've no idea how to implement it though.

view this post on Zulip Cyril Cohen (Sep 12 2019 at 16:59):

(_ _) is an abbreviation for fun f x => f x, and (traditional) views consume only one item on the stack whereas in the idiom you are pointing out, there are two items, which means you must use at least two (traditional) intro pattern items. (By traditional I mean with coq < 8.10)

view this post on Zulip Cyril Cohen (Sep 12 2019 at 17:01):

The generalization you may want is a kind of "super view" //H which tries to consume every argument of H using items on the stack, in which case //(_ _) would do what you wanted intially :laughing:

view this post on Zulip Pierre-Yves Strub (Sep 12 2019 at 19:26):

In Ec, we have way to temporarily introduce stuffs. I don’t remember exactly the syntax (usually, I take a curse of Capitaine Haddock based on #, @, $, % and & to find the syntax).

view this post on Zulip Pierre-Yves Strub (Sep 12 2019 at 19:27):

You can do stuff like move=> +h /h - and continue

view this post on Zulip Florent Hivert (Sep 12 2019 at 21:32):

@Cyril Cohen So you says my syntax has already a meaning but ! Darn ! I would love to have this multiview and indeed if / is the view notation // is a good notation for a multiview. So the question is: is it implementable ? Any chance to have that in a future Coq/SSReflect release ?

view this post on Zulip Assia Mahboubi (Sep 16 2019 at 12:34):

Anyone using nix-shellhere? I have some trouble adding real-closed in the dependencies of a project. I asked in the "analysis" lobby but I realize it is not specific so I will repeat here.

view this post on Zulip Assia Mahboubi (Sep 16 2019 at 12:35):

I am trying to add mathcomp-real-closed to the packages made available in a nix-shell configured by the shell.nix of the repo. When I am adding mathcomp-real-closed to this line and restart nix-shell, I get an error

view this post on Zulip Assia Mahboubi (Sep 16 2019 at 12:36):

error: undefined variable 'mathcomp-real-closed' at /home/assia/Sources/math-comp/analysis-main/shell.nix:26:50
(use '--show-trace' to show detailed location information)
`` `

view this post on Zulip Anton Trunov (Oct 01 2019 at 18:43):

How do people generally deal with implicit coercions not inserted inside Search command? E.g. Search _ (~~ ?b -> ~~ ?c). does not find anything which makes it confusing for newcomers. I guess I usually use textual search in this case. Is there any better solution?

view this post on Zulip Anton Trunov (Oct 01 2019 at 18:44):

Btw, I opened an issue about this here: https://github.com/coq/coq/issues/10808

view this post on Zulip Karl Palmskog (Oct 01 2019 at 22:28):

@Anton Trunov we discussed trying approaches like this for code completion: https://ml4code.github.io/publications/wang2016neural/

view this post on Zulip Karl Palmskog (Oct 01 2019 at 22:30):

it could likely be done by training, for a MathComp corpus, on all of: (1) raw textual Gallina, (2) parsed Gallina, (3) parsed and notation-resolved Gallina

view this post on Zulip Karl Palmskog (Oct 01 2019 at 22:40):

we have (1)+(2) but don't have (3) at the moment due to not currently supported/implemented in SerAPI, but it is definitely possible

view this post on Zulip Anton Trunov (Oct 02 2019 at 05:58):

@Karl Palmskog Thank you for the pointers. looks very promising!

view this post on Zulip Karl Palmskog (Oct 02 2019 at 06:13):

(paper pdf: https://openreview.net/pdf?id=rJbPBt9lg - example on p. 4 reminiscent of Anton's query)

view this post on Zulip Karl Palmskog (Oct 02 2019 at 06:45):

@Anton Trunov how about we set up a MathComp wiki page for search gotchas, this could be used to benchmark different solutions

view this post on Zulip Anton Trunov (Oct 02 2019 at 07:55):

Great idea!

view this post on Zulip Karl Palmskog (Oct 02 2019 at 07:57):

I was clueless for a long time that the initial _ was even needed

view this post on Zulip Anton Trunov (Oct 02 2019 at 07:57):

Yes, that’s a frequent thing :)

view this post on Zulip Anton Trunov (Oct 02 2019 at 08:07):

@Karl Palmskog Ok, I just added an initial stub for the page: https://github.com/math-comp/math-comp/wiki/Search

view this post on Zulip Anton Trunov (Oct 02 2019 at 08:07):

Feel free to restructure it and edit however you like

view this post on Zulip Anton Trunov (Oct 02 2019 at 08:08):

It lacks examples currently, though

view this post on Zulip Karl Palmskog (Oct 02 2019 at 08:47):

:thumbsup:

view this post on Zulip Karl Palmskog (Oct 02 2019 at 09:52):

arguably one needs machine learning based code completion for Search itself...

view this post on Zulip Karl Palmskog (Oct 02 2019 at 09:52):

but there is no dataset for that as far as I know

view this post on Zulip Anton Trunov (Oct 02 2019 at 17:49):

@Karl Palmskog I added some more pain points and also notes from the manual to the Search wiki page.

view this post on Zulip Karl Palmskog (Oct 02 2019 at 19:52):

wow, those are great, really sets the stage for measuring improvements

view this post on Zulip Karl Palmskog (Oct 02 2019 at 19:54):

learning based search/completion has the disadvantage of not handling outside-of-training-set notations/lemmas

view this post on Zulip Karl Palmskog (Oct 02 2019 at 19:56):

so it looks like it's kind of complementary with Search in some scenarios, but both will fail for some cases like definitions in unknown/unrequired packages

view this post on Zulip Antonio Nikishaev (Oct 02 2019 at 20:55):

BTW, there is a frequent warning “Listing only lemmas with conclusion matching …” when one is trying to use Search ⟨smth⟩ (aka SearchHead ⟨smth⟩, as opposed to Search _ ⟨smth⟩). It’s been there at least since ssr→coq merge (~ 2017).
Should that warning even be there? It feels more off-putting than useful. (My experience = just learning, so maybe I’m totally wrong.)

view this post on Zulip Anton Trunov (Oct 03 2019 at 06:02):

@Antonio Nikishaev I think the warning should stay, but the message could be more suggestive: something like “Use Search _ … to look in premises and conclusion.

view this post on Zulip Karl Palmskog (Oct 03 2019 at 08:41):

agree 100% with Anton about the warning

view this post on Zulip Yves Bertot (Oct 04 2019 at 11:36):

Would it make sense to add theorem with the following statement? I have a use case for it.

view this post on Zulip Yves Bertot (Oct 04 2019 at 11:37):

```Lemma pair_eqE (A B : eqType) (p1 p2 : A * B) :
(p1 == p2) = (p1.1 == p2.1) && (p1.2 == p2.2).
Proof.
case: p1 p2 => [a b] [c d] /=; apply/idP/idP.
by move=>/eqP [] -> ->; rewrite !eqxx.
by move=>/andP[] /eqP -> /eqP ->.
Qed.


view this post on Zulip Reynald Affeldt (Oct 04 2019 at 11:42):

isn't it pair_eqE from eqtype.v?

view this post on Zulip Cyril Cohen (Oct 04 2019 at 11:43):

yes it is

view this post on Zulip Yves Bertot (Oct 04 2019 at 11:44):

My mistake, then.

view this post on Zulip Yves Bertot (Oct 04 2019 at 12:02):

In fact, pair_eqE as provided in eqtype.v is not useful to me, because I want to use the rewrite from right to left, and I cannot put (- pair_eqE) in a multi-rule, can I?

view this post on Zulip Cyril Cohen (Oct 04 2019 at 12:05):

yes you can

view this post on Zulip Cyril Cohen (Oct 04 2019 at 12:05):

(=^~pair_eqE)

view this post on Zulip Cyril Cohen (Oct 04 2019 at 12:06):

oops I cannot remember the syntax :laughing:

view this post on Zulip Yves Bertot (Oct 04 2019 at 12:06):

Where would be the def?

view this post on Zulip Cyril Cohen (Oct 04 2019 at 12:07):

ssreflect.v

view this post on Zulip Cyril Cohen (Oct 04 2019 at 12:07):

I found it and corrected it up there

view this post on Zulip Cyril Cohen (Oct 04 2019 at 12:07):

( =^~)

view this post on Zulip Yves Bertot (Oct 04 2019 at 12:21):

Okay, I tried and I am still blocked. after rewriting with (=~pair_eqE), I transform (a == b) into (pair_eq a b), this is convertible to (a.1 == b.1) && (a.2 == b.2) as per the definition of pair_eq, but I still don't know how to include the unfolding of pair_eq in the multi-rule.

view this post on Zulip Cyril Cohen (Oct 04 2019 at 12:35):

oh ok

view this post on Zulip Cyril Cohen (Oct 04 2019 at 12:35):

you need to fold indeed :-/

view this post on Zulip Kazuhiko Sakaguchi (Oct 09 2019 at 07:41):

Coercions from Sortclass can be defined since Coq 8.8, so I think now we can deprecate predArgType trick. https://github.com/coq/coq/pull/6480

view this post on Zulip Giovanni Mascellani (Gitter import) (Oct 28 2019 at 10:34):

What is the syntax in Coq to compose two functions?

view this post on Zulip Cyril Cohen (Oct 28 2019 at 10:45):

@Giovanni Mascellani f \o g (in mathcomp)

view this post on Zulip Giovanni Mascellani (Gitter import) (Oct 28 2019 at 10:55):

Thank!

view this post on Zulip Giovanni Mascellani (Gitter import) (Oct 28 2019 at 11:06):

Also, what does it mean when a variable of a theorem or definition is between braces instead of brackets? Like in Lemma idP {b : bool} : reflect b b..

view this post on Zulip Giovanni Mascellani (Gitter import) (Oct 28 2019 at 11:32):

Maybe it means that the argument is implicit?

view this post on Zulip Cyril Cohen (Oct 28 2019 at 11:45):

@Giovanni Mascellani yes it means the argument is maximally implicit

view this post on Zulip Kazuhiko Sakaguchi (Oct 28 2019 at 11:46):

@Giovanni Mascellani That's documented here: https://coq.github.io/doc/master/refman/language/gallina-extensions.html#implicit-argument-binders

view this post on Zulip Giovanni Mascellani (Gitter import) (Oct 29 2019 at 10:05):

I don't understand what happens with non maximally inserted arguments; the ref says "In the first case, the function is considered to have no arguments furtherly: one says that the implicit argument is not maximally inserted": what does this mean? How can I evaluate the function if it is considered to have not further arguments?

view this post on Zulip Anton Trunov (Oct 29 2019 at 10:39):

@Giovanni Mascellani Perhaps an example can help. Suppose we have a definition with let’s say 2 parameters like this: foo x y. If x is maximally inserted implicit parameter and y is jus t a regular parameter, then one you mention foo, Coq considers it to be @foo _, i.e. it does not wait for you to apply foo to some y to infer x and insert it.

view this post on Zulip Anton Trunov (Oct 29 2019 at 10:40):

If x is not maximally inserted, but an implicit argument, then foo is just @foo, but foo y is @foo _ y

view this post on Zulip Giovanni Mascellani (Gitter import) (Oct 29 2019 at 11:53):

Oh, I see. Thanks!

view this post on Zulip Florent Hivert (Oct 31 2019 at 08:51):

Hi ! I'd like to write the universal property for multivariate polynomials (ie : they form the free commutative algebra). However, I can't find the interface for commutative algebras (neither comUnitAlgebra by the way). I guess there is no reason why it's not there except that no one has needed it yet. If so, I'll open a pull request as soon as I managed to get around the inheritance diamond com/unit. @Cyril Cohen I can't wait having a practical tool to do that.

view this post on Zulip Cyril Cohen (Oct 31 2019 at 18:36):

:thumbsup:

view this post on Zulip Bas Spitters (Nov 01 2019 at 12:50):

In my group we occassionally make improvements on math-comp. What's currently the best way to see whether it is worthwhile to get them integrated. Github issues?
https://github.com/math-comp/math-comp/issues/401

view this post on Zulip Cyril Cohen (Nov 02 2019 at 13:53):

@Bas Spitters thanks for reminding us of the issue. Github issues is indeed the best way, we try to be reactive, but sometimes we fail, please do not hesitate to ping us when the answer gets late.

view this post on Zulip Cyril Cohen (Nov 02 2019 at 13:53):

have a good weekend

view this post on Zulip Bas Spitters (Nov 03 2019 at 20:23):

@Cyril Cohen Thanks!

view this post on Zulip Assia Mahboubi (Nov 04 2019 at 09:55):

@Bas Spitters , thanks for your interest. Do not hesitate to send pull requests directly when relevant.

view this post on Zulip Yves Bertot (Nov 14 2019 at 12:24):

Hello, this is a question for math-comp developers. Is there a good reason that Howto-Release.md is not pointed to by any other page of the wiki? I think it would be sensible to add as the fourth point in the Contributing section of the Home page. Any opinion?

view this post on Zulip Cyril Cohen (Nov 14 2019 at 12:24):

@Yves Bertot yes please add it

view this post on Zulip Yves Bertot (Nov 15 2019 at 12:22):

I reworded the 3rd point of the Contributing section of the Home page, hoping that the opportunity to prepare overlays becomes easier to understand for external contributors.

view this post on Zulip Yves Bertot (Nov 15 2019 at 12:26):

I also edited the page Checklist-for...reviewing-and-playing-with-a-PR to mention that one should check that CI tests have passed and that one should suggest to the author that they should prepare an overlay, pointing the overlay tutorial. Tell me if you think this appropriate, or not.

view this post on Zulip Gabriel Taumaturgo (Gitter import) (Nov 16 2019 at 04:44):

Hello. I'm having some trouble understanding how to work with units(and the associated group) of a ring. I only found the file "finalg" related to units, are there any extra examples on how to work with them? I'm having a hard time just by reading the file documentation/code.

view this post on Zulip Florent Hivert (Nov 16 2019 at 08:55):

@Gabriel Taumaturgo One problem with the current mathcomp hierarchy is that all groups are assumed to be finite. So depending on your ring, you can't write that the its units form a group. If the multiplication is also commutative then, as a workaround, you can put a Z-module structure (which is the same as a commutative group). I don't know if someone already attempted to generalize the group theory and how hard It would be.

view this post on Zulip Florent Hivert (Nov 16 2019 at 09:02):

I hit the problem recently twice: once with power series over a non commutative ring. I defined the right inverse then the left inverse, and then showed by a standard group theoretical argument that two two agrees. Then latter I was considering power series of the form 1 + X + ... under composition they also form a group so that the inverse is unique. But I has to redo the (admitedly simple) argument. So I'm strongly supporting any attempt to generalize group to the infinite case. As a matter of research interest I would also suggest to start with semigroups which have a very rich but not so well known theory.

view this post on Zulip Florent Hivert (Nov 16 2019 at 09:25):

I created https://github.com/math-comp/math-comp/issues/430 for infinite groups.

view this post on Zulip Gabriel Taumaturgo (Gitter import) (Nov 16 2019 at 13:22):

Actually the units i'm trying to work with are finite. These are the units of 'Z_n.+2

view this post on Zulip Gabriel Taumaturgo (Gitter import) (Nov 17 2019 at 02:19):

Well, the property i'm trying to express is "for a natural n, coprime with r, the order of n in the units of 'Z_r is x"

view this post on Zulip Gabriel Taumaturgo (Gitter import) (Nov 17 2019 at 02:20):

but i'm having problems instantiating a unit.

view this post on Zulip Gabriel Taumaturgo (Gitter import) (Nov 19 2019 at 06:05):

Another question, is fermat's little theorem defined for ordinals?

view this post on Zulip Valentin Robert (Nov 22 2019 at 20:22):

I don't understand how to reason about tuples. I'm trying to prove cat_tuple [tuple h] t = [tuple of h :: t] and can't even prove the base case cat_tuple [tuple h] [tuple] = [tuple of h :: [tuple]] because I'm not sure how to handle cat_tuple :(

view this post on Zulip Reynald Affeldt (Nov 22 2019 at 20:32):

Lemma test n T (h : T) (t : n.-tuple T) : cat_tuple [tuple h] t = [tuple of h :: t].
Proof. exact: val_inj. Qed.

A tuple is a list together with a proof that the list has a given length, val_inj is a generic lemma for such dependent types that strips the proofs, leaving only the lists to compare.

view this post on Zulip Valentin Robert (Nov 22 2019 at 20:44):

ah, that was exactly my problem, getting rid of the proofs, thanks!

view this post on Zulip Valentin Robert (Nov 22 2019 at 22:42):

other thing I'm bad at, in a case like this (trivial but for the sake of example), how do I retain the fact that the n0 after elim is the same as the ambient n?

Lemma minimal n T : forall (v : Vector.t T n.+1), v = v.
Proof. elim / @Vector.caseS.

view this post on Zulip Cyril Cohen (Nov 23 2019 at 14:30):

@Valentin Robert using cat_tuple is usually not what you may want to do. Indeed cat_tuple is the canonical instance of tuple on the cat of two tuples. So in general you may want to use plain cat and let unification figure out cat_tuple for you when you use lemmas on tuples. Of course maybe you are in a particular case where you really need it...

view this post on Zulip Cyril Cohen (Nov 23 2019 at 14:33):

About elimination, the next mathcomp version will contain lemma ubnPeq which you might want to use like this.
move: v; have [m] := ubnPeq n.+1; elim. (untested code)

view this post on Zulip Valentin Robert (Nov 23 2019 at 21:46):

@Cyril Cohen which cat are you talking about? the one I have in scope is seq.cat, which seems to return a monomorphized seq.seq, that AFAIU does not seem coercible into a tuple type.

view this post on Zulip Emilio Jesús Gallego Arias (Nov 23 2019 at 23:27):

What @Cyril Cohen means is that if you do [tuple of s ++ r] then Coq will infer the tuple structure [as long as it can infer one for r and s

view this post on Zulip Valentin Robert (Nov 23 2019 at 23:44):

ah

view this post on Zulip Karl Palmskog (Nov 25 2019 at 15:10):

so is there any general heuristics for fixing ambiguous-paths warnings?

view this post on Zulip Kenji Maillard (Nov 29 2019 at 17:32):

there is a small issue in the CHANGELOg.md, the link for the mathcomp documentation in the section infrastructure sends to

view this post on Zulip Kenji Maillard (Nov 29 2019 at 17:32):

mathcomp.github.io instead of math-comp.github.io

view this post on Zulip Gabriel Taumaturgo (Gitter import) (Nov 30 2019 at 04:26):

Hi, i'm struggling with a proof that is seemingly simple, but i believe that due to my inexperience with the library i'm having a hard time.
https://pastebin.com/SwLBVVdB

In this subgoal i have to show that due to the fact that the binomial coeficients 'C(n,i) (0 < i < n) divide n, this term results in the null polynomial, but i have been stuck in this step for some days, can anyone give me some help?

6 subgoals (ID 1361)

  n' : nat
  a : 'F_n
  pn : prime n
  n_dvd_coef : forall n0 : nat, (0 < n0 < n)%N -> (n %| 'C(n, n0))%N
  i : nat
  range : (0 <= i < n'.+1)%N
  range_Si : (0 < i.+1 < n)%N
  S_i_dvd_n : (n %| 'C(n, i.+1))%N
  x : nat
  H : 'C(n, i.+1) = (x * n)%N
  ============================
  'X^(n - i.+1) * a%:P ^+ i.+1 *+ (x * n) = 0%:P

view this post on Zulip Reynald Affeldt (Nov 30 2019 at 10:03):

what about this?

Proof.
  move=> a; split.
  move=> pn.
rewrite exprDn_char ?EulerFermatPoly //=.
apply/pnatP; first by rewrite prime_gt0.
move=> p pp; rewrite dvdn_prime2 // => /eqP ->.
move: (char_Fp pn).
suff : {rmorphism 'F_n -> {poly 'F_n}} by move/rmorph_char; exact.
exists (fun x => x%:P) => //; eexists.
exact: polyC_sub.
split => //; exact: polyC_mul.

view this post on Zulip Gabriel Taumaturgo (Gitter import) (Nov 30 2019 at 12:53):

Thanks for answering me @affeldt-aist, but what imports are you using? I tried to reproduce this proof here and it fails on "rewrite exprDn_char". I tried importing all mathcomp.

view this post on Zulip Gabriel Taumaturgo (Gitter import) (Nov 30 2019 at 13:08):

Weird. I googled this Lemma and found it on ssralg.v, but I do have all_algebra imported.

view this post on Zulip Reynald Affeldt (Nov 30 2019 at 13:44):

maybe I added this Import GRing.Theory.

view this post on Zulip Reynald Affeldt (Nov 30 2019 at 13:46):

Locate exprDn_char could have given you this information

view this post on Zulip Gabriel Taumaturgo (Gitter import) (Nov 30 2019 at 15:58):

With this import the proof worked.

view this post on Zulip Gabriel Taumaturgo (Gitter import) (Nov 30 2019 at 15:59):

Does the library have papers describing this things like character and morphisms? My main source of learning was the mathcomp book, but it does not mention these parts of the library and i did not know where nor what to look for to solve this

view this post on Zulip Gabriel Taumaturgo (Gitter import) (Nov 30 2019 at 15:59):

And thank you again! @affeldt-aist

view this post on Zulip Reynald Affeldt (Nov 30 2019 at 19:17):

@Gabriel Taumaturgo for advanced topics, I am afraid you will need to look at the documentation inside the code, and go through through the papers (a non-exhaustive list can be found here https://math-comp.github.io/papers.html) to collect hints

view this post on Zulip Gabriel Taumaturgo (Gitter import) (Nov 30 2019 at 20:03):

Okay. The process people usually learn mathcomp is reading the papers? That is how you learned it?

view this post on Zulip Assia Mahboubi (Dec 02 2019 at 12:42):

Hi @Gabriel Taumaturgo ! What kind of information would you like to have? mathematical scope of what has been formalized or formalization technique?

view this post on Zulip Gabriel Taumaturgo (Gitter import) (Dec 03 2019 at 18:14):

Hi, @Assia Mahboubi .About Morphisms I would like to know if there exists some kind material i could use to learn how to apply them using SSReflect, and in my last message I would like to know how people usually "learn" how to use the library, I'm slowly making progress but there are lots of things in the library I don't know how to work with. For example, i read the MathComp book and there i learned about polynomials and the main algebraic structures, but i had no idea what morphisms were for(although I found them while browsing the documentation, i did not know they could be used to help me in the question I made here).

view this post on Zulip Karl Palmskog (Dec 03 2019 at 18:37):

@Gabriel Taumaturgo besides the MathComp book, you might find this book useful, it talks about things like SSReflect-specific proof automation techniques: https://ilyasergey.net/pnp/

view this post on Zulip Karl Palmskog (Dec 03 2019 at 18:46):

more generally, there are few substitutes to actually reading a lot of code that uses MathComp, many projects are listed in the Coq OPAM archive at https://github.com/coq/opam-coq-archive (e.g., after adding the released Coq OPAM repo, opam search --depends-on=coq-mathcomp-ssreflect)

view this post on Zulip Karl Palmskog (Dec 03 2019 at 19:28):

(in addition to reading, manually stepping through proof scripts and experimenting with definitions in many projects may also help)

view this post on Zulip Assia Mahboubi (Dec 03 2019 at 22:27):

@Gabriel Taumaturgo In addition to @Karl Palmskog 's excellent suggestions, may be the material of research schools like this one (beginner) or this one (more advanced) could help?

view this post on Zulip Assia Mahboubi (Dec 03 2019 at 22:29):

I think that at some point, the only way to learn is indeed to look at the header documentation contained in the source code. But it really depends on what you want to work with. Could you give more information about the kind of material you would like to formalize?

view this post on Zulip Reynald Affeldt (Dec 04 2019 at 08:54):

With mathcomp 1.10, as the changelog indicates, eqVneq as changed from a sumbool to a dedicated inductive type. How would you recommend rewriting functions like the following one https://github.com/math-comp/analysis/blob/master/theories/topology.v#L2160-L2163 in such a way that it compiles with mathcomp 1.10 and mathcomp 1.9?

view this post on Zulip Reynald Affeldt (Dec 04 2019 at 08:55):

(this is really the one issue that I faced when using the new mathcomp 1.10: but when there is not problem, there is the problem that you want more ;-) )

view this post on Zulip Kazuhiko Sakaguchi (Dec 04 2019 at 08:57):

@affeldt_aist I think, you may use eqP rather than eqVneq.

view this post on Zulip Kazuhiko Sakaguchi (Dec 04 2019 at 08:58):

Also using ecast might be better for readability.

view this post on Zulip Reynald Affeldt (Dec 04 2019 at 08:59):

thanks, I try working around this idea

view this post on Zulip Kazuhiko Sakaguchi (Dec 04 2019 at 09:02):

@affeldt-aist See also: https://github.com/math-comp/math-comp/blob/master/mathcomp/ssreflect/finfun.v#L79

view this post on Zulip Reynald Affeldt (Dec 04 2019 at 09:03):

so much for readability ;-)

view this post on Zulip Reynald Affeldt (Dec 04 2019 at 09:44):

anyway that exactly answers my problem, many thanks!

view this post on Zulip Cyril Cohen (Dec 04 2019 at 16:11):

(:thumbsup:)

view this post on Zulip Valentin Robert (Dec 05 2019 at 23:31):

huh, I'm still struggling with eliminating vectors of known size without losing information

view this post on Zulip Valentin Robert (Dec 05 2019 at 23:32):

I have a goal Vector.t bool 2 -> Prop, I'd like to eliminate with Vector.caseS twice in a row, but naively doing it once generalizes the 1 away

view this post on Zulip Valentin Robert (Dec 05 2019 at 23:34):

well, I guess I can do the ubnPeq trick

view this post on Zulip Valentin Robert (Dec 05 2019 at 23:39):

if anyone knows how to make this less ceremonious, that'd be appreciated:

Definition inBounds : Vector.t bool 2 -> Prop.
  have [n] := ubnPeq 1 => N v.
  move : v N.
  elim / @Vector.caseS => b1 n' v / eqP N'.
  subst n'.
  move : v.
  elim / @Vector.caseS => b0 _ _.
  (* do something with b1 and b0 *)

view this post on Zulip Emilio Jesús Gallego Arias (Dec 05 2019 at 23:53):

@Valentin Robert that's the Vector.t from the standard library?

view this post on Zulip Valentin Robert (Dec 05 2019 at 23:53):

yes

view this post on Zulip Emilio Jesús Gallego Arias (Dec 05 2019 at 23:53):

If so advice is just not to use it

view this post on Zulip Emilio Jesús Gallego Arias (Dec 05 2019 at 23:55):

you could make it usable but it will be a lot of work

view this post on Zulip Emilio Jesús Gallego Arias (Dec 05 2019 at 23:55):

what's ubnPeq ?

view this post on Zulip Emilio Jesús Gallego Arias (Dec 05 2019 at 23:56):

ah, the new lemma

view this post on Zulip Valentin Robert (Dec 05 2019 at 23:58):

so I should use the sequence type from mathcomp instead?

view this post on Zulip Emilio Jesús Gallego Arias (Dec 05 2019 at 23:58):

anyways I'm not sure I understand the problem there, you can just use ubnPeq again, right?

view this post on Zulip Valentin Robert (Dec 05 2019 at 23:59):

yeah this works, it's just kind of tedious to write

view this post on Zulip Emilio Jesús Gallego Arias (Dec 06 2019 at 00:02):

have [n N] := ubnPeq 1 => v.
elim/@Vector.caseS: v N => b1 {}n v /eqP ?; subst n.
move: v; have [n N] := ubnPeq 0 => v.
elim/@Vector.caseS: v N => b2 {}n v /eqP ?; subst n.

view this post on Zulip Emilio Jesús Gallego Arias (Dec 06 2019 at 00:03):

Well the do something part is missing, IMO it is a bit hard to understand what the best solution is

view this post on Zulip Emilio Jesús Gallego Arias (Dec 06 2019 at 00:03):

in some cases the best strategy can be indeed to map the vector to a list and use a regular fold

view this post on Zulip Emilio Jesús Gallego Arias (Dec 06 2019 at 00:05):

or use the recursion principle

view this post on Zulip Emilio Jesús Gallego Arias (Dec 06 2019 at 00:09):

Definition inBounds : Vector.t bool 2 -> Prop.
Proof.
elim/Vector.t_rect=> [|b n v ihv]; first by exact: True.
case: b; [ exact: False | exact: (True /\ ihv) ].
Defined.

Compute (inBounds (Vector.cons _ false _ (Vector.cons _ true _ (@Vector.nil _)))).

view this post on Zulip Valentin Robert (Dec 06 2019 at 00:10):

oh yeah, using the recursion principle to turn into a list is fairly neat, thanks for the idea

view this post on Zulip Valentin Robert (Dec 06 2019 at 00:10):

it'll scale better when I want to deal with 32-bit vectors :)

view this post on Zulip Reynald Affeldt (Dec 06 2019 at 08:11):

(there has been a minor update of mathcomp-real-closed (1.0.4) so that it is compatible with mathcomp.1.10.0 (available on opam))

view this post on Zulip Valentin Robert (Dec 06 2019 at 17:07):

does mathcomp have length-indexed lists? I see vector refers to the geometric notion

view this post on Zulip Reynald Affeldt (Dec 06 2019 at 17:22):

n.-tuple A in the file tuple.v

view this post on Zulip Reynald Affeldt (Dec 06 2019 at 17:23):

(you may even consider the type of row vectors ‘rv[A]_n from the file matrix.v)

view this post on Zulip Valentin Robert (Dec 06 2019 at 17:28):

oh right

view this post on Zulip Karl Palmskog (Dec 07 2019 at 19:32):

we are seeing the following errors when using ssreflect dev from Nix in CI:

building '/nix/store/lsfra14m6kx9vrqv25y5y8ymci5q7cab-coq-8.11-git-ssreflect-dev.drv'...

/nix/store/7g6xj1kz46s8czlfkxfxc0zby8dvigsf-ocaml-findlib-1.8.1/nix-support/setup-hook: line 9: createFindlibDestdir: unbound variable

builder for '/nix/store/lsfra14m6kx9vrqv25y5y8ymci5q7cab-coq-8.11-git-ssreflect-dev.drv' failed with exit code 1

view this post on Zulip Karl Palmskog (Dec 07 2019 at 19:32):

does anyone know what's going on? Non-dev versions work fine in Nix

view this post on Zulip Karl Palmskog (Dec 08 2019 at 00:10):

I'm also getting CI issues with OPAM and ssreflect and 8.11+beta1, since < 8.11 is currently a requirement in coq-mathcomp-ssreflect.dev

view this post on Zulip Valentin Robert (Dec 10 2019 at 00:19):

other simple question: I have a hypothesis nth (tnth_default t (Ordinal (n := n) (m := i) I)) = ... and my goal is nth (tnth_default t (Ordinal (n := n.+1) (m := i.+1) I)). Supposedly, the values in the Ordinal should not matter to the proof, but they prevent me from rewriting. How do I rewrite in their presence?

view this post on Zulip Valentin Robert (Dec 10 2019 at 00:21):

hmm nevermind, I don't need this proof...

view this post on Zulip Valentin Robert (Dec 11 2019 at 02:10):

view this post on Zulip Valentin Robert (Dec 13 2019 at 00:29):

I'm finding reasoning about tnth, rcons_tuple, and rev_ord quite tedious. For instance, here are some of my proofs:
http://paste.awesom.eu/ruRH
Am I missing some abstraction that would make this reasoning simpler?

view this post on Zulip Valentin Robert (Dec 13 2019 at 00:31):

in particular, is there a way to do something like val_inj to the arguments that tnth receives?

view this post on Zulip Valentin Robert (Dec 13 2019 at 01:09):

I managed to simplify it a bit by exploiting set_nth_default...

view this post on Zulip Kazuhiko Sakaguchi (Dec 13 2019 at 03:30):

@Valentin Robert Hello. I found nth_rcons is useful to prove the first lemma.

From mathcomp Require Import ssreflect eqtype ssrnat seq fintype tuple.

Theorem nth_rcons_tuple_last {T n} def (tuple : n.-tuple T) last :
  nth def (rcons_tuple tuple last) n = last.
Proof. by rewrite nth_rcons size_tuple ltnn eqxx. Qed.

Theorem nth_rcons_tuple_last' {T n} def (tuple : n.-tuple T) last m :
  m = n -> nth def (rcons_tuple tuple last) m = last.
Proof. by move=> ->; rewrite nth_rcons_tuple_last. Qed.

Theorem tnth_rcons_tuple_rev_ord0 {T n} (tuple : n.-tuple T) last :
  tnth (rcons_tuple tuple last) (rev_ord ord0) = last.
Proof. by rewrite [LHS]nth_rcons_tuple_last' // [LHS]subn1. Qed.

view this post on Zulip Valentin Robert (Dec 13 2019 at 03:33):

thanks!

view this post on Zulip Kazuhiko Sakaguchi (Dec 13 2019 at 03:45):

Also, the following facts were useful to prove the last lemma: For any t : n.-tuple T and x : T, val (rcons_tuple tuple last) and rcons (val tuple) last are convertible. For any i : 'I_n, val (rev_ord i) and n - i.+1 are convertible.

view this post on Zulip Karl Palmskog (Dec 13 2019 at 11:11):

@Assia Mahboubi @Cyril Cohen can I update the relevant MathComp dev OPAM packages to support the 8.11 beta?

view this post on Zulip Karl Palmskog (Dec 13 2019 at 11:11):

e.g., https://github.com/coq/opam-coq-archive/blob/master/extra-dev/packages/coq-mathcomp-ssreflect/coq-mathcomp-ssreflect.dev/opam#L13

view this post on Zulip Karl Palmskog (Dec 13 2019 at 11:12):

we need this for CI in some projects, both locally and in Coq-Community

view this post on Zulip Assia Mahboubi (Dec 13 2019 at 11:54):

@Karl Palmskog I do not know why this package is not up to-date, but I think it is ok.

view this post on Zulip Assia Mahboubi (Dec 13 2019 at 11:55):

@Enrico Tassi @Yves Bertot any opinion?

view this post on Zulip Karl Palmskog (Dec 13 2019 at 12:12):

@Assia Mahboubi also, isn't 1.10 supposed to support 8.11beta? When I tried from sources, it worked at least, but you may not want to update bound for released packages?

view this post on Zulip Assia Mahboubi (Dec 13 2019 at 12:17):

@Karl Palmskog something weird happened and my comment disappeared. I just said that mathcomp release happened just a few days before the tag of the (Coq) beta. Which might be a silly reason for the discrepancy.

view this post on Zulip Karl Palmskog (Dec 13 2019 at 12:18):

@Assia Mahboubi thanks, I managed to read it before it disappeared. I will await comments from Yves or Enrico and submit packages to the repo if they give thumbs-up

view this post on Zulip Valentin Robert (Dec 13 2019 at 17:36):

I definitely had missed rcons_tuple because it was in seq and I was looking in tuple, woops...

view this post on Zulip Valentin Robert (Dec 13 2019 at 18:04):

here's a very dumb question... my goal contains a if 0 < i then ... else ..., and I have a hypothesis 1 < i. What is the ssreflect way of making progress here?

view this post on Zulip Emilio Jesús Gallego Arias (Dec 13 2019 at 18:11):

I'd use rewrite (ltnW H).

view this post on Zulip Valentin Robert (Dec 13 2019 at 21:44):

thanks Emilio!

view this post on Zulip Florent Hivert (Dec 16 2019 at 08:08):

Is there a way to debug inference mechanism ? I'm running into the following problem: I defined a notation

Notation "[ 'ringMixin' 'of' U 'by' <- ]" := (InvLimitRing.invlim_ringMixin (Phant U))
  (at level 0, format "[ 'ringMixin'  'of'  U  'by'  <- ]") : form_scope.

whatever it means. The following is supposed to trigger a bunch of canonical inferences:

Definition fps_ringMixin := [ringMixin of {series R} by <-].

However I got the following error:

Error: Cannot infer an internal placeholder of type "is_true (i <= j)%N" in environment:
R : ringType
i, j : nat
x : (i <= j)%O

which means that somewhere in the inference, Coq got a nat comparison using the order library where it expects a plain nat comparison.
I tried hard to provide intermediate canonical to bridge those, but I failed. I've no idea how to debug that. Any suggestion ?

view this post on Zulip Assia Mahboubi (Dec 16 2019 at 09:30):

Hi @Valentin Robert

I definitely had missed rcons_tuple because it was in seq and I was looking in tuple, woops...

Just in case: because of the combination coercion + canonical instances, rcons_tuple is not that often useful, and can be replaced by a mere rcons.

From mathcomp Require Import ssreflect eqtype ssrnat seq fintype tuple.

Variables (T : Type) (n : nat) (t : n.-tuple T) (last : T).
Variable (P : seq T -> Prop) (h : forall x : n.+1.-tuple T, P x).

Goal P (rcons t last). exact: h. Qed.

view this post on Zulip Assia Mahboubi (Dec 16 2019 at 09:33):

@Florent Hivert can you also provide the term whose type-checking raises the error?

view this post on Zulip Florent Hivert (Dec 16 2019 at 09:52):

@Assia Mahboubi How would I do that ? I'm not sure to understand the question ? Is it possible to write a term which doesn't type check ?

view this post on Zulip Pierre-Yves Strub (Dec 16 2019 at 09:53):

Yes: Check (0 0). But it is not possible to type-check it :)

view this post on Zulip Florent Hivert (Dec 16 2019 at 09:56):

Is that what you want:

Check [ringMixin of {series R} by <-].

The answer is:

[ringMixin of {series R} by <-]
     : GRing.Ring.mixin_of (invlim.InvLimitRing.Tinv_zmodType (fps_invlimType R))
where
?i : [R : ringType  i : nat  j : nat  x : (i <= j)%O |- is_true (i <= j)%N]

Basically, I don't understand where the obligation is_true (i <= j)%N comes from. I though I've solved all of those.

view this post on Zulip Florent Hivert (Dec 16 2019 at 10:02):

The culprit is probably:

Hypothesis H : n <= m.
Fact trXnt_is_multiplicative : multiplicative (@trXnt m n).
[...]
Canonical trXnt_multiplicative := AddRMorphism trXnt_is_multiplicative.

However, I should have provided the obligation with

Definition fps_bond := fun (i j : nat) of (i <= j)%O => @trXnt R j i.

Variables (i j : nat) (le_ij : (i <= j)%O).
Lemma bond_is_rmorphism : rmorphism (fps_bond le_ij).
Proof.
split; first exact: trXnt_is_linear.
rewrite /fps_bond; apply trXnt_is_multiplicative.
by rewrite -leEnat.               (* HERE HERE HERE *)
Qed.
Canonical bond_additive := Additive bond_is_rmorphism.
Canonical bond_rmorphism := RMorphism bond_is_rmorphism.

view this post on Zulip Florent Hivert (Dec 16 2019 at 10:16):

I'm suspecting, that the second canonical bond_rmorphism is not used at all.

view this post on Zulip Florent Hivert (Dec 16 2019 at 13:40):

Found the solution ! I'm not sure what is really happening but it now works !

view this post on Zulip Reynald Affeldt (Dec 16 2019 at 13:41):

please share the magical incantation ! :-)

view this post on Zulip Florent Hivert (Dec 16 2019 at 15:04):

It is complicated to explain. I replaced a parameter by a _ in the definition of the mixin for (fps_invlimType R) allowing Coq to infer the correct structure.

view this post on Zulip Florent Hivert (Dec 17 2019 at 11:50):

I just discovered Set Debug Unification. This looks both great and very scary. Coq just spit 17000 lines of "explanation" why I need a ring to be commutative !!!

view this post on Zulip Assia Mahboubi (Dec 18 2019 at 08:57):

@Florent Hivert I did not know this command either... Thanks! :)

view this post on Zulip Florent Hivert (Dec 18 2019 at 15:40):

@Assia Mahboubi :-) Then it is a big mystery to me how you manage to debug problems with canonicals !

view this post on Zulip Assia Mahboubi (Dec 18 2019 at 19:58):

With pen and paper...

view this post on Zulip Florent Hivert (Dec 18 2019 at 20:40):

I don't understand the "uniform inheritance condition". I'd like to have a coercion betweem polynomials {poly R} and formal power series {series R}. However

Coercion fps_poly : poly_of >-> fpseries_of.

doesn't work:

Warning: fps_poly does not respect the uniform inheritance condition

Note: both are defined using the phantom trick:

Definition fpseries_of of phant R := fpseries.
Identity Coercion type_fpseries_of : fpseries_of >-> fpseries.
Notation "{ 'fps' R }" := (fpseries_of (Phant R)).

Is it feasible ?

view this post on Zulip Florent Hivert (Dec 18 2019 at 20:44):

@Assia Mahboubi So you are writing with pen and paper the equivalent of the 17000 lines ! :-)

view this post on Zulip Kazuhiko Sakaguchi (Dec 19 2019 at 00:40):

The uniform inheritance condition is defined here: https://coq.inria.fr/refman/addendum/implicit-coercions.html#coercions
and Sect. 3.2 of https://dl.acm.org/citation.cfm?id=263742

view this post on Zulip Florent Hivert (Dec 19 2019 at 07:47):

@Kazuhiko Sakaguchi : Sure ! But I don't understand why it doesn't work with my example.

fps_poly : forall R : ringType, {poly R} -> {fps R}

Is it because of the phantom trick on the source {poly R} ?

view this post on Zulip Kazuhiko Sakaguchi (Dec 19 2019 at 07:51):

@Florent Hivert Yes. The type of fps_poly should be something like forall (R : ringType) (ph : phant R), poly_of R ph -> fpseries_of R ph.

poly_of
     : forall R : ringType, phant R -> Type

view this post on Zulip Kenji Maillard (Dec 20 2019 at 10:24):

A question on ssreflect : tactical (Is it the is the right room to ask these questions ?): I use from time to time the inversion tactic that messes with names and then want to revert an hypothesis generated by inversion. I can do this with a match goal construct but it is a bit heavy. Is there a way to do something like move: pattern reverting the hypothesis matching the pattern (instead of using the name of the hypothesis) ?

view this post on Zulip Reynald Affeldt (Dec 20 2019 at 11:19):

This is not an answer but in that kind of situation I prove a specialized lemma (possibly with inversion...) to have a better handling of the naming of variables and hypotheses.

view this post on Zulip Assia Mahboubi (Dec 20 2019 at 20:45):

@Kenji Maillard (at least it is a good place I would say). I do not know how to do what you ask for using ssreflect. As far as I can tell, the patterns used for subterm selection are only available for subterms in the goal. E.g., you can create an abbreviation for a subterm in the goal (under the bar) using set x := (_ + _) or set LHS := (X in X = _). Or even set p := (_ <> _). But if I understand correctly, you would like a pattern use to filter types of elements in the context.

view this post on Zulip Florent Hivert (Jan 09 2020 at 16:21):

Hi there, In need to prove a goal such as exists _ : {y : nat | (y < 1)%O}, True. I'm using Cyril's order package with nat. Currently I'm doing

have lt01 : 0%N < 1%N by rewrite ltEnat.
by exists (exist (fun x => x < 1%N) 0 lt01).

I'd rather have to provide the witness 0 and then the proof term. Is it feasible ?

view this post on Zulip Cyril Cohen (Jan 09 2020 at 17:13):

My question is why your goal isn't simply {y : nat | (y < 1)%O}?

view this post on Zulip Cyril Cohen (Jan 09 2020 at 17:14):

otherwise you could first have a proof of A -> exists _ : A, True

view this post on Zulip Florent Hivert (Jan 10 2020 at 10:45):

@Cyril Cohen The True is actually any Prop possibly depending on x. What I actually need is exists x : {y : nat | (y < 1)%O}, P x for a given P.
I guess a lemma such as forall x, (x < 1)%O -> P x -> exists x : {y : nat | (y < 1)%O}, P x should do the job.

view this post on Zulip Florent Hivert (Jan 10 2020 at 16:55):

@Cyril Cohen : Still having problem with dual order:

Section Def.
Variable (u : unit) (Ord : orderType u).
Implicit Type (x : Ord).
Definition down x := [pred y | y < x].
Definition up x := [pred y | y > x].
End Def.

Section Bla.
Variable (u : unit) (Ord : orderType u).
Implicit Type (x y : Ord).
Let Dual := [orderType of Ord^d].
Lemma OrdCE x y : ((x : Dual) <^d (y : Dual)) = (y < x). (* Looks Ok *)
Proof. by []. Qed.

Lemma bla x y :
  (x \in down y) = ((y : Dual) \in down (Ord := Dual) (x : Dual)).
Proof.
rewrite !inE /Dual /=.

Can't manage to have correct down of the dual order

view this post on Zulip Cyril Cohen (Jan 10 2020 at 17:52):

Thanks for spotting this... right now I must say I have no clue why this fails...

view this post on Zulip Cyril Cohen (Jan 10 2020 at 19:09):

and the culprit is: missing canonicals

view this post on Zulip Cyril Cohen (Jan 10 2020 at 19:09):

like... a lot

view this post on Zulip Cyril Cohen (Jan 10 2020 at 19:09):

:laughing: thanks for spotting this

view this post on Zulip Florent Hivert (Jan 10 2020 at 19:21):

@Cyril Cohen You are welcome ! It is maybe a little late, but as you see, I'm participating to the review PR #454 ;-)

view this post on Zulip Cyril Cohen (Jan 10 2020 at 19:22):

not too late at all

view this post on Zulip Florent Hivert (Jan 10 2020 at 19:54):

Any quick Fix ? I'm ready to beta test one !
No pressure actually ! After all, It the week-end and I'm going to watch a movie ;-)

view this post on Zulip Cyril Cohen (Jan 10 2020 at 20:17):

should be solved now

view this post on Zulip Florent Hivert (Jan 10 2020 at 23:01):

@Cyril Cohen My code is now working like a charm ! Thanks !

view this post on Zulip Cyril Cohen (Jan 10 2020 at 23:04):

@Florent Hivert I'm glad, thanks!

view this post on Zulip Kazuhiko Sakaguchi (Jan 11 2020 at 00:05):

:+1:

view this post on Zulip Valentin Robert (Jan 21 2020 at 19:36):

what's a ssreflect way of doing essentially pose proof?

view this post on Zulip Karl Palmskog (Jan 21 2020 at 19:43):

uh, have <name> := <term>?

view this post on Zulip Valentin Robert (Jan 21 2020 at 19:43):

ah, well anyway, I realized I was immediately rewriting with it so don't need it. but thanks!

view this post on Zulip Assia Mahboubi (Jan 22 2020 at 12:38):

@Valentin Robert Just in case, a variant of @Karl Palmskog 's suggestion is: have -> : lhs = rsh.
There is a number of intro patterns you can put after have and suff, including -> and <-.

view this post on Zulip Valentin Robert (Jan 30 2020 at 18:22):

hello again. Are there known issues about using ssreflect inversion tactics like case/elim in the presence of type classes? I'm encountering an issue where a call to case triggers a type class search that seems unnecessary and fails dramatically :\

view this post on Zulip Karl Palmskog (Jan 31 2020 at 14:31):

@Cyril Cohen do you know offhand which ones of your packages support 8.11.0? Latest finmap at least, right?

view this post on Zulip Karl Palmskog (Jan 31 2020 at 14:32):

in any case, I'm going to try do a small pass over MathComp-related OPAM packages which have < 8.11~ and see if they work, and adjust bounds in the OPAM repo

view this post on Zulip Karl Palmskog (Jan 31 2020 at 14:33):

if anyone has something against this, let me know here...

view this post on Zulip Karl Palmskog (Jan 31 2020 at 14:38):

what the heck, finmap-1.3.4 doesn't seem to require coq-mathcomp-bigenough?

view this post on Zulip Karl Palmskog (Jan 31 2020 at 14:51):

ah, now it's getting clearer, mathcomp-analysis requires bigenough but doesn't mention it, so that's where it is needed

view this post on Zulip Paolo Giarrusso (Feb 10 2020 at 20:06):

@Valentin Robert how does the call to case look like? Can that be fixed by passing more parameters explicitly?

view this post on Zulip Paolo Giarrusso (Feb 10 2020 at 20:07):

I've seen trouble for suff and have :=, but not elim or case.

view this post on Zulip vlj (Feb 10 2020 at 21:14):

I have an issue with ordinaland map, I have a function f that takes a 'I_nargument, which basically embeds a nat and a prof that this nat is less than n. I'd like to Compute the map with a proper function and a proper n, but it doesn't work because of opaque type so I'm trying to proof an equality instead. Issue is that I'm stuck and I don't really know why, at some point the map has an explicit seq 'I_n input but the =//tactic doesn't reduce it.
See https://gist.github.com/vlj/be8041d11efc4b5d30ff5f5723051ebe

What I have in the goal is
foldr +%R 0 [seq (\matrix_(_, _) 1) i j | i <- oapp (cons^~ (oapp (cons^~ (oapp (cons^~ [::]) [::] (insub 2))) (oapp (cons^~ [::]) [::] (insub 2)) (insub 1))) (oapp (cons^~ (oapp (cons^~ [::]) [::] (insub 2))) (oapp (cons^~ [::]) [::] (insub 2)) (insub 1)) (insub 0)] = 3

view this post on Zulip vlj (Feb 10 2020 at 21:14):

the whole oapp/cons things seem to be an explicit seq which should be explicitly mappable to the \ matrix_(_, _) 1 i jfunction right ?

view this post on Zulip vlj (Feb 10 2020 at 21:14):

(posted on coq/coq too)

view this post on Zulip Emilio Jesús Gallego Arias (Feb 10 2020 at 21:37):

by rewrite /test_kernel tmp0 /ord_enum /= !insubT /= !mxE. will help you progess here, you want remove the subType proof.

view this post on Zulip Emilio Jesús Gallego Arias (Feb 10 2020 at 21:38):

insub_eq does provide a version of insub that will compute @vlj

view this post on Zulip vlj (Feb 10 2020 at 21:41):

Thanks will try tomorrow

view this post on Zulip Cyril Cohen (Feb 11 2020 at 00:46):

I would avoid relying on foldr at all and use the following "non abstraction breaking" proof: by rewrite (eq_bigr (fun=> 1)) ?big_const_ord// => i; rewrite mxE.

view this post on Zulip Cyril Cohen (Feb 11 2020 at 00:51):

or the new by under eq_bigr => i do rewrite mxE; rewrite big_const_ord. (available from coq 8.10)

view this post on Zulip Emilio Jesús Gallego Arias (Feb 11 2020 at 09:51):

Yup I think Cyril's solution is much preferred

view this post on Zulip vlj (Feb 11 2020 at 18:34):

under is an equivalent of refine in standard coq ?

view this post on Zulip Reynald Affeldt (Feb 11 2020 at 18:37):

You are right to see a relation between both

view this post on Zulip Reynald Affeldt (Feb 11 2020 at 18:37):

You can find a bit of documentation here: https://staff.aist.go.jp/reynald.affeldt/coq2019/coqws2019-martindorel-tassi.pdf

view this post on Zulip Reynald Affeldt (Feb 11 2020 at 18:38):

with slides https://staff.aist.go.jp/reynald.affeldt/coq2019/coqws2019-martindorel-tassi-slides.pdf and a demo https://www.irit.fr/~Erik.Martin-Dorel/exposes/coq10_demo_under.v

view this post on Zulip Reynald Affeldt (Feb 11 2020 at 18:44):

the authors (Martin-Dorel and Tassi) explain how evars are used in the first page of the abstract

view this post on Zulip Bas Spitters (Feb 12 2020 at 14:34):

Are efficient machine integers available in math-comp? I would expect that Thomas Sibut-Pinote needed them in his thesis, but I cannot find the sources quickly.

view this post on Zulip Assia Mahboubi (Feb 12 2020 at 15:46):

Hi @Bas Spitters . What do you mean by "available in math-comp" ? As a start, you can certainly load both mathcomp libraries and any other library you wish. And no, they were not needed for the work done by Thomas in his thesis: arithmetic on ZArith was efficient enough.

view this post on Zulip Karl Palmskog (Feb 12 2020 at 15:51):

I think he means if there is some MathComp-compatible/MathComp-idiomatic way (e.g., some repo with experimental code) to leverage the new UInt63 and so on, not necessarily code that lives in MathComp itself

view this post on Zulip Karl Palmskog (Feb 12 2020 at 15:54):

I guess one could at least build the usual structures (choiceType, finType, etc.) for the int63 type, right?

view this post on Zulip Assia Mahboubi (Feb 12 2020 at 15:59):

@Karl Palmskog for equality, this is not clear to me: this is modular arithmetic so the relevant boolean comparison is modulo 2^63.

view this post on Zulip Assia Mahboubi (Feb 12 2020 at 16:02):

But you could indeed easily equip it with the trivial boolean equality, and then choice and countable structures.

view this post on Zulip Assia Mahboubi (Feb 12 2020 at 16:05):

However, I would prefer to know what @Bas Spitters had in mind before giving a more detailed answer.

view this post on Zulip Karl Palmskog (Feb 12 2020 at 16:05):

sure, he should confirm, although I was also interested in this particular answer, thanks

view this post on Zulip Bas Spitters (Feb 13 2020 at 10:10):

With @Jakob Botsch Nielsen we are formalizing some crypto for smart contracts which we like to compute relatively efficiently. nat is too slow. Meanwhile, we've found what we need in coq-prime.
This seems like another case where having univalence would be nice to transport between nat and N :-)
But general, yes my question was approximately what @Karl Palmskog mentioned.

view this post on Zulip Karl Palmskog (Feb 13 2020 at 10:11):

@Bas Spitters you probably want to use CoqEAL

view this post on Zulip Karl Palmskog (Feb 13 2020 at 10:12):

it does already provide transport between nat and N if I recall correctly

view this post on Zulip Karl Palmskog (Feb 13 2020 at 10:13):

it would be interesting to provide (non-bidirectional) transport between nat and int63 in CoqEAL

view this post on Zulip Bas Spitters (Feb 13 2020 at 10:13):

Yes, that could be enough. We'll have a look. Too many libraries not communicating ...

view this post on Zulip Karl Palmskog (Feb 13 2020 at 10:14):

unfortunately CoqEAL only works with 8.11 and MathComp 1.10 if you use Pierre Roux's pull request patch

view this post on Zulip Karl Palmskog (Feb 13 2020 at 10:15):

ping @Cyril Cohen that it would be very convenient if this was merged (and a new release would also be very welcome)

view this post on Zulip Cyril Cohen (Feb 13 2020 at 10:16):

@Karl Palmskog done

view this post on Zulip Karl Palmskog (Feb 13 2020 at 10:17):

:thumbsup: thanks!

view this post on Zulip Cyril Cohen (Feb 13 2020 at 10:17):

and released

view this post on Zulip Cyril Cohen (Feb 13 2020 at 10:18):

I do not have time to prepare the opam packages though

view this post on Zulip Karl Palmskog (Feb 13 2020 at 10:18):

I can do it if you don't mind

view this post on Zulip Cyril Cohen (Feb 13 2020 at 10:18):

I certainly do not mind ;)

view this post on Zulip Karl Palmskog (Feb 13 2020 at 10:19):

hmm, I have to double check, but I think finmap >= 1.4 is required now

view this post on Zulip Karl Palmskog (Feb 13 2020 at 11:01):

indeed this is the case, meaning that also multinomials 1.5 is required

view this post on Zulip Cyril Cohen (Feb 13 2020 at 12:50):

@Karl Palmskog yes, but everything is already here https://github.com/CoqEAL/CoqEAL/blob/master/coq-coqeal.opam#L20

view this post on Zulip Karl Palmskog (Feb 13 2020 at 12:53):

right (it's handled by the multinomials dep), but the text in the 1.0.3 release says finmap 1.3.4

view this post on Zulip Cyril Cohen (Feb 13 2020 at 12:54):

I can edit that, I screwed up

view this post on Zulip Cyril Cohen (Feb 13 2020 at 12:55):

:thumbsup:

view this post on Zulip Karl Palmskog (Feb 13 2020 at 12:56):

versioning is getting hard, I guess this is also a luxury problem, but I'm hoping Coq platform can help at some point (https://github.com/MSoegtropIMC/coq-platform/blob/master/charter.md)

view this post on Zulip Karl Palmskog (Feb 13 2020 at 12:59):

(for example, I think CoqEAL should definitely be in the platform, along with Analysis and some other MathComp stuff)

view this post on Zulip Cyril Cohen (Feb 13 2020 at 13:18):

I do not think these are mature software

view this post on Zulip Karl Palmskog (Feb 13 2020 at 13:21):

well, platform inclusion doesn't imply full maturity in my reading, usually just that a project has been found useful by other researchers/engineers

view this post on Zulip Karl Palmskog (Feb 13 2020 at 13:22):

for example, is there any other project that gives better or more convenient transfer nat <-> N? I haven't seen much in this direction

view this post on Zulip Paolo Giarrusso (Feb 13 2020 at 14:07):

I guess projects in the platform could specify their maturity level and guarantees.

view this post on Zulip Paolo Giarrusso (Feb 13 2020 at 14:09):

instead of hoping people guess the right thing.

view this post on Zulip Emilio Jesús Gallego Arias (Feb 13 2020 at 14:10):

Only reasonably mature stuff should be included in the platform IMHO

view this post on Zulip Karl Palmskog (Feb 13 2020 at 17:01):

CoqEAL 1.0.2 and 1.0.3 are now on the Coq OPAM archive

view this post on Zulip vlj (Feb 13 2020 at 20:40):

Platform has different package as opam ?

view this post on Zulip Karl Palmskog (Feb 13 2020 at 21:40):

the platform (which currently exists as the Windows distribution of Coq) is in theory independent of OPAM packages, but the intention is that platform eventually becomes an OPAM "meta-package" that specifies versions of each platform-included project

view this post on Zulip Karl Palmskog (Feb 13 2020 at 21:44):

or at least that's one possibility that's been discussed favorably

view this post on Zulip Valentin Robert (Feb 14 2020 at 14:18):

hi all, in ssreflect I sometimes use move : someLemma to add the lemma to the top of my goal stack. However, it often fails in the presence of typeclasses, and the only thing that seems to work is move : (@someLemma)., which makes it very painful to instantiate... is there any known trick? :\

view this post on Zulip Paolo Giarrusso (Feb 14 2020 at 14:28):

@Valentin Robert does have := someLemma work better? move: t is a bit hacky (it tries to generalize things).

view this post on Zulip Paolo Giarrusso (Feb 14 2020 at 14:29):

last I checked, have := won't instantiate typeclasses even when it should (and then I use pose proof)

view this post on Zulip Valentin Robert (Feb 14 2020 at 14:39):

@Paolo G. Giarrusso oh yeah this works much better!

view this post on Zulip Valentin Robert (Feb 14 2020 at 14:40):

ah yeah, it instantiates the type class arguments up to the last actual argument I pass, but leaves the ones after sadly...

view this post on Zulip Valentin Robert (Feb 14 2020 at 14:41):

yeah I've been using pose proof too...

view this post on Zulip Valentin Robert (Feb 14 2020 at 14:41):

guess I'll keep pose proof then :\

view this post on Zulip Cyril Cohen (Feb 14 2020 at 14:44):

There should eventually be a switch for have, but meanwhile you can use the following trick/hack, by @Enrico Tassi https://github.com/math-comp/analysis/blob/bb4938c2dee89e91668f8d6a251e968d2f5a05ae/theories/posnum.v#L51-L52

view this post on Zulip Cyril Cohen (Feb 14 2020 at 14:44):

You can then do have : !! term_with_tc

view this post on Zulip Valentin Robert (Feb 14 2020 at 14:44):

:D

view this post on Zulip Valentin Robert (Feb 14 2020 at 14:47):

thanks Cyril!

view this post on Zulip Valentin Robert (Feb 14 2020 at 21:50):

hmm, I still don't quite understand how to do inversion with equations properly

view this post on Zulip Valentin Robert (Feb 14 2020 at 21:52):

if I do case : indexVar / indVal, I get forall i, A i -> B i -> C i -> i = indexVar -> Goal, and this makes doing the substitution of indexVar for i complicated...

view this post on Zulip Valentin Robert (Feb 14 2020 at 21:53):

the only way I know of is to move => i Ai Bi Ci EQ, then move : EQ Ai Bi Ci => ->

view this post on Zulip Valentin Robert (Feb 14 2020 at 21:54):

because the equation is all the way after all the constructor arguments, but those need to be in the goal for the substitution

view this post on Zulip Valentin Robert (Feb 14 2020 at 22:14):

it's quite ugly how I am doing it:

      case : tv / wtv.
      move => tau__c' v__c' b P1 P2 EQ   (* move in everything so I can grab the equality *)
      move : EQ P1 P2 => [] <- <- P1 P2. (* move back things that depend on the equality, and substitute *)
      move : tau__c' v__c' => _ _.       (* now those introduced variables are pointless *)

view this post on Zulip Valentin Robert (Feb 14 2020 at 22:57):

ah, I just learned about clear_switch, I guess I can at least get rid of the last line

view this post on Zulip Paolo Giarrusso (Feb 14 2020 at 23:01):

Coq 8.10 added temporary introductions.

view this post on Zulip Paolo Giarrusso (Feb 14 2020 at 23:05):

For instance for the first two lines you can more or less do: move => ??? ++ []. move => <- <- P1 P2. @Valentin Robert

view this post on Zulip Paolo Giarrusso (Feb 14 2020 at 23:06):

The temporary introduction is done by +. More info in the changelog and links https://coq.inria.fr/refman/changes.html#id117

view this post on Zulip Paolo Giarrusso (Feb 14 2020 at 23:08):

however, when it matters I often prove separate inversion mini-lemmas that I can apply with ssreflect; for those mini-lemmas I use inversion.

view this post on Zulip Paolo Giarrusso (Feb 14 2020 at 23:08):

And subst.

view this post on Zulip Paolo Giarrusso (Feb 14 2020 at 23:11):

So clients can write ssreflect proofs, while those are written with inversion. See for instance nsteps_once_inv in https://gitlab.mpi-sws.org/iris/stdpp/blob/master/theories/relations.v#L145

view this post on Zulip Paolo Giarrusso (Feb 14 2020 at 23:11):

Or rtc_inv in https://gitlab.mpi-sws.org/iris/stdpp/blob/master/theories/relations.v#L113

view this post on Zulip Valentin Robert (Feb 14 2020 at 23:23):

I do have an inversion lemma for this, I was just trying to avoid the hassle of defining it :) thanks for all the pointers!

view this post on Zulip vlj (Feb 16 2020 at 12:41):

I have an issue, I have an expression involving le, and max, in mathcomp/ssrnat, but I cannot apply le_max_l. I'm trying to reflect the expression but it doesn't work.

view this post on Zulip vlj (Feb 16 2020 at 12:41):

https://gist.github.com/vlj/863f47cd5a3f55f3ab545a8f1af51830

view this post on Zulip vlj (Feb 16 2020 at 12:41):

No assumption in ((p <= Nat.max p q) = true)

view this post on Zulip vlj (Feb 16 2020 at 12:46):

apparently le is in %R and not in %N...

view this post on Zulip vlj (Feb 16 2020 at 12:49):

is there a way to "move" le in ring_scope to le in coq_nat, if all arguments are nat ?

view this post on Zulip vlj (Feb 16 2020 at 12:51):

(btw when I try to search using Search ((_ <= _)%R _ (_ <= _)%N). I get no head constant in head search pattern, the -> symbol is not supported ? )

view this post on Zulip Paolo Giarrusso (Feb 16 2020 at 12:53):

@vlj your search uses _ in place of ->

view this post on Zulip vlj (Feb 16 2020 at 12:56):

you mean Search ((_ <= _)%R _ (_ <= _)). ?

view this post on Zulip vlj (Feb 16 2020 at 12:56):

it complains : too many arguments in head search pattern

view this post on Zulip vlj (Feb 16 2020 at 13:03):

ler_nat doesn't work for me

view this post on Zulip Paolo Giarrusso (Feb 16 2020 at 13:11):

@vlj what I meant is that your search does not use ->; you could try Search ((_ <= _)%R -> (_ <= _)); if that fails, Search _ ((_ <= _)%R -> (_ <= _)).

view this post on Zulip Paolo Giarrusso (Feb 16 2020 at 13:11):

and okay, I guess the first will fails, because Search pattern only matches the conclusion — I always use Search _ pattern to match against the entire statement.

view this post on Zulip Anton Trunov (Feb 16 2020 at 16:06):

@vlj @Paolo G. Giarrusso FWIW, there is a wiki page about using SSReflect’s Search command: https://github.com/math-comp/math-comp/wiki/Search. It explains some gotchas and provides a number of tips and tricks.

view this post on Zulip vlj (Feb 17 2020 at 20:33):

I'm not able to prove that Num.ler p p is true... it looks like leand ler can't be unified, but I think I'm including near all of mathcomp so there should be a canonical somewhere

view this post on Zulip vlj (Feb 17 2020 at 20:33):

https://gist.github.com/vlj/ee3fd2c568cfd976e710a344b302910a

view this post on Zulip Reynald Affeldt (Feb 17 2020 at 21:52):

@vlj by rewrite lerr.

view this post on Zulip vlj (Feb 17 2020 at 22:20):

@affeldt-aist thanks ! how did you find it ?

view this post on Zulip Reynald Affeldt (Feb 17 2020 at 22:29):

I guessed the name.

view this post on Zulip Reynald Affeldt (Feb 17 2020 at 22:30):

The naming of such lemmas is very regular in MathComp and it is worth learning.

view this post on Zulip vlj (Feb 19 2020 at 20:07):

I'm completly stuck with Order.Theory. I'd like to prove that x <= max x y where max is defined in Order.Theory. It is defined as a join in a lattice, but I can't find a Lemma relating this to the fact that all element in the pair x, y are less or equal than the join.

view this post on Zulip vlj (Feb 19 2020 at 20:08):

I could rewrite /Order.join //= maxn. and then I could solve by case but it looks a bit unatural.

view this post on Zulip Emilio Jesús Gallego Arias (Feb 19 2020 at 20:38):

@vlj for me by rewrite lexUl. does the trick

view this post on Zulip Emilio Jesús Gallego Arias (Feb 19 2020 at 20:49):

the right lemma is leUl not lexUl

view this post on Zulip vlj (Feb 19 2020 at 21:11):

Thanks

view this post on Zulip vlj (Feb 19 2020 at 21:32):

it doesn't work for me :/

view this post on Zulip vlj (Feb 19 2020 at 21:33):

The LHS of Order.DistrLatticeTheoryJoin.leUl
    (_ <= _ `|` _)%O
does not match any subterm of the goal

view this post on Zulip vlj (Feb 19 2020 at 21:33):

with the gist it's easier maybe https://gist.github.com/vlj/408daf59ab39c4efae8e66658692dde0

view this post on Zulip vlj (Feb 19 2020 at 21:44):

apparently there is a conflict between Order.le and Num.Def.ler

view this post on Zulip Emilio Jesús Gallego Arias (Feb 19 2020 at 21:45):

You have indeed a bit of a mess there; you are using an operator from a different library for each of the operatros

view this post on Zulip Emilio Jesús Gallego Arias (Feb 19 2020 at 21:45):

max is the one from nat

view this post on Zulip Emilio Jesús Gallego Arias (Feb 19 2020 at 21:45):

<= the one from num

view this post on Zulip Emilio Jesús Gallego Arias (Feb 19 2020 at 21:45):

and you are injecting the nat from max to the ints by the Posz coercion

view this post on Zulip Emilio Jesús Gallego Arias (Feb 19 2020 at 21:45):

the thing can be proved actually by stripping all this, but you don't want to do that

view this post on Zulip Emilio Jesús Gallego Arias (Feb 19 2020 at 21:47):

Proof. by rewrite lez_nat leq_maxl. Qed.

view this post on Zulip vlj (Feb 19 2020 at 21:48):

thanks

view this post on Zulip Emilio Jesús Gallego Arias (Feb 19 2020 at 21:48):

you want to open order_scope if you wanna use the _ <= _ from order

view this post on Zulip vlj (Feb 19 2020 at 21:49):

I need to keep the max in nat

view this post on Zulip Emilio Jesús Gallego Arias (Feb 19 2020 at 21:49):

why?

view this post on Zulip vlj (Feb 19 2020 at 21:49):

what happen if I open several scope with conflicting definition

view this post on Zulip Emilio Jesús Gallego Arias (Feb 19 2020 at 21:49):

they work as a stack [roughly]

view this post on Zulip Emilio Jesús Gallego Arias (Feb 19 2020 at 21:49):

if you want to keep the max in nat use maxn

view this post on Zulip Emilio Jesús Gallego Arias (Feb 19 2020 at 21:50):

and <= from nat

view this post on Zulip Emilio Jesús Gallego Arias (Feb 19 2020 at 21:50):

if you want to see it as a lattice don't

view this post on Zulip Emilio Jesús Gallego Arias (Feb 19 2020 at 21:50):

but don't pick the <= from int

view this post on Zulip vlj (Feb 19 2020 at 21:50):

I'm trying to build a definition of a nat that follow a property, but the property is a distance between nat (ie '|x - y|

view this post on Zulip vlj (Feb 19 2020 at 21:50):

ok

view this post on Zulip Emilio Jesús Gallego Arias (Feb 19 2020 at 21:51):

You can use sections / modules to better manage scopes, IIRC this is used very often in math-comp

view this post on Zulip vlj (Feb 19 2020 at 21:51):

I mean the "big" lemma I need is Lemma tmp_ (x:int) (n:nat) (P:odd n) (i: 'I_n): '|x + i - n./2%:Z - x| <= n./2.

view this post on Zulip vlj (Feb 19 2020 at 21:51):

ok

view this post on Zulip vlj (Feb 19 2020 at 21:52):

with x being potentially negative, n being always positive, and i between 0 and n

view this post on Zulip vlj (Feb 19 2020 at 21:52):

so I need to have something in intin the distance (I don't want to "clamp" the value)

view this post on Zulip vlj (Feb 19 2020 at 21:53):

and I need to do that in 2 dimension, so I need to pick the max of n./2 and m./2, where m follow the same kind of property (but for other variable)

view this post on Zulip vlj (Feb 19 2020 at 21:54):

I will try to rewrite my complete proof script to use scope and try to stay in nat_scope

view this post on Zulip Emilio Jesús Gallego Arias (Feb 19 2020 at 21:57):

you could also move to (n : int) (h_n : 0 <= n)

view this post on Zulip Emilio Jesús Gallego Arias (Feb 19 2020 at 21:57):

hard to know

view this post on Zulip vlj (Feb 19 2020 at 22:08):

Actually the big issue I'm facing is in the way to define a "dist" function :

    Section CoordDistance.
        Local Open Scope ring_scope.
        Local Open Scope distn_scope.
        Definition dist (x:int) (n:nat) (i: 'I_n):nat :=
            `|x + i%:Z - n./2%:Z - x|%N.
    End CoordDistance.

view this post on Zulip vlj (Feb 19 2020 at 22:08):

it doesn't type, but that's what I would like to have : |x + i - n/2 - x|, but in N

view this post on Zulip vlj (Feb 19 2020 at 22:09):

x + i - n/2 - x is in Z (but for some reason it doesn't work with int_scope, I need to have ring_scope)

view this post on Zulip vlj (Feb 19 2020 at 22:10):

but for some reason it picks the norm in ring_scope and not the one in ssrint

view this post on Zulip vlj (Feb 19 2020 at 22:12):

it's strange, Definition dist (x:int) (n:nat) (i: 'I_n) := let tmp := x + i%:Z - n./2%:Z - x in |tmp|%N.` works but if I substitute tmp in the expression, it doesn't

view this post on Zulip vlj (Feb 19 2020 at 22:14):

seems like an issue in parsing

view this post on Zulip Paolo Giarrusso (Feb 19 2020 at 22:42):

@vlj %N affects the scope for everything inside the norm, so there's no reason for those two expressions to be equivalent

view this post on Zulip Paolo Giarrusso (Feb 19 2020 at 22:44):

(I'd honestly be tempted to use Locate for each notation you want to use and write the desugared expression, but I don't know how realistic it is; it might help debugging).

view this post on Zulip Paolo Giarrusso (Feb 19 2020 at 22:46):

Actually, ahem, you could maybe use tmp, or just force another scope inside the norm:

view this post on Zulip Paolo Giarrusso (Feb 19 2020 at 22:48):

`| (x + i....)%distn_scopr%ring_scope |%N

view this post on Zulip Paolo Giarrusso (Feb 19 2020 at 22:49):

scope not scopr, sorry. Caveat I haven't tried, but this should reenable the other scopes inside the parentheses. The question is which scopes must be enabled this way.

view this post on Zulip vlj (Feb 19 2020 at 22:56):

thanks, will give a try

view this post on Zulip Emilio Jesús Gallego Arias (Feb 20 2020 at 03:03):

Why you do x + i - n - x ? This is just i - n ?

view this post on Zulip Emilio Jesús Gallego Arias (Feb 20 2020 at 03:04):

so you have (n i : int), 0 <= n -> 0 <= i < n -> ``| i - n |?

view this post on Zulip Emilio Jesús Gallego Arias (Feb 20 2020 at 03:06):

but given that i < n you can rewrite it to use max?

view this post on Zulip Valentin Robert (Feb 20 2020 at 13:12):

it seems that the precedence of .+1 and [tuple of ... ] aren't quite happy with each other, the following require parenthesizing:
http://paste.awesom.eu/NmKS

view this post on Zulip Valentin Robert (Feb 20 2020 at 13:28):

let E := fresh "E" in case E : e. does not use the fresh name... is this impossible in ssreflect?

view this post on Zulip Valentin Robert (Feb 20 2020 at 13:29):

(I also tried case ? : e. which does not give me an equation...)

view this post on Zulip Paolo Giarrusso (Feb 20 2020 at 13:52):

@Valentin Robert sounds like a possible bug, especially if destruct e eqn:E works; based on https://github.com/coq/coq/issues/10928, I wonder if it relates to https://github.com/coq/coq/issues/6687.

view this post on Zulip Paolo Giarrusso (Feb 20 2020 at 13:53):

(the symptoms are not so close, but the first was marked as a dup of the second and both involve name resolution)

view this post on Zulip vlj (Feb 22 2020 at 00:02):

Is there a refinement for ssrint to /From "coq_int"? Looking at coqeal binint.v seems to redefine coq_int.

view this post on Zulip vlj (Feb 22 2020 at 00:03):

I'd like to do someyhing similar to @affeldt-aist 's ssromega but for ssrint, but omega/lia work with coq' s int not any int.

view this post on Zulip Kazuhiko Sakaguchi (Feb 22 2020 at 12:16):

@vlj https://github.com/pi8027/mczify This should work with Coq 8.11.

view this post on Zulip vlj (Feb 22 2020 at 16:17):

doesn't work with coq 8.0 ?

view this post on Zulip vlj (Feb 22 2020 at 16:17):

8.10*

view this post on Zulip vlj (Feb 22 2020 at 16:17):

opam only has 8.10 so far

view this post on Zulip vlj (Feb 22 2020 at 16:36):

@Kazuhiko Sakaguchi it works ! thanks

view this post on Zulip vlj (Feb 22 2020 at 17:13):

it works really well

view this post on Zulip Kazuhiko Sakaguchi (Feb 23 2020 at 11:54):

@vlj Good! If you see any bugs or possible improvements please let me know.

view this post on Zulip Karl Palmskog (Feb 25 2020 at 16:17):

@Kazuhiko Sakaguchi do you have plans to include that zify code in MathComp itself? Or should we copy it into other projects for now?

view this post on Zulip Karl Palmskog (Feb 25 2020 at 16:19):

by the way, there is an absolute path definition in the _CoqProject file in the repo that should probably be removed

view this post on Zulip Kazuhiko Sakaguchi (Feb 25 2020 at 23:47):

@Karl Palmskog I think it would be nice to integrate that repository to the MathComp organization, but not in MathComp itself. Since the extensible zify tactic will be generalized hopefully in Coq 8.12 (see coq/coq#10982), I prefer to wait until that change.

view this post on Zulip Kazuhiko Sakaguchi (Feb 25 2020 at 23:47):

Also, sure, I will remove that.

view this post on Zulip vlj (Feb 26 2020 at 07:12):

Generalised in which way ?

view this post on Zulip Karl Palmskog (Feb 26 2020 at 20:42):

@Kazuhiko Sakaguchi thanks! I tried porting some stuff from omega to zify+lia, but there were some silly failures that required workarounds, for example: https://github.com/coq-community/reglang/blob/shepherdson-zify/theories/shepherdson.v#L212

view this post on Zulip Karl Palmskog (Feb 26 2020 at 20:44):

specifically:

by move: (size x) (size z) Hk => n n0; lia. (* works, nats are "fresh variables", but why necessary? *)
by lia. (* won't work, no witness *)

view this post on Zulip Karl Palmskog (Feb 26 2020 at 20:45):

I wonder if this is due to zify or lia...

view this post on Zulip Karl Palmskog (Feb 26 2020 at 20:51):

ah, I also noticed that zify-nat and zify-ssrint, etc., should probably live in different files, so I don't need the whole mathcomp when my project only uses all_ssreflect and needs zify

view this post on Zulip Karl Palmskog (Feb 26 2020 at 20:59):

in any case, this was handy on 8.11, but apparently doesn't work at all on master

view this post on Zulip Kazuhiko Sakaguchi (Feb 27 2020 at 13:58):

@Karl Palmskog I guess that your move: ... => ... stuff unifies syntactically different but convertible terms of size x into one variable, but lia may not work in that way in the current implementation.

view this post on Zulip Kazuhiko Sakaguchi (Feb 27 2020 at 14:02):

For example, @size (GRing.Ring.sort int_ringType) x and @size int x where x : seq int are convertible but not syntactically equal.

view this post on Zulip Kazuhiko Sakaguchi (Feb 27 2020 at 14:04):

Also, thank you for suggestions.

view this post on Zulip Kazuhiko Sakaguchi (Feb 27 2020 at 15:02):

Now it works but only with the master branches of Coq and MathComp. The coq-8.11 branch is compatible with Coq 8.11 and MathComp 1.10.0 (and also previous versions maybe).

view this post on Zulip Kazuhiko Sakaguchi (Feb 27 2020 at 15:32):

Since instances for ssreflect.div are constructed using instances for ssralg.intdiv now, splitting requires some more work.

view this post on Zulip Valentin Robert (Feb 28 2020 at 13:14):

how do you use this notation Notation "@ 'sval'" := (@proj1_sig) (at level 10, format "@ 'sval'").? Isn't @ conflicting with the explicit annotation?

view this post on Zulip Paolo Giarrusso (Feb 28 2020 at 13:23):

Probably I miss something, but if that's an ssreflect notation, to apply it to e.g. arg what should work is just @ sval arg. Does that fail instead? (Not sure what's the "explicit annotation" either)

view this post on Zulip Valentin Robert (Feb 28 2020 at 13:48):

oh right, I was ignoring the single quotes around sval, I was reading this incorrectly

view this post on Zulip Valentin Robert (Feb 28 2020 at 13:48):

thanks

view this post on Zulip Valentin Robert (Feb 28 2020 at 14:54):

any clever way of specializing the top assumption? over move => A. move : (A arg).

view this post on Zulip Kazuhiko Sakaguchi (Feb 28 2020 at 19:34):

@Valentin Robert move/(_ arg).

view this post on Zulip vlj (Feb 29 2020 at 22:36):

btw what zify stands for ? Is it Z-ify, like "transforming into Z" ?

view this post on Zulip Paolo Giarrusso (Feb 29 2020 at 22:39):

Think so (https://coq.github.io/doc/master/refman/addendum/micromega.html#zify-pre-processing-of-arithmetic-goals)

view this post on Zulip Paolo Giarrusso (Feb 29 2020 at 22:39):

CommandShow Zify InjTyp
This command shows the list of types that can be injected into Z

view this post on Zulip Valentin Robert (Mar 01 2020 at 09:27):

yeah, I pronounce it "zed-ify"

view this post on Zulip Valentin Robert (Mar 01 2020 at 18:07):

I seem to recall a n-ary function abstraction, possibly in ssreflect, but I can't find it

view this post on Zulip vlj (Mar 01 2020 at 20:43):

RingType doesn't have a \max_ implementation ?

view this post on Zulip vlj (Mar 01 2020 at 20:46):

With the following snippet :

  Section MaxPool.
    Local Open Scope big_scope.
    Local Open Scope order_scope.
    Local Open Scope ring_scope.
    Definition IMG:= int -> int -> int.
    Definition maxpool (input:IMG) : IMG :=
      fun x => fun y => \max_(i < 2) \max_(j<2) (input i j).

I have an error, likely a missing canonical struct, The term "input i j" has type "int" while it is expected to have type "Order.DistrLattice.sort ?T2". but I find it strange that ssrint doesn't have such canonical struct

view this post on Zulip vlj (Mar 01 2020 at 20:47):

and there are is a comRing_distrLatticeType definition in ssrnum, which is canonical

view this post on Zulip Karl Palmskog (Mar 01 2020 at 21:59):

is there any SHA of odd-order that's compatible with MC 1.10? More generally, are there any plans for doing releases/tags of odd-order? We are using it for proof engineering research, and digging among SHAs can be quite a hassle....

view this post on Zulip Karl Palmskog (Mar 04 2020 at 16:07):

solved by https://github.com/coq/opam-coq-archive/pull/1185 - many thanks to Yves!

view this post on Zulip Kazuhiko Sakaguchi (Mar 04 2020 at 21:47):

@vlj I think that the \max notation requires the smallest element which int doesn't have. For non-negative numbers, posnum.v of MathComp Analysis might be useful to write this kind of expression.

view this post on Zulip vlj (Mar 05 2020 at 18:54):

Ho

view this post on Zulip vlj (Mar 05 2020 at 18:56):

So I need to define "another max" in ssrint ?

view this post on Zulip vlj (Mar 05 2020 at 18:57):

Btw ringType also doesn't necessarily have a min element so there is no max defined in R as well ?

view this post on Zulip vlj (Mar 08 2020 at 16:45):

it would be nice to have a "bigop like" that's defined for set with at least one element, sometimes there is no "neutral" element like 0 or 1

view this post on Zulip Pierre-Yves Strub (Mar 09 2020 at 11:53):

Hi. What is the notation for accessing the 0 of the dual lattice of a lattice L.

view this post on Zulip Pierre-Yves Strub (Mar 09 2020 at 11:53):

I tried (0 : L^c), but this is not working.

view this post on Zulip Pierre-Yves Strub (Mar 09 2020 at 11:53):

Goal (0 : L^c) = (0 : L).
Proof. by []. Qed.

view this post on Zulip Kazuhiko Sakaguchi (Mar 09 2020 at 12:15):

@Pierre-Yves Strub That has been changed to ^d.

view this post on Zulip Pierre-Yves Strub (Mar 09 2020 at 12:21):

Yes, sure. But is 0^d is going to be 1?

view this post on Zulip Cyril Cohen (Mar 09 2020 at 12:22):

@Pierre-Yves Strub it should be the case

view this post on Zulip Kazuhiko Sakaguchi (Mar 09 2020 at 12:23):

Yes.

view this post on Zulip Pierre-Yves Strub (Mar 09 2020 at 12:23):

Yes, this is why I ask. Because (0 : L^c) should also be 1. I am going to check.

view this post on Zulip Pierre-Yves Strub (Mar 09 2020 at 12:37):

Oh, I think that ^c was interpreted in the ring scope.

view this post on Zulip Cyril Cohen (Mar 09 2020 at 12:40):

Oh yes... that is why I eventually changed it to ^d

view this post on Zulip Cyril Cohen (Mar 09 2020 at 12:40):

Actually I think ^c is in the type_scope and was all the more conflicting with the one in order.v

view this post on Zulip Pierre-Yves Strub (Mar 09 2020 at 12:40):

Ok. Fixed. I was getting mad :)

view this post on Zulip Cyril Cohen (Mar 09 2020 at 12:41):

well spotted

view this post on Zulip Karl Palmskog (Mar 09 2020 at 14:43):

what does the "TI" actually stand for in lemmas such as cardMg_TI, partition_normedTI, im_sdpair_TI? Do all the "TI"s mean the same?

view this post on Zulip Karl Palmskog (Mar 09 2020 at 15:16):

ah, "Trivial Intersection" it seems

view this post on Zulip Karl Palmskog (Apr 17 2020 at 21:56):

IJCAR preprint on MathComp lemma naming using deep learning is out: https://arxiv.org/abs/2004.07761 (special thanks to Anton for help with eval on FCSL PCM, to Cyril for help with building our corpus, and to Emilio for SerAPI help and hacking)

view this post on Zulip Cyril Cohen (Apr 18 2020 at 11:47):

@Karl Palmskog hi, thanks for sharing, I would love to try it out! however, the link in the paper https://github.com/EngineeringSoftware/roosterize is broken

view this post on Zulip vlj (Apr 18 2020 at 12:25):

I'd like to test too

view this post on Zulip Karl Palmskog (Apr 18 2020 at 14:03):

as soon as we've handed in the camera ready, we'll work on getting all the components out, hopefully beginning of next week

view this post on Zulip Karl Palmskog (Apr 18 2020 at 14:07):

we wanted to refer to the arXiv version in the camera ready, so that's why it was a little bit early

view this post on Zulip Karl Palmskog (Apr 18 2020 at 14:23):

in any case, be aware that we will initially only support 8.10.2 (trained on MC 1.9.0), hopefully more up-to-date support will happen later

view this post on Zulip Cyril Cohen (Apr 20 2020 at 12:21):

HI /@all, last July https://github.com/math-comp/math-comp/wiki/Agenda-of-the-July-1st-2019-documentation-meeting-9h30-to-12h30#decisions we had taken the decision to migrate to zulip. This plan had been paused for a while, but now we are going to open a zulip chat for Coq, so math-comp will have one or many streams there. The data of the public mathcomp gitter rooms will be exported there.

view this post on Zulip Karl Palmskog (Apr 20 2020 at 12:26):

@Cyril Cohen so what is the planned date (or general timeframe)?

view this post on Zulip Cyril Cohen (Apr 20 2020 at 12:26):

this week I think

view this post on Zulip Karl Palmskog (Apr 20 2020 at 12:28):

OK, I see. It's great that Coq+MC has the same Zulip, and I guess the intention is also to welcome other Coq-related subprojects?

view this post on Zulip Karl Palmskog (Apr 20 2020 at 12:28):

(that do not already have something else)

view this post on Zulip Karl Palmskog (Apr 20 2020 at 12:29):

the main dilemma I see is between what goes on Discourse vs. what goes on Zulip

view this post on Zulip Bas Spitters (Apr 21 2020 at 07:39):

@Cyril Cohen For HoTT we got an academic (=free) license. You'll probably be able to get the same for Coq.
Is there any way in which the several zullips can play nicely? E.g. if a hott, or lean, discussion is relevant to coq is there an easy way to tag?

view this post on Zulip Bas Spitters (Apr 21 2020 at 12:32):

Is there a theory of semi-lattices in math-comp. It seems to be missing here:
https://github.com/math-comp/math-comp/blob/master/mathcomp/ssreflect/order.v

view this post on Zulip Cyril Cohen (Apr 21 2020 at 12:33):

Bas Spitters Bas Spitters 14:32
Is there a theory of semi-lattices in math-comp. It seems to be missing here:
https://github.com/math-comp/math-comp/blob/master/mathcomp/ssreflect/order.v

https://github.com/math-comp/math-comp/pull/464

view this post on Zulip Cyril Cohen (Apr 21 2020 at 12:34):

Bas Spitters Bas Spitters 09:39
Cyril Cohen For HoTT we got an academic (=free) license. You'll probably be able to get the same for Coq.
Is there any way in which the several zullips can play nicely? E.g. if a hott, or lean, discussion is relevant to coq is there an easy way to tag?

Zulipchat support indeed agreed to provide a free chatroom for coq. I do not know about zulip cross-interaction

view this post on Zulip Bas Spitters (Apr 21 2020 at 12:34):

Thanks!

view this post on Zulip Karl Palmskog (Apr 22 2020 at 07:55):

based on the relatively small sizes of our communities (compared to, say, big mainstream software projects), I think a joint Lean + Coq + MC + HoTT Zulip would be good for extending the reach and impact, but for internal-practical reasons it's probably not going to work out

view this post on Zulip Karl Palmskog (Apr 22 2020 at 07:56):

I also haven't been able to find anything about inter-instance communication in Zulip

view this post on Zulip Kenji Maillard (Apr 22 2020 at 14:00):

Hello! I was wondering if there was an idiomatic way to do the following in ssreflect: suppose I have a pattern pat selecting a subterm of the goal and I want to substitute pat by a term t and have an additional proof obligation that pat = t. I can do that with a combination of set, enough and rewritebut I was wondering if there is a way that does not require to name the subterm pat...

view this post on Zulip Kazuhiko Sakaguchi (Apr 22 2020 at 14:03):

@Kenji Maillard rewrite [pat](_ : _ = t) ?

view this post on Zulip Kazuhiko Sakaguchi (Apr 22 2020 at 14:04):

But if pat is in pat', it does not work I think.

view this post on Zulip Kenji Maillard (Apr 22 2020 at 14:06):

@Kazuhiko Sakaguchi works exactly as I wanted thanks a lot !

view this post on Zulip Kazuhiko Sakaguchi (Apr 22 2020 at 14:11):

:+1:


Last updated: Feb 08 2023 at 04:04 UTC