## Stream: math-comp devs

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

#### Anton Trunov (Apr 17 2019 at 13:54):

@Erik Martin-Dorel Thank you very much for setting up CI! I have a question, if you don’t mind.

#### Anton Trunov (Apr 17 2019 at 13:55):

Shouldn’t we also add CONTRIB_VERSION: 8.8.0 around this line: https://github.com/math-comp/math-comp/blob/master/.gitlab-ci.yml#L184?

#### Anton Trunov (Apr 17 2019 at 13:56):

I’m asking because lemma-overloading uses x.y.z format for release tags (for historical reasons): https://github.com/coq-community/lemma-overloading/releases

#### Anton Trunov (Apr 17 2019 at 13:56):

If this is the case, I can submit a PR

#### Erik Martin-Dorel (Apr 17 2019 at 15:53):

@Anton Trunov good question; first let me note that COQ_VERSION: "8.8" only deals with the version of Coq itself, not the branch or release of external libraries such as lemma-overloading; then regarding your question, technically the answer is both (adding or not adding CONTRIB_VERSION: "8.8.0") would be possible, it depends on what you want to test. Currently, that variable is not redefined so it defaults to: CONTRIB_VERSION: "master". So the job ci-lemma-overloading-8.8: checks that lemma-overloading's master build is not broken by the development version of math-comp. This CI job is important to have, but I'm unsure it is necessary to add other jobs to test that math-comp master stays compatible with a released version of lemma-overloading... and it seems to me that the CI setup of Coq does not contain such jobs for example... I Cc @Emilio Jesús Gallego Arias in case I'm mistaken here about Coq's CI.

#### Emilio Jesús Gallego Arias (Apr 17 2019 at 16:06):

Yeah that's a tricky topic of both cases may be possible; I dunno; in general to avoid explosion it make make sense to test only one particular setup for each version; so maybe indeed CONTRIB_VERSION is redundant and the logic should be derived from COQ_VERSION in each contrib

#### Erik Martin-Dorel (Apr 17 2019 at 16:08):

Hi @Emilio Jesús Gallego Arias, OK. However I don't think CONTRIB_VERSION is redundant because sometimes a single branch of a library is compatible with several versions of Coq, so I guess it makes sense to "uncouple" COQ_VERSION and CONTRIB_VERSION in the general case…

#### Anton Trunov (Apr 17 2019 at 17:26):

If the project at hand has an opam file, then it seems CONTRIB_VERSION is not really needed, right? We could let opam decide which version to install based on the set of constraints.

#### Erik Martin-Dorel (Apr 17 2019 at 18:10):

Hi @Anton Trunov ! − hopefully I didn't misread your question, so to sum up:
the opam file is useful, indeed, to automatically get the relevant versions of the lemma-overloading dependencies (and it is used here: https://github.com/math-comp/math-comp/blob/master/.gitlab-ci.yml#L178-L179), but the main question is: in which branch of the lemma-overloading repo the opam file should be read?
this choice of the branch (or tag) is thus determined by the value of CONTRIB_VERSION.

#### Anton Trunov (Apr 17 2019 at 18:18):

Hi @Erik Martin-Dorel! I was thinking about installing the default version of a library being tested for the current Coq version. E.g. for fcsl-pcm library, opam would choose fcsl-pcm.v1.0.0 in case of Coq 8.8 and fcsl-pcm.v1.1.0 for Coq 8.9 (https://github.com/coq/opam-coq-archive/tree/master/released/packages/coq-fcsl-pcm). Of course, this only works for the libraries from opam-coq-archive repo. For dev versions it should be master or any other dev branch specified with CONTRIB_VERSION. imho, it would be nice to reuse that kind of dependency information that was already published in central sources.

#### Erik Martin-Dorel (Apr 17 2019 at 18:25):

@Anton Trunov OK I see what you meant. The coq-dev configuration should be kept as is, but for testing stable versions of Coq, one may want to replace (or complement) the current test with a regular opam install without pinning the opam file of lemma-overloading master.

#### Anton Trunov (Apr 17 2019 at 18:26):

Yes, that would be great!

#### Erik Martin-Dorel (Apr 17 2019 at 18:27):

This is easy to do actually, as in the mathcomp/mathcomp-dev images, the coq-released repo is already available :)

#### Anton Trunov (Apr 17 2019 at 18:28):

Awesome, I’ll take a look at it. Thank you for all your hard work on CI!

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

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

#### Reynald Affeldt (Dec 12 2019 at 09:09):

now that PR#270 has been merged into master, should we also update the various mathcomp projects' masters that have a related branch? (I am thinking of finmap, real-closed, and mathcomp-analysis)

#### vlj (Jan 02 2020 at 17:17):

all groups in mathcomp are fingroup or is there a more general definition available ?

#### vlj (Jan 02 2020 at 17:18):

I'm looking at commutators, and it seems to be defined only for fingroup

#### Assia Mahboubi (Jan 05 2020 at 19:47):

Hi @vlj , yes indeed, the library is strongly biased on finite groups, and commutators are defined for finite groups only. What kind of result would you be interested in?

#### vlj (Jan 05 2020 at 21:00):

well I found out an exercice about "solvable" group (ie a group whose iterated commutator group ends up being identity group) and wanted to use it as a way to get familiar with mathcomp group/algebra

#### vlj (Jan 05 2020 at 21:01):

it's not a big deal anyway, if the result is true for any group it's also true for finite group and I'm trying to prove it that way but maybe some lemma are valid because of the finiteness of the underlying set

#### Assia Mahboubi (Jan 05 2020 at 21:07):

which for instance implies the finiteness of its composition series. Yes, you might end up using specific properties of the finite case.

ok

#### vlj (Jan 05 2020 at 21:33):

it's out of historical reason that fingroup were designed as finite ?

#### vlj (Jan 05 2020 at 21:33):

I mean, not as a subtype of a more general group type ?

#### Kazuhiko Sakaguchi (Jan 05 2020 at 21:55):

I think there are at least two technical reasons here. The group structure without finiteness should be an intermediate structure between choiceType and zmodType, but if we add one more layer here, it will lead us to a serious performance issue and galois.v may not compile anymore. Moreover, the interface of finite groups is split into two structures baseFinGroupType and finGroupType with the use of a telescope (see fingroup.v), which I don't understand how to factor out without breaking things.

ok

#### vlj (Jan 05 2020 at 22:04):

zmodType is like, Z / nZ ?

#### vlj (Jan 05 2020 at 22:06):

what is a telescope, is it a coq concept ?

#### Kazuhiko Sakaguchi (Jan 05 2020 at 22:08):

zmodType is the interface for additive Abelian groups (also called Z-modules).

#### Kazuhiko Sakaguchi (Jan 05 2020 at 22:17):

Sect. 2.3 of this paper explains telescopes. https://hal.inria.fr/inria-00368403v1/
The interfaces of structures are represented as records that have the name type. This record should bundle a carrier of type Type (not another structure) with the class_of record in the principle of MathComp (and packed classes), except for this finGroupType.

#### Assia Mahboubi (Jan 06 2020 at 01:07):

@vlj

it's out of historical reason that fingroup were designed as finite ?

Yes, because the origins of this library are in a formalization of the Feit Thompson theorem in finite group theory. Although not a severe issue, for non-necessarily finite groups, formalizing concepts like quotient groups would have a different flavour. Because the constructive logic of coq would require extending CIC with a form of choice principle, as an extra axiom.

#### Assia Mahboubi (Jan 06 2020 at 01:15):

@vlj Telescopes are related with dependent type theory. In think the concept and vocabulary originates from de Bruijn's Automath system in the 60's or may be slightly later. Here is a reference: https://www.win.tue.nl/automath/archive/pdf/aut103.pdf. There, it is in fact a context, i.e. a succession of declaration of variables, annotated with (possibly dependent) types. Each type can thus depend on the variables that come before in the telescope. By extension, and depending on the author, "telescope" can also refer to an iterated product type, or to a record type. In both case the important feature is the well-formed cascade of types.

#### vlj (Jan 06 2020 at 07:55):

Thanks for the info

#### Reynald Affeldt (Jan 09 2020 at 09:07):

（what is the visio number and PIN for today?）

#### Reynald Affeldt (Jan 09 2020 at 09:33):

(I didn't realize there was a link)

#### vlj (Jan 09 2020 at 19:45):

In morphism.v there are several result on injectiv morphism but none on surjectiv ones, is it expected ?

#### Zhangsheng Lai (Jan 30 2020 at 12:06):

I'm trying to use Fintypes:

From mathcomp Require Import all_ssreflect.

Inductive Thing := a | b | c | d.

Scheme Equality for Thing.

Lemma eq_ThingP : Equality.axiom Thing_beq.
Proof. by case; case; constructor. Qed.
Definition Thing_eqMixin := Equality.Mixin eq_ThingP.
Canonical Thing_eqType := Equality.Pack Thing_eqMixin Thing.

Lemma Thing_enumP : Finite.axiom [:: a; b; c; d].
Proof. by case. Qed.

Definition Thing_finMixin := Eval hnf in FinMixin Thing_enumP.


However, the last definition returns the error msg:

The term "Thing_enumP" has type
"Finite.axiom (T:=Thing_eqType) [:: a; b; c; d]"
while it is expected to have type "Finite.axiom ?e".


What am I doing wrong here?

#### vlj (Jan 30 2020 at 22:30):

Maybe thing needs to be countable but maybe not

I got it

#### vlj (Jan 31 2020 at 15:31):

@Zhangsheng Lai you need to define a canonical CountType and ChoiceType for Thing as well

#### Anton Trunov (Jan 31 2020 at 15:43):

@Zhangsheng Lai You might want to look at https://stackoverflow.com/questions/58219864/how-should-a-user-defined-enumerated-type-be-made-fintype

#### Zhangsheng Lai (Jan 31 2020 at 16:29):

@vlj @Anton Trunov thanks! I managed to get it be showing Thing is in bijection with a pre-existing finite type

#### Zhangsheng Lai (Jan 31 2020 at 16:30):

but the deriving package looks interesting too! will give it a try :)

:+1:

#### Zhangsheng Lai (Feb 01 2020 at 06:05):

I've got a question, finType provides functionalities like enum and #|T | to allow iteration over the finite types and its cardinality. However, when I do Eval compute in enum Thing_finType or #| Thing_finType | it doesn't give the explicit sequence or the value 4 but displays the whole algorithm on how the expression is evaluated. So how does these functionality help us? It is suppose to be used by extracting it out using OCaml as an algorithm?

#### vlj (Feb 02 2020 at 18:17):

I think it's because Finite.enum is opaque

#### Emilio Jesús Gallego Arias (Feb 02 2020 at 18:19):

IIANM the motivation for making Finite.enum opaque is so proofs cannot depend on a specific enumeration order; that was deemed by math-comp developers to be too fragile in terms of proof robustness.

#### vlj (Feb 02 2020 at 18:20):

I tried with something like lemma tmp : enum Thing_finType = [:: a; b; c; d]. and after simplification it yields something depending on Finite.enum, which I can't replace because it's opaque

#### Emilio Jesús Gallego Arias (Feb 02 2020 at 18:59):

@vlj the usual approach, as you have an explicit enumeration function is to have a lemma such as:

Lemma Thing_enumP : Finite.enum Thing =1 Thing_enum.


#### Emilio Jesús Gallego Arias (Feb 02 2020 at 18:59):

which you can prove by unlocking Finite.enum

#### Emilio Jesús Gallego Arias (Feb 02 2020 at 19:00):

oh, a well-kept secret of math-comp is rewrite unlock

#### Emilio Jesús Gallego Arias (Feb 02 2020 at 19:00):

if you dig on the proofs you will see indeed that Finite.enum is not opaque, but "locked"

#### Emilio Jesús Gallego Arias (Feb 02 2020 at 19:00):

indeed you can make it transparent by the above rewrite, ditto for some other stuff

#### Emilio Jesús Gallego Arias (Feb 02 2020 at 19:01):

I'm unsure what's the best reference for the locked pattern, IIRC the documentation of the implementation was pretty good

#### Zhangsheng Lai (Feb 05 2020 at 02:03):

Thanks @vlj @Emilio Jesús Gallego Arias for the interesting discussions. So if the deriving package was used, I won't be able to do the unlocking?

#### Zhangsheng Lai (Feb 05 2020 at 02:27):

For CanChoiceMixin fK, is fK : cancel f g the proof of f and g providing the bijection between T and cT? Also, is the cT here an existing choiceType or countType?

#### Emilio Jesús Gallego Arias (Feb 05 2020 at 11:04):

@Zhangsheng Lai unlocking is implemented for the exposed user operators [bigop / matrix / enum] so it doesn't matter how you generate your instances

#### Emilio Jesús Gallego Arias (Feb 05 2020 at 11:06):

About CanChoiceMixin outputs:

CanChoiceMixin :
forall (T : choiceType) (sT : Type) (f : sT -> T) (f' : T -> sT),
cancel f f' -> choiceMixin sT


#### Zhangsheng Lai (Feb 05 2020 at 11:49):

@Emilio Jesús Gallego Arias would u be able to explain sT and the functions f and f'? Like for a type that I'm trying to make for it to be a choiceType, what do those mean?

#### Emilio Jesús Gallego Arias (Feb 05 2020 at 11:56):

sT is the type you want to prove that can be embedded into T, which is already a choicetype

#### Emilio Jesús Gallego Arias (Feb 05 2020 at 11:56):

then f and f' are the embedding and the projection functions respectively

#### Emilio Jesús Gallego Arias (Feb 05 2020 at 11:57):

so for example T can be nat

#### vlj (Feb 08 2020 at 22:51):

bigop is opaque ?

#### vlj (Feb 08 2020 at 22:52):

I tried to compute something with \sum and know values but \sum isn't simplified, by doing rewrite /bigop coq tells me it is opaque which I didn't expect.

#### vlj (Feb 08 2020 at 22:56):

rewrite unlock is working well

#### vlj (Feb 08 2020 at 23:58):

I have some issue with bigops in mathcomp... I have an expression using \sum_i  , I'm trying to compute it on some example, it doesn't work with Compute because of opaque definition. I'm now trying to prove an equality instead, but with rewrite unlockI'm getting something rather untractable (due to fintype everywhere) so I'd like to turn the \sum_i  into something easier to work with. Ideally I would get a proper list instead of all the enum things but I don't know how to get it.
Here is my wip code : https://gist.github.com/vlj/4aee150f751182e5106b4eddbcacd6e0

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

yes @vlj , in general bigop is locked and the approach using unlockis not going to scale well; I'd recommend a refinement-based setup such as the one provided by CoqEAL

coqEAL ?

installing it

#### Emilio Jesús Gallego Arias (Feb 09 2020 at 00:26):

you can install it, but IMHO it is more important to get the idea, roughly speaking, before computing with a bigop you want to translate it to a "computable" representation using a rewrite lemma.

#### vlj (Feb 09 2020 at 00:31):

by refinement based setup you mean, using a pattern with the rewrite tactic ?

#### Emilio Jesús Gallego Arias (Feb 09 2020 at 00:47):

I am not expert here so @vlj we should welcome comments from experts in the channel, but the idea is that you have some lemma Lemma mycompE : proof_func =1 comp_func where comp_func is a version friednly to computation.

ok

#### Emilio Jesús Gallego Arias (Feb 09 2020 at 00:47):

refinement helps to prove that lemma (almost) automatically, for example refining ordinals to regular integers, etc...

#### vlj (Feb 09 2020 at 00:51):

is there a publication on the subject ?

#### vlj (Feb 09 2020 at 00:51):

I found something I think https://perso.crans.org/cohen/papers/refinements.pdf

#### Emilio Jesús Gallego Arias (Feb 09 2020 at 00:56):

yup, I understand that's the right paper, there is a previous one too I think

#### vlj (Feb 09 2020 at 20:37):

I'm trying to map \sum to foldr addnbut I'm stuck with ordinaland natinteraction

Here is the case :

From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq choice path.
From mathcomp Require Import div fintype tuple finfun bigop finset fingroup perm.
From mathcomp Require Import div prime binomial ssralg finalg zmodp countalg ssrnum falgebra.
From mathcomp Require Import ssrint matrix algC.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Lemma tmp0 n:
(\sum_(i < n) i) = foldr addn 0%N (iota 0 n).
Proof.
rewrite /index_enum !unlock => //=.
rewrite /ord_enum.
rewrite /reducebig /applybig /comp => //=.


The goal is foldr (fun x : 'I_n => [eta addn x]) 0 (pmap insub (iota 0 n)) = foldr addn 0 (iota 0 n) (or eq (foldr (fun (x : ordinal n) (x0 : nat) => addn x x0) O (pmap insub (iota O n))) (foldr addn O (iota O n)) without notation)

#### vlj (Feb 09 2020 at 20:37):

I don't know if there is a way to replace pmap insub iota to just iota

#### vlj (Feb 09 2020 at 20:41):

I'm not sure that fun (x : ordinal n) (x0 : nat) => addn x x0is equal to addn, it looks like there is some coercion happening but I don't know how to show it

#### vlj (Feb 09 2020 at 20:43):

actually it's trivially proven as a lemma

#### Emilio Jesús Gallego Arias (Feb 09 2020 at 21:23):

Yup, that's already proven.

#### Zhangsheng Lai (Feb 12 2020 at 06:50):

rewrite unlock is working well

@vlj can I get your code to see how rewrite unlock is used to make things transparent?

#### vlj (Feb 12 2020 at 19:06):

@Zhangsheng Lai

From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq choice path.
From mathcomp Require Import div fintype tuple finfun bigop finset fingroup perm.
From mathcomp Require Import div prime binomial ssralg finalg zmodp countalg ssrnum falgebra.
From mathcomp Require Import ssrint matrix algC.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Local Open Scope ring_scope.

Lemma tmp0 n (T:ringType) (f: 'I_n -> T):
\sum_(i<n) f i = foldr (+%R) 0%R (map f (ord_enum n)).
Proof.
rewrite !unlock /reducebig /index_enum /applybig => //=.
rewrite !unlock /comp => //=.
by rewrite foldr_map.
Qed.


#### Zhangsheng Lai (Feb 13 2020 at 01:49):

@vlj thanks :smile: did u get it to work for the enum for finTypes?

#### Zhangsheng Lai (Feb 13 2020 at 13:25):

Still unable to get the unlocking to work so reaching out again for some kind advice. I have managed to use deriving to get thing to be a finType. So my goal is to have access to enum, the sequence that enumerates the finite list of all terms of type thing. Eval compute in enum thing_finTyperuns but does not show the desired [:: a; b; c]. So what I have done is tried the rewrite unlock which doesn't seem to be working. Below is the code that I'm working with:

From mathcomp Require Import all_ssreflect.

From void Require Import void.
From deriving Require Import deriving.

Inductive thing : Type := a | b | c.

Canonical thing_indType := Eval hnf in IndType _ _ [indMixin for thing_rect].
Canonical thing_eqType := Eval hnf in EqType thing [derive eqMixin for thing].
Canonical thing_choiceType := Eval hnf in ChoiceType thing [derive choiceMixin for thing].
Canonical thing_countType := Eval hnf in CountType thing [derive countMixin for thing].
Canonical thing_finType := Eval hnf in FinType thing [derive finMixin for thing].

Eval compute in enum thing_finType.
Check enum thing_finType.

Lemma thing_enumP : Finite.enum thing_finType = [:: a; b; c].
Proof. rewrite unlock. by []. Defined.


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

you need first to unfold enough definitions that unlock is visible.

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

sorry, that lock is visible

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

where “visible” includes “hidden by notations” but not “hidden by definitions”.

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

I expect that’s why @vlj ‘s code seems magic.

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

@Zhangsheng Lai see above ^^

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

Hi! I must warn that unlocking is highly discouraged in most cases, i.e. cases where the code is not invariant by API changes. For example, there is no guarantee that thing_enumP will still be provable in future versions of mathcomp.

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

The invariant here is that enum contains all the elements and only once, but does not specify an order, any code that relies on this order (e.g. a theorem asserting it) is not robust.

#### Zhangsheng Lai (Feb 13 2020 at 14:42):

@Cyril Cohen Thanks for the advice. But when I try Eval compute in enum thing_finType I do not get the list of elements. Is there any way that I can access this list using enum without unlocking?

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

There is no way to do that, but it is not necessarily a problem to do it as long as nothing relies on it.

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

A robust statement would by perm_eq (enum thing) [:: a; b; c]

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

(and a robust proof would not rely on this order either, but can do unlock)

#### Paolo Giarrusso (Feb 13 2020 at 16:34):

@Zhangsheng Lai have you tried vm_compute? It does ignore some extra forms of opacity.

#### vlj (Feb 13 2020 at 19:58):

@Zhangsheng Lai try Unset Printing Notation. It will remove notation so that you know what to rewrite.

#### vlj (Feb 13 2020 at 19:58):

In my case ord_enum and insubT worked

#### Paolo Giarrusso (Feb 13 2020 at 21:13):

Fwiw Unset Printing Notation only works with proof general, other IDEs have different options.

#### vlj (Feb 14 2020 at 09:47):

It works with vscoq too

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

No, it gets disabled after one line.

#### vlj (Feb 14 2020 at 11:33):

Ho I though it was the expected behavior :s

#### Paolo Giarrusso (Feb 14 2020 at 11:51):

The vscoq version is (on Mac) Cmd-Shift-P (to type commands) then pick "Coq: Display All Basic lowlevel contents"

#### Paolo Giarrusso (Feb 14 2020 at 11:52):

on coqide you still need "Display All Basic lowlevel contents", but in the View menu.

#### Paolo Giarrusso (Feb 14 2020 at 11:52):

Ditto for all "display" options

#### Zhangsheng Lai (Feb 17 2020 at 01:10):

@Paolo G. Giarrusso vm_compute just freezes things up

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

Does auto work with mathcomp ?

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

I have another equation that could be solved via commutativity and associativity, is it possible to just have a rewrite database and let auto find the correct sequence ?

#### Paolo Giarrusso (Feb 18 2020 at 19:44):

auto doesn’t rewrite; there’s autorewrite.

Yes

#### Paolo Giarrusso (Feb 18 2020 at 19:44):

(okay, auto can use Hint Extern which can use anything including rewrite)

#### vlj (Feb 18 2020 at 19:45):

It will work with mathcomp ?

#### vlj (Feb 18 2020 at 19:52):

It would act as a poor man lia in my case

#### Paolo Giarrusso (Feb 18 2020 at 20:45):

Yeah, ltac and ssreflect work well together... But I think autorewrite uses the standard rewrite, not ssreflect's one, which might be a problem? If your lemmas work with plain rewrite you're good

#### Paolo Giarrusso (Feb 18 2020 at 20:45):

But you can't autorewrite with associativity and commutativity, they'll loop

#### Paolo Giarrusso (Feb 18 2020 at 20:47):

(at least I think; IIRC autorewrite only works with normalizing rewrite systems, because it keeps rewriting till it's done)

#### Paolo Giarrusso (Feb 18 2020 at 20:47):

(And it cannot rewrite anymore)

#### vlj (Feb 18 2020 at 21:40):

autorewrite doesn't try all possible rewrite chain up to a max size until it finds a solution ?

#### vlj (Feb 18 2020 at 21:42):

seems to take forever though

#### vlj (Feb 18 2020 at 21:46):

you're right it doesn't work, it loop

#### Paolo Giarrusso (Feb 18 2020 at 21:59):

https://coq.inria.fr/refman/proof-engine/tactics.html#coq:tacn.autorewrite

#### vlj (Feb 19 2020 at 11:59):

Hmmm yes it couldn't work

#### Zhangsheng Lai (Mar 25 2020 at 02:48):

Is there any differences between the tactics auto in coq and the tactic by [] available in mathcomp?

#### Emilio Jesús Gallego Arias (Mar 25 2020 at 04:27):

yes @Zhangsheng Lai

#### Emilio Jesús Gallego Arias (Mar 25 2020 at 04:28):

IIRC correctly by [] is equivalent to done [let me double-check that]

done is

#### Emilio Jesús Gallego Arias (Mar 25 2020 at 04:28):

Ltac done :=
trivial; hnf; intros; solve
[ do ![solve [trivial | apply: sym_equal; trivial]
| discriminate | contradiction | split]
| case not_locked_false_eq_true; assumption
| match goal with H : ~ _ |- _ => solve [case H; trivial] end ].


#### Emilio Jesús Gallego Arias (Mar 25 2020 at 04:31):

yup basically by [] is done

#### vlj (Mar 25 2020 at 18:11):

if I have a numFieldType what is the notation for division ?

#### Cyril Cohen (Mar 25 2020 at 18:12):

@vlj /

#### vlj (Mar 25 2020 at 18:12):

I found a x^-1 but that would be cumbersome to write * ^1

#### vlj (Mar 25 2020 at 18:12):

do I have to import a scope ?

#### Cyril Cohen (Mar 25 2020 at 18:13):

you have to Import module GRing.Theory and open scope ring_scope.

#### Cyril Cohen (Mar 25 2020 at 18:13):

the notation comes from ssralg

ok

#### vlj (Mar 25 2020 at 18:14):

Module import is not transitive ?

no

#### Cyril Cohen (Mar 25 2020 at 18:15):

Command Export is transitive

ok thanks

#### vlj (Mar 25 2020 at 22:06):

are ssreflect and Ltac2 compatible ? When I Import LTac2, I get error with move => H.for instance

#### vlj (Mar 25 2020 at 22:06):

Syntax error: [tactic:q_ident] expected after 'move' (in [tactic:tac2expr]).

#### Cyril Cohen (Mar 26 2020 at 17:31):

Hi @vlj this is unfortunate... if you did not do it yet would you mind checking whether there is an issue on coq's github describing the problem and if not, could you post one, tagging @Enrico Tassi and @Pierre-Marie Pédrot along the way?

#### Pierre-Marie Pédrot (Mar 26 2020 at 17:34):

this has been on my TODO list for quite a time actually

#### Pierre-Marie Pédrot (Mar 26 2020 at 17:34):

(note that you can still implement stuff in Ltac2 and export it to Ltac1 so as to be able to use ssr)

#### Cyril Cohen (Mar 26 2020 at 17:35):

thanks for the quick answer @Pierre-Marie Pédrot

#### vlj (Mar 26 2020 at 22:25):

I opened a bug : https://github.com/math-comp/math-comp/issues/467

#### vlj (Mar 26 2020 at 22:26):

apparently there is no (open) bug about ltac2 on issue in mathcomp

#### vlj (Mar 26 2020 at 22:28):

and there's nothing in coq issue, at least when I search for "ltac2" and "mathcomp"

#### vlj (Mar 29 2020 at 22:27):

Is there an équivalent of lia/zify for numFields ?

#### vlj (Mar 29 2020 at 22:29):

I have an equation like 1+ b x- b c + d = 1+d, but it's not in Z but R... Lia is decisive on Z, I suspect there is something preventing it to works on linear formula over R ?

#### vlj (Mar 29 2020 at 22:49):

Apparently there is Add Fields

#### Paolo Giarrusso (Mar 29 2020 at 22:58):

@vlj see also lra (https://coq.inria.fr/refman/addendum/micromega.html)

Thanks

#### vlj (Mar 29 2020 at 23:02):

Is there a mechanism to use lra with numFieldType ?

#### Paolo Giarrusso (Mar 29 2020 at 23:10):

not sure :-| ring and field are extensible (but not sure how powerful they are: https://coq.inria.fr/refman/addendum/ring.html). I thought you had found an extensibility for lra : https://gitter.im/math-comp/analysis?at=5e62ccedf953aa4499cfa8a2.

#### Paolo Giarrusso (Mar 29 2020 at 23:11):

@vlj btw the equation you write is only true if x = c or b = 0

#### Paolo Giarrusso (Mar 29 2020 at 23:16):

@vlj but I'm no expert on Coq reals, better wait for those with actual clue ;-)

Err yes b=x

#### Paolo Giarrusso (Mar 30 2020 at 08:29):

@vlj that, as written, is not enough. Do you have a typo?

#### vlj (Mar 30 2020 at 09:32):

yes sorry, I typed on my phone

#### vlj (Mar 30 2020 at 09:32):

the real equation is 1 + b * x - b * x + d = 1 + d, I need to simplify b * x - b * x

#### vlj (Mar 30 2020 at 17:45):

Actually I can use Reals

#### vlj (Mar 31 2020 at 18:06):

I made some progress, it seems that I have a type error I don't really understand.

#### vlj (Mar 31 2020 at 18:06):

with this snippet : https://gist.github.com/vlj/caebeb393abf76342a409d871ed39a86 I have the error cannot find a declared ring structure over "(GRing.Zmodule.sort R)"

#### vlj (Mar 31 2020 at 18:07):

But I don't understand why, GRing.Zmodule.sort R is a Zmodule, not a ring, but I used ring_scope so + should be defined over ring ?

#### vlj (Apr 05 2020 at 23:12):

In several place in math comp there is a variable "disp:unit" used

#### vlj (Apr 05 2020 at 23:14):

What does disp stand for ? My intuition is that it means display or dispatch but this doesn't make a lot of sense.

#### Cyril Cohen (Apr 05 2020 at 23:36):

@vlj can you tell me if this makes sense to you? https://github.com/math-comp/math-comp/blob/master/mathcomp/ssreflect/order.v#L70-L73 and
https://github.com/math-comp/math-comp/blob/master/mathcomp/ssreflect/order.v#L110-L119

#### vlj (Apr 06 2020 at 17:26):

not completly... if unit type has a single value, it means it will always be tt if I understand correctly, so it will be always displayed ?

#### Anton Trunov (Apr 06 2020 at 17:29):

@vlj You are right, but Qed. makes the definition opaque, so Coq cannot see that it’s just tt underneath. It looks sort of like an axiom to Coq

ok

#### vlj (Apr 07 2020 at 18:40):

Is there an exemple in mathcomp of lemma on 2 different structure but with the same carrier type ? For instance, 2 rings on T with different operator

#### vlj (Apr 07 2020 at 18:45):

I'd like to define a relation on topologicalType, eg Definition (A B:topologicalType):= forall x, @open A x -> @open B x. obviously it doesn't work since base A and base B don't share the same type, so I'd like to know if there is a standard way of handling such case

#### vlj (Apr 07 2020 at 18:48):

Is subtyping the good way of handling this ? Ideally it could be extended to support inclusion of topologicalType

#### Assia Mahboubi (Apr 08 2020 at 08:24):

Is there an exemple in mathcomp of lemma on 2 different structure but with the same carrier type ? For instance, 2 rings on T with different operator

@vlj there a converse ring structure in ssralg: for a possibly non commutative ring, same carrier and operations except for multiplication.

#### vlj (Apr 08 2020 at 16:50):

thanks, wil have a look at it

#### Yves Bertot (Apr 15 2020 at 09:02):

@affeldt-aist and I are going to start the release process for 1.11.0-beta, there is only one remaining PR in the milestone.

#### Yves Bertot (Apr 15 2020 at 09:22):

A personal thought: if we make a beta-release and we follow the instruction on the https://github.com/math-comp/math-comp/wiki/Howto-Release page, there is only the master branch. It seems that this prevents from integrating major changes until the final 1.11.0 is released. Is this clear for everybody?

#### Cyril Cohen (Apr 15 2020 at 11:38):

This means assignees must be extra careful wrt to which PR get merged and that any PR that is validated but should not go in the 1.11.0 must be labelled with a milestone >= 1.12.0

#### Assia Mahboubi (Apr 15 2020 at 12:19):

@Cyril Cohen I do not understand your sentence.

#### Assia Mahboubi (Apr 15 2020 at 12:21):

Could you clarify what does "must extra careful" mean? and what does "validated but should not go in the 11.10" mean?

#### Cyril Cohen (Apr 15 2020 at 12:28):

A PR being approved does not mean it should be merged yet. For the next 6 weeks we should merge only fixes of bugs (especially the ones 1.11.0+beta1 might have introduced), or features we think must be merged ASAP. Theses PR we will labeled "1.11.0" and can be merged as soon as they are approved. All other PRs must be labelled with a milestone with a larger revision number and merged only after the milestone just before has been released (e.g. "1.12.0" labelled issues/PRs can only be fixed/merged after "1.11.0" is released, and "1.13.0" issues/PRs can only be fixed/merged after "1.12.0" is (e.g. https://github.com/math-comp/math-comp/issues/476))

Thanks.

#### Assia Mahboubi (Apr 15 2020 at 14:32):

or features we think must be merged ASAP.

#### Assia Mahboubi (Apr 15 2020 at 14:32):

I would even remove this case.

#### Assia Mahboubi (Apr 15 2020 at 14:32):

Freeze means feature freeze.

#### Kazuhiko Sakaguchi (Apr 15 2020 at 15:46):

There is another option: we can set up a branch for 1.11.x as in Coq, but we have to backport a few PRs in this case.

#### Cyril Cohen (Apr 15 2020 at 15:51):

The purpose of the freeze is to avoid having to do backports, which would change the documented release process https://github.com/math-comp/math-comp/wiki/Howto-Release

#### Zhangsheng Lai (Apr 18 2020 at 05:30):

what is the difference between apply: term and apply/term ?
I understand that apply term is a Coq syntax and apply: term is for mathcomp. What I'm experiencing is in my application, apply term runs but apply: term returns an error:

Error:
Cannot apply lemma term


Anyone able to explain this phenomenon?

#### Assia Mahboubi (Apr 18 2020 at 05:59):

@Zhangsheng Lai can you provide the goal on which this happens?

#### Zhangsheng Lai (Apr 18 2020 at 06:04):

@Assia Mahboubi my goal is

?Goal   \in [seq x <- vertexL   | C   x]


where C : pred T. And I have a lemma

Lemma FindObj s r vl el : has (sub_rel s r) el -> (sub_rel2triple s r el).2 \in vl
-> (sub_rel2triple s r el).2 \in [seq x <- vl | getObj s r el x].


that will resolve it.

#### Zhangsheng Lai (Apr 18 2020 at 06:06):

so my goal can be solved with apply: term1 and apply term2, with the second one failing when I write apply: term2 instead. In case it matters, term2 looks like this

(FindObj _ (defaultU,defaultU,defaultU) _ _ vertexL edgeL)


#### Cyril Cohen (Apr 18 2020 at 11:54):

hi @Zhangsheng Lai what are term1 and term2 in your example?

#### vlj (Apr 18 2020 at 12:47):

Apply: findobj returns à other error ?

#### Zhangsheng Lai (Apr 18 2020 at 13:23):

term1 is just a record type constructor, term2 is what I have above

#### Zhangsheng Lai (Apr 18 2020 at 13:24):

so i was trying to do by apply term1/term2, but then realised the apply:term2 runs for a long time and fails. by works when its apply term2

#### vlj (Apr 27 2020 at 17:41):

What is the "mathcompish" way of saying a function is growing/increasing ? As far as I know there is a monotone somewhere, and I'm expecting increasing/decreasing to be defined for nat or even int, but is it possible to add another order ?

#### vlj (Apr 27 2020 at 17:41):

my use case is : interior and closure in topology are growing wrt subset inclusion

#### Reynald Affeldt (Apr 27 2020 at 18:26):

I don't think there is a definition or a notation for that

ok thanks

#### vlj (Apr 27 2020 at 18:26):

btw do you know where commutativeis defined ? I'm trying to use it

#### vlj (Apr 27 2020 at 18:28):

I added everything from order.v, and indeed there is a commutative defined, but I don't know how to "backtrace" which include added it

#### vlj (Apr 27 2020 at 18:28):

without dichotomic search

#### vlj (Apr 27 2020 at 18:29):

(it's in ssrfun but I'm still interested in knowing if there is a way to know which module includes a given lemma/definition)

#### Anton Trunov (Apr 27 2020 at 18:30):

From mathcomp Require Import all_ssreflect.
About commutative.


This should output the module you are looking for.

#### Reynald Affeldt (Apr 27 2020 at 18:30):

Locate commutative. also

thanks

#### Enrico Tassi (Apr 27 2020 at 18:38):

if I'm not mistaken it is in ssrfun, which is in Coq proper these days

Yes seems so

#### vlj (Apr 27 2020 at 20:46):

if I have a T -> T -> Prop, with T at least an eqType, is there a way to make coq cast it to a rel T ?

#### vlj (Apr 27 2020 at 20:47):

I'd like to create a lattice based on subset, but subset in classical_sets is defined as a set T -> set T -> Prop, not a rel T

#### Cyril Cohen (Apr 27 2020 at 20:47):

vlj vlj 19:41
What is the "mathcompish" way of saying a function is growing/increasing ? As far as I know there is a monotone somewhere, and I'm expecting increasing/decreasing to be defined for nat or even int, but is it possible to add another order ?
my use case is : interior and closure in topology are growing wrt subset inclusion

affeldt-aist affeldt-aist 20:26
I don't think there is a definition or a notation for that

Yes there is:

• {mono f : x y / x <= y} is strict monotonicity
• {homo f : x y / x < y} is loose monotonocity

and there are tons of helper lemma, in various locations (including order.v)

#### vlj (Apr 27 2020 at 20:48):

(I'd like the lattice to be defined on subset if possible, ie not on an helper subset)

#### Cyril Cohen (Apr 27 2020 at 20:49):

vlj vlj 22:46
if I have a T -> T -> Prop, with T at least an eqType, is there a way to make coq cast it to a rel T ?
I'd like to create a lattice based on subset, but subset in classical_sets is defined as a set T -> set T -> Prop, not a rel T

You can use [<_>] to cast Prop to bool in a classical setting

#### Cyril Cohen (Apr 27 2020 at 20:50):

decidability of equality on T does not matter in this setting.

#### vlj (Apr 27 2020 at 20:50):

but {mono f: x y / x <= y} is defined for function on R or is it defined for anything that can be compared ?

ok

#### Cyril Cohen (Apr 27 2020 at 20:51):

vlj vlj 22:50
but {mono f: x y / x <= y} is defined for function on R or is it defined for anything that can be compared ?

you can replace <= with any relation, and if it is an order relation from order.v in mathcomp-1.11.0+beta1, you get all the support for generic orders

thanks

#### vlj (Apr 27 2020 at 21:57):

I have an issue, I'm trying to add a canonical distrLatticeType for subset, but it looks like the lemma fail to identify the order structure. If I add some extra type hint it works. Snippet is here : https://gist.github.com/vlj/fb1e0d8186ad1cb89a6b6f3bea6123b8

#### vlj (Apr 28 2020 at 17:18):

thanks for the hint

#### vlj (Apr 28 2020 at 17:18):

coq doesn't resolve the notation if it's not <= ?

#### vlj (Apr 28 2020 at 18:26):

by the way how can I access mathcomp from zulip ? I just installed zulip, I joined funproc since there was some mention of coq in this organisation but it looks unofficial

Last updated: Feb 09 2023 at 02:02 UTC