Hello everybody!

Hi! Thanks for creating the channel!

Hi!

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

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

Hi all! :)

Hi all!

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

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?

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

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]

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

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

and lia et al. actually work with ssrnat?

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

or maybe it was Frederic Besson?

I don't recall now

but there was work toward making things work

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

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

yup is a pity

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

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

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

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

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

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

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

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

OK thanks

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

as to avoid having N copies of it floating around

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

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

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

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

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

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.

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

+1 :-)

sounds like a great idea

The idea is @Enrico Tassi'

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

no risk of conflict with the Coq workshop?

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

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

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

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

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

@Erik Martin-Dorel it seems quite strange that the package in`released`

should be compatible with `dev`

- it could be taken as a guarantee that 1.7.0 should work with `master`

in perpetuity

also is a bit disconcerting that packages in `released`

implicitly have ties to `core-dev`

, which is arguably "experts only"

I think the decision to change `< "8.9~"`

to `< "8.10~"`

in an existing package should be up to every project maintainer

not sure mathcomp has a policy here?

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.

is there any specific rationale for always beginning with `Require Import mathcomp.ssreflect.ssreflect.`

as a separate command?

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

and similar

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

please start with `From mathcomp Require Import [...]`

directly from now on

I see, thanks

I often use `From mathcomp Require Import all_ssreflect.`

and there's no reason to qualify like `From mathcomp.ssreflect Require ...`

, right?

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

yes indeed

:thumbsup:

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.

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

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

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

on the other hand, `finmap`

appeared to be under much higher churn and we were able to get it working easily

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

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.

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

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

for self study

starting in fact from 4 color to 1.6

I should publish it somehwere

let me know if you need a copy

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

Yeah I should ask the devs first tho

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

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.

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`

.

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.

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)

@Enrico Tassi great, hopefully we can sync during CoqPL

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?

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

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?

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)

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

@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

that seems like something a bit orthogonal to CoqEAL in itself

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

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

anywhere

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

so I short-circuited that out with an extraction directive

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

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

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

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

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

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.

@Assia Mahboubi, I agree

@Karl Palmskog I will gladly ask for your help

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 on`Notation bipoly := {poly {poly R}}`

for `R : ringType`

or `R : comRingType`

), anyway option 1. indeed seems a good choice

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?

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

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

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

so count with me to help in improving this

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

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

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

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

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

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

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

@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`

)

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

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

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

if you already have a `rel T`

, not sure how `dfs`

would help over `connect`

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.

yes, the only thing that happens in `connect`

is that you turn a `rel T`

into `T -> seq T`

via `rgraph`

before calling `dfs`

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.

So `let s := dfs (enfa_trans None) #|T| [::] x in [set q | q \in s]`

is better for computation.

hmm, that should be possible to improve further

@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

could be written in the `seq`

world using `foldl`

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

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

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

yeah that was just an experiment

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

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

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

specifically, I ad-hoc-refined `dfs`

to use red-black trees: https://github.com/palmskog/chip/blob/bf75377c2a3b29793f5e0058c752cd6b3c708c48/core/dfs_set.v#L117-L119

gave 10-30% speedups for sparse graphs

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

@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

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

@Karl Palmskog I'm not sure that they are bugs, but replacing them with `Variant`

s (and `Record`

s?) would be a good improvement. Can you send PR to fix it?

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

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

(also, I'll try to report the `Variant`

issues to the mathcomp repo this weekend)

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

my experience has been that one never wants to use the `rel V`

representation of graphs in practice, only the `V -> seq V`

one

but I guess for some algorithms it may work out

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

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

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

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

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/

(followup to this apparently controversial 1993 article)

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?

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

no

at least, I do not think so.

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.

well, me neither ;-) sorry

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.

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

Hello. mathcomp-1.8.

Is `homo_mono_in`

or `ltr_hornerW`

undefined?

They are defined: `ltr_hornerW`

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

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

did you manage to compile polyrcf?

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

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!

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

But other files need fix.

I continue.

Is this problem introduced by coq/coq#9995?

OK.

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.

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

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

@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

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

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

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.

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

@Karl Palmskog I just found `1.10.0`

in Milestones: https://github.com/math-comp/math-comp/milestones

ah, good to know

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.

Should we relocate the changelog file for new changes to `CHANGELOG_UNRELEASED.md`

as like as #210? @Cyril Cohen @Enrico Tassi

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

Now I see. Thanks.

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

@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

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

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

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

@Karl Palmskog Does toychain work with MC1.9.0?

oh right, I should check

if not I guess I should port

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

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

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

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

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

@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

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

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

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

ah ok I missed the link

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

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

however it misses some lemmas

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

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

I can do that next week

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

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

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

@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

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

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

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

oh, let fix that

thanks!

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

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

thanks @Pierre-Yves Strub for merging!

@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

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

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

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

does...

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

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

@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

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

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

@Karl Palmskog thanks

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

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

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

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

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

@Cyril Cohen OK thanks

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

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

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

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

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

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

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

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

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

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

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

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

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

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

yeah the cognitive load was just terrible after a while

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

you mean channels, right?

whatever terminology they use

a constant headache to choose a Slack channel :)

I mean, if you have one channel like `ocaml`

in Slack, then people open 300+ threads in that channel

that's basically Zulip

streams

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

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

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

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.

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

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.

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

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

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.

I agree that MathComp Discourse could make a lot of sense

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

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

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)

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?

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

ask Theo to create a MathComp/SSReflect category

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

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

ask Theo to create a MathComp/SSReflect category

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

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

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

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

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

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 ?

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

OK, understood

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

StackOverflow has searchability but still terrible for new users IMO

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"

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

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.

CC @Karl Palmskog

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.

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.

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

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.

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

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

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

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

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

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.

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

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)

@Anton Trunov I agree that tags would be nice.

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

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?

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

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

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

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

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

Like keywords for papers (I guess).

Yes, this is what I meant.

Or authors can just submit PRs to the website repostitory

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

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

again a good idea!

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.

and thank you @affeldt-aist :)

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

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

I will, thanks again.

I also do like Anton's suggestion.

Cool! Thanks for the feedback!

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

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

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 could it be within the scope of the website to also list/track MathComp-related projects on GitHub (and similar platforms)?

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

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.

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.

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?

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

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.

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.

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

What do people think about this tentative suggestion?

yeah it would definitely have to live under coq-community

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

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

yep, my thinking exactly :)

for example, this is what one should not have

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

links almost completely devoid of information

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.

right, there are just too many limitations with flat lists

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

oh, that’s a great idea

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

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

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.

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

not that one shouldn't look at stars

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

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

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

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

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

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

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

sure!

can at least contribute my current MathComp list

that would be awesome!

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

thanks for the pointer, that seems like a good start

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.

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

@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

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

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)

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

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

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

@affeldt-aist you probably want to enable the `with-test`

clause in your CI, I can submit a PR for that if you want

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.

@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

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

:thumbsup:

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

does anyone know what purpose it serves, if any?

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

?

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

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)

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.

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.

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

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

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 but the bottom line is that the one without newlines in MathComp is the preferred style now?

yes

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

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

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

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

A `grep "[^ ]{}/" **/*.v`

didn't find any similar trick in the whole mathcomp source... So I supposed there where a better trick...

@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

More suggestive notation for this would be much appreciated :)

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

Too long, too long ! (the name)

And I forgot to clear it :)

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

@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

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

@Cyril Cohen Sure! it looks fantastic

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) -> D`

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

`(_ _)`

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)

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:

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

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

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

Anyone using `nix-shell`

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

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

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

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?

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

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

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

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

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

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

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

Great idea!

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

Yes, that’s a frequent thing :)

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

Feel free to restructure it and edit however you like

It lacks examples currently, though

:thumbsup:

arguably one needs machine learning based code completion for `Search`

itself...

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

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

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

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

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

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

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

agree 100% with Anton about the warning

Would it make sense to add theorem with the following statement? I have a use case for it.

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

```
```

isn't it pair_eqE from eqtype.v?

yes it is

My mistake, then.

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

`(=^~pair_eqE)`

oops I cannot remember the syntax :laughing:

Where would be the def?

ssreflect.v

I found it and corrected it up there

( `=^~`

)

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

you need to fold indeed :-/

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

What is the syntax in Coq to compose two functions?

@Giovanni Mascellani `f \o g`

(in mathcomp)

Thank!

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

.

Maybe it means that the argument is implicit?

@Giovanni Mascellani yes it means the argument is maximally implicit

@Giovanni Mascellani That's documented here: https://coq.github.io/doc/master/refman/language/gallina-extensions.html#implicit-argument-binders

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?

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

If `x`

is not maximally inserted, but an implicit argument, then `foo`

is just `@foo`

, but `foo y`

is `@foo _ y`

Oh, I see. Thanks!

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:

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

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

have a good weekend

@Cyril Cohen Thanks!

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

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 yes please add it

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.

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.

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.

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

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.

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

Actually the units i'm trying to work with are finite. These are the units of 'Z_n.+2

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"

but i'm having problems instantiating a unit.

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

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`

:(

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

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

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

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

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)

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

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

so is there any general heuristics for fixing `ambiguous-paths`

warnings?

there is a small issue in the CHANGELOg.md, the link for the mathcomp documentation in the section infrastructure sends to

`mathcomp.github.io`

instead of `math-comp.github.io`

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

what about this?

```
Proof.
move=> a; split.
move=> pn.
rewrite exprDn_char ?EulerFermatPoly //=.
apply/pnatP; first by rewrite prime_gt0.
move=> p pp; rewrite dvdn_prime2 // => /eqP ->.
move: (char_Fp pn).
suff : {rmorphism 'F_n -> {poly 'F_n}} by move/rmorph_char; exact.
exists (fun x => x%:P) => //; eexists.
exact: polyC_sub.
split => //; exact: polyC_mul.
```

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.

Weird. I googled this Lemma and found it on ssralg.v, but I do have all_algebra imported.

maybe I added this `Import GRing.Theory.`

Locate exprDn_char could have given you this information

With this import the proof worked.

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

And thank you again! @affeldt-aist

@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

Okay. The process people usually learn mathcomp is reading the papers? That is how you learned it?

Hi @Gabriel Taumaturgo ! What kind of information would you like to have? mathematical scope of what has been formalized or formalization technique?

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

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

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`

)

(in addition to reading, manually stepping through proof scripts and experimenting with definitions in many projects may also help)

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

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?

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?

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

@affeldt_aist I think, you may use `eqP`

rather than `eqVneq`

.

Also using `ecast`

might be better for readability.

thanks, I try working around this idea

@affeldt-aist See also: https://github.com/math-comp/math-comp/blob/master/mathcomp/ssreflect/finfun.v#L79

so much for readability ;-)

anyway that exactly answers my problem, many thanks!

(:thumbsup:)

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

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

well, I guess I can do the `ubnPeq`

trick

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

@Valentin Robert that's the `Vector.t`

from the standard library?

yes

If so advice is just not to use it

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

what's ubnPeq ?

ah, the new lemma

so I should use the sequence type from mathcomp instead?

anyways I'm not sure I understand the problem there, you can just use `ubnPeq`

again, right?

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

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

Well the do something part is missing, IMO it is a bit hard to understand what the best solution is

in some cases the best strategy can be indeed to map the vector to a list and use a regular fold

or use the recursion principle

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

oh yeah, using the recursion principle to turn into a list is fairly neat, thanks for the idea

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

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

does mathcomp have length-indexed lists? I see `vector`

refers to the geometric notion

n.-tuple A in the file tuple.v

(you may even consider the type of row vectors ‘rv[A]_n from the file matrix.v)

oh right

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

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

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`

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?

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

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?

in particular, is there a way to do something like `val_inj`

to the arguments that `tnth`

receives?

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

...

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

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.

@Assia Mahboubi @Cyril Cohen can I update the relevant MathComp dev OPAM packages to support the 8.11 beta?

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

@Karl Palmskog I do not know why this package is not up to-date, but I think it is ok.

@Enrico Tassi @Yves Bertot any opinion?

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

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

@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

I definitely had missed `rcons_tuple`

because it was in `seq`

and I was looking in `tuple`

, woops...

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?

I'd use `rewrite (ltnW H).`

thanks Emilio!

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 ?

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

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

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

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

Is that what you want:

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

The answer is:

```
[ringMixin of {series R} by <-]
: GRing.Ring.mixin_of (invlim.InvLimitRing.Tinv_zmodType (fps_invlimType R))
where
?i : [R : ringType i : nat j : nat x : (i <= j)%O |- is_true (i <= j)%N]
```

Basically, I don't understand where the obligation `is_true (i <= j)%N`

comes from. I though I've solved all of those.

The culprit is probably:

```
Hypothesis H : n <= m.
Fact trXnt_is_multiplicative : multiplicative (@trXnt m n).
[...]
Canonical trXnt_multiplicative := AddRMorphism trXnt_is_multiplicative.
```

However, I should have provided the obligation with

```
Definition fps_bond := fun (i j : nat) of (i <= j)%O => @trXnt R j i.
Variables (i j : nat) (le_ij : (i <= j)%O).
Lemma bond_is_rmorphism : rmorphism (fps_bond le_ij).
Proof.
split; first exact: trXnt_is_linear.
rewrite /fps_bond; apply trXnt_is_multiplicative.
by rewrite -leEnat. (* HERE HERE HERE *)
Qed.
Canonical bond_additive := Additive bond_is_rmorphism.
Canonical bond_rmorphism := RMorphism bond_is_rmorphism.
```

I'm suspecting, that the second canonical `bond_rmorphism`

is not used at all.

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

please share the magical incantation ! :-)

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.

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

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

@Assia Mahboubi :-) Then it is a big mystery to me how you manage to debug problems with canonicals !

With pen and paper...

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 ?

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

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

@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}`

?

@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
```

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

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.

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

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 ?

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

?

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

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

@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

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

and the culprit is: missing canonicals

like... a lot

:laughing: thanks for spotting this

@Cyril Cohen You are welcome ! It is maybe a little late, but as you see, I'm participating to the review PR #454 ;-)

not too late at all

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

should be solved now

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

@Florent Hivert I'm glad, thanks!

:+1:

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

?

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

?

ah, well anyway, I realized I was immediately rewriting with it so don't need it. but thanks!

@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 `<-`

.

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

@Cyril Cohen do you know offhand which ones of your packages support 8.11.0? Latest finmap at least, right?

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

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

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

?

ah, now it's getting clearer, `mathcomp-analysis`

requires `bigenough`

but doesn't mention it, so that's where it is needed

@Valentin Robert how does the call to case look like? Can that be fixed by passing more parameters explicitly?

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

I have an issue with `ordinal`

and `map`

, I have a function f that takes a `'I_n`

argument, 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
```

the whole oapp/cons things seem to be an explicit seq which should be explicitly mappable to the `\ matrix_(_, _) 1 i j`

function right ?

(posted on coq/coq too)

`by rewrite /test_kernel tmp0 /ord_enum /= !insubT /= !mxE.`

will help you progess here, you want remove the subType proof.

`insub_eq`

does provide a version of `insub`

that will compute @vlj

Thanks will try tomorrow

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

or the new `by under eq_bigr => i do rewrite mxE; rewrite big_const_ord.`

(available from coq 8.10)

Yup I think Cyril's solution is much preferred

under is an equivalent of refine in standard coq ?

You are right to see a relation between both

You can find a bit of documentation here: https://staff.aist.go.jp/reynald.affeldt/coq2019/coqws2019-martindorel-tassi.pdf

with slides https://staff.aist.go.jp/reynald.affeldt/coq2019/coqws2019-martindorel-tassi-slides.pdf and a demo https://www.irit.fr/~Erik.Martin-Dorel/exposes/coq10_demo_under.v

the authors (Martin-Dorel and Tassi) explain how evars are used in the first page of the abstract

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.

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.

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

I guess one could at least build the usual structures (choiceType, finType, etc.) for the `int63`

type, right?

@Karl Palmskog for equality, this is not clear to me: this is modular arithmetic so the relevant boolean comparison is modulo 2^63.

But you could indeed easily equip it with the trivial boolean equality, and then choice and countable structures.

However, I would prefer to know what @Bas Spitters had in mind before giving a more detailed answer.

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

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.

@Bas Spitters you probably want to use CoqEAL

it does already provide transport between `nat`

and `N`

if I recall correctly

it would be interesting to provide (non-bidirectional) transport between `nat`

and `int63`

in CoqEAL

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

unfortunately CoqEAL only works with 8.11 and MathComp 1.10 if you use Pierre Roux's pull request patch

ping @Cyril Cohen that it would be very convenient if this was merged (and a new release would also be very welcome)

@Karl Palmskog done

:thumbsup: thanks!

and released

I do not have time to prepare the opam packages though

I can do it if you don't mind

I certainly do not mind ;)

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

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

@Karl Palmskog yes, but everything is already here https://github.com/CoqEAL/CoqEAL/blob/master/coq-coqeal.opam#L20

right (it's handled by the multinomials dep), but the text in the 1.0.3 release says finmap 1.3.4

I can edit that, I screwed up

:thumbsup:

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)

(for example, I think CoqEAL should definitely be in the platform, along with Analysis and some other MathComp stuff)

I do not think these are mature software

well, platform inclusion doesn't imply full maturity in my reading, usually just that a project has been found useful by other researchers/engineers

for example, is there any other project that gives better or more convenient transfer `nat`

<-> `N`

? I haven't seen much in this direction

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

instead of hoping people guess the right thing.

Only reasonably mature stuff should be included in the platform IMHO

CoqEAL 1.0.2 and 1.0.3 are now on the Coq OPAM archive

Platform has different package as opam ?

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

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

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

@Valentin Robert does `have := someLemma`

work better? `move: t`

is a bit hacky (it tries to generalize things).

last I checked, `have :=`

won't instantiate typeclasses even when it should (and then I use `pose proof`

)

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

ah yeah, it instantiates the type class arguments up to the last actual argument I pass, but leaves the ones after sadly...

yeah I've been using `pose proof`

too...

guess I'll keep `pose proof`

then :\

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

You can then do `have : !! term_with_tc`

:D

thanks Cyril!

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

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

the only way I know of is to `move => i Ai Bi Ci EQ`

, then `move : EQ Ai Bi Ci => ->`

because the equation is all the way after all the constructor arguments, but those need to be in the goal for the substitution

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

ah, I just learned about `clear_switch`

, I guess I can at least get rid of the last line

Coq 8.10 added temporary introductions.

For instance for the first two lines you can more or less do: `move => ??? ++ []. move => <- <- P1 P2.`

@Valentin Robert

The temporary introduction is done by +. More info in the changelog and links https://coq.inria.fr/refman/changes.html#id117

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

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

Or rtc_inv in https://gitlab.mpi-sws.org/iris/stdpp/blob/master/theories/relations.v#L113

I do have an inversion lemma for this, I was just trying to avoid the hassle of defining it :) thanks for all the pointers!

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.

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

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

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

is there a way to "move" le in ring_scope to le in coq_nat, if all arguments are nat ?

(btw when I try to search using ` Search ((_ <= _)%R _ (_ <= _)%N).`

I get `no head constant in head search pattern`

, the `->`

symbol is not supported ? )

@vlj your search uses `_`

in place of `->`

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

?

it complains : `too many arguments in head search pattern`

ler_nat doesn't work for me

@vlj what I meant is that your search does *not* use `->`

; you could try `Search ((_ <= _)%R -> (_ <= _))`

; if that fails, `Search _ ((_ <= _)%R -> (_ <= _)).`

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.

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

I'm not able to prove that `Num.ler p p`

is true... it looks like `le`

and `ler`

can't be unified, but I think I'm including near all of mathcomp so there should be a canonical somewhere

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

@vlj by rewrite lerr.

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

I guessed the name.

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

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.

I could `rewrite /Order.join //= maxn.`

and then I could solve by case but it looks a bit unatural.

@vlj for me `by rewrite lexUl.`

does the trick

the right lemma is `leUl`

not `lexUl`

Thanks

it doesn't work for me :/

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

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

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

You have indeed a bit of a mess there; you are using an operator from a different library for each of the operatros

max is the one from nat

<= the one from num

and you are injecting the nat from max to the ints by the Posz coercion

the thing can be proved actually by stripping all this, but you don't want to do that

`Proof. by rewrite lez_nat leq_maxl. Qed.`

thanks

you want to open `order_scope`

if you wanna use the `_ <= _`

from order

I need to keep the max in nat

why?

what happen if I open several scope with conflicting definition

they work as a stack [roughly]

if you want to keep the max in nat use maxn

and <= from nat

if you want to see it as a lattice don't

but don't pick the <= from int

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

You can use sections / modules to better manage scopes, IIRC this is used very often in math-comp

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

with x being potentially negative, n being always positive, and i between 0 and n

so I need to have something in `int`

in the distance (I don't want to "clamp" the value)

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)

I will try to rewrite my complete proof script to use scope and try to stay in nat_scope

you could also move to `(n : int) (h_n : 0 <= n)`

hard to know

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

it doesn't type, but that's what I would like to have : |x + i - n/2 - x|, but in N

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

but for some reason it picks the norm in ring_scope and not the one in ssrint

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

seems like an issue in parsing

@vlj %N affects the scope for everything inside the norm, so there's no reason for those two expressions to be equivalent

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

Actually, ahem, you could maybe use tmp, or just force another scope inside the norm:

```
`| (x + i....)%distn_scopr%ring_scope |%N
```

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.

thanks, will give a try

Why you do ` x + i - n - x`

? This is just i - n ?

so you have `(n i : int), 0 <= n -> 0 <= i < n -> ``| i - n |`

?

but given that i < n you can rewrite it to use max?

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

`let E := fresh "E" in case E : e.`

does not use the fresh name... is this impossible in ssreflect?

(I also tried `case ? : e.`

which does not give me an equation...)

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

(the symptoms are not so close, but the first was marked as a dup of the second and both involve name resolution)

Is there a refinement for ssrint to /From "coq_int"? Looking at coqeal binint.v seems to redefine coq_int.

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.

@vlj https://github.com/pi8027/mczify This should work with Coq 8.11.

doesn't work with coq 8.0 ?

8.10*

opam only has 8.10 so far

@Kazuhiko Sakaguchi it works ! thanks

it works really well

@vlj Good! If you see any bugs or possible improvements please let me know.

@Kazuhiko Sakaguchi do you have plans to include that zify code in MathComp itself? Or should we copy it into other projects for now?

by the way, there is an absolute path definition in the _CoqProject file in the repo that should probably be removed

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

Also, sure, I will remove that.

Generalised in which way ?

@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

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

I wonder if this is due to `zify`

or `lia`

...

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

in any case, this was handy on 8.11, but apparently doesn't work at all on `master`

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

For example, `@size (GRing.Ring.sort int_ringType) x`

and `@size int x`

where `x : seq int`

are convertible but not syntactically equal.

Also, thank you for suggestions.

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

Since instances for `ssreflect.div`

are constructed using instances for `ssralg.intdiv`

now, splitting requires some more work.

how do you use this notation ` Notation "@ 'sval'" := (@proj1_sig) (at level 10, format "@ 'sval'").`

? Isn't `@`

conflicting with the explicit annotation?

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)

oh right, I was ignoring the single quotes around `sval`

, I was reading this incorrectly

thanks

any clever way of specializing the top assumption? over `move => A. move : (A arg).`

@Valentin Robert `move/(_ arg)`

.

btw what zify stands for ? Is it Z-ify, like "transforming into Z" ?

CommandShow Zify InjTyp

This command shows the list of types that can be injected into Z

yeah, I pronounce it "zed-ify"

I seem to recall a n-ary function abstraction, possibly in ssreflect, but I can't find it

RingType doesn't have a \max_ implementation ?

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

and there are is a comRing_distrLatticeType definition in ssrnum, which is canonical

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

solved by https://github.com/coq/opam-coq-archive/pull/1185 - many thanks to Yves!

@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

So I need to define "another max" in ssrint ?

Btw ringType also doesn't necessarily have a min element so there is no max defined in R as well ?

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

Hi. What is the notation for accessing the 0 of the dual lattice of a lattice L.

I tried `(0 : L^c)`

, but this is not working.

```
Goal (0 : L^c) = (0 : L).
Proof. by []. Qed.
```

@Pierre-Yves Strub That has been changed to ^d.

Yes, sure. But is `0^d`

is going to be `1`

?

@Pierre-Yves Strub it should be the case

Yes.

Yes, this is why I ask. Because `(0 : L^c)`

should also be `1`

. I am going to check.

Oh, I think that `^c`

was interpreted in the `ring`

scope.

Oh yes... that is why I eventually changed it to `^d`

Actually I think `^c`

is in the `type_scope`

and was all the more conflicting with the one in `order.v`

Ok. Fixed. I was getting mad :)

well spotted

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?

ah, "Trivial Intersection" it seems

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)

@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

I'd like to test too

as soon as we've handed in the camera ready, we'll work on getting all the components out, hopefully beginning of next week

we wanted to refer to the arXiv version in the camera ready, so that's why it was a little bit early

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

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.

@Cyril Cohen so what is the planned date (or general timeframe)?

this week I think

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?

(that do not already have something else)

the main dilemma I see is between what goes on Discourse vs. what goes on Zulip

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

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

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

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!

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

I also haven't been able to find anything about inter-instance communication in Zulip

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 `rewrite`

but I was wondering if there is a way that does not require to name the subterm `pat`

...

@Kenji Maillard `rewrite [pat](_ : _ = t)`

?

But if `pat`

is `in pat'`

, it does not work I think.

@Kazuhiko Sakaguchi works exactly as I wanted thanks a lot !

:+1:

Last updated: Feb 22 2024 at 04:02 UTC