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

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?

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

If this is the case, I can submit a PR

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

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

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…

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.

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`

.

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.

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

Yes, that would be great!

This is easy to do actually, as in the `mathcomp/mathcomp-dev`

images, the `coq-released`

repo is already available :)

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

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

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)

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

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

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?

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

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

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

ok

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

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

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

zmodType is like, Z / nZ ?

what is a telescope, is it a coq concept ?

`zmodType`

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

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`

.

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

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

Thanks for the info

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

(I didn't realize there was a link)

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

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?

Maybe thing needs to be countable but maybe not

I got it

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

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

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

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

:+1:

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?

I think it's because Finite.enum is opaque

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.

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

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

which you can prove by `unlocking`

`Finite.enum`

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

if you dig on the proofs you will see indeed that `Finite.enum`

is not opaque, but "locked"

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

I'm unsure what's the best reference for the `locked`

pattern, IIRC the documentation of the implementation was pretty good

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`

?

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`

?

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

`About CanChoiceMixin`

outputs:

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

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

`sT`

is the type you want to prove that can be embedded into `T`

, which is already a choicetype

then `f`

and `f'`

are the embedding and the projection functions respectively

so for example `T`

can be `nat`

bigop is opaque ?

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.

rewrite unlock is working well

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

I'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

yes @vlj , in general bigop is locked and the approach using `unlock`

is not going to scale well; I'd recommend a refinement-based setup such as the one provided by CoqEAL

coqEAL ?

installing it

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.

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

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

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

is there a publication on the subject ?

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

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

I'm trying to map `\sum`

to `foldr addn`

but I'm stuck with `ordinal`

and `nat`

interaction

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)

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

I'm not sure that `fun (x : ordinal n) (x0 : nat) => addn x x0`

is equal to `addn`

, it looks like there is some coercion happening but I don't know how to show it

actually it's trivially proven as a lemma

Yup, that's already proven.

rewrite unlock is working well

@vlj can I get your code to see how `rewrite unlock`

is used to make things transparent?

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

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

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

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

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

sorry, that *lock* is visible

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

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

@Zhangsheng Lai see above ^^

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.

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.

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

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

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

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

@Zhangsheng Lai have you tried `vm_compute`

? It does ignore some extra forms of opacity.

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

In my case ord_enum and insubT worked

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

It works with vscoq too

No, it gets disabled after one line.

Ho I though it was the expected behavior :s

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

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

Ditto for all "display" options

@Paolo G. Giarrusso `vm_compute`

just freezes things up

Does auto work with mathcomp ?

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 ?

auto doesn’t rewrite; there’s autorewrite.

Yes

(okay, `auto`

can use `Hint Extern`

which can use anything including rewrite)

It will work with mathcomp ?

It would act as a poor man lia in my case

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

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

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

(And it cannot rewrite anymore)

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

seems to take forever though

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

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

Hmmm yes it couldn't work

Is there any differences between the tactics `auto`

in coq and the tactic `by []`

available in mathcomp?

yes @Zhangsheng Lai

IIRC correctly `by []`

is equivalent to `done`

[let me double-check that]

done is

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

yup basically `by []`

is done

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

@vlj `/`

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

do I have to import a scope ?

you have to Import module `GRing.Theory`

and open scope `ring_scope`

.

the notation comes from ssralg

ok

Module import is not transitive ?

no

Command `Export`

is transitive

ok thanks

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

for instance

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

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?

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

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

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

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

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

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

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

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 ?

Apparently there is Add Fields

@vlj see also `lra`

(https://coq.inria.fr/refman/addendum/micromega.html)

Thanks

Is there a mechanism to use lra with numFieldType ?

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.

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

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

Err yes b=x

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

yes sorry, I typed on my phone

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

Actually I can use Reals

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

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

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 ?

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

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

@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

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 ?

@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

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

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

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

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.

thanks, wil have a look at it

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

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?

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

@Cyril Cohen I do not understand your sentence.

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

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.

or features we think must be merged ASAP.

I would even remove this case.

Freeze means feature freeze.

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.

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

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?

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

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

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

hi @Zhangsheng Lai what are `term1`

and `term2`

in your example?

Apply: findobj returns à other error ?

`term1`

is just a record type constructor, `term2`

is what I have above

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`

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

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

ok thanks

btw do you know where `commutative`

is defined ? I'm trying to use it

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

without dichotomic search

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

```
From mathcomp Require Import all_ssreflect.
About commutative.
```

This should output the module you are looking for.

`Locate commutative.`

also

thanks

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

Yes seems so

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

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

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

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

decidability of equality on `T`

does not matter in this setting.

but `{mono f: x y / x <= y}`

is defined for function on R or is it defined for anything that can be compared ?

ok

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

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

thanks for the hint

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

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: Sep 30 2023 at 15:01 UTC