## Stream: math-comp users

### Topic: imported from gitter room math-comp/Lobby

Hello everybody!

#### Anton Trunov (Dec 11 2018 at 18:21):

Hi! Thanks for creating the channel!

Hi!

#### 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?)

#### Anton Trunov (Dec 11 2018 at 18:25):

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

Hi all! :)

Hi all!

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

Hi There ! :-)

#### 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?

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

#### 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]

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

#### Emilio Jesús Gallego Arias (Dec 12 2018 at 20:58):

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

#### Karl Palmskog (Dec 12 2018 at 21:40):

and lia et al. actually work with ssrnat?

#### 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"

#### Emilio Jesús Gallego Arias (Dec 12 2018 at 22:07):

or maybe it was Frederic Besson?

#### Emilio Jesús Gallego Arias (Dec 12 2018 at 22:08):

I don't recall now

#### Emilio Jesús Gallego Arias (Dec 12 2018 at 22:08):

but there was work toward making things work

#### Karl Palmskog (Dec 12 2018 at 22:11):

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

#### Karl Palmskog (Dec 12 2018 at 22:15):

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

yup is a pity

#### Emilio Jesús Gallego Arias (Dec 12 2018 at 23:22):

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

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

#### Karl Palmskog (Dec 13 2018 at 00:13):

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

#### Karl Palmskog (Dec 13 2018 at 00:14):

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

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

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

#### 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?)

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

OK thanks

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

#### Emilio Jesús Gallego Arias (Dec 13 2018 at 01:33):

as to avoid having N copies of it floating around

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

#### Karl Palmskog (Dec 13 2018 at 01:36):

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

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

#### Reynald Affeldt (Dec 13 2018 at 02:02):

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

#### Laurent Théry (Gitter import) (Dec 13 2018 at 09:06):

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

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

#### 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?

+1 :-)

#### Maxime Dénès (Dec 13 2018 at 12:32):

sounds like a great idea

#### Cyril Cohen (Dec 13 2018 at 13:08):

The idea is @Enrico Tassi'

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

+1 for workshop

#### Reynald Affeldt (Dec 14 2018 at 05:59):

no risk of conflict with the Coq workshop?

#### Cyril Cohen (Dec 14 2018 at 09:14):

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

#### Reynald Affeldt (Dec 14 2018 at 12:09):

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

#### 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?

#### Karl Palmskog (Dec 14 2018 at 21:32):

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

#### 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 (?)

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

#### 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"

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

#### Karl Palmskog (Dec 15 2018 at 18:36):

not sure mathcomp has a policy here?

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

#### 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?

#### Karl Palmskog (Dec 18 2018 at 23:39):

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

#### Cyril Cohen (Dec 18 2018 at 23:39):

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

#### Cyril Cohen (Dec 18 2018 at 23:40):

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

I see, thanks

#### Cyril Cohen (Dec 18 2018 at 23:40):

I often use From mathcomp Require Import all_ssreflect.

#### Karl Palmskog (Dec 18 2018 at 23:41):

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

#### Karl Palmskog (Dec 18 2018 at 23:41):

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

yes indeed

:thumbsup:

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

#### 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?

#### Karl Palmskog (Dec 19 2018 at 18:05):

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

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

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

#### 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")

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

#### 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/

#### Emilio Jesús Gallego Arias (Dec 20 2018 at 18:13):

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

for self study

#### Emilio Jesús Gallego Arias (Dec 20 2018 at 18:13):

starting in fact from 4 color to 1.6

#### Emilio Jesús Gallego Arias (Dec 20 2018 at 18:13):

I should publish it somehwere

#### Emilio Jesús Gallego Arias (Dec 20 2018 at 18:14):

let me know if you need a copy

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

#### Emilio Jesús Gallego Arias (Dec 20 2018 at 20:08):

Yeah I should ask the devs first tho

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

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

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

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

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

#### Karl Palmskog (Jan 18 2019 at 19:06):

@Enrico Tassi great, hopefully we can sync during CoqPL

#### 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?

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

#### 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?

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

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

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

#### Karl Palmskog (Jan 28 2019 at 14:02):

that seems like something a bit orthogonal to CoqEAL in itself

#### 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"

#### Karl Palmskog (Jan 28 2019 at 14:03):

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

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

#### Karl Palmskog (Jan 28 2019 at 14:05):

so I short-circuited that out with an extraction directive

#### Karl Palmskog (Jan 28 2019 at 14:06):

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

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

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

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

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

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

#### Cyril Cohen (Jan 28 2019 at 15:13):

@Assia Mahboubi, I agree

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

#### 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?

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

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

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

#### Emilio Jesús Gallego Arias (Jan 29 2019 at 18:59):

so count with me to help in improving this

#### Pierre-Yves Strub (Jan 30 2019 at 12:51):

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

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

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

#### Karl Palmskog (Feb 07 2019 at 16:24):

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

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

#### 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?

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

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

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

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

#### Karl Palmskog (Mar 25 2019 at 17:42):

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

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

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

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

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

#### Karl Palmskog (Mar 25 2019 at 18:12):

hmm, that should be possible to improve further

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

#### Karl Palmskog (Mar 25 2019 at 19:07):

could be written in the seqworld using foldl

#### Karl Palmskog (Mar 25 2019 at 19:19):

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

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

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

#### Karl Palmskog (Mar 25 2019 at 19:23):

yeah that was just an experiment

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

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

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

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

#### Karl Palmskog (Mar 25 2019 at 19:34):

gave 10-30% speedups for sparse graphs

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

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

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


#### 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?

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

#### Karl Palmskog (Mar 27 2019 at 18:58):

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

#### Karl Palmskog (Mar 27 2019 at 18:59):

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

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

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

#### Karl Palmskog (Mar 28 2019 at 21:01):

but I guess for some algorithms it may work out

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

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

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

#### Karl Palmskog (Apr 01 2019 at 15:16):

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

#### 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/

#### Karl Palmskog (Apr 03 2019 at 04:15):

(followup to this apparently controversial 1993 article)

#### 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?

#### 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?

no

#### Assia Mahboubi (May 22 2019 at 11:50):

at least, I do not think so.

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

#### Enrico Tassi (May 22 2019 at 11:56):

well, me neither ;-) sorry

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

#### Kazuhiko Sakaguchi (May 22 2019 at 12:01):

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

#### Assia Mahboubi (May 22 2019 at 12:02):

Hello. mathcomp-1.8.

#### Kazuhiko Sakaguchi (May 22 2019 at 12:13):

Is homo_mono_in or ltr_hornerW undefined?

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

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

#### Assia Mahboubi (May 22 2019 at 12:26):

did you manage to compile polyrcf?

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

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

Many thanks!

#### Assia Mahboubi (May 22 2019 at 12:48):

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

#### Assia Mahboubi (May 22 2019 at 12:48):

But other files need fix.

I continue.

#### Kazuhiko Sakaguchi (May 22 2019 at 12:49):

Is this problem introduced by coq/coq#9995?

OK.

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

#### Assia Mahboubi (May 22 2019 at 12:53):

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

#### Assia Mahboubi (May 22 2019 at 13:01):

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

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

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

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

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

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

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

ah, good to know

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

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

#### Kazuhiko Sakaguchi (May 27 2019 at 08:35):

Now I see. Thanks.

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

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

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


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

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

#### Anton Trunov (Jun 05 2019 at 08:52):

@Karl Palmskog Does toychain work with MC1.9.0?

#### Karl Palmskog (Jun 05 2019 at 08:52):

oh right, I should check

#### Karl Palmskog (Jun 05 2019 at 08:53):

if not I guess I should port

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

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

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

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

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

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

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

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

#### Karl Palmskog (Jun 05 2019 at 09:02):

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

#### Karl Palmskog (Jun 05 2019 at 09:04):

ah ok I missed the link

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

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

#### Emilio Jesús Gallego Arias (Jun 05 2019 at 10:05):

however it misses some lemmas

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

#### 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?

#### Emilio Jesús Gallego Arias (Jun 05 2019 at 10:20):

I can do that next week

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

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

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

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

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

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

#### 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 :(

oh, let fix that

thanks!

#### Anton Trunov (Jun 05 2019 at 10:40):

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

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

#### Karl Palmskog (Jun 06 2019 at 08:06):

thanks @Pierre-Yves Strub for merging!

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

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

#### Kazuhiko Sakaguchi (Jun 07 2019 at 08:27):

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

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

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

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

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

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

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

#### Cyril Cohen (Jun 19 2019 at 19:53):

@Karl Palmskog thanks

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

#### 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?

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


#### 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?

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

#### Erik Martin-Dorel (Jun 25 2019 at 09:20):

@Cyril Cohen OK thanks

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

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

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

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

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

:thumbsup:

#### Cyril Cohen (Jul 01 2019 at 14:44):

Dear math-comp users and developpers. Tomorrow I will migrate all math-comp channels to 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

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

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

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

#### Karl Palmskog (Jul 01 2019 at 15:20):

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

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

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

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

#### Karl Palmskog (Jul 01 2019 at 15:27):

yeah the cognitive load was just terrible after a while

#### Karl Palmskog (Jul 01 2019 at 15:28):

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

#### Anton Trunov (Jul 01 2019 at 15:28):

you mean channels, right?

#### Karl Palmskog (Jul 01 2019 at 15:28):

whatever terminology they use

#### Anton Trunov (Jul 01 2019 at 15:29):

a constant headache to choose a Slack channel :)

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

#### Karl Palmskog (Jul 01 2019 at 15:30):

that's basically Zulip

streams

#### Karl Palmskog (Jul 01 2019 at 15:32):

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

#### Karl Palmskog (Jul 01 2019 at 15:32):

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

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

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

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

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

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

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

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

#### Karl Palmskog (Jul 02 2019 at 17:19):

I agree that MathComp Discourse could make a lot of sense

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

#### Karl Palmskog (Jul 02 2019 at 17:22):

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

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

#### 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?

#### Karl Palmskog (Jul 02 2019 at 21:00):

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

#### Karl Palmskog (Jul 02 2019 at 21:00):

ask Theo to create a MathComp/SSReflect category

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

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

#### Cyril Cohen (Jul 02 2019 at 21:15):

ask Theo to create a MathComp/SSReflect category

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

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

#### Karl Palmskog (Jul 02 2019 at 21:21):

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

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

#### Karl Palmskog (Jul 02 2019 at 21:22):

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

#### 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 ?

#### Cyril Cohen (Jul 02 2019 at 21:25):

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

OK, understood

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

#### Karl Palmskog (Jul 02 2019 at 22:25):

StackOverflow has searchability but still terrible for new users IMO

#### 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"

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

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

#### Anton Trunov (Jul 03 2019 at 07:13):

CC @Karl Palmskog

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

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

#### 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?

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

#### 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?

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

#### Reynald Affeldt (Jul 03 2019 at 12:19):

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

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

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

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

#### Karl Palmskog (Jul 03 2019 at 12:40):

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

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

#### Reynald Affeldt (Jul 03 2019 at 12:50):

@Anton Trunov I agree that tags would be nice.

#### Assia Mahboubi (Jul 03 2019 at 13:30):

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

#### 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?

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

#### 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 :-/

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

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

#### Reynald Affeldt (Jul 03 2019 at 13:39):

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

#### Anton Trunov (Jul 03 2019 at 13:40):

Like keywords for papers (I guess).

Yes, this is what I meant.

#### Anton Trunov (Jul 03 2019 at 13:40):

Or authors can just submit PRs to the website repostitory

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

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

#### Reynald Affeldt (Jul 03 2019 at 13:46):

again a good idea!

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

#### Anton Trunov (Jul 03 2019 at 13:52):

and thank you @affeldt-aist :)

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

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

#### Assia Mahboubi (Jul 03 2019 at 14:00):

I will, thanks again.

#### Pierre-Yves Strub (Jul 03 2019 at 14:05):

I also do like Anton's suggestion.

#### Assia Mahboubi (Jul 03 2019 at 14:09):

Cool! Thanks for the feedback!

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

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

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

#### 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)?

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

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

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

#### 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?

#### Assia Mahboubi (Jul 03 2019 at 16:17):

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

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

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

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

#### Karl Palmskog (Jul 03 2019 at 16:39):

yeah it would definitely have to live under coq-community

#### Karl Palmskog (Jul 03 2019 at 16:40):

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

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

#### Karl Palmskog (Jul 03 2019 at 16:42):

for example, this is what one should not have

#### Karl Palmskog (Jul 03 2019 at 16:42):

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

#### Karl Palmskog (Jul 03 2019 at 16:42):

links almost completely devoid of information

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

#### Karl Palmskog (Jul 03 2019 at 16:47):

right, there are just too many limitations with flat lists

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

#### Anton Trunov (Jul 03 2019 at 16:47):

oh, that’s a great idea

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

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

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

#### Karl Palmskog (Jul 03 2019 at 16:56):

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

#### Karl Palmskog (Jul 03 2019 at 16:56):

not that one shouldn't look at stars

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

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

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

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

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

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

#### Karl Palmskog (Jul 03 2019 at 17:07):

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

sure!

#### Karl Palmskog (Jul 03 2019 at 17:07):

can at least contribute my current MathComp list

#### Anton Trunov (Jul 03 2019 at 17:07):

that would be awesome!

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

#### Anton Trunov (Jul 03 2019 at 17:18):

thanks for the pointer, that seems like a good start

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

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

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

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

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

#### 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?

#### Karl Palmskog (Jul 04 2019 at 16:42):

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

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

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

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

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

#### Reynald Affeldt (Aug 05 2019 at 13:13):

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

:thumbsup:

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

#### Karl Palmskog (Aug 13 2019 at 20:20):

does anyone know what purpose it serves, if any?

#### Karl Palmskog (Aug 13 2019 at 20:20):

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

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

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

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

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

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

#### 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?

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

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

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

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

#### Pierre-Yves Strub (Sep 11 2019 at 15:26):

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

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

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

#### Anton Trunov (Sep 11 2019 at 19:21):

More suggestive notation for this would be much appreciated :)

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

#### Pierre-Yves Strub (Sep 12 2019 at 13:11):

Too long, too long ! (the name)

#### Cyril Cohen (Sep 12 2019 at 13:11):

And I forgot to clear it :)

#### Cyril Cohen (Sep 12 2019 at 13:12):

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

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

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

#### Anton Trunov (Sep 12 2019 at 13:31):

@Cyril Cohen Sure! it looks fantastic

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

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

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

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

#### Pierre-Yves Strub (Sep 12 2019 at 19:27):

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

#### 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 ?

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

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

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


#### 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?

#### 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/

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

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

#### Anton Trunov (Oct 02 2019 at 05:58):

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

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

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

Great idea!

#### Karl Palmskog (Oct 02 2019 at 07:57):

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

#### Anton Trunov (Oct 02 2019 at 07:57):

Yes, that’s a frequent thing :)

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

#### Anton Trunov (Oct 02 2019 at 08:07):

Feel free to restructure it and edit however you like

#### Anton Trunov (Oct 02 2019 at 08:08):

It lacks examples currently, though

:thumbsup:

#### Karl Palmskog (Oct 02 2019 at 09:52):

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

#### Karl Palmskog (Oct 02 2019 at 09:52):

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

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

#### Karl Palmskog (Oct 02 2019 at 19:52):

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

#### Karl Palmskog (Oct 02 2019 at 19:54):

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

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

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

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

#### Karl Palmskog (Oct 03 2019 at 08:41):

agree 100% with Anton about the warning

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

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




#### Reynald Affeldt (Oct 04 2019 at 11:42):

isn't it pair_eqE from eqtype.v?

yes it is

#### Yves Bertot (Oct 04 2019 at 11:44):

My mistake, then.

#### 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?

yes you can

#### Cyril Cohen (Oct 04 2019 at 12:05):

(=^~pair_eqE)

#### Cyril Cohen (Oct 04 2019 at 12:06):

oops I cannot remember the syntax :laughing:

#### Yves Bertot (Oct 04 2019 at 12:06):

Where would be the def?

ssreflect.v

#### Cyril Cohen (Oct 04 2019 at 12:07):

I found it and corrected it up there

#### Cyril Cohen (Oct 04 2019 at 12:07):

( =^~)

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

oh ok

#### Cyril Cohen (Oct 04 2019 at 12:35):

you need to fold indeed :-/

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

#### Giovanni Mascellani (Gitter import) (Oct 28 2019 at 10:34):

What is the syntax in Coq to compose two functions?

#### Cyril Cohen (Oct 28 2019 at 10:45):

@Giovanni Mascellani f \o g (in mathcomp)

Thank!

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

#### Giovanni Mascellani (Gitter import) (Oct 28 2019 at 11:32):

Maybe it means that the argument is implicit?

#### Cyril Cohen (Oct 28 2019 at 11:45):

@Giovanni Mascellani yes it means the argument is maximally implicit

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

#### 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?

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

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

#### Giovanni Mascellani (Gitter import) (Oct 29 2019 at 11:53):

Oh, I see. Thanks!

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

:thumbsup:

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

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

#### Cyril Cohen (Nov 02 2019 at 13:53):

have a good weekend

#### Bas Spitters (Nov 03 2019 at 20:23):

@Cyril Cohen Thanks!

#### Assia Mahboubi (Nov 04 2019 at 09:55):

@Bas Spitters , thanks for your interest. Do not hesitate to send pull requests directly when relevant.

#### 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?

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

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

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

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

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

#### Florent Hivert (Nov 16 2019 at 09:25):

I created https://github.com/math-comp/math-comp/issues/430 for infinite groups.

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

#### 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"

#### Gabriel Taumaturgo (Gitter import) (Nov 17 2019 at 02:20):

but i'm having problems instantiating a unit.

#### Gabriel Taumaturgo (Gitter import) (Nov 19 2019 at 06:05):

Another question, is fermat's little theorem defined for ordinals?

#### 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 :(

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

#### Valentin Robert (Nov 22 2019 at 20:44):

ah, that was exactly my problem, getting rid of the proofs, thanks!

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


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

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

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

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

ah

#### Karl Palmskog (Nov 25 2019 at 15:10):

so is there any general heuristics for fixing ambiguous-paths warnings?

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

#### Kenji Maillard (Nov 29 2019 at 17:32):

mathcomp.github.io instead of math-comp.github.io

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


#### Reynald Affeldt (Nov 30 2019 at 10:03):

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.


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

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

#### Reynald Affeldt (Nov 30 2019 at 13:44):

maybe I added this Import GRing.Theory.

#### Reynald Affeldt (Nov 30 2019 at 13:46):

Locate exprDn_char could have given you this information

#### Gabriel Taumaturgo (Gitter import) (Nov 30 2019 at 15:58):

With this import the proof worked.

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

#### Gabriel Taumaturgo (Gitter import) (Nov 30 2019 at 15:59):

And thank you again! @affeldt-aist

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

#### 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?

#### 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?

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

#### 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/

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

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

#### 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?

#### 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?

#### 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?

#### 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 ;-) )

#### Kazuhiko Sakaguchi (Dec 04 2019 at 08:57):

@affeldt_aist I think, you may use eqP rather than eqVneq.

#### Kazuhiko Sakaguchi (Dec 04 2019 at 08:58):

Also using ecast might be better for readability.

#### Reynald Affeldt (Dec 04 2019 at 08:59):

thanks, I try working around this idea

#### Reynald Affeldt (Dec 04 2019 at 09:03):

so much for readability ;-)

#### Reynald Affeldt (Dec 04 2019 at 09:44):

anyway that exactly answers my problem, many thanks!

(:thumbsup:)

#### Valentin Robert (Dec 05 2019 at 23:31):

huh, I'm still struggling with eliminating vectors of known size without losing information

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

#### Valentin Robert (Dec 05 2019 at 23:34):

well, I guess I can do the ubnPeq trick

#### 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 *)


#### Emilio Jesús Gallego Arias (Dec 05 2019 at 23:53):

@Valentin Robert that's the Vector.t from the standard library?

yes

#### Emilio Jesús Gallego Arias (Dec 05 2019 at 23:53):

If so advice is just not to use it

#### Emilio Jesús Gallego Arias (Dec 05 2019 at 23:55):

you could make it usable but it will be a lot of work

what's ubnPeq ?

#### Emilio Jesús Gallego Arias (Dec 05 2019 at 23:56):

ah, the new lemma

#### Valentin Robert (Dec 05 2019 at 23:58):

so I should use the sequence type from mathcomp instead?

#### 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?

#### Valentin Robert (Dec 05 2019 at 23:59):

yeah this works, it's just kind of tedious to write

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


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

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

#### Emilio Jesús Gallego Arias (Dec 06 2019 at 00:05):

or use the recursion principle

#### 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 _)))).


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

#### Valentin Robert (Dec 06 2019 at 00:10):

it'll scale better when I want to deal with 32-bit vectors :)

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

#### Valentin Robert (Dec 06 2019 at 17:07):

does mathcomp have length-indexed lists? I see vector refers to the geometric notion

#### Reynald Affeldt (Dec 06 2019 at 17:22):

n.-tuple A in the file tuple.v

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

oh right

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


#### Karl Palmskog (Dec 07 2019 at 19:32):

does anyone know what's going on? Non-dev versions work fine in Nix

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

#### 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?

#### Valentin Robert (Dec 10 2019 at 00:21):

hmm nevermind, I don't need this proof...

#### 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?

#### 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?

#### Valentin Robert (Dec 13 2019 at 01:09):

I managed to simplify it a bit by exploiting set_nth_default...

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


thanks!

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

#### 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?

#### Karl Palmskog (Dec 13 2019 at 11:12):

we need this for CI in some projects, both locally and in Coq-Community

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

#### Assia Mahboubi (Dec 13 2019 at 11:55):

@Enrico Tassi @Yves Bertot any opinion?

#### 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?

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

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

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

#### 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?

#### Emilio Jesús Gallego Arias (Dec 13 2019 at 18:11):

I'd use rewrite (ltnW H).

thanks Emilio!

#### 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 ?

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


#### Assia Mahboubi (Dec 16 2019 at 09:33):

@Florent Hivert can you also provide the term whose type-checking raises the error?

#### 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 ?

#### Pierre-Yves Strub (Dec 16 2019 at 09:53):

Yes: Check (0 0). But it is not possible to type-check it :)

#### Florent Hivert (Dec 16 2019 at 09:56):

Is that what you want:

Check [ringMixin of {series R} by <-].


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

#### 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_rmorphism := RMorphism bond_is_rmorphism.


#### Florent Hivert (Dec 16 2019 at 10:16):

I'm suspecting, that the second canonical bond_rmorphism is not used at all.

#### Florent Hivert (Dec 16 2019 at 13:40):

Found the solution ! I'm not sure what is really happening but it now works !

#### Reynald Affeldt (Dec 16 2019 at 13:41):

please share the magical incantation ! :-)

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

#### 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 !!!

#### Assia Mahboubi (Dec 18 2019 at 08:57):

@Florent Hivert I did not know this command either... Thanks! :)

#### 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 !

#### Assia Mahboubi (Dec 18 2019 at 19:58):

With pen and paper...

#### 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 ?

#### Florent Hivert (Dec 18 2019 at 20:44):

@Assia Mahboubi So you are writing with pen and paper the equivalent of the 17000 lines ! :-)

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

#### 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} ?

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


#### 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) ?

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

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

#### 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 ?

#### Cyril Cohen (Jan 09 2020 at 17:13):

My question is why your goal isn't simply {y : nat | (y < 1)%O}?

#### Cyril Cohen (Jan 09 2020 at 17:14):

otherwise you could first have a proof of A -> exists _ : A, True

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

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

#### Cyril Cohen (Jan 10 2020 at 17:52):

Thanks for spotting this... right now I must say I have no clue why this fails...

#### Cyril Cohen (Jan 10 2020 at 19:09):

and the culprit is: missing canonicals

like... a lot

#### Cyril Cohen (Jan 10 2020 at 19:09):

:laughing: thanks for spotting this

#### 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 ;-)

#### Cyril Cohen (Jan 10 2020 at 19:22):

not too late at all

#### 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 ;-)

#### Cyril Cohen (Jan 10 2020 at 20:17):

should be solved now

#### Florent Hivert (Jan 10 2020 at 23:01):

@Cyril Cohen My code is now working like a charm ! Thanks !

#### Cyril Cohen (Jan 10 2020 at 23:04):

@Florent Hivert I'm glad, thanks!

:+1:

#### Valentin Robert (Jan 21 2020 at 19:36):

what's a ssreflect way of doing essentially pose proof?

#### Karl Palmskog (Jan 21 2020 at 19:43):

uh, have <name> := <term>?

#### 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!

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

#### 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 :\

#### 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?

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

#### Karl Palmskog (Jan 31 2020 at 14:33):

if anyone has something against this, let me know here...

#### Karl Palmskog (Jan 31 2020 at 14:38):

what the heck, finmap-1.3.4 doesn't seem to require coq-mathcomp-bigenough?

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

#### 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?

#### Paolo Giarrusso (Feb 10 2020 at 20:07):

I've seen trouble for suff and have :=, but not elim or case.

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

#### 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 ?

#### vlj (Feb 10 2020 at 21:14):

(posted on coq/coq too)

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

#### Emilio Jesús Gallego Arias (Feb 10 2020 at 21:38):

insub_eq does provide a version of insub that will compute @vlj

#### vlj (Feb 10 2020 at 21:41):

Thanks will try tomorrow

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

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

#### Emilio Jesús Gallego Arias (Feb 11 2020 at 09:51):

Yup I think Cyril's solution is much preferred

#### vlj (Feb 11 2020 at 18:34):

under is an equivalent of refine in standard coq ?

#### Reynald Affeldt (Feb 11 2020 at 18:37):

You are right to see a relation between both

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

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

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

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

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

#### 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?

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

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

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

#### Karl Palmskog (Feb 12 2020 at 16:05):

sure, he should confirm, although I was also interested in this particular answer, thanks

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

#### Karl Palmskog (Feb 13 2020 at 10:11):

@Bas Spitters you probably want to use CoqEAL

#### Karl Palmskog (Feb 13 2020 at 10:12):

it does already provide transport between nat and N if I recall correctly

#### Karl Palmskog (Feb 13 2020 at 10:13):

it would be interesting to provide (non-bidirectional) transport between nat and int63 in CoqEAL

#### Bas Spitters (Feb 13 2020 at 10:13):

Yes, that could be enough. We'll have a look. Too many libraries not communicating ...

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

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

#### Cyril Cohen (Feb 13 2020 at 10:16):

@Karl Palmskog done

#### Karl Palmskog (Feb 13 2020 at 10:17):

:thumbsup: thanks!

and released

#### Cyril Cohen (Feb 13 2020 at 10:18):

I do not have time to prepare the opam packages though

#### Karl Palmskog (Feb 13 2020 at 10:18):

I can do it if you don't mind

#### Cyril Cohen (Feb 13 2020 at 10:18):

I certainly do not mind ;)

#### Karl Palmskog (Feb 13 2020 at 10:19):

hmm, I have to double check, but I think finmap >= 1.4 is required now

#### Karl Palmskog (Feb 13 2020 at 11:01):

indeed this is the case, meaning that also multinomials 1.5 is required

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

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

#### Cyril Cohen (Feb 13 2020 at 12:54):

I can edit that, I screwed up

:thumbsup:

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

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

#### Cyril Cohen (Feb 13 2020 at 13:18):

I do not think these are mature software

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

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

#### Paolo Giarrusso (Feb 13 2020 at 14:07):

I guess projects in the platform could specify their maturity level and guarantees.

#### Paolo Giarrusso (Feb 13 2020 at 14:09):

instead of hoping people guess the right thing.

#### Emilio Jesús Gallego Arias (Feb 13 2020 at 14:10):

Only reasonably mature stuff should be included in the platform IMHO

#### Karl Palmskog (Feb 13 2020 at 17:01):

CoqEAL 1.0.2 and 1.0.3 are now on the Coq OPAM archive

#### vlj (Feb 13 2020 at 20:40):

Platform has different package as opam ?

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

#### Karl Palmskog (Feb 13 2020 at 21:44):

or at least that's one possibility that's been discussed favorably

#### 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? :\

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

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

#### Valentin Robert (Feb 14 2020 at 14:39):

@Paolo G. Giarrusso oh yeah this works much better!

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

#### Valentin Robert (Feb 14 2020 at 14:41):

yeah I've been using pose proof too...

#### Valentin Robert (Feb 14 2020 at 14:41):

guess I'll keep pose proof then :\

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

#### Cyril Cohen (Feb 14 2020 at 14:44):

You can then do have : !! term_with_tc

:D

thanks Cyril!

#### Valentin Robert (Feb 14 2020 at 21:50):

hmm, I still don't quite understand how to do inversion with equations properly

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

#### 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 => ->

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

#### 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 *)


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

#### Paolo Giarrusso (Feb 14 2020 at 23:01):

Coq 8.10 added temporary introductions.

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

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

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

And subst.

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

#### 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!

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

#### vlj (Feb 16 2020 at 12:41):

https://gist.github.com/vlj/863f47cd5a3f55f3ab545a8f1af51830

#### vlj (Feb 16 2020 at 12:41):

No assumption in ((p <= Nat.max p q) = true)

#### vlj (Feb 16 2020 at 12:46):

apparently le is in %R and not in %N...

#### 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 ?

#### 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 ? )

#### Paolo Giarrusso (Feb 16 2020 at 12:53):

@vlj your search uses _ in place of ->

#### vlj (Feb 16 2020 at 12:56):

you mean Search ((_ <= _)%R _ (_ <= _)). ?

#### vlj (Feb 16 2020 at 12:56):

it complains : too many arguments in head search pattern

#### vlj (Feb 16 2020 at 13:03):

ler_nat doesn't work for me

#### 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 -> (_ <= _)).

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

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

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

#### vlj (Feb 17 2020 at 20:33):

https://gist.github.com/vlj/ee3fd2c568cfd976e710a344b302910a

#### Reynald Affeldt (Feb 17 2020 at 21:52):

@vlj by rewrite lerr.

#### vlj (Feb 17 2020 at 22:20):

@affeldt-aist thanks ! how did you find it ?

#### Reynald Affeldt (Feb 17 2020 at 22:29):

I guessed the name.

#### Reynald Affeldt (Feb 17 2020 at 22:30):

The naming of such lemmas is very regular in MathComp and it is worth learning.

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

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

#### Emilio Jesús Gallego Arias (Feb 19 2020 at 20:38):

@vlj for me by rewrite lexUl. does the trick

#### Emilio Jesús Gallego Arias (Feb 19 2020 at 20:49):

the right lemma is leUl not lexUl

Thanks

#### vlj (Feb 19 2020 at 21:32):

it doesn't work for me :/

#### vlj (Feb 19 2020 at 21:33):

The LHS of Order.DistrLatticeTheoryJoin.leUl
(_ <= _ | _)%O
does not match any subterm of the goal


#### vlj (Feb 19 2020 at 21:33):

with the gist it's easier maybe https://gist.github.com/vlj/408daf59ab39c4efae8e66658692dde0

#### vlj (Feb 19 2020 at 21:44):

apparently there is a conflict between Order.le and Num.Def.ler

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

#### Emilio Jesús Gallego Arias (Feb 19 2020 at 21:45):

max is the one from nat

#### Emilio Jesús Gallego Arias (Feb 19 2020 at 21:45):

<= the one from num

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

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

#### Emilio Jesús Gallego Arias (Feb 19 2020 at 21:47):

Proof. by rewrite lez_nat leq_maxl. Qed.

thanks

#### Emilio Jesús Gallego Arias (Feb 19 2020 at 21:48):

you want to open order_scope if you wanna use the _ <= _ from order

#### vlj (Feb 19 2020 at 21:49):

I need to keep the max in nat

why?

#### vlj (Feb 19 2020 at 21:49):

what happen if I open several scope with conflicting definition

#### Emilio Jesús Gallego Arias (Feb 19 2020 at 21:49):

they work as a stack [roughly]

#### Emilio Jesús Gallego Arias (Feb 19 2020 at 21:49):

if you want to keep the max in nat use maxn

and <= from nat

#### Emilio Jesús Gallego Arias (Feb 19 2020 at 21:50):

if you want to see it as a lattice don't

#### Emilio Jesús Gallego Arias (Feb 19 2020 at 21:50):

but don't pick the <= from int

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

ok

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

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

ok

#### vlj (Feb 19 2020 at 21:52):

with x being potentially negative, n being always positive, and i between 0 and n

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

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

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

#### Emilio Jesús Gallego Arias (Feb 19 2020 at 21:57):

you could also move to (n : int) (h_n : 0 <= n)

hard to know

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


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

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

#### vlj (Feb 19 2020 at 22:10):

but for some reason it picks the norm in ring_scope and not the one in ssrint

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

#### vlj (Feb 19 2020 at 22:14):

seems like an issue in parsing

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

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

#### Paolo Giarrusso (Feb 19 2020 at 22:46):

Actually, ahem, you could maybe use tmp, or just force another scope inside the norm:

#### Paolo Giarrusso (Feb 19 2020 at 22:48):

| (x + i....)%distn_scopr%ring_scope |%N


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

#### vlj (Feb 19 2020 at 22:56):

thanks, will give a try

#### Emilio Jesús Gallego Arias (Feb 20 2020 at 03:03):

Why you do  x + i - n - x ? This is just i - n ?

#### Emilio Jesús Gallego Arias (Feb 20 2020 at 03:04):

so you have (n i : int), 0 <= n -> 0 <= i < n -> | i - n |?

#### Emilio Jesús Gallego Arias (Feb 20 2020 at 03:06):

but given that i < n you can rewrite it to use max?

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

#### 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?

#### Valentin Robert (Feb 20 2020 at 13:29):

(I also tried case ? : e. which does not give me an equation...)

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

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

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

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

#### Kazuhiko Sakaguchi (Feb 22 2020 at 12:16):

@vlj https://github.com/pi8027/mczify This should work with Coq 8.11.

#### vlj (Feb 22 2020 at 16:17):

doesn't work with coq 8.0 ?

8.10*

#### vlj (Feb 22 2020 at 16:17):

opam only has 8.10 so far

#### vlj (Feb 22 2020 at 16:36):

@Kazuhiko Sakaguchi it works ! thanks

#### vlj (Feb 22 2020 at 17:13):

it works really well

#### Kazuhiko Sakaguchi (Feb 23 2020 at 11:54):

@vlj Good! If you see any bugs or possible improvements please let me know.

#### 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?

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

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

#### Kazuhiko Sakaguchi (Feb 25 2020 at 23:47):

Also, sure, I will remove that.

#### vlj (Feb 26 2020 at 07:12):

Generalised in which way ?

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

#### 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 *)


#### Karl Palmskog (Feb 26 2020 at 20:45):

I wonder if this is due to zify or lia...

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

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

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

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

#### Kazuhiko Sakaguchi (Feb 27 2020 at 14:04):

Also, thank you for suggestions.

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

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

#### 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?

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

#### Valentin Robert (Feb 28 2020 at 13:48):

oh right, I was ignoring the single quotes around sval, I was reading this incorrectly

thanks

#### Valentin Robert (Feb 28 2020 at 14:54):

any clever way of specializing the top assumption? over move => A. move : (A arg).

#### Kazuhiko Sakaguchi (Feb 28 2020 at 19:34):

@Valentin Robert move/(_ arg).

#### vlj (Feb 29 2020 at 22:36):

btw what zify stands for ? Is it Z-ify, like "transforming into Z" ?

#### Paolo Giarrusso (Feb 29 2020 at 22:39):

CommandShow Zify InjTyp
This command shows the list of types that can be injected into Z

#### Valentin Robert (Mar 01 2020 at 09:27):

yeah, I pronounce it "zed-ify"

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

#### vlj (Mar 01 2020 at 20:43):

RingType doesn't have a \max_ implementation ?

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

#### vlj (Mar 01 2020 at 20:47):

and there are is a comRing_distrLatticeType definition in ssrnum, which is canonical

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

#### Karl Palmskog (Mar 04 2020 at 16:07):

solved by https://github.com/coq/opam-coq-archive/pull/1185 - many thanks to Yves!

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

Ho

#### vlj (Mar 05 2020 at 18:56):

So I need to define "another max" in ssrint ?

#### 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 ?

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

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

#### Pierre-Yves Strub (Mar 09 2020 at 11:53):

I tried (0 : L^c), but this is not working.

#### Pierre-Yves Strub (Mar 09 2020 at 11:53):

Goal (0 : L^c) = (0 : L).
Proof. by []. Qed.


#### Kazuhiko Sakaguchi (Mar 09 2020 at 12:15):

@Pierre-Yves Strub That has been changed to ^d.

#### Pierre-Yves Strub (Mar 09 2020 at 12:21):

Yes, sure. But is 0^d is going to be 1?

#### Cyril Cohen (Mar 09 2020 at 12:22):

@Pierre-Yves Strub it should be the case

Yes.

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

#### Pierre-Yves Strub (Mar 09 2020 at 12:37):

Oh, I think that ^c was interpreted in the ring scope.

#### Cyril Cohen (Mar 09 2020 at 12:40):

Oh yes... that is why I eventually changed it to ^d

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

#### Pierre-Yves Strub (Mar 09 2020 at 12:40):

Ok. Fixed. I was getting mad :)

well spotted

#### 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?

#### Karl Palmskog (Mar 09 2020 at 15:16):

ah, "Trivial Intersection" it seems

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

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

#### vlj (Apr 18 2020 at 12:25):

I'd like to test too

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

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

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

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

#### Karl Palmskog (Apr 20 2020 at 12:26):

@Cyril Cohen so what is the planned date (or general timeframe)?

#### Cyril Cohen (Apr 20 2020 at 12:26):

this week I think

#### 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?

#### Karl Palmskog (Apr 20 2020 at 12:28):

(that do not already have something else)

#### Karl Palmskog (Apr 20 2020 at 12:29):

the main dilemma I see is between what goes on Discourse vs. what goes 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?

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

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

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

Thanks!

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

#### Karl Palmskog (Apr 22 2020 at 07:56):

I also haven't been able to find anything about inter-instance communication in 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...

#### Kazuhiko Sakaguchi (Apr 22 2020 at 14:03):

@Kenji Maillard rewrite [pat](_ : _ = t) ?

#### Kazuhiko Sakaguchi (Apr 22 2020 at 14:04):

But if pat is in pat'`, it does not work I think.

#### Kenji Maillard (Apr 22 2020 at 14:06):

@Kazuhiko Sakaguchi works exactly as I wanted thanks a lot !

#### Kazuhiko Sakaguchi (Apr 22 2020 at 14:11):

:+1:

Last updated: Feb 08 2023 at 04:04 UTC