imported from gitter room math-comp/math-comp · math-comp devs

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

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

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

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

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

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.

vlj (Jan 05 2020 at 21:32):

vlj (Jan 05 2020 at 21:33):

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.

vlj (Jan 05 2020 at 22:04):

vlj (Jan 05 2020 at 22:06):

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

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

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

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

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

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.

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

vlj (Jan 30 2020 at 22:30):

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

Anton Trunov (Jan 31 2020 at 16:39):

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

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

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

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

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

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

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

vlj (Feb 08 2020 at 22:51):

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

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

vlj (Feb 09 2020 at 00:13):

vlj (Feb 09 2020 at 00:20):

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

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.

vlj (Feb 09 2020 at 00:47):

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

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

vlj (Feb 09 2020 at 20:37):

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

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

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

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

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

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

vlj (Feb 12 2020 at 19:06):

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

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

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

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

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

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

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

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

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

vlj (Feb 14 2020 at 11:33):

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

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

vlj (Feb 18 2020 at 19:33):

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

vlj (Feb 18 2020 at 19:44):

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

vlj (Feb 18 2020 at 19:45):

vlj (Feb 18 2020 at 19:52):

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

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

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

vlj (Feb 18 2020 at 21:46):

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

vlj (Feb 19 2020 at 11:59):

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

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

vlj (Mar 25 2020 at 18:11):

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

vlj (Mar 25 2020 at 18:12):

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

vlj (Mar 25 2020 at 18:13):

vlj (Mar 25 2020 at 18:14):

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

vlj (Mar 25 2020 at 18:17):

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

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

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

vlj (Mar 26 2020 at 22:25):

vlj (Mar 26 2020 at 22:26):

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

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

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

vlj (Mar 29 2020 at 22:59):

vlj (Mar 29 2020 at 23:02):

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

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

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

vlj (Mar 30 2020 at 07:06):

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

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

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

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

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

vlj (Apr 06 2020 at 17:37):

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

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

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

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

Assia Mahboubi (Apr 15 2020 at 14:31):

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

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

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

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

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

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

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

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

vlj (Apr 18 2020 at 12:47):

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

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

vlj (Apr 27 2020 at 18:26):

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

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.

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

vlj (Apr 27 2020 at 18:30):

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

vlj (Apr 27 2020 at 18:50):

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

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

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 ?

vlj (Apr 27 2020 at 20:50):

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

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

vlj (Apr 27 2020 at 20:52):

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

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

Stream: math-comp devs

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

vlj (Jan 02 2020 at 17:17):

vlj (Jan 02 2020 at 17:18):

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

vlj (Jan 05 2020 at 21:00):

vlj (Jan 05 2020 at 21:01):

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

vlj (Jan 05 2020 at 21:32):

vlj (Jan 05 2020 at 21:33):

vlj (Jan 05 2020 at 21:33):

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

vlj (Jan 05 2020 at 22:04):

vlj (Jan 05 2020 at 22:04):

vlj (Jan 05 2020 at 22:06):

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

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

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

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

vlj (Jan 06 2020 at 07:55):

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

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

vlj (Jan 09 2020 at 19:45):

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

vlj (Jan 30 2020 at 22:30):

vlj (Jan 31 2020 at 15:31):

vlj (Jan 31 2020 at 15:31):

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

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

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

Anton Trunov (Jan 31 2020 at 16:39):

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

vlj (Feb 02 2020 at 18:17):

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

vlj (Feb 02 2020 at 18:20):

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

vlj (Feb 08 2020 at 22:51):

vlj (Feb 08 2020 at 22:52):

vlj (Feb 08 2020 at 22:56):

vlj (Feb 08 2020 at 23:58):

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

vlj (Feb 09 2020 at 00:13):

vlj (Feb 09 2020 at 00:20):

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

vlj (Feb 09 2020 at 00:31):

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

vlj (Feb 09 2020 at 00:47):

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

vlj (Feb 09 2020 at 00:51):

vlj (Feb 09 2020 at 00:51):