Stream: math-comp devs

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


view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Anton Trunov (Apr 17 2019 at 13:56):

If this is the case, I can submit a PR

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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…

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Anton Trunov (Apr 17 2019 at 18:26):

Yes, that would be great!

view this post on Zulip 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 :)

view this post on Zulip 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!

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

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

view this post on Zulip 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)

view this post on Zulip vlj (Jan 02 2020 at 17:17):

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

view this post on Zulip vlj (Jan 02 2020 at 17:18):

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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip vlj (Jan 05 2020 at 21:32):

ok

view this post on Zulip vlj (Jan 05 2020 at 21:33):

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

view this post on Zulip vlj (Jan 05 2020 at 21:33):

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

view this post on Zulip 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.

view this post on Zulip vlj (Jan 05 2020 at 22:04):

ok

view this post on Zulip vlj (Jan 05 2020 at 22:04):

zmodType is like, Z / nZ ?

view this post on Zulip vlj (Jan 05 2020 at 22:06):

what is a telescope, is it a coq concept ?

view this post on Zulip Kazuhiko Sakaguchi (Jan 05 2020 at 22:08):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip vlj (Jan 06 2020 at 07:55):

Thanks for the info

view this post on Zulip Reynald Affeldt (Jan 09 2020 at 09:07):

(what is the visio number and PIN for today?)

view this post on Zulip Reynald Affeldt (Jan 09 2020 at 09:33):

(I didn't realize there was a link)

view this post on Zulip 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 ?

view this post on Zulip 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?

view this post on Zulip vlj (Jan 30 2020 at 22:30):

Maybe thing needs to be countable but maybe not

view this post on Zulip vlj (Jan 31 2020 at 15:31):

I got it

view this post on Zulip vlj (Jan 31 2020 at 15:31):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Zhangsheng Lai (Jan 31 2020 at 16:30):

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

view this post on Zulip Anton Trunov (Jan 31 2020 at 16:39):

:+1:

view this post on Zulip 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?

view this post on Zulip vlj (Feb 02 2020 at 18:17):

I think it's because Finite.enum is opaque

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Emilio Jesús Gallego Arias (Feb 02 2020 at 18:59):

which you can prove by unlocking Finite.enum

view this post on Zulip Emilio Jesús Gallego Arias (Feb 02 2020 at 19:00):

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

view this post on Zulip 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"

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Feb 05 2020 at 11:06):

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Feb 05 2020 at 11:56):

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

view this post on Zulip Emilio Jesús Gallego Arias (Feb 05 2020 at 11:57):

so for example T can be nat

view this post on Zulip vlj (Feb 08 2020 at 22:51):

bigop is opaque ?

view this post on Zulip 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.

view this post on Zulip vlj (Feb 08 2020 at 22:56):

rewrite unlock is working well

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip vlj (Feb 09 2020 at 00:13):

coqEAL ?

view this post on Zulip vlj (Feb 09 2020 at 00:20):

installing it

view this post on Zulip 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.

view this post on Zulip vlj (Feb 09 2020 at 00:31):

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

view this post on Zulip 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.

view this post on Zulip vlj (Feb 09 2020 at 00:47):

ok

view this post on Zulip 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...

view this post on Zulip vlj (Feb 09 2020 at 00:51):

is there a publication on the subject ?

view this post on Zulip vlj (Feb 09 2020 at 00:51):

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

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip vlj (Feb 09 2020 at 20:37):

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

view this post on Zulip 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

view this post on Zulip vlj (Feb 09 2020 at 20:43):

actually it's trivially proven as a lemma

view this post on Zulip Emilio Jesús Gallego Arias (Feb 09 2020 at 21:23):

Yup, that's already proven.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Zhangsheng Lai (Feb 13 2020 at 01:49):

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

view this post on Zulip 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.

view this post on Zulip Paolo Giarrusso (Feb 13 2020 at 14:05):

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

view this post on Zulip Paolo Giarrusso (Feb 13 2020 at 14:05):

sorry, that lock is visible

view this post on Zulip Paolo Giarrusso (Feb 13 2020 at 14:05):

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

view this post on Zulip Paolo Giarrusso (Feb 13 2020 at 14:06):

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

view this post on Zulip Paolo Giarrusso (Feb 13 2020 at 14:06):

@Zhangsheng Lai see above ^^

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Cyril Cohen (Feb 13 2020 at 15:13):

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

view this post on Zulip Cyril Cohen (Feb 13 2020 at 15:16):

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

view this post on Zulip Paolo Giarrusso (Feb 13 2020 at 16:34):

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

view this post on Zulip vlj (Feb 13 2020 at 19:58):

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

view this post on Zulip vlj (Feb 13 2020 at 19:58):

In my case ord_enum and insubT worked

view this post on Zulip Paolo Giarrusso (Feb 13 2020 at 21:13):

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

view this post on Zulip vlj (Feb 14 2020 at 09:47):

It works with vscoq too

view this post on Zulip Paolo Giarrusso (Feb 14 2020 at 09:55):

No, it gets disabled after one line.

view this post on Zulip vlj (Feb 14 2020 at 11:33):

Ho I though it was the expected behavior :s

view this post on Zulip 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"

view this post on Zulip Paolo Giarrusso (Feb 14 2020 at 11:52):

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

view this post on Zulip Paolo Giarrusso (Feb 14 2020 at 11:52):

Ditto for all "display" options

view this post on Zulip Zhangsheng Lai (Feb 17 2020 at 01:10):

@Paolo G. Giarrusso vm_compute just freezes things up

view this post on Zulip vlj (Feb 18 2020 at 19:33):

Does auto work with mathcomp ?

view this post on Zulip 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 ?

view this post on Zulip Paolo Giarrusso (Feb 18 2020 at 19:44):

auto doesn’t rewrite; there’s autorewrite.

view this post on Zulip vlj (Feb 18 2020 at 19:44):

Yes

view this post on Zulip Paolo Giarrusso (Feb 18 2020 at 19:44):

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

view this post on Zulip vlj (Feb 18 2020 at 19:45):

It will work with mathcomp ?

view this post on Zulip vlj (Feb 18 2020 at 19:52):

It would act as a poor man lia in my case

view this post on Zulip 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

view this post on Zulip Paolo Giarrusso (Feb 18 2020 at 20:45):

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

view this post on Zulip 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)

view this post on Zulip Paolo Giarrusso (Feb 18 2020 at 20:47):

(And it cannot rewrite anymore)

view this post on Zulip 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 ?

view this post on Zulip vlj (Feb 18 2020 at 21:42):

seems to take forever though

view this post on Zulip vlj (Feb 18 2020 at 21:46):

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

view this post on Zulip Paolo Giarrusso (Feb 18 2020 at 21:59):

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

view this post on Zulip vlj (Feb 19 2020 at 11:59):

Hmmm yes it couldn't work

view this post on Zulip 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?

view this post on Zulip Emilio Jesús Gallego Arias (Mar 25 2020 at 04:27):

yes @Zhangsheng Lai

view this post on Zulip Emilio Jesús Gallego Arias (Mar 25 2020 at 04:28):

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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 25 2020 at 04:28):

done is

view this post on Zulip 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 ].

view this post on Zulip Emilio Jesús Gallego Arias (Mar 25 2020 at 04:31):

yup basically by [] is done

view this post on Zulip vlj (Mar 25 2020 at 18:11):

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

view this post on Zulip Cyril Cohen (Mar 25 2020 at 18:12):

@vlj /

view this post on Zulip vlj (Mar 25 2020 at 18:12):

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

view this post on Zulip vlj (Mar 25 2020 at 18:12):

do I have to import a scope ?

view this post on Zulip Cyril Cohen (Mar 25 2020 at 18:13):

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

view this post on Zulip Cyril Cohen (Mar 25 2020 at 18:13):

the notation comes from ssralg

view this post on Zulip vlj (Mar 25 2020 at 18:13):

ok

view this post on Zulip vlj (Mar 25 2020 at 18:14):

Module import is not transitive ?

view this post on Zulip Cyril Cohen (Mar 25 2020 at 18:15):

no

view this post on Zulip Cyril Cohen (Mar 25 2020 at 18:15):

Command Export is transitive

view this post on Zulip vlj (Mar 25 2020 at 18:17):

ok thanks

view this post on Zulip vlj (Mar 25 2020 at 22:06):

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

view this post on Zulip vlj (Mar 25 2020 at 22:06):

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

view this post on Zulip 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?

view this post on Zulip Pierre-Marie Pédrot (Mar 26 2020 at 17:34):

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

view this post on Zulip 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)

view this post on Zulip Cyril Cohen (Mar 26 2020 at 17:35):

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

view this post on Zulip vlj (Mar 26 2020 at 22:25):

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

view this post on Zulip vlj (Mar 26 2020 at 22:26):

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

view this post on Zulip vlj (Mar 26 2020 at 22:28):

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

view this post on Zulip vlj (Mar 29 2020 at 22:27):

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

view this post on Zulip 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 ?

view this post on Zulip vlj (Mar 29 2020 at 22:49):

Apparently there is Add Fields

view this post on Zulip Paolo Giarrusso (Mar 29 2020 at 22:58):

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

view this post on Zulip vlj (Mar 29 2020 at 22:59):

Thanks

view this post on Zulip vlj (Mar 29 2020 at 23:02):

Is there a mechanism to use lra with numFieldType ?

view this post on Zulip 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.

view this post on Zulip Paolo Giarrusso (Mar 29 2020 at 23:11):

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

view this post on Zulip Paolo Giarrusso (Mar 29 2020 at 23:16):

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

view this post on Zulip vlj (Mar 30 2020 at 07:06):

Err yes b=x

view this post on Zulip Paolo Giarrusso (Mar 30 2020 at 08:29):

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

view this post on Zulip vlj (Mar 30 2020 at 09:32):

yes sorry, I typed on my phone

view this post on Zulip 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

view this post on Zulip vlj (Mar 30 2020 at 17:45):

Actually I can use Reals

view this post on Zulip vlj (Mar 31 2020 at 18:06):

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

view this post on Zulip 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)"

view this post on Zulip 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 ?

view this post on Zulip vlj (Apr 05 2020 at 23:12):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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 ?

view this post on Zulip 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

view this post on Zulip vlj (Apr 06 2020 at 17:37):

ok

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip vlj (Apr 08 2020 at 16:50):

thanks, wil have a look at it

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Assia Mahboubi (Apr 15 2020 at 12:19):

@Cyril Cohen I do not understand your sentence.

view this post on Zulip 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?

view this post on Zulip 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))

view this post on Zulip Assia Mahboubi (Apr 15 2020 at 14:31):

Thanks.

view this post on Zulip Assia Mahboubi (Apr 15 2020 at 14:32):

or features we think must be merged ASAP.

view this post on Zulip Assia Mahboubi (Apr 15 2020 at 14:32):

I would even remove this case.

view this post on Zulip Assia Mahboubi (Apr 15 2020 at 14:32):

Freeze means feature freeze.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Assia Mahboubi (Apr 18 2020 at 05:59):

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

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip Cyril Cohen (Apr 18 2020 at 11:54):

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

view this post on Zulip vlj (Apr 18 2020 at 12:47):

Apply: findobj returns à other error ?

view this post on Zulip Zhangsheng Lai (Apr 18 2020 at 13:23):

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

view this post on Zulip 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

view this post on Zulip 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 ?

view this post on Zulip vlj (Apr 27 2020 at 17:41):

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

view this post on Zulip Reynald Affeldt (Apr 27 2020 at 18:26):

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

view this post on Zulip vlj (Apr 27 2020 at 18:26):

ok thanks

view this post on Zulip vlj (Apr 27 2020 at 18:26):

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

view this post on Zulip 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

view this post on Zulip vlj (Apr 27 2020 at 18:28):

without dichotomic search

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip Reynald Affeldt (Apr 27 2020 at 18:30):

Locate commutative. also

view this post on Zulip vlj (Apr 27 2020 at 18:30):

thanks

view this post on Zulip Enrico Tassi (Apr 27 2020 at 18:38):

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

view this post on Zulip vlj (Apr 27 2020 at 18:50):

Yes seems so

view this post on Zulip 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 ?

view this post on Zulip 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

view this post on Zulip 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:

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

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip Cyril Cohen (Apr 27 2020 at 20:50):

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

view this post on Zulip 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 ?

view this post on Zulip vlj (Apr 27 2020 at 20:50):

ok

view this post on Zulip 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

view this post on Zulip vlj (Apr 27 2020 at 20:52):

thanks

view this post on Zulip 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

view this post on Zulip vlj (Apr 28 2020 at 17:18):

thanks for the hint

view this post on Zulip vlj (Apr 28 2020 at 17:18):

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

view this post on Zulip 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: Aug 11 2022 at 01:03 UTC