Stream: math-comp devs

Topic: Github Notifications


view this post on Zulip Mathcomp Github Bot (May 08 2020 at 22:20):

CohenCyril milestoned Issue #501 Intro pattern extensions for rewrite, dup, swap and apply (assigned to gares):

Motivation for this change

Intro pattern ltac views (rewrite, dup, swap, apply)

- calling rewrite from an intro pattern, use with parsimony
=> /[1 rules] does rewrite rules
=> /[-1 rules] does rewrite rules
=> /[! rules] does rewrite rules
=> /[-! rules] does rewrite rules
=> /[? rules] does rewrite rules
=> /[-? rules] does rewrite rules
=> /[/def] does rewrite /def

- top of the stack actions:
=> /apply does => hyp {}/hyp
=> /swap does => x y; move: y x (also swap and perserves let bindings)
=> /dup does => x; have copy := x; move: copy x (also copies and preserves let bindings)

This is a part of #372, simplified, rewritten and rebased.

Things done/to do

<!-- please fill in the following checklist -->

<!-- Cross-out the above items using ~crossed out item~ if they happen not to be relevent -->
<!-- You may also add more items to explain what you did and what remains to do -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (May 08 2020 at 22:20):

CohenCyril assigned PR #501 Intro pattern extensions for rewrite, dup, swap and apply to gares.

view this post on Zulip Mathcomp Github Bot (May 08 2020 at 22:20):

CohenCyril opened PR #501 Intro pattern extensions for rewrite, dup, swap and apply (assigned to gares) from intro_rw to master:

Motivation for this change

Intro pattern ltac views (rewrite, dup, swap, apply)

- calling rewrite from an intro pattern, use with parsimony
=> /[1 rules] does rewrite rules
=> /[-1 rules] does rewrite rules
=> /[! rules] does rewrite rules
=> /[-! rules] does rewrite rules
=> /[? rules] does rewrite rules
=> /[-? rules] does rewrite rules
=> /[/def] does rewrite /def

- top of the stack actions:
=> /apply does => hyp {}/hyp
=> /swap does => x y; move: y x (also swap and perserves let bindings)
=> /dup does => x; have copy := x; move: copy x (also copies and preserves let bindings)

This is a part of #372, simplified, rewritten and rebased.

Things done/to do

<!-- please fill in the following checklist -->

<!-- Cross-out the above items using ~crossed out item~ if they happen not to be relevent -->
<!-- You may also add more items to explain what you did and what remains to do -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (May 08 2020 at 22:20):

CohenCyril edited PR #501 Intro pattern extensions for rewrite, dup, swap and apply (assigned to gares) from intro_rw to master:

Motivation for this change

Intro pattern ltac views (rewrite, dup, swap, apply) in order not to break intro patterns for silly rewrites.

- calling rewrite from an intro pattern, use with parsimony
=> /[1 rules] does rewrite rules
=> /[-1 rules] does rewrite rules
=> /[! rules] does rewrite rules
=> /[-! rules] does rewrite rules
=> /[? rules] does rewrite rules
=> /[-? rules] does rewrite rules
=> /[/def] does rewrite /def

- top of the stack actions:
=> /apply does => hyp {}/hyp
=> /swap does => x y; move: y x (also swap and perserves let bindings)
=> /dup does => x; have copy := x; move: copy x (also copies and preserves let bindings)

This is a part of #372, simplified, rewritten and rebased.

Things done/to do

<!-- please fill in the following checklist -->

<!-- Cross-out the above items using ~crossed out item~ if they happen not to be relevent -->
<!-- You may also add more items to explain what you did and what remains to do -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (May 08 2020 at 22:38):

CohenCyril updated PR #501 Intro pattern extensions for rewrite, dup, swap and apply (assigned to gares) from intro_rw to master:

Motivation for this change

Intro pattern ltac views (rewrite, dup, swap, apply) in order not to break intro patterns for silly rewrites.

- calling rewrite from an intro pattern, use with parsimony
=> /[1 rules] does rewrite rules
=> /[-1 rules] does rewrite rules
=> /[! rules] does rewrite rules
=> /[-! rules] does rewrite rules
=> /[? rules] does rewrite rules
=> /[-? rules] does rewrite rules
=> /[/def] does rewrite /def

- top of the stack actions:
=> /apply does => hyp {}/hyp
=> /swap does => x y; move: y x (also swap and perserves let bindings)
=> /dup does => x; have copy := x; move: copy x (also copies and preserves let bindings)

This is a part of #372, simplified, rewritten and rebased.

Things done/to do

<!-- please fill in the following checklist -->

<!-- Cross-out the above items using ~crossed out item~ if they happen not to be relevent -->
<!-- You may also add more items to explain what you did and what remains to do -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (May 08 2020 at 22:46):

CohenCyril updated PR #501 Intro pattern extensions for rewrite, dup, swap and apply (assigned to gares) from intro_rw to master:

Motivation for this change

Intro pattern ltac views (rewrite, dup, swap, apply) in order not to break intro patterns for silly rewrites.

- calling rewrite from an intro pattern, use with parsimony
=> /[1 rules] does rewrite rules
=> /[-1 rules] does rewrite rules
=> /[! rules] does rewrite rules
=> /[-! rules] does rewrite rules
=> /[? rules] does rewrite rules
=> /[-? rules] does rewrite rules
=> /[/def] does rewrite /def

- top of the stack actions:
=> /apply does => hyp {}/hyp
=> /swap does => x y; move: y x (also swap and perserves let bindings)
=> /dup does => x; have copy := x; move: copy x (also copies and preserves let bindings)

This is a part of #372, simplified, rewritten and rebased.

Things done/to do

<!-- please fill in the following checklist -->

<!-- Cross-out the above items using ~crossed out item~ if they happen not to be relevent -->
<!-- You may also add more items to explain what you did and what remains to do -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (May 08 2020 at 22:50):

CohenCyril opened PR #502 Intro discharge subst from intro_discharge_subst to master:

Motivation for this change

Adding to intro pattern: discharge in and rewrite in.
Working syntax /[: x @y z], (limited to three variables)
and /[-> in x0 .. x6], and /[<- in x0 .. x6] (limited to seven variables).

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (May 08 2020 at 22:53):

CohenCyril edited PR #502 Intro discharge subst from intro_discharge_subst to master:

Motivation for this change

Adding to intro pattern: discharge in and rewrite in.
Working syntax /[: x @y z], (limited to three variables)
and /[-> in x0 .. x6], and /[<- in x0 .. x6] (limited to seven variables).

(This is another simplified part of #377, and sequel of #501)

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (May 08 2020 at 22:53):

CohenCyril edited PR #502 Intro discharge subst from intro_discharge_subst to master:

Motivation for this change

Adding to intro pattern: discharge in and rewrite in.
Working syntax /[: x @y z], (limited to three variables)
and /[-> in x0 .. x6], and /[<- in x0 .. x6] (limited to seven variables).

(This is a sequel of #501, which should close #372)

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (May 09 2020 at 14:12):

amahboubi:

view this post on Zulip Mathcomp Github Bot (May 09 2020 at 21:53):

CohenCyril edited PR #501 Intro pattern extensions for rewrite, dup, swap and apply (assigned to gares) from intro_rw to master:

Motivation for this change

Intro pattern ltac views (rewrite, dup, swap, apply) in order not to break intro patterns for silly rewrites.

- calling rewrite from an intro pattern, use with parsimony
=> /[1 rules] does rewrite rules
=> /[-1 rules] does rewrite -rules
=> /[! rules] does rewrite !rules
=> /[-! rules] does rewrite -!rules
=> /[? rules] does rewrite ?rules
=> /[-? rules] does rewrite -?rules
=> /[/def] does rewrite /def

- top of the stack actions:
=> /apply does => hyp {}/hyp
=> /swap does => x y; move: y x (also swap and perserves let bindings)
=> /dup does => x; have copy := x; move: copy x (also copies and preserves let bindings)

This is a part of #372, simplified, rewritten and rebased.

Things done/to do

<!-- please fill in the following checklist -->

<!-- Cross-out the above items using ~crossed out item~ if they happen not to be relevent -->
<!-- You may also add more items to explain what you did and what remains to do -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (May 11 2020 at 12:08):

CohenCyril:

view this post on Zulip Mathcomp Github Bot (May 11 2020 at 13:03):

chdoc opened PR #503 closed/closure for non-symmetric relations from fix-closure to master:

Motivation for this change

Adapt the definitions of closed and closure so that they apply to general relations (i.e., those for which connect_sym does not hold.

Resolves #466

Observation: for mathcomp, no changes are required outside of fingraph.v.

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (May 13 2020 at 04:39):

pi8027 opened PR #504 Revise proofs in ssreflect/*.v from selectors to master:

Motivation for this change

<!-- please explain your reason for doing this change -->

This PR reduces

and improves use of comparison predicates such as posnP, leqP, ltnP, ltngtP, and eqVneq.

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (May 13 2020 at 05:09):

pi8027 updated PR #504 Revise proofs in ssreflect/*.v from selectors to master:

Motivation for this change

<!-- please explain your reason for doing this change -->

This PR reduces

and improves use of comparison predicates such as posnP, leqP, ltnP, ltngtP, and eqVneq.

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (May 13 2020 at 08:40):

MrSet opened Issue #505 Suggestions for various additions to seq.v, ssrnat.v and order.v:

Hi,
I have been using math-comp for a while and have by doing so created a few lemmas which I thought might be useful for others than just me.

I would like opinions on if you think that some of the Lemmas should be submitted in a PR. Before submitting such a PR I will, of course, try to make the naming-conventions and phrasings adhere to the contributing.md specifications. I have excluded proofs as I for the moment being only are interested in knowing whether you find the lemmas relevant or not.

It might very well be that some of the content already is and math-comp and I simply have not been able to locate it. Any comments/suggestions are welcome!

Suggestions for seq.v

Addition of a find-first-option function

I suggest to add the following function to seq.v as right now there is only an indexing function to get the first element that fullfills a predicate from a list. Also, this function ensures that it is actually the first element that fulfills the predicate that is returned (i have founds this useful for constructing proofs).

Fixpoint findo {T : Type} (p : ssrbool.pred T) (s : seq T) :=
  if s is x :: xs then if p x then Some x else findo p xs else None.

Lemma findo_has {T : Type} (p : ssrbool.pred T) (s : seq T) :
  ((findo p s) : bool) = has p s.

Lemma perm_findo {T : eqType} (p : ssrbool.pred T) (s1 s2  : seq T):
  perm_eq s1 s2 -> (findo p s1 : bool) = (findo p s2 : bool).

Lemma mem_findo {T : eqType} (p : ssrbool.pred T) (s1 s2  : seq T):
  s1 =i s2 -> (findo p s1 : bool) = (findo p s2 : bool).

Lemma findoP {T : eqType} (p : ssrbool.pred T) (s : seq T) (x : T):
  reflect
    (exists s1 s2, s1 ++ [:: x] ++ s2 = s /\ p x /\ all (predC p) s1)
    ((Some x) == (findo p s)).

Lemma findo_pred  {T : eqType} (p : ssrbool.pred T) (s : seq T) (x : T) :
  (findo p s) = Some x -> p x.

Lemma findo_mem {T : eqType} (p : ssrbool.pred T) (s : seq T) (x : T) :
  Some x = findo p s -> x \in s.

Also I suggest to add an function that finds the last element of a list that satisfies some predicate.

Definition rfindo {T : Type} (p : ssrbool.pred T) (s : seq T) :=
  findo p (rev s).

Lemma rfindo_has {T : Type} (p : ssrbool.pred T) (s : seq T) :
  ((rfindo p s) : bool) = has p s.

Lemma rfindoP {T : Type} (p : ssrbool.pred T) (s : seq T) :
  reflect
    (exists s1 s2 x, s1 ++ [:: x] ++ s2 = s /\ p x /\ all (predC p) s2)
    (rfindo p s).

Subset lemmas

Lemma subset_trans {T : eqType} (s1 s2 s3  : seq T) :
  {subset s1 <= s2} -> {subset s2 <= s3} -> {subset s1 <= s3}.

Lemma subset_all {T : eqType} p (s1 s2 : seq T) :
  {subset s1 <= s2} -> all p s2 -> all p s1.

Lemma subset_cons {T : eqType} (s: seq T) (x : T):
  {subset s <= x:: s}.

Lemma subset_cons2 {T : eqType} (s1 s2: seq T) (x : T):
  {subset s1 <= s2} -> {subset x::s1 <= x:: s2}.

Lemma subset_catl {T : eqType} (s s': seq T):
  {subset s <= s' ++ s}.

Lemma subset_catr {T : eqType} (s s': seq T):
  {subset s <= s' ++ s}.

Lemma subset_cat2 {T : eqType} (s1 s2 s3: seq T):
  {subset s1 <= s2} -> {subset s3 ++ s1 <= s3 ++ s2}.

Lemma filter_subset {T : eqType} p (s : seq T) :
  {subset [seq a <- s | p a] <= s}.

Lemma subset_filter {T : eqType} p (s1 s2 : seq T) :
  {subset s1 <= s2} -> {subset [seq a <- s1 | p a] <= [seq a <- s2 | p a]}.

Lemma map_subset {T1 T2 : eqType} (s1 s2 : seq T1) (f : T1 -> T2) :
  {subset s1 <= s2} -> {subset [seq f x | x <- s1 ] <= [seq f x | x <- s2]}.

Membership equality

Lemma map_mem_eq  {T A : eqType} (f : T -> A) (s1 s2 : seq T) :
  s1 =i s2 -> [seq f a | a <- s1 ] =i [seq f a | a <- s2].

Lemma filter_mem_eq {T : eqType} p (s1 s2 : seq T) :
  s1 =i s2 -> [seq a <- s1 | p a] =i [seq a <- s2 | p a].

Various

All of these are fairly obvious but is handy to have when proving other stuff.

Lemma inP {T : eqType} (s : seq T) a :
  reflect (exists s' s'', s = s' ++ (a :: s'')) (a \in s).

Lemma map_map {A B C : Type} (f : A -> B) (g : B -> C) (s : seq A):
  [seq g x | x <- [seq f x | x <- s] ] = [seq g (f x) | x <- s].

Lemma cat_injr {T : Type} (s : seq T) : injective (cat s).

Lemma cat_injl {T : Type} (s : seq T) : injective (cat^~ s).

Lemma ohead_cat_some {T : Type} (a b : seq T) x :
  ohead a = Some x -> ohead a = ohead (a ++ b).

Lemma all_count0 {T: Type} (p : ssrbool.pred T) (s : seq T):
  count p s == 0 = all (predC p) s.

Lemma perm_rem {T : eqType} (x : T) (s1 s2 : seq T) :
  perm_eq s1 s2 -> perm_eq (rem x s1) (rem x s2).

Suggestions for ssrnat.v

These follow immediately by the corresponding lemmas for ltn, but I find them use to have specialized as these can easier be found by searching.

Lemma gtn_trans : transitive gtn.
Lemma gtn_irr : irreflexive gtn.

Also: Is there any reason why the irreflextivity lemma of ltn is named ltnn and does not use the irreflexive construction?

I also wondered if the following should be provided:

Lemma addn_injl n: injective (addn^~ n).
Lemma addn_injr n: injective (addn n).

I also wondered why there is a lemma called leq_ltn_trans but not the symmetric one:

Lemma ltn_leq_trans n m p : m < n -> n <= p -> m < p.

Suggestions for order.v

I have also my self found it useful to have sequences of equality types as a meet-semi-lattice, ordered by the suffix-relation and with longest-common-suffix as meet.

In general, I think that is reasonable to include the suffix predicate in seq.v (excluding the notation)?

Fixpoint suffix {T : eqType} (s1 s2 : seq T) : bool :=
  (s1 == s2) ||  if s2 is (x :: xs)
                then suffix s1 xs
                else false.

Lemma suffix_rec {T : eqType} (s1 s2 : seq T) : suffix s1 s2 = (s1 == s2) || suffix s1 s2.

Notation "a ⪯ b" := (suffix a b) (at level 20).

Lemma suffix_refl {T : eqType} : reflexive (@suffix T).

Lemma suffixP {T : eqType} (s1 s2 : seq T) :
  reflect (exists xs, xs ++ s1 = s2) (s1  s2).

Lemma suffix_catl {T : eqType} (xs ys : seq T) :  xs  (ys ++ xs).

Lemma suffix_trans {T : eqType} : transitive (@suffix T).

Lemma suffix_anti {T : eqType} : antisymmetric (@suffix T).

Lemma suffix_nil {T : eqType} (s : seq T) : [::]  s.

Fixpoint lcs {T : eqType} (s1 s2 : seq T) : seq T :=
  if s1  s2
  then s1
  else if s1 is x :: xs
       then lcs xs s2
       else [::].

Lemma lcs_suffix {T : eqType} (s1 s2 : seq T) :
  lcs s1 s2  s1 && lcs s1 s2  s2.

Lemma lcsP {T : eqType} (s s1 s2 : seq T) :
  s  s1 && s  s2 = s  lcs s1 s2.

Lemma lcsC {T : eqType} : commutative (@lcs T).

Lemma lcsA {T : eqType} : associative (@lcs T).

Lemma lcsss {T : eqType} : idempotent (@lcs T).

Should I suggest this to #464 or make it a separate PR?

Random

I often find my self trying to prove a goal of the form: (true -> B) -> A, where it somehow follows from the context that B -> A. In these situations, I find it useful to use the following lemma instead of doing move/(_ (eq_refl true)) to get rid of the true.

Lemma trueI (A : Type) : (true -> A) -> A.

Also: I needed the following at some point and couldn't find it:

Lemma predIC {T : Type} (p1 p2 : ssrbool.pred T):
  predI p1 p2 =1 predI p2 p1.

view this post on Zulip Mathcomp Github Bot (May 13 2020 at 12:58):

CohenCyril:

view this post on Zulip Mathcomp Github Bot (May 13 2020 at 14:26):

anton-trunov opened PR #506 ssrnat: add subnA, addnCB, addnCAC, addnAl lemmas from ssrnat-extra-assoc-lemmas to master:

Motivation for this change

This PR addresses issue #212 by adding some lemmas about natural numbers.

I find addnCAC and addnAl sometimes convenient because having them in the library might save several rewrites once in a while.

I'm open to suggestions (including removing some of this PR's lemmas altogether). Thank you for your time.

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (May 13 2020 at 14:30):

anton-trunov edited PR #506 ssrnat: add subnA, addnCB, addnCAC, addnAl lemmas from ssrnat-extra-assoc-lemmas to master:

Motivation for this change

This PR addresses issue #212 by adding some lemmas about natural numbers.

I find addnCAC and addnAl sometimes convenient because having them in the library might save several rewrites once in a while.

I'm open to suggestions (including removing some of this PR's lemmas altogether). Thank you for your time.

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (May 13 2020 at 14:31):

pi8027 opened PR #507 Add more test cases for higher-order recursive functions in seq.v w.r.t. the guard condition from test-guard-cond to master:

Motivation for this change

This PR adds some test cases in test_suite/test_guard.v which I promised to do in https://github.com/math-comp/math-comp/pull/471#issuecomment-611521366.

<!-- please explain your reason for doing this change -->

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (May 13 2020 at 18:03):

pi8027 edited PR #507 Add more test cases for higher-order recursive functions in seq.v w.r.t. the guard condition from test-guard-cond to master:

Motivation for this change

This PR adds some test cases in test_suite/test_guard.v which I promised to do in https://github.com/math-comp/math-comp/pull/471#issuecomment-611521366. Currently, test cases for find, filter, count, pmap, pairmap, scanl are missing.

<!-- please explain your reason for doing this change -->

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (May 14 2020 at 16:04):

chdoc opened Issue #508 mem_imset mem_map naming/statement inconsistency:

while cleaning, I noticed the following oddity:

Lemma mem_imset (aT rT : finType) (f : aT -> rT) (D : {pred aT}) (x : aT) :
  x \in D -> f x \in [set f x | x in D]

Lemma map_f (T1 T2 : eqType) (f : T1 -> T2) (s : seq T1) (x : T1) :
   x \in s -> f x \in [seq f i | i <- s]
Lemma mem_map (T1 T2 : eqType) (f : T1 -> T2),
  injective f -> forall (s : seq T1) (x : T1), (f x \in [seq f i | i <- s]) = (x \in s)

Wouldn't it be more consistent to rename mem_imset to imset_f and add the following lemma:

Lemma mem_imset (aT rT : finType) (f : aT -> rT) (A : {set aT}) (x : aT) :
  injective f -> (f x \in f @: A) = (x \in A).

view this post on Zulip Mathcomp Github Bot (May 14 2020 at 18:12):

chdoc opened PR #509 Card lemmas from card-lemmas to master:

Motivation for this change

Additional lemmas about cardinalities of predicates and sets. Mainly picking n distinct elements for an a predicate with n <= #|A|.

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (May 14 2020 at 20:22):

CohenCyril submitted PR Review for #509 Card lemmas.

view this post on Zulip Mathcomp Github Bot (May 14 2020 at 20:22):

CohenCyril created PR Review Comment on #509 Card lemmas:

In thought I did that one when I added fintype_le1P tomorrow. :laughing: I will double check tomorrow, if I forgot to push something.

view this post on Zulip Mathcomp Github Bot (May 14 2020 at 20:28):

CohenCyril submitted PR Review for #509 Card lemmas.

view this post on Zulip Mathcomp Github Bot (May 14 2020 at 20:28):

CohenCyril created PR Review Comment on #509 Card lemmas:

Nice one to have indeed, I think there is a lot of refactoring to do with all the card_* lemma you added, through enum (which is uniq which size is the cardinal of the considered set). Indeed, I think card_eqP would be almost a one liner and card_geqP, and cards2P is a simple twice case analysis (the main step being something like case: (enum A) (enum_uniq A) (size_enum ...) => [|x [|y []//]; exists x; exists y). I also think it would be nice to have le/lt variants and pred` variants.

view this post on Zulip Mathcomp Github Bot (May 14 2020 at 20:28):

CohenCyril edited PR Review Comment on #509 Card lemmas.

view this post on Zulip Mathcomp Github Bot (May 14 2020 at 20:29):

CohenCyril edited PR Review Comment on #509 Card lemmas.

view this post on Zulip Mathcomp Github Bot (May 14 2020 at 20:29):

CohenCyril edited PR Review Comment on #509 Card lemmas.

view this post on Zulip Mathcomp Github Bot (May 14 2020 at 20:30):

CohenCyril edited PR Review Comment on #509 Card lemmas.

view this post on Zulip Mathcomp Github Bot (May 15 2020 at 00:55):

CohenCyril opened Issue #510 Filling as many holes as convenient for lemma composition:

Hi @math-comp/core, @pi8027, @chdoc, @erikmd, @anton-trunov and everyone else (sorry for my non-exhaustivity)...

When combining lemmas in a high-order way, (e.g. can_inj, le_trans, ...) the leafs of the term that I build are often of the form (my_thm _ _ _ _), which makes it harder to read and write: my personal methodology varies from About to "wildguessing and adjusting". The nice exceptions are some well adjusted reflect lemmas, which often have all arguments but reflect hypotheses as maximal implicits, which means they can either be used combined with other reflect (as such), or used as a simple implication (by performing a single application without @).

I was wondering if we could deal with cancel, inequalities and the like in some way... Since we sometimes need to provide arguments and sometimes not, we cannot simply put everything as maximal implicits. So what about using a symbol, let's say % for the example, to denote _"fill as many holes as needed if I am going to compose"_?
That way,

  1. A simple implementation that comes to mind with Notation will naturally impose that in such cases we always need the same number of filled holes... which may be a good enough approximation?
    I this case I am still wondering how we could do that without adding manually Notation "%stuff" = (@stuff _ _ _). everywhere in the library (maybe an attribute?).

  2. Another (more robust?) implementation would be to modify Coq's pretyper...

Does someone have other ideas that would solve the same problem? (Both in terms of specification or implementation of this issue.)

view this post on Zulip Mathcomp Github Bot (May 15 2020 at 00:56):

CohenCyril edited Issue #510 Filling as many holes as convenient for lemma composition:

Hi @math-comp/core, @pi8027, @chdoc, @erikmd, @anton-trunov and everyone else (sorry for my non-exhaustivity)...

When combining lemmas in a high-order way, (e.g. can_inj, le_trans, ...) the leafs of the term that I build are often of the form (my_thm _ _ _ _), which makes it hard to read and write: my personal methodology varies from About to "wildguessing and adjusting". The nice exceptions are some well adjusted reflect lemmas, which often have all arguments but reflect hypotheses as maximal implicits, which means they can either be used combined with other reflect (as such), or used as a simple implication (by performing a single application without @).

I was wondering if we could deal with cancel, inequalities and the like in some way... Since we sometimes need to provide arguments and sometimes not, we cannot simply put everything as maximal implicits. So what about using a symbol, let's say % for the example, to denote _"fill as many holes as needed if I am going to compose"_?
That way,

  1. A simple implementation that comes to mind with Notation will naturally impose that in such cases we always need the same number of filled holes... which may be a good enough approximation?
    I this case I am still wondering how we could do that without adding manually Notation "%stuff" = (@stuff _ _ _). everywhere in the library (maybe an attribute?).

  2. Another (more robust?) implementation would be to modify Coq's pretyper...

Does someone have other ideas that would solve the same problem? (Both in terms of specification or implementation of this issue.)

view this post on Zulip Mathcomp Github Bot (May 15 2020 at 00:56):

CohenCyril edited Issue #510 Filling as many holes as convenient for lemma composition:

Hi @math-comp/core, @pi8027, @chdoc, @erikmd, @anton-trunov and everyone else (sorry for my non-exhaustivity)...

When combining lemmas in a high-order way, (e.g. can_inj, le_trans, ...) the leafs of the term that I build are often of the form (my_thm _ _ _ _), which makes it hard to read and write: my personal methodology varies from About to "wildguessing and adjusting". The nice exceptions are some well adjusted reflect lemmas, which often have all arguments but reflect hypotheses as maximal implicits, which means they can either be combined with other reflect (as such), or used as a simple implication (by performing a single application without @).

I was wondering if we could deal with cancel, inequalities and the like in some way... Since we sometimes need to provide arguments and sometimes not, we cannot simply put everything as maximal implicits. So what about using a symbol, let's say % for the example, to denote _"fill as many holes as needed if I am going to compose"_?
That way,

  1. A simple implementation that comes to mind with Notation will naturally impose that in such cases we always need the same number of filled holes... which may be a good enough approximation?
    I this case I am still wondering how we could do that without adding manually Notation "%stuff" = (@stuff _ _ _). everywhere in the library (maybe an attribute?).

  2. Another (more robust?) implementation would be to modify Coq's pretyper...

Does someone have other ideas that would solve the same problem? (Both in terms of specification or implementation of this issue.)

view this post on Zulip Mathcomp Github Bot (May 15 2020 at 00:57):

CohenCyril edited Issue #510 Filling as many holes as convenient for lemma composition:

Hi @math-comp/core, @pi8027, @chdoc, @erikmd, @anton-trunov and everyone else (sorry for my non-exhaustivity)...

When combining lemmas in a high-order way, (e.g. can_inj, le_trans, ...) the leafs of the term that I build are often of the form (my_thm _ _ _ _), which makes it hard to read and write: my personal methodology varies from About to "wildguessing and adjusting". The nice exceptions are some well adjusted reflect lemmas, which often have all arguments but reflect hypotheses as maximal implicits, which means they can either be combined with other reflect (as such), or used as a simple implication (by performing a single application without @).

I was wondering if we could deal with cancel, inequalities and the like in some way... Since we sometimes need to provide arguments and sometimes not, we cannot simply put everything as maximal implicits. So what about using a symbol, let's say % for the example, to denote _"fill as many holes as needed if I am going to compose"_?
That way,

Now

  1. A simple implementation that comes to mind with Notation will naturally impose that in such cases we always need the same number of filled holes... which may be a good enough approximation?
    I this case I am still wondering how we could do that without adding manually Notation "%stuff" = (@stuff _ _ _). everywhere in the library (maybe an attribute?).

  2. Another (more robust?) implementation would be to modify Coq's pretyper...

Does someone have other ideas that would solve the same problem? (Both in terms of specification or implementation of this issue.)

view this post on Zulip Mathcomp Github Bot (May 15 2020 at 00:57):

CohenCyril edited Issue #510 Filling as many holes as convenient for lemma composition:

Hi @math-comp/core, @pi8027, @chdoc, @erikmd, @anton-trunov and everyone else (sorry for my non-exhaustivity)...

When combining lemmas in a high-order way, (e.g. can_inj, le_trans, ...) the leafs of the term that I build are often of the form (my_thm _ _ _ _), which makes it hard to read and write: my personal methodology varies from About to "wildguessing and adjusting". The nice exceptions are some well adjusted reflect lemmas, which often have all arguments but reflect hypotheses as maximal implicits, which means they can either be combined with other reflect (as such), or used as a simple implication (by performing a single application without @).

I was wondering if we could deal with cancel, inequalities and the like in some way... Since we sometimes need to provide arguments and sometimes not, we cannot simply put everything as maximal implicits. So what about using a symbol, let's say % for the example, to denote _"fill as many holes as needed if I am going to compose"_?
That way,

Implementation-wise,

  1. A simple implementation that comes to mind with Notation will naturally impose that in such cases we always need the same number of filled holes... which may be a good enough approximation?
    I this case I am still wondering how we could do that without adding manually Notation "%stuff" = (@stuff _ _ _). everywhere in the library (maybe an attribute?).

  2. Another (more robust?) implementation would be to modify Coq's pretyper...

Does someone have other ideas that would solve the same problem? (Both in terms of specification or implementation of this issue.)

view this post on Zulip Mathcomp Github Bot (May 15 2020 at 01:26):

CohenCyril opened PR #511 adding default nix shell from nix to master:

Motivation for this change

Adding a default nix-shell.

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (May 15 2020 at 02:34):

CohenCyril edited Issue #510 Filling as many holes as convenient for lemma composition:

Hi @math-comp/core, @pi8027, @chdoc, @erikmd, @anton-trunov and everyone else (sorry for my non-exhaustivity)...

When combining lemmas in a high-order way, (e.g. can_inj, le_trans, ...) the leafs of the term that I build are often of the form (my_thm _ _ _ _), which makes it hard to read and write: my personal methodology varies from About to "wildguessing and adjusting". The nice exceptions are some well adjusted reflect lemmas, which often have all arguments but reflect hypotheses as maximal implicits, which means they can either be combined with other reflect (as such), or used as a simple implication (by performing a single application without @).

I was wondering if we could deal with cancel, inequalities and the like in some way... Since we sometimes need to provide arguments and sometimes not, we cannot simply put everything as maximal implicits. So what about using a symbol, let's say % for the example, to denote _"fill as many holes as needed if I am going to compose"_?
That way,

Implementation-wise,

  1. A simple implementation that comes to mind with Notation will naturally impose that in such cases we always need the same number of filled holes... which may be a good enough approximation?
    I this case I am still wondering how we could do that without adding manually Notation "%stuff" = (@stuff _ _ _). everywhere in the library (maybe an attribute?).

  2. Another (more robust?) implementation would be to modify Coq's pretyper...

Does someone have other ideas that would solve the same problem? (Both in terms of specification or implementation of this issue.)

view this post on Zulip Mathcomp Github Bot (May 15 2020 at 07:34):

affeldt-aist requested affeldt-aist for a review on PR #504 Revise proofs in ssreflect/*.v.

view this post on Zulip Mathcomp Github Bot (May 15 2020 at 07:35):

ybertot requested ybertot for a review on PR #504 Revise proofs in ssreflect/*.v.

view this post on Zulip Mathcomp Github Bot (May 15 2020 at 07:35):

affeldt-aist requested ybertot and affeldt-aist for a review on PR #504 Revise proofs in ssreflect/*.v.

view this post on Zulip Mathcomp Github Bot (May 15 2020 at 07:35):

affeldt-aist assigned PR #504 Revise proofs in ssreflect/*.v.

view this post on Zulip Mathcomp Github Bot (May 15 2020 at 07:36):

affeldt-aist milestoned Issue #504 Revise proofs in ssreflect/*.v (assigned to affeldt-aist):

Motivation for this change

<!-- please explain your reason for doing this change -->

This PR reduces

and improves use of comparison predicates such as posnP, leqP, ltnP, ltngtP, and eqVneq.

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (May 15 2020 at 07:44):

affeldt-aist milestoned Issue #509 Card lemmas:

Motivation for this change

Additional lemmas about cardinalities of predicates and sets. Mainly picking n distinct elements for an a predicate with n <= #|A|.

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (May 15 2020 at 07:49):

affeldt-aist milestoned Issue #507 Add more test cases for higher-order recursive functions in seq.v w.r.t. the guard condition:

Motivation for this change

This PR adds some test cases in test_suite/test_guard.v which I promised to do in https://github.com/math-comp/math-comp/pull/471#issuecomment-611521366. Currently, test cases for find, filter, count, pmap, pairmap, scanl are missing.

<!-- please explain your reason for doing this change -->

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (May 15 2020 at 07:49):

affeldt-aist milestoned Issue #506 ssrnat: add subnA, addnCB, addnCAC, addnAl lemmas:

Motivation for this change

This PR addresses issue #212 by adding some lemmas about natural numbers.

I find addnCAC and addnAl sometimes convenient because having them in the library might save several rewrites once in a while.

I'm open to suggestions (including removing some of this PR's lemmas altogether). Thank you for your time.

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (May 15 2020 at 07:50):

affeldt-aist milestoned Issue #499 contra lemmas involving propositions:

Motivation for this change

Various forms of contraposition are constructively provable and having a collection of lemmas whose naming is consistent with the contra lemmas already in mathcomp makes it easier and more idiomatic to use them.

fixes #491

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (May 15 2020 at 07:52):

affeldt-aist milestoned Issue #210 The vector space of bounded degree polynomials:

Includes a decidable predicate for irreducibly of polynomials of
bounded size over a finite field, and the 'X^i and lagrange basis.

view this post on Zulip Mathcomp Github Bot (May 15 2020 at 08:07):

affeldt-aist:

view this post on Zulip Mathcomp Github Bot (May 15 2020 at 08:33):

chdoc submitted PR Review for #509 Card lemmas.

view this post on Zulip Mathcomp Github Bot (May 15 2020 at 08:33):

chdoc created PR Review Comment on #509 Card lemmas:

I'm not sure I follow. There is no card_eqP (yet) and indeed I'm not sure that would be useful, since enum A has already good lemma support. And card_geqP is about encapsulating the picking of a subsequence of enum A, if one only has a lower bound.
Admittedly, using the _gt?P lemmas to prove cards2P may be overkill.

view this post on Zulip Mathcomp Github Bot (May 15 2020 at 09:54):

affeldt-aist submitted PR Review for #504 Revise proofs in ssreflect/*.v.

view this post on Zulip Mathcomp Github Bot (May 15 2020 at 09:54):

affeldt-aist submitted PR Review for #504 Revise proofs in ssreflect/*.v.

view this post on Zulip Mathcomp Github Bot (May 15 2020 at 12:01):

ybertot submitted PR Review for #504 Revise proofs in ssreflect/*.v.

view this post on Zulip Mathcomp Github Bot (May 15 2020 at 12:01):

ybertot created PR Review Comment on #504 Revise proofs in ssreflect/*.v:

In other contexts you would write -[RHS]partnT // ... would it be suitable here?

view this post on Zulip Mathcomp Github Bot (May 15 2020 at 12:01):

ybertot submitted PR Review for #504 Revise proofs in ssreflect/*.v.

view this post on Zulip Mathcomp Github Bot (May 15 2020 at 13:10):

CohenCyril submitted PR Review for #509 Card lemmas.

view this post on Zulip Mathcomp Github Bot (May 15 2020 at 13:10):

CohenCyril created PR Review Comment on #509 Card lemmas:

Here is an elaboration of what I had in mind:

Lemma set_enum A : [set x | x \in enum A] = A.
Proof. by apply/setP => x; rewrite inE mem_enum. Qed.

Variant cards_eq_spec A : seq T -> {set T} -> nat -> Type :=
| CardEq (s : seq T) & uniq s : cards_eq_spec A s [set x | x \in s] (size s).

Lemma cards_eqP A : cards_eq_spec A (enum A) A #|A|.
Proof.
by move: (enum A) (cardE A) (set_enum A) (enum_uniq A) => s -> <-; constructor.
Qed.

Lemma cards1P A : reflect (exists x, A = [set x]) (#|A| == 1).
Proof.
apply: (iffP idP) => [|[x ->]]; last by rewrite cards1.
have [[|x []]// _] := cards_eqP; exists x; apply/setP => y; rewrite !inE.
Qed.

Lemma cards2P A : reflect (exists x y : T, x != y /\ A = [set x; y]) (#|A| == 2).
Proof.
apply: (iffP idP) => [|[x] [y] [xy ->]]; last by rewrite cards2 xy.
have [[|x [|y [|z s]]]//= s_uniq] := cards_eqP; rewrite !inE andbT in s_uniq.
by exists x, y; split=> //; apply/setP => z; rewrite !inE.
Qed.

and something like this for fintype...

view this post on Zulip Mathcomp Github Bot (May 15 2020 at 13:11):

CohenCyril edited PR Review Comment on #509 Card lemmas.

view this post on Zulip Mathcomp Github Bot (May 15 2020 at 13:11):

CohenCyril edited PR Review Comment on #509 Card lemmas.

view this post on Zulip Mathcomp Github Bot (May 15 2020 at 13:16):

CohenCyril submitted PR Review for #509 Card lemmas.

view this post on Zulip Mathcomp Github Bot (May 15 2020 at 13:16):

CohenCyril created PR Review Comment on #509 Card lemmas:

And card_geqP is about encapsulating the picking of a subsequence of enum A, if one only has a lower bound.

Indeed, I missed that...

view this post on Zulip Mathcomp Github Bot (May 16 2020 at 00:01):

pi8027 submitted PR Review for #504 Revise proofs in ssreflect/*.v.

view this post on Zulip Mathcomp Github Bot (May 16 2020 at 00:01):

pi8027 created PR Review Comment on #504 Revise proofs in ssreflect/*.v:

That's right.

view this post on Zulip Mathcomp Github Bot (May 16 2020 at 00:05):

pi8027 updated PR #504 Revise proofs in ssreflect/*.v (assigned to affeldt-aist) from selectors to master:

Motivation for this change

<!-- please explain your reason for doing this change -->

This PR reduces

and improves use of comparison predicates such as posnP, leqP, ltnP, ltngtP, and eqVneq.

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (May 16 2020 at 00:59):

pi8027 updated PR #504 Revise proofs in ssreflect/*.v (assigned to affeldt-aist) from selectors to master:

Motivation for this change

<!-- please explain your reason for doing this change -->

This PR reduces

and improves use of comparison predicates such as posnP, leqP, ltnP, ltngtP, and eqVneq.

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (May 18 2020 at 18:31):

chdoc opened Issue #512 lemma for proper and setC?

I noticed that there are quite a few lemmas combining _ \subset _ and ~: _ but none for
_ \proper _ and ~: _.

How about adding (possibly with a different name):

Lemma properC (T : finType) (A B : {set T}) : A \proper B = (~: B \proper ~: A).
Proof.
rewrite !properEneq setCS [~: _ == _]inj_eq 1?eq_sym //; exact/inv_inj/setCK.
Qed.

I think this is sufficient, since any introduced double complement can easily be eliminated with ?setCK.

view this post on Zulip Mathcomp Github Bot (May 19 2020 at 16:14):

chdoc submitted PR Review for #509 Card lemmas.

view this post on Zulip Mathcomp Github Bot (May 19 2020 at 16:14):

chdoc created PR Review Comment on #509 Card lemmas:

Okay, for {set _} what you propose is indeed more general and more direct than what I had proposed. However, I'm not sure it transfers all that well to predicates: due to the lack of extensionality, one cannot pull the [set x | x \in enum A] trick. One could instead generate s =i A as an assumption, but I'm not sure this view would be all that useful.

The same goes for lower bounds, albeit for a different reason: there one doesn't even want to replace the original predicate/set.

view this post on Zulip Mathcomp Github Bot (May 19 2020 at 16:21):

chdoc:

view this post on Zulip Mathcomp Github Bot (May 19 2020 at 16:23):

chdoc updated PR #509 Card lemmas from card-lemmas to master:

Motivation for this change

Additional lemmas about cardinalities of predicates and sets. Mainly picking n distinct elements for an a predicate with n <= #|A|.

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (May 20 2020 at 11:07):

amahboubi:

view this post on Zulip Mathcomp Github Bot (May 20 2020 at 11:15):

amahboubi:

view this post on Zulip Mathcomp Github Bot (May 20 2020 at 13:19):

amahboubi:

view this post on Zulip Mathcomp Github Bot (May 20 2020 at 13:20):

amahboubi:

view this post on Zulip Mathcomp Github Bot (May 20 2020 at 17:42):

CohenCyril milestoned Issue #511 adding default nix shell:

Motivation for this change

Adding a default nix-shell.

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (May 20 2020 at 18:27):

CohenCyril pushed 1 commit to branch mono_lemmas.

view this post on Zulip Mathcomp Github Bot (May 20 2020 at 18:51):

CohenCyril deleted the branch mono_lemmas.

view this post on Zulip Mathcomp Github Bot (May 20 2020 at 18:53):

CohenCyril opened PR #513 Missing mono lemmas from mono_lemmas to master:

Motivation for this change

Added lemmas about monotony of functions nat -> T where T is an ordered type

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (May 21 2020 at 14:39):

affeldt-aist milestoned Issue #514 Lemma addition to ssralg and ssrnum (assigned to ybertot):

Motivation for this change

Three lemmas that we found useful in the context of the mathcomp-analysis project (https://github.com/math-comp/analysis/blob/f8d361a93db5906a73327d4fcf1fe9070e1960b8/theories/normedtype.v#L90-L103) and which we think are better suited to mathcomp.

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (May 21 2020 at 14:39):

affeldt-aist assigned PR #514 Lemma addition to ssralg and ssrnum to ybertot.

view this post on Zulip Mathcomp Github Bot (May 21 2020 at 14:39):

affeldt-aist requested CohenCyril for a review on PR #514 Lemma addition to ssralg and ssrnum.

view this post on Zulip Mathcomp Github Bot (May 21 2020 at 14:39):

affeldt-aist opened PR #514 Lemma addition to ssralg and ssrnum (assigned to ybertot) from lemmas_from_analysis_20200521 to master:

Motivation for this change

Three lemmas that we found useful in the context of the mathcomp-analysis project (https://github.com/math-comp/analysis/blob/f8d361a93db5906a73327d4fcf1fe9070e1960b8/theories/normedtype.v#L90-L103) and which we think are better suited to mathcomp.

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (May 21 2020 at 16:34):

CohenCyril submitted PR Review for #514 Lemma addition to ssralg and ssrnum.

view this post on Zulip Mathcomp Github Bot (May 21 2020 at 16:34):

CohenCyril submitted PR Review for #514 Lemma addition to ssralg and ssrnum.

view this post on Zulip Mathcomp Github Bot (May 21 2020 at 16:34):

CohenCyril created PR Review Comment on #514 Lemma addition to ssralg and ssrnum:

This lemma was already generalized and added as subrKA (just above), math-comp analysis should use it instead now.

view this post on Zulip Mathcomp Github Bot (May 21 2020 at 16:34):

CohenCyril created PR Review Comment on #514 Lemma addition to ssralg and ssrnum:

I believe the naming I picked in mathcomp analysis is wrong, and we should provide a more complete interface the following lemmas:

and the naming convention should encompass all these variants

view this post on Zulip Mathcomp Github Bot (May 21 2020 at 16:35):

CohenCyril submitted PR Review for #514 Lemma addition to ssralg and ssrnum.

view this post on Zulip Mathcomp Github Bot (May 21 2020 at 16:35):

CohenCyril created PR Review Comment on #514 Lemma addition to ssralg and ssrnum:

maybe something like (gtr|ltr)_dist[lr]? WDYT?

view this post on Zulip Mathcomp Github Bot (May 21 2020 at 16:36):

CohenCyril edited PR Review Comment on #514 Lemma addition to ssralg and ssrnum.

view this post on Zulip Mathcomp Github Bot (May 21 2020 at 16:37):

CohenCyril edited PR Review Comment on #514 Lemma addition to ssralg and ssrnum.

view this post on Zulip Mathcomp Github Bot (May 21 2020 at 18:55):

affeldt-aist updated PR #514 Lemma addition to ssralg and ssrnum (assigned to ybertot) from lemmas_from_analysis_20200521 to master:

Motivation for this change

Three lemmas that we found useful in the context of the mathcomp-analysis project (https://github.com/math-comp/analysis/blob/f8d361a93db5906a73327d4fcf1fe9070e1960b8/theories/normedtype.v#L90-L103) and which we think are better suited to mathcomp.

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (May 21 2020 at 18:59):

affeldt-aist submitted PR Review for #514 Lemma addition to ssralg and ssrnum.

view this post on Zulip Mathcomp Github Bot (May 21 2020 at 18:59):

affeldt-aist created PR Review Comment on #514 Lemma addition to ssralg and ssrnum:

I couldn't make sense of it right away so I looked for an alternative (also for the sake of the conversation). What about?

view this post on Zulip Mathcomp Github Bot (May 22 2020 at 00:14):

affeldt-aist edited PR #514 Lemma addition to ssrnum (assigned to ybertot) from lemmas_from_analysis_20200521 to master:

Motivation for this change

Three lemmas that we found useful in the context of the mathcomp-analysis project (https://github.com/math-comp/analysis/blob/f8d361a93db5906a73327d4fcf1fe9070e1960b8/theories/normedtype.v#L90-L103) and which we think are better suited to mathcomp.

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (May 26 2020 at 10:07):

chdoc updated PR #509 Card lemmas from card-lemmas to master:

Motivation for this change

Additional lemmas about cardinalities of predicates and sets. Mainly picking n distinct elements for an a predicate with n <= #|A|.

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (May 26 2020 at 15:08):

amahboubi:

view this post on Zulip Mathcomp Github Bot (May 26 2020 at 15:08):

amahboubi:

view this post on Zulip Mathcomp Github Bot (May 27 2020 at 14:37):

ybertot prereleased release The Mathematical Components Library 1.11+beta1 for tag mathcomp-1.11+beta1.

view this post on Zulip Mathcomp Github Bot (May 27 2020 at 14:37):

ybertot created release The Mathematical Components Library 1.11+beta1 for tag mathcomp-1.11+beta1.

view this post on Zulip Mathcomp Github Bot (May 27 2020 at 14:37):

ybertot published release The Mathematical Components Library 1.11+beta1 for tag mathcomp-1.11+beta1.

view this post on Zulip Mathcomp Github Bot (May 27 2020 at 14:37):

ybertot pushed tag mathcomp-1.11+beta1.

view this post on Zulip Mathcomp Github Bot (May 27 2020 at 16:02):

CohenCyril:

view this post on Zulip Mathcomp Github Bot (May 27 2020 at 17:36):

CohenCyril:

view this post on Zulip Mathcomp Github Bot (May 27 2020 at 17:36):

CohenCyril:

view this post on Zulip Mathcomp Github Bot (May 27 2020 at 17:39):

CohenCyril:

view this post on Zulip Mathcomp Github Bot (May 27 2020 at 17:40):

CohenCyril:

view this post on Zulip Mathcomp Github Bot (May 27 2020 at 17:50):

CohenCyril pushed 1 commit to branch master.

view this post on Zulip Mathcomp Github Bot (May 27 2020 at 22:15):

CohenCyril:

view this post on Zulip Mathcomp Github Bot (May 27 2020 at 22:18):

CohenCyril:

view this post on Zulip Mathcomp Github Bot (May 27 2020 at 22:19):

CohenCyril edited release The Mathematical Components Library 1.11+beta1 for tag mathcomp-1.11+beta1.

view this post on Zulip Mathcomp Github Bot (May 27 2020 at 22:19):

CohenCyril edited release The Mathematical Components Library 1.11+beta1 for tag mathcomp-1.11+beta1.

view this post on Zulip Mathcomp Github Bot (May 28 2020 at 10:12):

amahboubi:

view this post on Zulip Mathcomp Github Bot (May 28 2020 at 14:24):

ybertot submitted PR Review for #504 Revise proofs in ssreflect/*.v.

view this post on Zulip Mathcomp Github Bot (May 28 2020 at 14:24):

affeldt-aist merged PR #504 Revise proofs in ssreflect/*.v.

view this post on Zulip Mathcomp Github Bot (May 28 2020 at 14:24):

affeldt-aist pushed 3 commits to branch master. Commits by pi8027 (2) and affeldt-aist (1).

view this post on Zulip Mathcomp Github Bot (May 28 2020 at 14:33):

ybertot merged PR #511 adding default nix shell.

view this post on Zulip Mathcomp Github Bot (May 28 2020 at 14:33):

ybertot pushed 2 commits to branch master. Commits by CohenCyril (1) and ybertot (1).

view this post on Zulip Mathcomp Github Bot (May 28 2020 at 14:48):

CohenCyril opened Issue #515 max and min are too specific:

From 1.10 to 1.11+beta1 we lost in generality in ssrnum.v````: indeed max and min where defined in a numDomainType, but they are now defined in terms of meet and join, which requires at least lattice, which a numDomainType`` is not...

One possible fix is to reintroduce Order.max (and Order.min) as if x <= y then y else x (and similar for min), and develop their theory in a partial order, when elements are all comparable between themselves. Then link them with meet and join when appropriate.

Another fix is to reintroduce Num.max and Num.min but this would be confusing if we keep Order.min and Order.max.

view this post on Zulip Mathcomp Github Bot (May 28 2020 at 14:51):

CohenCyril closed Issue #496 Bugfixes for 1.11.0 (assigned to CohenCyril):

view this post on Zulip Mathcomp Github Bot (May 28 2020 at 14:52):

CohenCyril reopened Issue #496 Bugfixes for 1.11.0 (assigned to CohenCyril):

view this post on Zulip Mathcomp Github Bot (May 28 2020 at 14:55):

CohenCyril edited Issue #515 max and min are too specific:

From 1.10 to 1.11+beta1 we lost in generality in ssrnum.v: indeed max and min where defined in a numDomainType, but they are now defined in terms of meet and join, which requires at least lattice, which a numDomainType is not...

One possible fix is to reintroduce Order.max (and Order.min) as if x <= y then y else x (and similar for min), and develop their theory in a partial order, when elements are all comparable between themselves. Then link them with meet and join when appropriate.

Another fix is to reintroduce Num.max and Num.min but this would be confusing if we keep Order.min and Order.max.

view this post on Zulip Mathcomp Github Bot (May 28 2020 at 14:57):

CohenCyril edited Issue #515 max and min are too specific:

From 1.10 to 1.11+beta1 we lost in generality in ssrnum.v: indeed max and min where defined in a numDomainType, but they are now defined in terms of meet and join, which requires at least lattice, which a numDomainType is not...

One possible fix is to reintroduce Order.max (and Order.min) as if x <= y then y else x (and similar for min), and develop their theory in a partial order, when elements are all comparable between themselves. Then link them with meet and join when appropriate.

Another fix is to reintroduce Num.max and Num.min but this would be confusing if we keep Order.min and Order.max.

In any case these definitions must match exactly the one that existed in 1.10.0 for backward compatiblity reasons and the equations given in the factories for total order (which should be updated if they do not match).

view this post on Zulip Mathcomp Github Bot (May 28 2020 at 14:59):

CohenCyril milestoned Issue #513 Missing mono lemmas:

Motivation for this change

Added lemmas about monotony of functions nat -> T where T is an ordered type

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (May 29 2020 at 15:33):

CohenCyril updated PR #513 Missing mono lemmas from mono_lemmas to master:

Motivation for this change

Added lemmas about monotony of functions nat -> T where T is an ordered type

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (May 29 2020 at 15:34):

CohenCyril submitted PR Review for #513 Missing mono lemmas.

view this post on Zulip Mathcomp Github Bot (May 29 2020 at 15:34):

CohenCyril created PR Review Comment on #513 Missing mono lemmas:

done?

view this post on Zulip Mathcomp Github Bot (May 29 2020 at 16:38):

ybertot submitted PR Review for #513 Missing mono lemmas.

view this post on Zulip Mathcomp Github Bot (May 29 2020 at 16:38):

ybertot created PR Review Comment on #513 Missing mono lemmas:

Good for me!

view this post on Zulip Mathcomp Github Bot (May 29 2020 at 21:31):

CohenCyril requested ybertot for a review on PR #513 Missing mono lemmas.

view this post on Zulip Mathcomp Github Bot (May 30 2020 at 03:47):

CohenCyril opened PR #516 Greneralizing max and min to porderType from maxr to master:

Motivation for this change

From 1.10 to 1.11+beta1, max and min had lost their generality, introducing a regression.
This PR redefines max and min with a general theory in order.v, and thus fixes #515.
It also fixes several potential bugs in their definition.

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (May 30 2020 at 09:30):

ybertot submitted PR Review for #513 Missing mono lemmas.

view this post on Zulip Mathcomp Github Bot (May 30 2020 at 12:29):

CohenCyril milestoned Issue #516 Greneralizing max and min to porderType:

Motivation for this change

From 1.10 to 1.11+beta1, max and min had lost their generality, introducing a regression.
This PR redefines max and min with a general theory in order.v, and thus fixes #515.
It also fixes several potential bugs in their definition.

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (May 30 2020 at 12:29):

CohenCyril edited PR #516 Generalizing max and min to porderType from maxr to master:

Motivation for this change

From 1.10 to 1.11+beta1, max and min had lost their generality, introducing a regression.
This PR redefines max and min with a general theory in order.v, and thus fixes #515.
It also fixes several potential bugs in their definition.

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (May 30 2020 at 17:14):

affeldt-aist updated PR #516 Generalizing max and min to porderType from maxr to master:

Motivation for this change

From 1.10 to 1.11+beta1, max and min had lost their generality, introducing a regression.
This PR redefines max and min with a general theory in order.v, and thus fixes #515.
It also fixes several potential bugs in their definition.

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (May 31 2020 at 14:42):

thery opened PR #517 Extra theorems about subn min and max from minn to master:

Motivation for this change

<!-- please explain your reason for doing this change -->

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

The theorems are missing but I am not very happy about their proofs

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (May 31 2020 at 15:11):

thery updated PR #517 Extra theorems about subn min and max from minn to master:

Motivation for this change

<!-- please explain your reason for doing this change -->

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

The theorems are missing but I am not very happy about their proofs

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (May 31 2020 at 15:13):

thery updated PR #517 Extra theorems about subn min and max from minn to master:

Motivation for this change

<!-- please explain your reason for doing this change -->

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

The theorems are missing but I am not very happy about their proofs

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (May 31 2020 at 15:14):

thery updated PR #517 Extra theorems about subn min and max from minn to master:

Motivation for this change

<!-- please explain your reason for doing this change -->

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

The theorems are missing but I am not very happy about their proofs

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (May 31 2020 at 15:15):

thery updated PR #517 Extra theorems about subn min and max from minn to master:

Motivation for this change

<!-- please explain your reason for doing this change -->

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

The theorems are missing but I am not very happy about their proofs

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Jun 02 2020 at 00:02):

erikmd:

view this post on Zulip Mathcomp Github Bot (Jun 02 2020 at 08:00):

gares:

view this post on Zulip Mathcomp Github Bot (Jun 02 2020 at 08:04):

gares:

view this post on Zulip Mathcomp Github Bot (Jun 02 2020 at 08:04):

gares:

view this post on Zulip Mathcomp Github Bot (Jun 02 2020 at 09:11):

gares:

view this post on Zulip Mathcomp Github Bot (Jun 02 2020 at 09:14):

affeldt-aist updated PR #514 Lemma addition to ssrnum (assigned to ybertot) from lemmas_from_analysis_20200521 to master:

Motivation for this change

Three lemmas that we found useful in the context of the mathcomp-analysis project (https://github.com/math-comp/analysis/blob/f8d361a93db5906a73327d4fcf1fe9070e1960b8/theories/normedtype.v#L90-L103) and which we think are better suited to mathcomp.

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Jun 02 2020 at 09:15):

gares:

view this post on Zulip Mathcomp Github Bot (Jun 02 2020 at 09:16):

affeldt-aist edited PR #514 Lemma addition to ssrnum (assigned to ybertot) from lemmas_from_analysis_20200521 to master:

Motivation for this change

A few lemmas about norm that we found useful in the context of the mathcomp-analysis project (among them: https://github.com/math-comp/analysis/blob/f8d361a93db5906a73327d4fcf1fe9070e1960b8/theories/normedtype.v#L90-L103) and which we think are better suited to mathcomp.

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Jun 02 2020 at 09:20):

gares edited PR #517 Extra theorems about subn minn and maxn from minn to master:

Motivation for this change

<!-- please explain your reason for doing this change -->

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

The theorems are missing but I am not very happy about their proofs

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Jun 02 2020 at 09:29):

CohenCyril opened Issue #518 Missing mono/homo lemmas:

https://github.com/math-comp/analysis/blob/d38d70a1d224ca4b895375bb6f32639c4545bf32/theories/normedtype.v#L87-L196

view this post on Zulip Mathcomp Github Bot (Jun 02 2020 at 09:29):

CohenCyril milestoned Issue #518 Missing mono/homo lemmas:

https://github.com/math-comp/analysis/blob/d38d70a1d224ca4b895375bb6f32639c4545bf32/theories/normedtype.v#L87-L196

view this post on Zulip Mathcomp Github Bot (Jun 02 2020 at 09:30):

gares:

view this post on Zulip Mathcomp Github Bot (Jun 02 2020 at 09:31):

CohenCyril created PR Review Comment on #514 Lemma addition to ssrnum:

The prefix n for norm does not exist yet, and I am not in favor if it. I suggest this is renamed norm_lt_eqF.

view this post on Zulip Mathcomp Github Bot (Jun 02 2020 at 09:31):

CohenCyril submitted PR Review for #514 Lemma addition to ssrnum.

view this post on Zulip Mathcomp Github Bot (Jun 02 2020 at 09:32):

pi8027 submitted PR Review for #516 Generalizing max and min to porderType.

view this post on Zulip Mathcomp Github Bot (Jun 02 2020 at 09:32):

pi8027 created PR Review Comment on #516 Generalizing max and min to porderType:

If we wish to make it compatible as much as possible with minr and maxr of version 1.10.0, shouldn't we use <= rather than <? https://github.com/math-comp/math-comp/blob/mathcomp-1.10.0/mathcomp/algebra/ssrnum.v#L256-L257

view this post on Zulip Mathcomp Github Bot (Jun 02 2020 at 09:32):

CohenCyril edited PR Review Comment on #514 Lemma addition to ssrnum.

view this post on Zulip Mathcomp Github Bot (Jun 02 2020 at 09:35):

gares:

view this post on Zulip Mathcomp Github Bot (Jun 02 2020 at 09:38):

CohenCyril submitted PR Review for #516 Generalizing max and min to porderType.

view this post on Zulip Mathcomp Github Bot (Jun 02 2020 at 09:38):

CohenCyril created PR Review Comment on #516 Generalizing max and min to porderType:

minn and maxn are defined using < and <=, I'd rather loose backward compatibility than convertibility with nat definitions.

view this post on Zulip Mathcomp Github Bot (Jun 02 2020 at 09:39):

CohenCyril edited PR Review Comment on #516 Generalizing max and min to porderType.

view this post on Zulip Mathcomp Github Bot (Jun 02 2020 at 09:45):

pi8027 submitted PR Review for #516 Generalizing max and min to porderType.

view this post on Zulip Mathcomp Github Bot (Jun 02 2020 at 09:45):

pi8027 created PR Review Comment on #516 Generalizing max and min to porderType:

OK. That's fine (as I said in a MC call).

view this post on Zulip Mathcomp Github Bot (Jun 02 2020 at 09:53):

CohenCyril updated PR #501 Intro pattern extensions for rewrite, dup, swap and apply (assigned to gares) from intro_rw to master:

Motivation for this change

Intro pattern ltac views (rewrite, dup, swap, apply) in order not to break intro patterns for silly rewrites.

- calling rewrite from an intro pattern, use with parsimony
=> /[1 rules] does rewrite rules
=> /[-1 rules] does rewrite -rules
=> /[! rules] does rewrite !rules
=> /[-! rules] does rewrite -!rules
=> /[? rules] does rewrite ?rules
=> /[-? rules] does rewrite -?rules
=> /[/def] does rewrite /def

- top of the stack actions:
=> /apply does => hyp {}/hyp
=> /swap does => x y; move: y x (also swap and perserves let bindings)
=> /dup does => x; have copy := x; move: copy x (also copies and preserves let bindings)

This is a part of #372, simplified, rewritten and rebased.

Things done/to do

<!-- please fill in the following checklist -->

<!-- Cross-out the above items using ~crossed out item~ if they happen not to be relevent -->
<!-- You may also add more items to explain what you did and what remains to do -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Jun 02 2020 at 09:55):

gares:

view this post on Zulip Mathcomp Github Bot (Jun 02 2020 at 09:56):

CohenCyril edited PR #501 Intro pattern extensions for rewrite, dup, swap and apply (assigned to gares) from intro_rw to master:

Motivation for this change

Intro pattern ltac views (rewrite, dup, swap, apply) in order not to break intro patterns for silly rewrites.

- calling rewrite from an intro pattern, use with parsimony
=> /[1! rules] does rewrite rules
=> /[-1! rules] does rewrite -rules
=> /[! rules] does rewrite !rules
=> /[-! rules] does rewrite -!rules
=> /[? rules] does rewrite ?rules
=> /[-? rules] does rewrite -?rules
=> /[/def] does rewrite /def

- top of the stack actions:
=> /apply does => hyp {}/hyp
=> /swap does => x y; move: y x (also swap and perserves let bindings)
=> /dup does => x; have copy := x; move: copy x (also copies and preserves let bindings)

This is a part of #372, simplified, rewritten and rebased.

Things done/to do

<!-- please fill in the following checklist -->

<!-- Cross-out the above items using ~crossed out item~ if they happen not to be relevent -->
<!-- You may also add more items to explain what you did and what remains to do -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Jun 02 2020 at 10:01):

gares:

view this post on Zulip Mathcomp Github Bot (Jun 02 2020 at 10:09):

gares:

view this post on Zulip Mathcomp Github Bot (Jun 02 2020 at 10:09):

gares:

view this post on Zulip Mathcomp Github Bot (Jun 02 2020 at 10:11):

gares:

view this post on Zulip Mathcomp Github Bot (Jun 02 2020 at 10:12):

gares:

view this post on Zulip Mathcomp Github Bot (Jun 02 2020 at 10:53):

affeldt-aist updated PR #514 Lemma addition to ssrnum (assigned to ybertot) from lemmas_from_analysis_20200521 to master:

Motivation for this change

A few lemmas about norm that we found useful in the context of the mathcomp-analysis project (among them: https://github.com/math-comp/analysis/blob/f8d361a93db5906a73327d4fcf1fe9070e1960b8/theories/normedtype.v#L90-L103) and which we think are better suited to mathcomp.

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Jun 02 2020 at 12:12):

CohenCyril submitted PR Review for #514 Lemma addition to ssrnum.

view this post on Zulip Mathcomp Github Bot (Jun 02 2020 at 12:12):

CohenCyril created PR Review Comment on #514 Lemma addition to ssrnum:

@affeldt-aist I edited my comment by the mail you might have received was not. I prefer gt_norm_eqF

view this post on Zulip Mathcomp Github Bot (Jun 02 2020 at 12:26):

pi8027 closed Issue #442 Generalization of order (in fingraph.v) and related lemmas to non-frel graphs:

order f x (in fingraph.v) means the size of f-orbit of x:

Definition order (T : finType) (f : T -> T) (x : T) := #|fconnect f x|.

This definition can naturally be generalized to non frel-graphs, which means the number of reachable elements from x in general. Some lemmas that use order can probably be generalized as well. At least, the following lemma introduced by #261 seems to hold in general.

eq_order_cycle
     : forall p : seq T, fcycle f p -> {in p &, forall x y : T, order y = order x}

view this post on Zulip Mathcomp Github Bot (Jun 02 2020 at 13:55):

CohenCyril opened PR #519 Missing homo/mono lemmas in the presence of cancellation from homomono_in to master:

Motivation for this change

The current section MonoHomoMorphismTheory_in from coq/theories/ssr/ssrbool.v is completely unusable because it's rD is too specific, and the cancellation hypothesis is too restrictive {on D, cancel f a g} which barely covers the use cases (e.g. in mathcomp/analysis).

Fixes #518

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Jun 02 2020 at 13:57):

CohenCyril milestoned Issue #519 Missing homo/mono lemmas in the presence of cancellation:

Motivation for this change

The current section MonoHomoMorphismTheory_in from coq/theories/ssr/ssrbool.v is completely unusable because it's rD is too specific, and the cancellation hypothesis is too restrictive {on D, cancel f a g} which barely covers the use cases (e.g. in mathcomp/analysis).

Fixes #518

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Jun 02 2020 at 13:58):

CohenCyril submitted PR Review for #514 Lemma addition to ssrnum.

view this post on Zulip Mathcomp Github Bot (Jun 02 2020 at 13:58):

CohenCyril created PR Review Comment on #514 Lemma addition to ssrnum:

Lemma gt_norm_eqF (x y : R) : `|x| < y -> (x == - y = false) * (x == y = false).

view this post on Zulip Mathcomp Github Bot (Jun 02 2020 at 14:10):

CohenCyril submitted PR Review for #514 Lemma addition to ssrnum.

view this post on Zulip Mathcomp Github Bot (Jun 02 2020 at 14:10):

CohenCyril submitted PR Review for #514 Lemma addition to ssrnum.

view this post on Zulip Mathcomp Github Bot (Jun 02 2020 at 14:10):

CohenCyril created PR Review Comment on #514 Lemma addition to ssrnum:

For consistency, we should also add

Lemma gtr_norm : `|x| < y -> x < y.
Lemma gtrNnorm : `|x| < y -> - y < x.
Lemma ger_norm : `|x| <= y -> x <= y.
Lemma gerNnorm : `|x| <= y -> - y <= x.

and all the real_ variants...

view this post on Zulip Mathcomp Github Bot (Jun 02 2020 at 15:04):

CohenCyril updated PR #516 Generalizing max and min to porderType from maxr to master:

Motivation for this change

From 1.10 to 1.11+beta1, max and min had lost their generality, introducing a regression.
This PR redefines max and min with a general theory in order.v, and thus fixes #515.
It also fixes several potential bugs in their definition.

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Jun 02 2020 at 15:27):

CohenCyril updated PR #516 Generalizing max and min to porderType from maxr to master:

Motivation for this change

From 1.10 to 1.11+beta1, max and min had lost their generality, introducing a regression.
This PR redefines max and min with a general theory in order.v, and thus fixes #515.
It also fixes several potential bugs in their definition.

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Jun 02 2020 at 15:42):

CohenCyril updated PR #516 Generalizing max and min to porderType from maxr to master:

Motivation for this change

From 1.10 to 1.11+beta1, max and min had lost their generality, introducing a regression.
This PR redefines max and min with a general theory in order.v, and thus fixes #515.
It also fixes several potential bugs in their definition.

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Jun 02 2020 at 15:43):

CohenCyril edited PR #516 Generalizing max and min to porderType from maxr to master:

Motivation for this change

From 1.10 to 1.11+beta1, max and min had lost their generality, introducing a regression.
This PR redefines max and min with a general theory in order.v, and thus fixes #515.
It also fixes several potential bugs in their definition.

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Jun 02 2020 at 15:43):

CohenCyril has marked PR #516 as ready for review.

view this post on Zulip Mathcomp Github Bot (Jun 02 2020 at 16:04):

pi8027 submitted PR Review for #516 Generalizing max and min to porderType.

view this post on Zulip Mathcomp Github Bot (Jun 02 2020 at 16:04):

pi8027 created PR Review Comment on #516 Generalizing max and min to porderType:

I think this was left as a comment on purpose. See L.293 (and L.351 which you may also want to remove).

view this post on Zulip Mathcomp Github Bot (Jun 02 2020 at 16:13):

CohenCyril updated PR #516 Generalizing max and min to porderType from maxr to master:

Motivation for this change

From 1.10 to 1.11+beta1, max and min had lost their generality, introducing a regression.
This PR redefines max and min with a general theory in order.v, and thus fixes #515.
It also fixes several potential bugs in their definition.

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Jun 02 2020 at 16:14):

CohenCyril submitted PR Review for #516 Generalizing max and min to porderType.

view this post on Zulip Mathcomp Github Bot (Jun 02 2020 at 16:14):

CohenCyril created PR Review Comment on #516 Generalizing max and min to porderType:

:+1: I withdrew this deletion from the PR, since it was an accidental removal unrelated to the changes in this PR, maybe we can open an issue to document or remove this comment.

view this post on Zulip Mathcomp Github Bot (Jun 02 2020 at 16:57):

CohenCyril updated PR #516 Generalizing max and min to porderType from maxr to master:

Motivation for this change

From 1.10 to 1.11+beta1, max and min had lost their generality, introducing a regression.
This PR redefines max and min with a general theory in order.v, and thus fixes #515.
It also fixes several potential bugs in their definition.

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Jun 02 2020 at 17:25):

CohenCyril opened PR #520 Cachix action from cachix-action to master:

Motivation for this change

Setting up a github action for mathcomp.

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Jun 02 2020 at 17:28):

CohenCyril updated PR #520 Cachix action from cachix-action to master:

Motivation for this change

Setting up a github action for mathcomp.

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Jun 02 2020 at 17:33):

CohenCyril updated PR #520 Cachix action from cachix-action to master:

Motivation for this change

Setting up a github action for mathcomp.

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Jun 02 2020 at 17:35):

CohenCyril updated PR #520 Cachix action from cachix-action to master:

Motivation for this change

Setting up a github action for mathcomp.

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Jun 02 2020 at 17:41):

CohenCyril updated PR #520 Cachix action from cachix-action to master:

Motivation for this change

Setting up a github action for mathcomp.

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Jun 02 2020 at 17:46):

CohenCyril updated PR #520 Cachix action from cachix-action to master:

Motivation for this change

Setting up a github action for mathcomp.

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Jun 02 2020 at 17:51):

CohenCyril updated PR #520 Cachix action from cachix-action to master:

Motivation for this change

Setting up a github action for mathcomp.

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Jun 02 2020 at 17:53):

CohenCyril updated PR #520 Cachix action from cachix-action to master:

Motivation for this change

Setting up a github action for mathcomp.

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Jun 02 2020 at 17:55):

CohenCyril updated PR #520 Cachix action from cachix-action to master:

Motivation for this change

Setting up a github action for mathcomp.

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Jun 02 2020 at 17:57):

CohenCyril updated PR #520 Cachix action from cachix-action to master:

Motivation for this change

Setting up a github action for mathcomp.

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Jun 02 2020 at 17:58):

CohenCyril updated PR #520 Cachix action from cachix-action to master:

Motivation for this change

Setting up a github action for mathcomp.

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Jun 02 2020 at 18:04):

CohenCyril updated PR #520 Cachix action from cachix-action to master:

Motivation for this change

Setting up a github action for mathcomp.

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Jun 02 2020 at 19:48):

affeldt-aist updated PR #514 Lemma addition to ssrnum (assigned to ybertot) from lemmas_from_analysis_20200521 to master:

Motivation for this change

A few lemmas about norm that we found useful in the context of the mathcomp-analysis project (among them: https://github.com/math-comp/analysis/blob/f8d361a93db5906a73327d4fcf1fe9070e1960b8/theories/normedtype.v#L90-L103) and which we think are better suited to mathcomp.

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Jun 03 2020 at 11:41):

CohenCyril updated PR #520 Cachix action from cachix-action to master:

Motivation for this change

Setting up a github action for mathcomp.

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Jun 03 2020 at 14:54):

CohenCyril has marked PR #520 as ready for review.

view this post on Zulip Mathcomp Github Bot (Jun 03 2020 at 14:54):

CohenCyril edited PR #520 Cachix action from cachix-action to master:

Motivation for this change

Setting up a github action for mathcomp.
This adds a new CI that also building mathcomp on nix and making it available via cachix.

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Jun 03 2020 at 14:56):

CohenCyril pushed 2 commits to branch master.

view this post on Zulip Mathcomp Github Bot (Jun 03 2020 at 14:56):

CohenCyril merged PR #520 Cachix action.

view this post on Zulip Mathcomp Github Bot (Jun 03 2020 at 16:02):

CohenCyril updated PR #516 Generalizing max and min to porderType from maxr to master:

Motivation for this change

From 1.10 to 1.11+beta1, max and min had lost their generality, introducing a regression.
This PR redefines max and min with a general theory in order.v, and thus fixes #515.
It also fixes several potential bugs in their definition.

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Jun 04 2020 at 03:00):

CohenCyril submitted PR Review for #514 Lemma addition to ssrnum.

view this post on Zulip Mathcomp Github Bot (Jun 04 2020 at 03:00):

CohenCyril created PR Review Comment on #514 Lemma addition to ssrnum:

Actually I believe this one should be obtained by letting the user compose a gtr_norm lemma with gt_eqF, otherwise there are two many variants and multi-rules to take into account.

view this post on Zulip Mathcomp Github Bot (Jun 04 2020 at 03:00):

CohenCyril edited PR Review Comment on #514 Lemma addition to ssrnum.

view this post on Zulip Mathcomp Github Bot (Jun 04 2020 at 03:11):

CohenCyril submitted PR Review for #514 Lemma addition to ssrnum.

view this post on Zulip Mathcomp Github Bot (Jun 04 2020 at 03:11):

CohenCyril created PR Review Comment on #514 Lemma addition to ssrnum:

I do not like the lack of symmetry between dist and distr, (the former should then be distl), but actually all of them must be distl because dist is on the left side of <, swapping arguments of dist should be replaced with the use of suffix C.

BTW I noticed a discrepancy introduced by this PR:

view this post on Zulip Mathcomp Github Bot (Jun 04 2020 at 03:40):

CohenCyril updated PR #516 Generalizing max and min to porderType from maxr to master:

Motivation for this change

From 1.10 to 1.11+beta1, max and min had lost their generality, introducing a regression.
This PR redefines max and min with a general theory in order.v, and thus fixes #515.
It also fixes several potential bugs in their definition.

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Jun 04 2020 at 03:47):

CohenCyril pushed 11 commits to branch maxr. Commits by CohenCyril (10) and affeldt-aist (1).

view this post on Zulip Mathcomp Github Bot (Jun 04 2020 at 03:48):

CohenCyril updated PR #516 Generalizing max and min to porderType from maxr to master:

Motivation for this change

From 1.10 to 1.11+beta1, max and min had lost their generality, introducing a regression.
This PR redefines max and min with a general theory in order.v, and thus fixes #515.
It also fixes several potential bugs in their definition.

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Jun 04 2020 at 03:48):

CohenCyril deleted the branch maxr.

view this post on Zulip Mathcomp Github Bot (Jun 04 2020 at 04:09):

CohenCyril updated PR #516 Generalizing max and min to porderType from maxr to master:

Motivation for this change

From 1.10 to 1.11+beta1, max and min had lost their generality, introducing a regression.
This PR redefines max and min with a general theory in order.v, and thus fixes #515.
It also fixes several potential bugs in their definition.

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Jun 04 2020 at 04:13):

CohenCyril updated PR #516 Generalizing max and min to porderType from maxr to master:

Motivation for this change

From 1.10 to 1.11+beta1, max and min had lost their generality, introducing a regression.
This PR redefines max and min with a general theory in order.v, and thus fixes #515.
It also fixes several potential bugs in their definition.

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Jun 04 2020 at 10:26):

affeldt-aist updated PR #514 Lemma addition to ssrnum (assigned to ybertot) from lemmas_from_analysis_20200521 to master:

Motivation for this change

A few lemmas about norm that we found useful in the context of the mathcomp-analysis project (among them: https://github.com/math-comp/analysis/blob/f8d361a93db5906a73327d4fcf1fe9070e1960b8/theories/normedtype.v#L90-L103) and which we think are better suited to mathcomp.

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Jun 04 2020 at 10:28):

affeldt-aist updated PR #514 Lemma addition to ssrnum (assigned to ybertot) from lemmas_from_analysis_20200521 to master:

Motivation for this change

A few lemmas about norm that we found useful in the context of the mathcomp-analysis project (among them: https://github.com/math-comp/analysis/blob/f8d361a93db5906a73327d4fcf1fe9070e1960b8/theories/normedtype.v#L90-L103) and which we think are better suited to mathcomp.

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Jun 04 2020 at 10:36):

pi8027 submitted PR Review for #514 Lemma addition to ssrnum.

view this post on Zulip Mathcomp Github Bot (Jun 04 2020 at 10:36):

pi8027 created PR Review Comment on #514 Lemma addition to ssrnum:

Using (real_) rather than {real_,} would be consistent with the released changelog. See, e.g.: https://github.com/math-comp/math-comp/blob/master/CHANGELOG.md#renamed

view this post on Zulip Mathcomp Github Bot (Jun 04 2020 at 11:46):

affeldt-aist updated PR #514 Lemma addition to ssrnum (assigned to ybertot) from lemmas_from_analysis_20200521 to master:

Motivation for this change

A few lemmas about norm that we found useful in the context of the mathcomp-analysis project (among them: https://github.com/math-comp/analysis/blob/f8d361a93db5906a73327d4fcf1fe9070e1960b8/theories/normedtype.v#L90-L103) and which we think are better suited to mathcomp.

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Jun 04 2020 at 13:00):

amahboubi:

view this post on Zulip Mathcomp Github Bot (Jun 04 2020 at 13:24):

affeldt-aist updated PR #516 Generalizing max and min to porderType from maxr to master:

Motivation for this change

From 1.10 to 1.11+beta1, max and min had lost their generality, introducing a regression.
This PR redefines max and min with a general theory in order.v, and thus fixes #515.
It also fixes several potential bugs in their definition.

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Jun 04 2020 at 13:50):

affeldt-aist updated PR #519 Missing homo/mono lemmas in the presence of cancellation from homomono_in to master:

Motivation for this change

The current section MonoHomoMorphismTheory_in from coq/theories/ssr/ssrbool.v is completely unusable because it's rD is too specific, and the cancellation hypothesis is too restrictive {on D, cancel f a g} which barely covers the use cases (e.g. in mathcomp/analysis).

Fixes #518

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Jun 04 2020 at 13:51):

affeldt-aist edited PR #519 Missing homo/mono lemmas in the presence of cancellation from homomono_in to master:

Motivation for this change

The current section MonoHomoMorphismTheory_in from coq/theories/ssr/ssrbool.v is completely unusable because it's rD is too specific, and the cancellation hypothesis is too restrictive {on D, cancel f a g} which barely covers the use cases (e.g. in mathcomp/analysis).

Fixes #518

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Jun 04 2020 at 13:57):

affeldt-aist updated PR #519 Missing homo/mono lemmas in the presence of cancellation from homomono_in to master:

Motivation for this change

The current section MonoHomoMorphismTheory_in from coq/theories/ssr/ssrbool.v is completely unusable because it's rD is too specific, and the cancellation hypothesis is too restrictive {on D, cancel f a g} which barely covers the use cases (e.g. in mathcomp/analysis).

Fixes #518

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Jun 04 2020 at 14:10):

CohenCyril updated PR #519 Missing homo/mono lemmas in the presence of cancellation from homomono_in to master:

Motivation for this change

The current section MonoHomoMorphismTheory_in from coq/theories/ssr/ssrbool.v is completely unusable because it's rD is too specific, and the cancellation hypothesis is too restrictive {on D, cancel f a g} which barely covers the use cases (e.g. in mathcomp/analysis).

Fixes #518

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Jun 04 2020 at 15:08):

CohenCyril updated PR #519 Missing homo/mono lemmas in the presence of cancellation from homomono_in to master:

Motivation for this change

The current section MonoHomoMorphismTheory_in from coq/theories/ssr/ssrbool.v is completely unusable because it's rD is too specific, and the cancellation hypothesis is too restrictive {on D, cancel f a g} which barely covers the use cases (e.g. in mathcomp/analysis).

Fixes #518

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Jun 04 2020 at 15:09):

CohenCyril updated PR #519 Missing homo/mono lemmas in the presence of cancellation from homomono_in to master:

Motivation for this change

The current section MonoHomoMorphismTheory_in from coq/theories/ssr/ssrbool.v is completely unusable because it's rD is too specific, and the cancellation hypothesis is too restrictive {on D, cancel f a g} which barely covers the use cases (e.g. in mathcomp/analysis).

Fixes #518

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Jun 04 2020 at 15:11):

CohenCyril has marked PR #519 as ready for review.

view this post on Zulip Mathcomp Github Bot (Jun 04 2020 at 15:12):

CohenCyril milestoned Issue #521 In and on:

Motivation for this change

These new lemmas describe more precisely the possible interactions between in and on.

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Jun 04 2020 at 15:12):

CohenCyril opened PR #521 In and on from in_on to master:

Motivation for this change

These new lemmas describe more precisely the possible interactions between in and on.

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Jun 04 2020 at 15:13):

CohenCyril edited PR #207 Work In Progress: adding forms and spectral theorems from experiment/forms to master:

Content:

TODO:

TODO update after @LaurenceRideau tried on the odd-order repo (https://github.com/math-comp/odd-order/pull/2)

view this post on Zulip Mathcomp Github Bot (Jun 04 2020 at 15:15):

CohenCyril closed without merge PR #372 Taking advantage of Coq 8.10 ssreflect new features.

view this post on Zulip Mathcomp Github Bot (Jun 04 2020 at 15:15):

coqbot demilestoned Issue #372 Taking advantage of Coq 8.10 ssreflect new features (assigned to gares):

Motivation for this change

<!-- please explain your reason for doing this change -->
Mostly testing ltac in notations in views:

Things done/to do

<!-- please fill in the following checklist -->

<!-- if items above are irrelevant, explain what you did here -->

<!-- please fill in the following checklist -->
<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Jun 04 2020 at 15:35):

affeldt-aist merged PR #513 Missing mono lemmas.

view this post on Zulip Mathcomp Github Bot (Jun 04 2020 at 15:35):

affeldt-aist pushed 1 commit to branch master. Commits by CohenCyril (1).

view this post on Zulip Mathcomp Github Bot (Jun 04 2020 at 15:48):

CohenCyril updated PR #516 Generalizing max and min to porderType from maxr to master:

Motivation for this change

From 1.10 to 1.11+beta1, max and min had lost their generality, introducing a regression.
This PR redefines max and min with a general theory in order.v, and thus fixes #515.
It also fixes several potential bugs in their definition.

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Jun 04 2020 at 15:49):

affeldt-aist updated PR #514 Lemma addition to ssrnum (assigned to ybertot) from lemmas_from_analysis_20200521 to master:

Motivation for this change

A few lemmas about norm that we found useful in the context of the mathcomp-analysis project (among them: https://github.com/math-comp/analysis/blob/f8d361a93db5906a73327d4fcf1fe9070e1960b8/theories/normedtype.v#L90-L103) and which we think are better suited to mathcomp.

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Jun 04 2020 at 17:02):

CohenCyril updated PR #516 Generalizing max and min to porderType from maxr to master:

Motivation for this change

From 1.10 to 1.11+beta1, max and min had lost their generality, introducing a regression.
This PR redefines max and min with a general theory in order.v, and thus fixes #515.
It also fixes several potential bugs in their definition.

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Jun 04 2020 at 21:50):

CohenCyril updated PR #501 Intro pattern extensions for rewrite, dup, swap and apply (assigned to gares) from intro_rw to master:

Motivation for this change

Intro pattern ltac views (rewrite, dup, swap, apply) in order not to break intro patterns for silly rewrites.

- calling rewrite from an intro pattern, use with parsimony
=> /[1! rules] does rewrite rules
=> /[-1! rules] does rewrite -rules
=> /[! rules] does rewrite !rules
=> /[-! rules] does rewrite -!rules
=> /[? rules] does rewrite ?rules
=> /[-? rules] does rewrite -?rules
=> /[/def] does rewrite /def

- top of the stack actions:
=> /apply does => hyp {}/hyp
=> /swap does => x y; move: y x (also swap and perserves let bindings)
=> /dup does => x; have copy := x; move: copy x (also copies and preserves let bindings)

This is a part of #372, simplified, rewritten and rebased.

Things done/to do

<!-- please fill in the following checklist -->

<!-- Cross-out the above items using ~crossed out item~ if they happen not to be relevent -->
<!-- You may also add more items to explain what you did and what remains to do -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Jun 04 2020 at 21:51):

CohenCyril edited PR #501 Intro pattern extensions for rewrite, dup, swap and apply (assigned to gares) from intro_rw to master:

Motivation for this change

Intro pattern ltac views (rewrite, dup, swap, apply) in order not to break intro patterns for silly rewrites.

- calling rewrite from an intro pattern, use with parsimony
=> /[1! rules] does rewrite rules
=> /[! rules] does rewrite !rules

- top of the stack actions:
=> /apply does => hyp {}/hyp
=> /swap does => x y; move: y x (also swap and perserves let bindings)
=> /dup does => x; have copy := x; move: copy x (also copies and preserves let bindings)

This is a part of #372, simplified, rewritten and rebased.

Things done/to do

<!-- please fill in the following checklist -->

<!-- Cross-out the above items using ~crossed out item~ if they happen not to be relevent -->
<!-- You may also add more items to explain what you did and what remains to do -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Jun 04 2020 at 22:56):

CohenCyril updated PR #519 Missing homo/mono lemmas in the presence of cancellation from homomono_in to master:

Motivation for this change

The current section MonoHomoMorphismTheory_in from coq/theories/ssr/ssrbool.v is completely unusable because it's rD is too specific, and the cancellation hypothesis is too restrictive {on D, cancel f a g} which barely covers the use cases (e.g. in mathcomp/analysis).

Fixes #518

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Jun 04 2020 at 22:58):

CohenCyril submitted PR Review for #516 Generalizing max and min to porderType.

view this post on Zulip Mathcomp Github Bot (Jun 04 2020 at 22:58):

CohenCyril created PR Review Comment on #516 Generalizing max and min to porderType:

(*   [arg min_(i < i0 | P) M] == a value i : T minimizing M : R, subject to  *)

view this post on Zulip Mathcomp Github Bot (Jun 04 2020 at 22:58):

CohenCyril edited PR Review Comment on #516 Generalizing max and min to porderType.

view this post on Zulip Mathcomp Github Bot (Jun 04 2020 at 22:59):

CohenCyril updated PR #516 Generalizing max and min to porderType from maxr to master:

Motivation for this change

From 1.10 to 1.11+beta1, max and min had lost their generality, introducing a regression.
This PR redefines max and min with a general theory in order.v, and thus fixes #515.
It also fixes several potential bugs in their definition.

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Jun 04 2020 at 23:00):

CohenCyril submitted PR Review for #516 Generalizing max and min to porderType.

view this post on Zulip Mathcomp Github Bot (Jun 04 2020 at 23:00):

CohenCyril created PR Review Comment on #516 Generalizing max and min to porderType:

(*   [arg max_(i > i0 | P) M] == a value i maximizing M subject to P and      *)

view this post on Zulip Mathcomp Github Bot (Jun 04 2020 at 23:02):

CohenCyril updated PR #516 Generalizing max and min to porderType from maxr to master:

Motivation for this change

From 1.10 to 1.11+beta1, max and min had lost their generality, introducing a regression.
This PR redefines max and min with a general theory in order.v, and thus fixes #515.
It also fixes several potential bugs in their definition.

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Jun 04 2020 at 23:36):

CohenCyril submitted PR Review for #514 Lemma addition to ssrnum.

view this post on Zulip Mathcomp Github Bot (Jun 04 2020 at 23:37):

CohenCyril edited PR #519 Missing homo/mono lemmas in the presence of cancellation from homomono_in to master:

Motivation for this change

The current section MonoHomoMorphismTheory_in from coq/theories/ssr/ssrbool.v is completely unusable because it's rD is too specific, and the cancellation hypothesis is too restrictive {on D, cancel f a g} which barely covers the use cases (e.g. in mathcomp/analysis).

Fixes #518

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Jun 05 2020 at 03:37):

pi8027 submitted PR Review for #516 Generalizing max and min to porderType.

view this post on Zulip Mathcomp Github Bot (Jun 05 2020 at 03:37):

pi8027 submitted PR Review for #516 Generalizing max and min to porderType.

view this post on Zulip Mathcomp Github Bot (Jun 05 2020 at 03:37):

pi8027 created PR Review Comment on #516 Generalizing max and min to porderType:

  `join`, and providing a theory about for min and max, hence generalizing

view this post on Zulip Mathcomp Github Bot (Jun 05 2020 at 05:28):

CohenCyril updated PR #516 Generalizing max and min to porderType from maxr to master:

Motivation for this change

From 1.10 to 1.11+beta1, max and min had lost their generality, introducing a regression.
This PR redefines max and min with a general theory in order.v, and thus fixes #515.
It also fixes several potential bugs in their definition.

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Jun 05 2020 at 05:28):

CohenCyril updated PR #516 Generalizing max and min to porderType from maxr to master:

Motivation for this change

From 1.10 to 1.11+beta1, max and min had lost their generality, introducing a regression.
This PR redefines max and min with a general theory in order.v, and thus fixes #515.
It also fixes several potential bugs in their definition.

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Jun 05 2020 at 06:55):

ybertot merged PR #514 Lemma addition to ssrnum.

view this post on Zulip Mathcomp Github Bot (Jun 05 2020 at 06:55):

ybertot pushed 9 commits to branch master. Commits by affeldt-aist (8) and ybertot (1).

view this post on Zulip Mathcomp Github Bot (Jun 05 2020 at 23:30):

affeldt-aist opened PR #522 change links to the wiki to links to the website from update_readme to master:

Motivation for this change

The README points to pages of the wiki that have not been updated while the website contains more up-to-date and better formatted information.

Things done/to do

<!-- please fill in the following checklist -->
~- [ ] added corresponding entries in CHANGELOG_UNRELEASED.md~
~- [ ] added corresponding documentation in the headers~
<!-- Cross-out the above items using ~crossed out item~ if they happen not to be relevent -->
<!-- You may also add more items to explain what you did and what remains to do -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Jun 05 2020 at 23:33):

affeldt-aist updated PR #522 change links to the wiki to links to the website from update_readme to master:

Motivation for this change

The README points to pages of the wiki that have not been updated while the website contains more up-to-date and better formatted information.

Things done/to do

<!-- please fill in the following checklist -->
~- [ ] added corresponding entries in CHANGELOG_UNRELEASED.md~
~- [ ] added corresponding documentation in the headers~
<!-- Cross-out the above items using ~crossed out item~ if they happen not to be relevent -->
<!-- You may also add more items to explain what you did and what remains to do -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Jun 05 2020 at 23:45):

CohenCyril updated PR #516 Generalizing max and min to porderType from maxr to master:

Motivation for this change

From 1.10 to 1.11+beta1, max and min had lost their generality, introducing a regression.
This PR redefines max and min with a general theory in order.v, and thus fixes #515.
It also fixes several potential bugs in their definition.

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Jun 05 2020 at 23:48):

CohenCyril updated PR #519 Missing homo/mono lemmas in the presence of cancellation from homomono_in to master:

Motivation for this change

The current section MonoHomoMorphismTheory_in from coq/theories/ssr/ssrbool.v is completely unusable because it's rD is too specific, and the cancellation hypothesis is too restrictive {on D, cancel f a g} which barely covers the use cases (e.g. in mathcomp/analysis).

Fixes #518

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Jun 06 2020 at 08:09):

affeldt-aist closed Issue #515 max and min are too specific:

From 1.10 to 1.11+beta1 we lost in generality in ssrnum.v: indeed max and min where defined in a numDomainType, but they are now defined in terms of meet and join, which requires at least lattice, which a numDomainType is not...

One possible fix is to reintroduce Order.max (and Order.min) as if x <= y then y else x (and similar for min), and develop their theory in a partial order, when elements are all comparable between themselves. Then link them with meet and join when appropriate.

Another fix is to reintroduce Num.max and Num.min but this would be confusing if we keep Order.min and Order.max.

In any case these definitions must match exactly the one that existed in 1.10.0 for backward compatiblity reasons and the equations given in the factories for total order (which should be updated if they do not match).

view this post on Zulip Mathcomp Github Bot (Jun 06 2020 at 08:09):

affeldt-aist merged PR #516 Generalizing max and min to porderType.

view this post on Zulip Mathcomp Github Bot (Jun 06 2020 at 08:09):

affeldt-aist pushed 6 commits to branch master. Commits by CohenCyril (4) and affeldt-aist (2).

view this post on Zulip Mathcomp Github Bot (Jun 06 2020 at 17:39):

CohenCyril updated PR #519 Missing homo/mono lemmas in the presence of cancellation from homomono_in to master:

Motivation for this change

The current section MonoHomoMorphismTheory_in from coq/theories/ssr/ssrbool.v is completely unusable because it's rD is too specific, and the cancellation hypothesis is too restrictive {on D, cancel f a g} which barely covers the use cases (e.g. in mathcomp/analysis).

Fixes #518

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Jun 06 2020 at 17:40):

CohenCyril merged PR #522 change links to the wiki to links to the website.

view this post on Zulip Mathcomp Github Bot (Jun 06 2020 at 17:40):

CohenCyril pushed 2 commits to branch master. Commits by CohenCyril (1) and affeldt-aist (1).

view this post on Zulip Mathcomp Github Bot (Jun 07 2020 at 02:03):

CohenCyril closed Issue #496 Bugfixes for 1.11.0 (assigned to CohenCyril):

view this post on Zulip Mathcomp Github Bot (Jun 07 2020 at 02:18):

CohenCyril submitted PR Review for #509 Card lemmas.

view this post on Zulip Mathcomp Github Bot (Jun 07 2020 at 02:18):

CohenCyril submitted PR Review for #509 Card lemmas.

view this post on Zulip Mathcomp Github Bot (Jun 07 2020 at 02:18):

CohenCyril created PR Review Comment on #509 Card lemmas:

if you are going to add take_uniq, also add drop_uniq

view this post on Zulip Mathcomp Github Bot (Jun 07 2020 at 02:18):

CohenCyril created PR Review Comment on #509 Card lemmas:

exists [:: x; y; z]; rewrite /= !inE negb_or xDy xDz eq_sym yDz; split=> // u.

view this post on Zulip Mathcomp Github Bot (Jun 07 2020 at 02:18):

CohenCyril created PR Review Comment on #509 Card lemmas:

  by exists a, b; rewrite aDb !subD ?inE ?eqxx ?orbT.

view this post on Zulip Mathcomp Github Bot (Jun 07 2020 at 02:18):

CohenCyril created PR Review Comment on #509 Card lemmas:

  by exists x, y, z; rewrite xDy yDz eq_sym xDz !subA ?inE ?eqxx ?orbT.

view this post on Zulip Mathcomp Github Bot (Jun 07 2020 at 02:18):

CohenCyril created PR Review Comment on #509 Card lemmas:

by exists [:: x; y]; rewrite /= !inE xDy ; split=> // z; rewrite !inE => /pred2P[]->.

view this post on Zulip Mathcomp Github Bot (Jun 07 2020 at 02:18):

CohenCyril created PR Review Comment on #509 Card lemmas:

Proof. apply: (iffP (card_le1_eqP {:T})); [exact: in2T | exact: in2W]. Qed.

view this post on Zulip Mathcomp Github Bot (Jun 07 2020 at 02:18):

CohenCyril created PR Review Comment on #509 Card lemmas:

  reflect {in A &, forall x, all_equal_to x} (#|A| <= 1).

view this post on Zulip Mathcomp Github Bot (Jun 07 2020 at 02:18):

CohenCyril created PR Review Comment on #509 Card lemmas:


view this post on Zulip Mathcomp Github Bot (Jun 07 2020 at 02:18):

CohenCyril created PR Review Comment on #509 Card lemmas:

  by exists x; do 1?exists y; rewrite // -root_connect // (eqP rfx) (eqP rfy).

view this post on Zulip Mathcomp Github Bot (Jun 07 2020 at 02:18):

CohenCyril created PR Review Comment on #509 Card lemmas:

  move=> [x] [y] [/andP [/= rfx xA]] [/andP[/= rfy yA] xDy].

view this post on Zulip Mathcomp Github Bot (Jun 07 2020 at 02:18):

CohenCyril created PR Review Comment on #509 Card lemmas:

  case: s => [|x [|y [|z []]]]//=; rewrite !inE !andbT negb_or -andbA.

view this post on Zulip Mathcomp Github Bot (Jun 07 2020 at 02:18):

CohenCyril created PR Review Comment on #509 Card lemmas:

  case: s => [|a [|b []]]//=; rewrite inE andbT => aDb _ subD.

view this post on Zulip Mathcomp Github Bot (Jun 07 2020 at 02:18):

CohenCyril created PR Review Comment on #509 Card lemmas:

by rewrite !inE => /or3P [] /eqP->.

view this post on Zulip Mathcomp Github Bot (Jun 07 2020 at 09:08):

chdoc submitted PR Review for #509 Card lemmas.

view this post on Zulip Mathcomp Github Bot (Jun 07 2020 at 09:08):

chdoc created PR Review Comment on #509 Card lemmas:

Will do.

view this post on Zulip Mathcomp Github Bot (Jun 07 2020 at 09:08):

chdoc updated PR #509 Card lemmas from card-lemmas to master:

Motivation for this change

Additional lemmas about cardinalities of predicates and sets. Mainly picking n distinct elements for an a predicate with n <= #|A|.

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Jun 07 2020 at 09:30):

chdoc updated PR #509 Card lemmas from card-lemmas to master:

Motivation for this change

Additional lemmas about cardinalities of predicates and sets. Mainly picking n distinct elements for an a predicate with n <= #|A|.

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Jun 07 2020 at 12:35):

chdoc requested CohenCyril for a review on PR #509 Card lemmas.

view this post on Zulip Mathcomp Github Bot (Jun 07 2020 at 12:52):

chdoc opened Issue #523 Cachix actions running and failing on forks:

Unlike the GitLab CI pipeline, which is not executed on forks of math-comp, the cachix actions are trying to execute and fail (while they succeed on the same commits in the math-comp context).

See https://github.com/chdoc/math-comp/runs/746817379

This means that updating the master branch of a fork generates emails about run failures.

view this post on Zulip Mathcomp Github Bot (Jun 07 2020 at 19:25):

erikmd opened PR #524 [CI/CD] Deploy mathcomp/mathcomp-dev:coq-8.12 (with Coq 8.12+alpha) from coq-8.12 to master:

Motivation for this change

Coq 8.12+beta1 is not yet released (see this wiki page for the roadmap) but as suggested by @palmskog on Zulip, it can be useful to test projects with Coq 8.12+alpha in advance.

So a coqorg/coq:8.12 = coqorg/coq:8.12-alpha is now available and rebuilt every night from the v8.12 branch. Also, this PR will auto-deploy an accompanying version of mathcomp.dev in mathcomp/mathcomp-dev:coq-8.12.

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Jun 07 2020 at 19:26):

erikmd edited PR #524 [CI/CD] Deploy mathcomp/mathcomp-dev:coq-8.12 (with Coq 8.12+alpha) from coq-8.12 to master:

Motivation for this change

Coq 8.12+beta1 is not yet released (see this wiki page for the roadmap) but as suggested by @palmskog on Zulip, it can be useful to test projects with Coq 8.12+alpha in advance.

So a coqorg/coq:8.12 = coqorg/coq:8.12-alpha is now available and rebuilt every night from the v8.12 branch. Also, this PR will auto-deploy an accompanying version of mathcomp.dev in mathcomp/mathcomp-dev:coq-8.12.

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Jun 07 2020 at 19:28):

erikmd updated PR #524 [CI/CD] Deploy mathcomp/mathcomp-dev:coq-8.12 (with Coq 8.12+alpha) from coq-8.12 to master:

Motivation for this change

Coq 8.12+beta1 is not yet released (see this wiki page for the roadmap) but as suggested by @palmskog on Zulip, it can be useful to test projects with Coq 8.12+alpha in advance.

So a coqorg/coq:8.12 = coqorg/coq:8.12-alpha is now available and rebuilt every night from the v8.12 branch. Also, this PR will auto-deploy an accompanying version of mathcomp.dev in mathcomp/mathcomp-dev:coq-8.12.

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Jun 07 2020 at 19:30):

erikmd updated PR #524 [CI/CD] Deploy mathcomp/mathcomp-dev:coq-8.12 (with Coq 8.12+alpha) from coq-8.12 to master:

Motivation for this change

Coq 8.12+beta1 is not yet released (see this wiki page for the roadmap) but as suggested by @palmskog on Zulip, it can be useful to test projects with Coq 8.12+alpha in advance.

So a coqorg/coq:8.12 = coqorg/coq:8.12-alpha is now available and rebuilt every night from the v8.12 branch. Also, this PR will auto-deploy an accompanying version of mathcomp.dev in mathcomp/mathcomp-dev:coq-8.12.

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Jun 07 2020 at 21:38):

erikmd closed without merge PR #524 [CI/CD] Deploy mathcomp/mathcomp-dev:coq-8.12 (with Coq 8.12+alpha)

view this post on Zulip Mathcomp Github Bot (Jun 07 2020 at 21:38):

erikmd reopened PR #524 [CI/CD] Deploy mathcomp/mathcomp-dev:coq-8.12 (with Coq 8.12+alpha) from coq-8.12 to master:

Motivation for this change

Coq 8.12+beta1 is not yet released (see this wiki page for the roadmap) but as suggested by @palmskog on Zulip, it can be useful to test projects with Coq 8.12+alpha in advance.

So a coqorg/coq:8.12 = coqorg/coq:8.12-alpha is now available and rebuilt every night from the v8.12 branch. Also, this PR will auto-deploy an accompanying version of mathcomp.dev in mathcomp/mathcomp-dev:coq-8.12.

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Jun 08 2020 at 10:25):

CohenCyril merged PR #524 [CI/CD] Deploy mathcomp/mathcomp-dev:coq-8.12 (with Coq 8.12+alpha)

view this post on Zulip Mathcomp Github Bot (Jun 08 2020 at 10:25):

CohenCyril pushed 2 commits to branch master. Commits by CohenCyril (1) and erikmd (1).

view this post on Zulip Mathcomp Github Bot (Jun 08 2020 at 10:32):

CohenCyril updated PR #519 Missing homo/mono lemmas in the presence of cancellation from homomono_in to master:

Motivation for this change

The current section MonoHomoMorphismTheory_in from coq/theories/ssr/ssrbool.v is completely unusable because it's rD is too specific, and the cancellation hypothesis is too restrictive {on D, cancel f a g} which barely covers the use cases (e.g. in mathcomp/analysis).

Fixes #518

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Jun 08 2020 at 12:08):

CohenCyril submitted PR Review for #509 Card lemmas.

view this post on Zulip Mathcomp Github Bot (Jun 08 2020 at 12:08):

CohenCyril created PR Review Comment on #509 Card lemmas:

this is not resolved...

view this post on Zulip Mathcomp Github Bot (Jun 08 2020 at 12:09):

CohenCyril submitted PR Review for #509 Card lemmas.

view this post on Zulip Mathcomp Github Bot (Jun 08 2020 at 12:09):

CohenCyril created PR Review Comment on #509 Card lemmas:

move=> clfA; apply: (iffP card_gt0P) => [[x /andP[]]|[x xA]]; first by exists x.

view this post on Zulip Mathcomp Github Bot (Jun 08 2020 at 12:10):

CohenCyril submitted PR Review for #509 Card lemmas.

view this post on Zulip Mathcomp Github Bot (Jun 08 2020 at 12:10):

CohenCyril created PR Review Comment on #509 Card lemmas:

This change I suggested apparently causes an overflow of the 80 character liimit, I suggest splitting the line as follows:

exists [:: x; y]; rewrite /= !inE xDy.
by split=> // z; rewrite !inE => /pred2P[]->.

view this post on Zulip Mathcomp Github Bot (Jun 08 2020 at 12:12):

CohenCyril opened PR #525 Cachix action from cachix-action to master:

Motivation for this change

Fixes #523

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Jun 08 2020 at 12:23):

CohenCyril updated PR #525 Cachix action from cachix-action to master:

Motivation for this change

Fixes #523

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Jun 08 2020 at 12:27):

CohenCyril updated PR #525 Cachix action from cachix-action to master:

Motivation for this change

Fixes #523

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Yves Bertot (Jun 08 2020 at 12:36):

we are just about to merge #519 and then start the release process.

view this post on Zulip Yves Bertot (Jun 08 2020 at 12:36):

we wish to invite you on skype

view this post on Zulip Mathcomp Github Bot (Jun 08 2020 at 12:47):

affeldt-aist opened Issue #526 backport ssrbool and ssrfun to Coq:

Backport ssrbool.v (PR #513 PR #519 ) and ssrfun.v.

NB: https://github.com/affeldt-aist/coq/tree/ssrbool_backport_MathComp1.11
already contains an ssrbool.v file with PR #513 and PR #519.

@CohenCyril @ybertot

view this post on Zulip Mathcomp Github Bot (Jun 08 2020 at 12:47):

CohenCyril closed Issue #523 Cachix actions running and failing on forks:

Unlike the GitLab CI pipeline, which is not executed on forks of math-comp, the cachix actions are trying to execute and fail (while they succeed on the same commits in the math-comp context).

See https://github.com/chdoc/math-comp/runs/746817379

This means that updating the master branch of a fork generates emails about run failures.

view this post on Zulip Mathcomp Github Bot (Jun 08 2020 at 12:47):

CohenCyril merged PR #525 Cachix action.

view this post on Zulip Mathcomp Github Bot (Jun 08 2020 at 12:47):

CohenCyril pushed 1 commit to branch master.

view this post on Zulip Mathcomp Github Bot (Jun 08 2020 at 13:02):

affeldt-aist milestoned Issue #447 treating deprecation warnings that appear with coq-8.10 (assigned to CohenCyril):

Motivation for this change

<!-- please explain your reason for doing this change -->
Remove deprecation warnings that became apparent at the time of the 1.10.0 release.

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Jun 08 2020 at 13:02):

affeldt-aist demilestoned Issue #447 treating deprecation warnings that appear with coq-8.10 (assigned to CohenCyril):

Motivation for this change

<!-- please explain your reason for doing this change -->
Remove deprecation warnings that became apparent at the time of the 1.10.0 release.

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Jun 08 2020 at 13:06):

ybertot edited PR #519 Missing homo/mono lemmas in the presence of cancellation from homomono_in to master:

Motivation for this change

The current section MonoHomoMorphismTheory_in from coq/theories/ssr/ssrbool.v is completely unusable because it's rD is too specific, and the cancellation hypothesis is too restrictive {on D, cancel f a g} which barely covers the use cases (e.g. in mathcomp/analysis).

Fixes #518

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Jun 08 2020 at 13:06):

CohenCyril opened PR #527 Adding only parsong to notations in ssrAC from ssrAC_only_parsing_fix to master:

Motivation for this change

Silence warning by declaring some notations only parsing.

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Jun 08 2020 at 13:07):

affeldt-aist edited Issue #526 backport ssrbool and ssrfun to Coq:

TODO: Backport ssrbool.v (PR #513 PR #519 ) and ssrfun.v.

NB: https://github.com/affeldt-aist/coq/tree/ssrbool_backport_MathComp1.11
already contains an ssrbool.v file with PR #513 and PR #519.

@CohenCyril @ybertot

view this post on Zulip Mathcomp Github Bot (Jun 08 2020 at 13:10):

ybertot closed Issue #518 Missing mono/homo lemmas:

https://github.com/math-comp/analysis/blob/d38d70a1d224ca4b895375bb6f32639c4545bf32/theories/normedtype.v#L87-L196

view this post on Zulip Mathcomp Github Bot (Jun 08 2020 at 13:10):

ybertot merged PR #519 Missing homo/mono lemmas in the presence of cancellation.

view this post on Zulip Mathcomp Github Bot (Jun 08 2020 at 13:10):

ybertot pushed 6 commits to branch master. Commits by CohenCyril (3), affeldt-aist (2) and ybertot (1).

view this post on Zulip Mathcomp Github Bot (Jun 08 2020 at 13:17):

CohenCyril opened PR #528 silencing warnings in individual packages from silence_warnings to master:

Motivation for this change

Subsumes and closes #447
We opt for an aggressive silencing in package subdirectories Make in order for users of individual packages (through opam and nix mainly) to get no warnings.
We keep the current, light, silencing in the main Make to make sure we get some diagnostics.

We should open an issue for silencing in a better way (by fixing the code) from 1.12.0 is we support only Coq >= 8.10.0

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Jun 08 2020 at 13:17):

CohenCyril milestoned Issue #528 silencing warnings in individual packages:

Motivation for this change

Subsumes and closes #447
We opt for an aggressive silencing in package subdirectories Make in order for users of individual packages (through opam and nix mainly) to get no warnings.
We keep the current, light, silencing in the main Make to make sure we get some diagnostics.

We should open an issue for silencing in a better way (by fixing the code) from 1.12.0 is we support only Coq >= 8.10.0

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Jun 08 2020 at 13:23):

affeldt-aist opened Issue #529 Reducing the number of displayed warnings:

This issue records comments that occurred with PR #447
(merged on the occasion of the release of MathComp 1.11).

By default, there are many warnings and we do not want to have
too much of them when compiling, in particular for end-users
(likely to compile via opam and thus using Makefiles in MathComp
subdirectories).

Currently, we silence (see mathcomp/Make):

TODO:

@CohenCyril @ybertot

view this post on Zulip Mathcomp Github Bot (Jun 08 2020 at 13:35):

affeldt-aist edited Issue #529 Reducing the number of displayed warnings:

This issue records comments that occurred with PR #447
(merged on the occasion of the release of MathComp 1.11).

By default, there are many warnings and we do not want to have
too much of them when compiling, in particular for end-users
(likely to compile via opam and thus using Makefiles in MathComp
subdirectories).

See PR #528 for current policy.

Currently, we silence (see mathcomp/Make):

TODO:

@CohenCyril @ybertot

view this post on Zulip Mathcomp Github Bot (Jun 08 2020 at 13:42):

affeldt-aist edited Issue #526 backport ssrbool to Coq:

TODO: Backport ssrbool.v (PR #513 PR #519 ) and ssrfun.v.

NB: https://github.com/affeldt-aist/coq/tree/ssrbool_backport_MathComp1.11
already contains an ssrbool.v file with PR #513 and PR #519.

@CohenCyril @ybertot

view this post on Zulip Mathcomp Github Bot (Jun 08 2020 at 13:44):

affeldt-aist edited Issue #526 backport ssrbool to Coq:

Backport to Coq new contents from ssrbool.v (as introduced by PR #513 PR #519 ).

https://github.com/affeldt-aist/coq/tree/ssrbool_backport_MathComp1.11
already contains an ssrbool.v file with an integration of PR #513 and PR #519
and is ready to be PRed.

@CohenCyril @ybertot

(NB: this issue has been edited, it was mentioning ssrfun.v but its contents have already made their way to Coq)

view this post on Zulip Mathcomp Github Bot (Jun 08 2020 at 13:51):

affeldt-aist milestoned Issue #529 Reducing the number of displayed warnings:

This issue records comments that occurred with PR #447
(merged on the occasion of the release of MathComp 1.11).

By default, there are many warnings and we do not want to have
too much of them when compiling, in particular for end-users
(likely to compile via opam and thus using Makefiles in MathComp
subdirectories).

See PR #528 for current policy.

Currently, we silence (see mathcomp/Make):

TODO:

@CohenCyril @ybertot

view this post on Zulip Mathcomp Github Bot (Jun 08 2020 at 13:52):

affeldt-aist labeled Issue #529 Reducing the number of displayed warnings:

This issue records comments that occurred with PR #447
(merged on the occasion of the release of MathComp 1.11).

By default, there are many warnings and we do not want to have
too much of them when compiling, in particular for end-users
(likely to compile via opam and thus using Makefiles in MathComp
subdirectories).

See PR #528 for current policy.

Currently, we silence (see mathcomp/Make):

TODO:

@CohenCyril @ybertot

view this post on Zulip Mathcomp Github Bot (Jun 08 2020 at 13:52):

affeldt-aist milestoned Issue #526 backport ssrbool to Coq:

Backport to Coq new contents from ssrbool.v (as introduced by PR #513 PR #519 ).

https://github.com/affeldt-aist/coq/tree/ssrbool_backport_MathComp1.11
already contains an ssrbool.v file with an integration of PR #513 and PR #519
and is ready to be PRed.

@CohenCyril @ybertot

(NB: this issue has been edited, it was mentioning ssrfun.v but its contents have already made their way to Coq)

view this post on Zulip Mathcomp Github Bot (Jun 08 2020 at 14:48):

CohenCyril merged PR #528 silencing warnings in individual packages.

view this post on Zulip Mathcomp Github Bot (Jun 08 2020 at 14:48):

CohenCyril closed without merge PR #447 treating deprecation warnings that appear with coq-8.10.

view this post on Zulip Mathcomp Github Bot (Jun 08 2020 at 14:48):

CohenCyril pushed 2 commits to branch master.

view this post on Zulip Mathcomp Github Bot (Jun 08 2020 at 14:48):

coqbot demilestoned Issue #447 treating deprecation warnings that appear with coq-8.10 (assigned to CohenCyril):

Motivation for this change

<!-- please explain your reason for doing this change -->
Remove deprecation warnings that became apparent at the time of the 1.10.0 release.

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Jun 08 2020 at 14:48):

CohenCyril opened PR #530 More CI from moreCI to master:

Motivation for this change

<!-- please explain your reason for doing this change -->

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Jun 08 2020 at 14:49):

CohenCyril updated PR #530 More CI from moreCI to master:

Motivation for this change

<!-- please explain your reason for doing this change -->

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Jun 08 2020 at 15:31):

CohenCyril opened PR #531 turning let into local definition from fix_cyclotomic to master:

Motivation for this change

This silences a warning, by replacing a toplevel Let with a Local Definition as sugested by the warning.
```
Warning: Interpreting this declaration as if a global declaration prefixed by
"Local", i.e. as a global declaration which shall not be available without
qualification when imported. [local-declaration,scope]

##### Things done/to do

<!-- please fill in the following checklist -->

- ~added corresponding entries in `CHANGELOG_UNRELEASED.md`~
- ~added corresponding documentation in the headers~
<!-- Cross-out the above items using ~crossed out item~ if they happen not to be relevent -->
<!-- You may also add more items to explain what you did and what remains to do -->

<!-- leave this note as a reminder to reviewers -->
##### Automatic note to reviewers

Read [this Checklist](https://github.com/math-comp/math-comp/wiki/Checklist-for-following,-reviewing-and-playing-with-a-PR#checklist-for-reviewing-a-pr) and make sure there is a milestone.

~~~

view this post on Zulip Mathcomp Github Bot (Jun 08 2020 at 20:02):

CohenCyril milestoned Issue #531 turning let into local definition:

Motivation for this change

This silences a warning, by replacing a toplevel Let with a Local Definition as sugested by the warning.
```
Warning: Interpreting this declaration as if a global declaration prefixed by
"Local", i.e. as a global declaration which shall not be available without
qualification when imported. [local-declaration,scope]

##### Things done/to do

<!-- please fill in the following checklist -->

- ~added corresponding entries in `CHANGELOG_UNRELEASED.md`~
- ~added corresponding documentation in the headers~
<!-- Cross-out the above items using ~crossed out item~ if they happen not to be relevent -->
<!-- You may also add more items to explain what you did and what remains to do -->

<!-- leave this note as a reminder to reviewers -->
##### Automatic note to reviewers

Read [this Checklist](https://github.com/math-comp/math-comp/wiki/Checklist-for-following,-reviewing-and-playing-with-a-PR#checklist-for-reviewing-a-pr) and make sure there is a milestone.

~~~

view this post on Zulip Mathcomp Github Bot (Jun 08 2020 at 20:02):

CohenCyril merged PR #531 turning let into local definition.

view this post on Zulip Mathcomp Github Bot (Jun 08 2020 at 20:02):

CohenCyril pushed 2 commits to branch master.

view this post on Zulip Mathcomp Github Bot (Jun 08 2020 at 23:18):

CohenCyril opened PR #532 fix coq 8.12 warnings from silence-8.12-warnings to master:

Motivation for this change

We address new warnings that arise from coq 8.12

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Jun 08 2020 at 23:18):

CohenCyril edited PR #527 Adding only parsing to notations in ssrAC from ssrAC_only_parsing_fix to master:

Motivation for this change

Silence warning by declaring some notations only parsing.

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Jun 09 2020 at 00:01):

CohenCyril updated PR #532 fix coq 8.12 warnings from silence-8.12-warnings to master:

Motivation for this change

We address new warnings that arise from coq 8.12

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Jun 09 2020 at 02:45):

CohenCyril updated PR #532 fix coq 8.12 warnings from silence-8.12-warnings to master:

Motivation for this change

We address new warnings that arise from coq 8.12

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Jun 09 2020 at 02:45):

CohenCyril milestoned Issue #532 fix coq 8.12 warnings:

Motivation for this change

We address new warnings that arise from coq 8.12

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Jun 09 2020 at 04:27):

CohenCyril merged PR #532 fix coq 8.12 warnings.

view this post on Zulip Mathcomp Github Bot (Jun 09 2020 at 04:27):

CohenCyril pushed 2 commits to branch master.

view this post on Zulip Mathcomp Github Bot (Jun 09 2020 at 12:45):

ybertot:

view this post on Zulip Mathcomp Github Bot (Jun 09 2020 at 12:46):

ybertot:

view this post on Zulip Mathcomp Github Bot (Jun 09 2020 at 12:47):

ybertot:

view this post on Zulip Mathcomp Github Bot (Jun 09 2020 at 12:56):

CohenCyril:

view this post on Zulip Mathcomp Github Bot (Jun 09 2020 at 12:56):

CohenCyril:

view this post on Zulip Mathcomp Github Bot (Jun 09 2020 at 12:57):

CohenCyril:

view this post on Zulip Mathcomp Github Bot (Jun 09 2020 at 12:58):

CohenCyril:

view this post on Zulip Mathcomp Github Bot (Jun 09 2020 at 13:01):

affeldt-aist opened PR #533 edit changelogs before release from changelogs_before_release to master:

Motivation for this change

Update changelogs before release

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Jun 09 2020 at 13:01):

affeldt-aist requested CohenCyril for a review on PR #533 edit changelogs before release.

view this post on Zulip Mathcomp Github Bot (Jun 09 2020 at 13:02):

affeldt-aist requested CohenCyril and ybertot for a review on PR #533 edit changelogs before release.

view this post on Zulip Mathcomp Github Bot (Jun 09 2020 at 13:06):

affeldt-aist updated PR #533 edit changelogs before release from changelogs_before_release to master:

Motivation for this change

Update changelogs before release

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Jun 09 2020 at 13:08):

CohenCyril:

view this post on Zulip Mathcomp Github Bot (Jun 09 2020 at 13:11):

affeldt-aist updated PR #533 edit changelogs before release from changelogs_before_release to master:

Motivation for this change

Update changelogs before release

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Jun 09 2020 at 13:11):

ybertot:

view this post on Zulip Mathcomp Github Bot (Jun 09 2020 at 13:13):

CohenCyril:

view this post on Zulip Mathcomp Github Bot (Jun 09 2020 at 13:14):

CohenCyril:

view this post on Zulip Mathcomp Github Bot (Jun 09 2020 at 13:15):

CohenCyril milestoned Issue #533 edit changelogs before release:

Motivation for this change

Update changelogs before release

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Jun 09 2020 at 13:16):

CohenCyril submitted PR Review for #533 edit changelogs before release.

view this post on Zulip Mathcomp Github Bot (Jun 09 2020 at 13:50):

CohenCyril opened PR #534 add lua&sed to shell and switch to coq 8.11 + fixing doc from doc-1.11 to master:

Motivation for this change
Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Jun 09 2020 at 13:51):

CohenCyril edited PR #534 add lua&sed to nixshell and switch to coq 8.11 + fixing doc from doc-1.11 to master:

Motivation for this change
Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Jun 09 2020 at 13:51):

CohenCyril merged PR #534 add lua&sed to nixshell and switch to coq 8.11 + fixing doc.

view this post on Zulip Mathcomp Github Bot (Jun 09 2020 at 13:51):

CohenCyril pushed 2 commits to branch master.

view this post on Zulip Mathcomp Github Bot (Jun 09 2020 at 13:53):

affeldt-aist merged PR #533 edit changelogs before release.

view this post on Zulip Mathcomp Github Bot (Jun 09 2020 at 13:53):

affeldt-aist pushed 2 commits to branch master.

view this post on Zulip Mathcomp Github Bot (Jun 09 2020 at 13:54):

CohenCyril milestoned Issue #534 add lua&sed to nixshell and switch to coq 8.11 + fixing doc:

Motivation for this change
Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Jun 09 2020 at 14:00):

ybertot created release The Mathematical Components Library 1.11.0 for tag mathcomp-1.11.0.

view this post on Zulip Mathcomp Github Bot (Jun 09 2020 at 14:00):

ybertot published release The Mathematical Components Library 1.11.0 for tag mathcomp-1.11.0.

view this post on Zulip Mathcomp Github Bot (Jun 09 2020 at 14:00):

ybertot prereleased release The Mathematical Components Library 1.11.0 for tag mathcomp-1.11.0.

view this post on Zulip Mathcomp Github Bot (Jun 09 2020 at 14:00):

ybertot pushed tag mathcomp-1.11.0.

view this post on Zulip Mathcomp Github Bot (Jun 09 2020 at 14:02):

ybertot released release The Mathematical Components Library 1.11.0 for tag mathcomp-1.11.0.

view this post on Zulip Mathcomp Github Bot (Jun 09 2020 at 14:02):

CohenCyril deleted release The Mathematical Components Library 1.11.0+beta1 for tag mathcomp-1.11.0+beta1.

view this post on Zulip Mathcomp Github Bot (Jun 09 2020 at 14:03):

CohenCyril edited release The Mathematical Components Library 1.11.0 for tag mathcomp-1.11.0.

view this post on Zulip Mathcomp Github Bot (Jun 09 2020 at 14:06):

CohenCyril:

view this post on Zulip Mathcomp Github Bot (Jun 09 2020 at 14:09):

CohenCyril:

view this post on Zulip Mathcomp Github Bot (Jun 09 2020 at 14:16):

CohenCyril pushed 1 commit to branch master.

view this post on Zulip Mathcomp Github Bot (Jun 09 2020 at 14:22):

ybertot:

view this post on Zulip Mathcomp Github Bot (Jun 09 2020 at 14:27):

CohenCyril pushed 1 commit to branch master.

view this post on Zulip Mathcomp Github Bot (Jun 09 2020 at 14:35):

CohenCyril edited release The Mathematical Components Library 1.11.0 for tag mathcomp-1.11.0.

view this post on Zulip Mathcomp Github Bot (Jun 09 2020 at 14:43):

CohenCyril:

view this post on Zulip Mathcomp Github Bot (Jun 09 2020 at 14:51):

CohenCyril:

view this post on Zulip Mathcomp Github Bot (Jun 09 2020 at 14:55):

CohenCyril edited release The Mathematical Components Library 1.11+beta1 for tag mathcomp-1.11+beta1.

view this post on Zulip Mathcomp Github Bot (Jun 09 2020 at 15:03):

CohenCyril pushed 1 commit to branch master.

view this post on Zulip Mathcomp Github Bot (Jun 09 2020 at 15:09):

CohenCyril pushed 1 commit to branch master.

view this post on Zulip Mathcomp Github Bot (Jun 09 2020 at 15:26):

CohenCyril:

view this post on Zulip Mathcomp Github Bot (Jun 09 2020 at 15:29):

ybertot:

view this post on Zulip Mathcomp Github Bot (Jun 10 2020 at 11:24):

ybertot:

view this post on Zulip Mathcomp Github Bot (Jun 10 2020 at 13:38):

CohenCyril opened PR #535 Generated opam packages allow coq-dev again from allow-coq-dev to master:

Motivation for this change

As a result of a discussion on Zulip
Reverts "removing opam | (= "dev") for released packages"
(commit 313e44316177c918b363c118f15297e08d13eb4e).

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Jun 10 2020 at 13:38):

CohenCyril merged PR #535 Generated opam packages allow coq-dev again.

view this post on Zulip Mathcomp Github Bot (Jun 10 2020 at 13:38):

CohenCyril pushed 2 commits to branch master.

view this post on Zulip Mathcomp Github Bot (Jun 10 2020 at 14:27):

CohenCyril updated PR #501 Intro pattern extensions for rewrite, dup, swap and apply (assigned to gares) from intro_rw to master:

Motivation for this change

Intro pattern ltac views (rewrite, dup, swap, apply) in order not to break intro patterns for silly rewrites.

- calling rewrite from an intro pattern, use with parsimony
=> /[1! rules] does rewrite rules
=> /[! rules] does rewrite !rules

- top of the stack actions:
=> /apply does => hyp {}/hyp
=> /swap does => x y; move: y x (also swap and perserves let bindings)
=> /dup does => x; have copy := x; move: copy x (also copies and preserves let bindings)

This is a part of #372, simplified, rewritten and rebased.

Things done/to do

<!-- please fill in the following checklist -->

<!-- Cross-out the above items using ~crossed out item~ if they happen not to be relevent -->
<!-- You may also add more items to explain what you did and what remains to do -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Jun 10 2020 at 15:54):

CohenCyril edited PR #530 More CI from moreCI to master:

Motivation for this change

<!-- please explain your reason for doing this change -->

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Jun 10 2020 at 20:13):

CohenCyril updated PR #521 In and on from in_on to master:

Motivation for this change

These new lemmas describe more precisely the possible interactions between in and on.

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Jun 13 2020 at 12:03):

pi8027 updated PR #507 Add more test cases for higher-order recursive functions in seq.v w.r.t. the guard condition from test-guard-cond to master:

Motivation for this change

This PR adds some test cases in test_suite/test_guard.v which I promised to do in https://github.com/math-comp/math-comp/pull/471#issuecomment-611521366. Currently, test cases for find, filter, count, pmap, pairmap, scanl are missing.

<!-- please explain your reason for doing this change -->

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Jun 13 2020 at 13:07):

pi8027 updated PR #464 [WIP] meet semilattice structures from semilattices to master:

Motivation for this change

This PR adds the following structures:

cc: @strub

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Jun 13 2020 at 13:07):

pi8027 updated PR #494 Get rid of displays in class fields and mixin parameters (assigned to CohenCyril) from rm-displays-in-classes to master:

Motivation for this change

This PR removes displays from class fields and mixin parameters, and also refactor factories and builders, as preliminary work for PR #464.

<!-- please explain your reason for doing this change -->

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Jun 14 2020 at 13:19):

pi8027 updated PR #458 [WIP] new interval library from interval to master:

Motivation for this change

This PR generalizes the results in interval.v using order structures. The main achievements are that intervals on a latticeType form a latticeType where join is the intersection and meet is the convex hull, and intervals on an orderType form a distrLatticeType as well.

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Jun 14 2020 at 13:35):

pi8027 updated PR #458 [WIP] new interval library from interval to master:

Motivation for this change

This PR generalizes the results in interval.v using order structures. The main achievements are that intervals on a latticeType form a latticeType where join is the intersection and meet is the convex hull, and intervals on an orderType form a distrLatticeType as well.

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Jun 15 2020 at 17:26):

pi8027 opened PR #536 Fix some hierarchy.ml related issues from hierarchy to master:

Motivation for this change
Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Jun 15 2020 at 17:44):

pi8027 edited PR #536 Fix some hierarchy.ml related issues from hierarchy to master:

Motivation for this change
Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Jun 15 2020 at 18:26):

pi8027 submitted PR Review for #536 Fix some hierarchy.ml related issues.

view this post on Zulip Mathcomp Github Bot (Jun 15 2020 at 18:26):

pi8027 created PR Review Comment on #536 Fix some hierarchy.ml related issues:

@CohenCyril I meant "order-only prerequisites" in this documentation. If we remove this pipe symbol, repeating make test-suite forces us to rerun the test suite.

view this post on Zulip Mathcomp Github Bot (Jun 15 2020 at 18:45):

pi8027 submitted PR Review for #536 Fix some hierarchy.ml related issues.

view this post on Zulip Mathcomp Github Bot (Jun 15 2020 at 18:45):

pi8027 created PR Review Comment on #536 Fix some hierarchy.ml related issues:

After re-reading the documentation, I think this is not the right solution. Sorry for the mess.

view this post on Zulip Mathcomp Github Bot (Jun 15 2020 at 20:00):

CohenCyril submitted PR Review for #499 contra lemmas involving propositions.

view this post on Zulip Mathcomp Github Bot (Jun 15 2020 at 20:00):

CohenCyril submitted PR Review for #499 contra lemmas involving propositions.

view this post on Zulip Mathcomp Github Bot (Jun 15 2020 at 20:00):

CohenCyril created PR Review Comment on #499 contra lemmas involving propositions:

auto has an impredictable behavior wrt the use of the section context. So I'd recommend doing the proof by hand or writing an explicit Proof using T1. to make sure T2 is not pulled in by accident...

view this post on Zulip Mathcomp Github Bot (Jun 16 2020 at 06:12):

pi8027 edited PR #536 Fix some hierarchy.ml related issues from hierarchy to master:

Motivation for this change
Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Jun 16 2020 at 06:13):

pi8027 updated PR #536 Fix some hierarchy.ml related issues from hierarchy to master:

Motivation for this change
Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Jun 16 2020 at 08:55):

gares:

view this post on Zulip Mathcomp Github Bot (Jun 16 2020 at 08:55):

gares:

view this post on Zulip Mathcomp Github Bot (Jun 16 2020 at 09:34):

gares:

view this post on Zulip Mathcomp Github Bot (Jun 16 2020 at 09:39):

CohenCyril closed Issue #327 Issue with the Howto release:

Missing steps for Howto Release:

cc @gares
cc @erikmd

view this post on Zulip Mathcomp Github Bot (Jun 16 2020 at 10:09):

gares:

view this post on Zulip Mathcomp Github Bot (Jun 16 2020 at 10:24):

gares:

view this post on Zulip Mathcomp Github Bot (Jun 16 2020 at 11:00):

pi8027 updated PR #536 Fix some hierarchy.ml related issues from hierarchy to master:

Motivation for this change
Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Jun 16 2020 at 13:21):

CohenCyril:

view this post on Zulip Mathcomp Github Bot (Jun 16 2020 at 21:47):

affeldt-aist opened PR #537 missing bigop lemmas from from_analysis_20200617 to master:

Co-authored-by: Cohen Cyril <cyril.cohen@inria.fr>

Motivation for this change

missing lemmas discovered while developing mathcomp-analysis

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Jun 17 2020 at 08:25):

chdoc updated PR #499 contra lemmas involving propositions from contra-prop to master:

Motivation for this change

Various forms of contraposition are constructively provable and having a collection of lemmas whose naming is consistent with the contra lemmas already in mathcomp makes it easier and more idiomatic to use them.

fixes #491

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Jun 17 2020 at 08:37):

chdoc updated PR #499 contra lemmas involving propositions from contra-prop to master:

Motivation for this change

Various forms of contraposition are constructively provable and having a collection of lemmas whose naming is consistent with the contra lemmas already in mathcomp makes it easier and more idiomatic to use them.

fixes #491

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Jun 17 2020 at 08:50):

chdoc submitted PR Review for #499 contra lemmas involving propositions.

view this post on Zulip Mathcomp Github Bot (Jun 17 2020 at 08:50):

chdoc created PR Review Comment on #499 contra lemmas involving propositions:

Done.

view this post on Zulip Mathcomp Github Bot (Jun 17 2020 at 08:59):

chdoc updated PR #509 Card lemmas from card-lemmas to master:

Motivation for this change

Additional lemmas about cardinalities of predicates and sets. Mainly picking n distinct elements for an a predicate with n <= #|A|.

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Jun 17 2020 at 08:59):

chdoc updated PR #509 Card lemmas from card-lemmas to master:

Motivation for this change

Additional lemmas about cardinalities of predicates and sets. Mainly picking n distinct elements for an a predicate with n <= #|A|.

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Jun 17 2020 at 09:45):

chdoc updated PR #509 Card lemmas from card-lemmas to master:

Motivation for this change

Additional lemmas about cardinalities of predicates and sets. Mainly picking n distinct elements for an a predicate with n <= #|A|.

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Jun 17 2020 at 12:08):

CohenCyril submitted PR Review for #509 Card lemmas.

view this post on Zulip Mathcomp Github Bot (Jun 17 2020 at 12:08):

CohenCyril created PR Review Comment on #509 Card lemmas:

One last nitpicking that I did not see (we should really have a linter):

  reflect (exists x y z, [/\ x \in A, y \in A & z \in A] /\ [/\ x != y, y != z & z != x])

view this post on Zulip Mathcomp Github Bot (Jun 17 2020 at 12:09):

CohenCyril updated PR #509 Card lemmas from card-lemmas to master:

Motivation for this change

Additional lemmas about cardinalities of predicates and sets. Mainly picking n distinct elements for an a predicate with n <= #|A|.

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Jun 17 2020 at 12:09):

CohenCyril updated PR #509 Card lemmas from card-lemmas to master:

Motivation for this change

Additional lemmas about cardinalities of predicates and sets. Mainly picking n distinct elements for an a predicate with n <= #|A|.

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Jun 17 2020 at 12:09):

CohenCyril submitted PR Review for #509 Card lemmas.

view this post on Zulip Mathcomp Github Bot (Jun 17 2020 at 12:26):

CohenCyril submitted PR Review for #509 Card lemmas.

view this post on Zulip Mathcomp Github Bot (Jun 17 2020 at 12:41):

CohenCyril created PR Review Comment on #537 missing bigop lemmas:

In ssrnum, %O can and must be omitted (unless I am mistaken, but if they can, they must).

view this post on Zulip Mathcomp Github Bot (Jun 17 2020 at 12:41):

CohenCyril submitted PR Review for #537 missing bigop lemmas.

view this post on Zulip Mathcomp Github Bot (Jun 17 2020 at 12:43):

CohenCyril submitted PR Review for #499 contra lemmas involving propositions.

view this post on Zulip Mathcomp Github Bot (Jun 17 2020 at 12:47):

CohenCyril closed Issue #491 "contra" lemmas for propositions:

I've grown quite accustomed to using the various "contra" lemmas to be found ssrbool. However, sometimes the involved facts are actual propositions and their negations. For this purpose, I've started to use the following collection of lemmas:

Lemma contraTnot b (P : Prop) : (P -> ~~ b) -> (b -> ~ P).
Lemma contraNnot (b : bool) (P : Prop) : (P -> b) -> (~~ b -> ~ P).
Lemma contraPT (P : Prop) (b : bool) : (~~ b -> ~ P) -> P -> b.
Lemma contra_notT (b : bool) (P : Prop) : (~~ b -> P) -> ~ P -> b.
Lemma contraPN (b : bool) (P : Prop) : (b -> ~ P) -> (P -> ~~ b).
Lemma contraPneq (T:eqType) (a b : T) (P : Prop) : (a = b -> ~ P) -> (P -> a != b).
Lemma contraPeq (T:eqType) (a b : T) (P : Prop) : (a != b -> ~ P) -> (P -> a = b).

The naming scheme is inspired by the remaining contra lemmas, using "P" for assumptions with type in Prop and "not" for ~ P. Do you think this is useful? Should I create a pull request?

view this post on Zulip Mathcomp Github Bot (Jun 17 2020 at 12:47):

CohenCyril merged PR #499 contra lemmas involving propositions.

view this post on Zulip Mathcomp Github Bot (Jun 17 2020 at 12:47):

CohenCyril pushed 2 commits to branch master. Commits by CohenCyril (1) and chdoc (1).

view this post on Zulip Mathcomp Github Bot (Jun 17 2020 at 12:52):

affeldt-aist updated PR #537 missing bigop lemmas from from_analysis_20200617 to master:

Co-authored-by: Cohen Cyril <cyril.cohen@inria.fr>

Motivation for this change

missing lemmas discovered while developing mathcomp-analysis

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Jun 17 2020 at 12:54):

affeldt-aist updated PR #537 missing bigop lemmas from from_analysis_20200617 to master:

Co-authored-by: Cohen Cyril <cyril.cohen@inria.fr>

Motivation for this change

missing lemmas discovered while developing mathcomp-analysis

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Jun 17 2020 at 13:13):

thery requested thery for a review on PR #537 missing bigop lemmas.

view this post on Zulip Mathcomp Github Bot (Jun 17 2020 at 13:14):

thery milestoned Issue #537 missing bigop lemmas:

Co-authored-by: Cohen Cyril <cyril.cohen@inria.fr>

Motivation for this change

missing lemmas discovered while developing mathcomp-analysis

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Jun 17 2020 at 13:17):

CohenCyril submitted PR Review for #507 Add more test cases for higher-order recursive functions in seq.v w.r.t. the guard condition.

view this post on Zulip Mathcomp Github Bot (Jun 18 2020 at 09:18):

chdoc updated PR #509 Card lemmas from card-lemmas to master:

Motivation for this change

Additional lemmas about cardinalities of predicates and sets. Mainly picking n distinct elements for an a predicate with n <= #|A|.

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Jun 18 2020 at 11:21):

affeldt-aist edited Issue #526 backport ssrbool to Coq:

Backport to Coq new contents from ssrbool.v (as introduced by PR #513 PR #519 PR #499 ).

https://github.com/affeldt-aist/coq/tree/ssrbool_backport_MathComp1.11
already contains an ssrbool.v file with an integration of PR #513, PR #519, and PR #499
and is ready to be PRed.

@CohenCyril @ybertot

(NB: this issue has been edited, it was mentioning ssrfun.v but its contents have already made their way to Coq)

view this post on Zulip Mathcomp Github Bot (Jun 18 2020 at 14:46):

chdoc updated PR #509 Card lemmas from card-lemmas to master:

Motivation for this change

Additional lemmas about cardinalities of predicates and sets. Mainly picking n distinct elements for an a predicate with n <= #|A|.

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Jun 18 2020 at 14:56):

chdoc:

view this post on Zulip Mathcomp Github Bot (Jun 18 2020 at 14:57):

chdoc:

view this post on Zulip Mathcomp Github Bot (Jun 19 2020 at 02:59):

CohenCyril submitted PR Review for #509 Card lemmas.

view this post on Zulip Mathcomp Github Bot (Jun 19 2020 at 02:59):

CohenCyril merged PR #509 Card lemmas.

view this post on Zulip Mathcomp Github Bot (Jun 19 2020 at 02:59):

CohenCyril pushed 8 commits to branch master. Commits by chdoc (6) and CohenCyril (2).

view this post on Zulip Mathcomp Github Bot (Jun 19 2020 at 09:20):

pi8027 opened Issue #538 Shouldn't notations dual_(bottom|top|join|meet|max|min) be qualified by Order module?

https://github.com/math-comp/math-comp/blob/f25ef67ad2f58a30f1e700da89811b193755d84e/mathcomp/ssreflect/order.v#L2541-L2546

Since Order.bottom, etc. are qualified, I thought they should, but actually they are not. @CohenCyril

view this post on Zulip Mathcomp Github Bot (Jun 19 2020 at 18:26):

pi8027 edited Issue #538 Notations dual_(bottom|top|join|meet|max|min) should be qualified by the Order module:

https://github.com/math-comp/math-comp/blob/f25ef67ad2f58a30f1e700da89811b193755d84e/mathcomp/ssreflect/order.v#L2541-L2546

Since Order.bottom, etc. are qualified, I thought they should, but actually they are not. @CohenCyril

view this post on Zulip Mathcomp Github Bot (Jun 22 2020 at 07:03):

pi8027 updated PR #494 Get rid of displays in class fields and mixin parameters (assigned to CohenCyril) from rm-displays-in-classes to master:

Motivation for this change

This PR removes displays from class fields and mixin parameters, and also refactor factories and builders, as preliminary work for PR #464.

<!-- please explain your reason for doing this change -->

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Jun 22 2020 at 07:03):

pi8027 updated PR #464 [WIP] meet semilattice structures from semilattices to master:

Motivation for this change

This PR adds the following structures:

cc: @strub

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Jun 22 2020 at 07:04):

pi8027 edited PR #494 Get rid of displays in class fields and mixin parameters (assigned to CohenCyril) from rm-displays-in-classes to master:

Motivation for this change

This PR removes displays from class fields and mixin parameters, and also refactor factories and builders, as preliminary work for PR #464.

<!-- please explain your reason for doing this change -->

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Jun 22 2020 at 07:04):

pi8027 edited PR #494 Get rid of displays in class fields and mixin parameters (assigned to CohenCyril) from rm-displays-in-classes to master:

Motivation for this change

This PR removes displays from class fields and mixin parameters, and also refactor factories and builders, as preliminary work for PR #464.

<!-- please explain your reason for doing this change -->

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Jun 24 2020 at 13:53):

thery submitted PR Review for #537 missing bigop lemmas.

view this post on Zulip Mathcomp Github Bot (Jun 24 2020 at 13:53):

thery submitted PR Review for #537 missing bigop lemmas.

view this post on Zulip Mathcomp Github Bot (Jun 24 2020 at 13:53):

thery created PR Review Comment on #537 missing bigop lemmas:

Maybe in two moves (there is a iter_addn_0 for nat)

Lemma iter_addr_0 n (m : V) : iter n (+%R m) 0 = m *+ n.
Proof. by elim: n => //= n ->; rewrite mulrS. Qed.

Lemma sumr_const_nat (m n : nat) (x : V) :
   \sum_(n <= i < m) x = x *+ (m - n).
Proof. by rewrite big_const_nat iter_addr_0. Qed.

view this post on Zulip Mathcomp Github Bot (Jun 24 2020 at 13:53):

thery created PR Review Comment on #537 missing bigop lemmas:

Maybe this is simpler

Lemma ler_sum_nat  (m n : nat) (F G : nat -> R) :
  (forall i, (m <= i < n)%N -> F i <= G i) ->
  \sum_(m <= i < n) F i <= \sum_(m <= i < n) G i.
Proof.
move=> leFG.
by rewrite ![\sum_(_ <= _ < _) _]big_nat_cond ler_sum // => i /andP[] /leFG.
Qed.

view this post on Zulip Mathcomp Github Bot (Jun 24 2020 at 14:05):

thery opened PR #539 simpler proof from sum_nat_const to master:

Motivation for this change

While reviewing #537. I've noticed that we could take advantage of iter_addn_0 to simplify the proof of sum_nat_const_nat

<!-- please explain your reason for doing this change -->

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Jun 24 2020 at 14:06):

thery edited PR #539 simpler proof of sum_nat_const_nat in bigop from sum_nat_const to master:

Motivation for this change

While reviewing #537. I've noticed that we could take advantage of iter_addn_0 to simplify the proof of sum_nat_const_nat

<!-- please explain your reason for doing this change -->

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Jun 24 2020 at 14:06):

thery edited PR #539 simpler proof of sum_nat_const_nat in bigop.v from sum_nat_const to master:

Motivation for this change

While reviewing #537. I've noticed that we could take advantage of iter_addn_0 to simplify the proof of sum_nat_const_nat

<!-- please explain your reason for doing this change -->

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Jun 24 2020 at 14:06):

thery edited PR #539 simpler proof of sum_nat_const_nat in bigop.v from sum_nat_const to master:

Motivation for this change

While reviewing #537. I've noticed that we could take advantage of iter_addn_0 to simplify the proof of sum_nat_const_nat

<!-- please explain your reason for doing this change -->

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Jun 24 2020 at 14:11):

CohenCyril edited PR #539 simpler proof of sum_nat_const_nat in bigop.v from sum_nat_const to master:

Motivation for this change

While reviewing #537. I've noticed that we could take advantage of iter_addn_0 to simplify the proof of sum_nat_const_nat

<!-- please explain your reason for doing this change -->

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Jun 24 2020 at 14:12):

CohenCyril submitted PR Review for #539 simpler proof of sum_nat_const_nat in bigop.v.

view this post on Zulip Mathcomp Github Bot (Jun 24 2020 at 14:29):

CohenCyril pushed 2 commits to branch pr/537. Commits by CohenCyril (1) and affeldt-aist (1).

view this post on Zulip Mathcomp Github Bot (Jun 24 2020 at 14:29):

CohenCyril pushed the branch pulls/537.

view this post on Zulip Mathcomp Github Bot (Jun 24 2020 at 14:29):

CohenCyril deleted the branch pulls/537.

view this post on Zulip Mathcomp Github Bot (Jun 24 2020 at 14:29):

CohenCyril deleted the branch pr/537.

view this post on Zulip Mathcomp Github Bot (Jun 24 2020 at 14:30):

CohenCyril pushed 2 commits to branch pull/537. Commits by CohenCyril (1) and affeldt-aist (1).

view this post on Zulip Mathcomp Github Bot (Jun 24 2020 at 14:30):

CohenCyril deleted the branch pull/537.

view this post on Zulip Mathcomp Github Bot (Jun 24 2020 at 14:31):

CohenCyril pushed 2 commits to branch pull/537/head. Commits by CohenCyril (1) and affeldt-aist (1).

view this post on Zulip Mathcomp Github Bot (Jun 24 2020 at 14:31):

CohenCyril deleted the branch pull/537/head.

view this post on Zulip Mathcomp Github Bot (Jun 24 2020 at 14:32):

CohenCyril updated PR #537 missing bigop lemmas from from_analysis_20200617 to master:

Co-authored-by: Cohen Cyril <cyril.cohen@inria.fr>

Motivation for this change

missing lemmas discovered while developing mathcomp-analysis

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Jun 24 2020 at 15:30):

thery opened PR #540 fix the doc for ubnP in ssrnat from doc to master:

Motivation for this change

<!-- please explain your reason for doing this change -->

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Jun 24 2020 at 15:30):

thery edited PR #540 fix the doc for ubnP in ssrnat from doc to master:

Motivation for this change

<!-- please explain your reason for doing this change -->

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Jun 24 2020 at 15:30):

thery requested ggonthier for a review on PR #540 fix the doc for ubnP in ssrnat.

view this post on Zulip Mathcomp Github Bot (Jun 24 2020 at 15:30):

thery requested ybertot for a review on PR #540 fix the doc for ubnP in ssrnat.

view this post on Zulip Mathcomp Github Bot (Jun 24 2020 at 16:12):

CohenCyril updated PR #537 missing bigop lemmas from from_analysis_20200617 to master:

Co-authored-by: Cohen Cyril <cyril.cohen@inria.fr>

Motivation for this change

missing lemmas discovered while developing mathcomp-analysis

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Jun 24 2020 at 16:13):

CohenCyril updated PR #537 missing bigop lemmas from from_analysis_20200617 to master:

Co-authored-by: Cohen Cyril <cyril.cohen@inria.fr>

Motivation for this change

missing lemmas discovered while developing mathcomp-analysis

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Jun 24 2020 at 16:15):

CohenCyril edited PR #540 fix the doc for ubnP in ssrnat from doc to master:

Motivation for this change

<!-- please explain your reason for doing this change -->

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Jun 24 2020 at 16:15):

thery merged PR #537 missing bigop lemmas.

view this post on Zulip Mathcomp Github Bot (Jun 24 2020 at 16:15):

thery pushed 2 commits to branch master. Commits by affeldt-aist (1) and thery (1).

view this post on Zulip Mathcomp Github Bot (Jun 24 2020 at 16:15):

CohenCyril submitted PR Review for #540 fix the doc for ubnP in ssrnat.

view this post on Zulip Mathcomp Github Bot (Jun 24 2020 at 16:16):

CohenCyril milestoned Issue #540 fix the doc for ubnP in ssrnat:

Motivation for this change

<!-- please explain your reason for doing this change -->

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Jun 24 2020 at 16:16):

CohenCyril milestoned Issue #539 simpler proof of sum_nat_const_nat in bigop.v:

Motivation for this change

While reviewing #537. I've noticed that we could take advantage of iter_addn_0 to simplify the proof of sum_nat_const_nat

<!-- please explain your reason for doing this change -->

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Jun 24 2020 at 16:17):

CohenCyril merged PR #539 simpler proof of sum_nat_const_nat in bigop.v.

view this post on Zulip Mathcomp Github Bot (Jun 24 2020 at 16:17):

CohenCyril pushed 2 commits to branch master. Commits by CohenCyril (1) and thery (1).

view this post on Zulip Mathcomp Github Bot (Jun 24 2020 at 16:24):

CohenCyril merged PR #540 fix the doc for ubnP in ssrnat.

view this post on Zulip Mathcomp Github Bot (Jun 24 2020 at 16:24):

CohenCyril pushed 2 commits to branch master. Commits by CohenCyril (1) and thery (1).

view this post on Zulip Mathcomp Github Bot (Jun 25 2020 at 23:12):

CohenCyril requested maximedenes for a review on PR #536 Fix some hierarchy.ml related issues.

view this post on Zulip Mathcomp Github Bot (Jun 25 2020 at 23:12):

CohenCyril assigned PR #536 Fix some hierarchy.ml related issues to CohenCyril.

view this post on Zulip Mathcomp Github Bot (Jun 25 2020 at 23:17):

CohenCyril:

view this post on Zulip Mathcomp Github Bot (Jun 26 2020 at 09:26):

chdoc opened PR #541 lemmas for proper and setC from properC to master:

Motivation for this change

This adds a few trivial lemmas on proper and setC

closes #512

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Jun 26 2020 at 10:56):

chdoc opened PR #542 fix "Nothing to inject" warnings from nothing-to-inject to master:

Motivation for this change

This fixes two "Noting to inject" warnings introduced by #509 :disappointed:

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Jun 27 2020 at 04:28):

pi8027 updated PR #464 [WIP] meet semilattice structures from semilattices to master:

Motivation for this change

This PR adds the following structures:

cc: @strub

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Jun 27 2020 at 04:28):

pi8027 updated PR #494 Get rid of displays in class fields and mixin parameters (assigned to CohenCyril) from rm-displays-in-classes to master:

Motivation for this change

This PR removes displays from class fields and mixin parameters, and also refactor factories and builders, as preliminary work for PR #464.

<!-- please explain your reason for doing this change -->

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Jun 27 2020 at 04:28):

pi8027 updated PR #536 Fix some hierarchy.ml related issues (assigned to CohenCyril) from hierarchy to master:

Motivation for this change
Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Jun 30 2020 at 06:26):

pi8027:

view this post on Zulip Mathcomp Github Bot (Jun 30 2020 at 09:06):

gares:

view this post on Zulip Mathcomp Github Bot (Jun 30 2020 at 09:06):

gares:

view this post on Zulip Mathcomp Github Bot (Jun 30 2020 at 09:35):

gares:

view this post on Zulip Mathcomp Github Bot (Jun 30 2020 at 09:56):

CohenCyril milestoned Issue #508 mem_imset mem_map naming/statement inconsistency:

while cleaning, I noticed the following oddity:

Lemma mem_imset (aT rT : finType) (f : aT -> rT) (D : {pred aT}) (x : aT) :
  x \in D -> f x \in [set f x | x in D]

Lemma map_f (T1 T2 : eqType) (f : T1 -> T2) (s : seq T1) (x : T1) :
   x \in s -> f x \in [seq f i | i <- s]
Lemma mem_map (T1 T2 : eqType) (f : T1 -> T2),
  injective f -> forall (s : seq T1) (x : T1), (f x \in [seq f i | i <- s]) = (x \in s)

Wouldn't it be more consistent to rename mem_imset to imset_f and add the following lemma:

Lemma mem_imset (aT rT : finType) (f : aT -> rT) (A : {set aT}) (x : aT) :
  injective f -> (f x \in f @: A) = (x \in A).

view this post on Zulip Mathcomp Github Bot (Jun 30 2020 at 10:15):

gares:

view this post on Zulip Mathcomp Github Bot (Jun 30 2020 at 10:16):

gares:

view this post on Zulip Mathcomp Github Bot (Jun 30 2020 at 20:00):

erikmd:

view this post on Zulip Mathcomp Github Bot (Jun 30 2020 at 20:39):

erikmd:

view this post on Zulip Mathcomp Github Bot (Jun 30 2020 at 20:40):

erikmd:

view this post on Zulip Mathcomp Github Bot (Jun 30 2020 at 20:40):

erikmd:

view this post on Zulip Mathcomp Github Bot (Jun 30 2020 at 20:53):

erikmd:

view this post on Zulip Mathcomp Github Bot (Jul 01 2020 at 06:16):

pi8027:

view this post on Zulip Mathcomp Github Bot (Jul 05 2020 at 10:30):

affeldt-aist:

view this post on Zulip Mathcomp Github Bot (Jul 08 2020 at 14:23):

chdoc opened Issue #543 Definition of "rot" suboptomal?

I tried to use list (cycle) rotation today, I and I was surprised to see that rot n s only performs a rotation if n <= size s. In fact, there is even a lemma stating this. Moreover, several lemmas need (unexpected) side conditions:

rot_oversize: forall (T : Type) (n : nat) (s : seq T), size s <= n -> rot n s = s
rotD: forall (T : Type) (m n : nat) (s : seq T), m + n <= size s -> rot (m + n) s = rot m (rot n s)
rotS: forall (T : Type) (n : nat) (s : seq T), n < size s -> rot n.+1 s = rot 1 (rot n s)
rot_add_mod: forall (T : Type) (m n : nat) (s : seq T),
  n <= size s -> m <= size s -> rot m (rot n s) = rot (if m + n <= size s then m + n else m + n - size s) s

Wouldn't it be more natural to define rot as follows:

Definition rot n s :=  drop (n %% size s) s ++ take (n %% size s) s.

(the original definition is without the _ %% size s)

From this one can prove

Lemma rot_size_r n s : rot (n + size s) s = rot n s.
Lemma rot_cons n x s : rot n.+1 (x::s) = rot n (rcons s x).

This allows removing the side conditions from rotD and rotS, making rot_add_mod redundant.

view this post on Zulip Mathcomp Github Bot (Jul 08 2020 at 14:35):

CohenCyril edited PR #541 lemmas for proper and setC from properC to master:

Motivation for this change

This adds a few trivial lemmas on proper and setC

closes #512

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Jul 08 2020 at 14:36):

CohenCyril submitted PR Review for #541 lemmas for proper and setC.

view this post on Zulip Mathcomp Github Bot (Jul 08 2020 at 21:55):

pi8027 opened Issue #544 Ambiguous coercion paths in fieldext.v:

I guess we do too much eta expansion somewhere:

Warning:
New coercion path [FieldExt.base6; GRing.ComUnitAlgebra.base2] : FieldExt.class_of >-> GRing.UnitAlgebra.class_of is ambiguous with existing
[FieldExt.base; Falgebra.base1] : FieldExt.class_of >-> GRing.UnitAlgebra.class_of. [ambiguous-paths,typechecker]
Warning:
New coercion path [FieldExt.comUnitAlgType; GRing.ComUnitAlgebra.unitAlgType] : FieldExt.type >-> GRing.UnitAlgebra.type is ambiguous with existing
[FieldExt.unitAlgType] : FieldExt.type >-> GRing.UnitAlgebra.type. [ambiguous-paths,typechecker]

view this post on Zulip Mathcomp Github Bot (Jul 08 2020 at 22:09):

pi8027 opened PR #545 Make [fieldExtType F of L] work for abstract instances from fieldext to master:

Motivation for this change

If L is an abstract fieldType, this pack notation did not work as in https://github.com/math-comp/analysis/pull/205#discussion_r451832262. CC: @CohenCyril

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Jul 08 2020 at 22:20):

CohenCyril requested CohenCyril for a review on PR #545 Make [fieldExtType F of L] work for abstract instances.

view this post on Zulip Mathcomp Github Bot (Jul 08 2020 at 22:20):

CohenCyril assigned PR #545 Make [fieldExtType F of L] work for abstract instances.

view this post on Zulip Mathcomp Github Bot (Jul 09 2020 at 21:29):

pi8027 opened PR #546 Fix ambiguous coercion paths in fieldext.v from fieldext-coherence to master:

Motivation for this change

The coercion paths from fieldExtType to unitAlgType were ambiguous because the base of FalgType was unitAlgType but the base of comUnitAlgType was comAlgType. This PR fixes it by changing the base of comUnitAlgType to unitAlgType.

Fixes: #544.

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Jul 12 2020 at 20:25):

pi8027 updated PR #546 Fix ambiguous coercion paths in fieldext.v from fieldext-coherence to master:

Motivation for this change

The coercion paths from fieldExtType to unitAlgType were ambiguous because the base of FalgType was unitAlgType but the base of comUnitAlgType was comAlgType. This PR fixes it by changing the base of comUnitAlgType to unitAlgType.

Fixes: #544.

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Jul 12 2020 at 20:26):

pi8027 edited PR #546 Fix ambiguous coercion paths in fieldext.v from fieldext-coherence to master:

Motivation for this change

The coercion paths from fieldExtType to unitAlgType were ambiguous because the base of FalgType was unitAlgType but the base of comUnitAlgType was comAlgType. This PR fixes it by changing the base of comUnitAlgType to unitAlgType.

Fixes: #544.

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Jul 12 2020 at 20:29):

pi8027 edited PR #546 Fix a coherence (ambiguous paths) issue of fieldExtType and a conversion issue of "regular" instances from fieldext-coherence to master:

Motivation for this change

The coercion paths from fieldExtType to unitAlgType were ambiguous because the base of FalgType was unitAlgType but the base of comUnitAlgType was comAlgType. This PR fixes it by changing the base of comUnitAlgType to unitAlgType.

Fixes: #544.

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Jul 12 2020 at 20:38):

pi8027 edited PR #546 Fix a coherence (ambiguous paths) issue of fieldExtType and a conversion issue of "regular" instances from fieldext-coherence to master:

Motivation for this change
Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Jul 12 2020 at 20:48):

pi8027 submitted PR Review for #546 Fix a coherence (ambiguous paths) issue of fieldExtType and a conversion issue of "regular" instances.

view this post on Zulip Mathcomp Github Bot (Jul 12 2020 at 20:48):

pi8027 created PR Review Comment on #546 Fix a coherence (ambiguous paths) issue of fieldExtType and a conversion issue of "regular" instances:

Since the [comUnitRingType of R] notation does an extra record eta expansion, I had to avoid it. :(

view this post on Zulip Mathcomp Github Bot (Jul 12 2020 at 21:04):

pi8027 updated PR #458 [WIP] new interval library from interval to master:

Motivation for this change

This PR generalizes the results in interval.v using order structures. The main achievements are that intervals on a latticeType form a latticeType where join is the intersection and meet is the convex hull, and intervals on an orderType form a distrLatticeType as well.

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Jul 12 2020 at 23:27):

pi8027 edited PR #546 Fix a coherence (ambiguous paths) issue of fieldExtType and a conversion issue of "regular" instances from fieldext-coherence to master:

Motivation for this change
Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Jul 14 2020 at 04:38):

pi8027 opened PR #547 Qualify the dual_* notations with the Order module from qualified-dual-op to master:

Motivation for this change
Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Jul 14 2020 at 05:20):

pi8027 edited PR #547 Qualify the dual_* notations with the Order module from qualified-dual-op to master:

Motivation for this change
Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Jul 14 2020 at 05:43):

pi8027 edited PR #546 Fix a coherence (ambiguous paths) issue of fieldExtType and a conversion issue of "regular" instances from fieldext-coherence to master:

Motivation for this change
Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Jul 14 2020 at 05:57):

pi8027 updated PR #547 Qualify the dual_* notations with the Order module from qualified-dual-op to master:

Motivation for this change
Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Jul 14 2020 at 21:36):

pi8027 edited PR #546 Fix a coherence (ambiguous paths) issue of fieldExtType and a conversion issue of "regular" instances from fieldext-coherence to master:

Motivation for this change
Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Jul 16 2020 at 05:07):

pi8027 opened PR #548 Use predicators even extensively from predicators to master:

Motivation for this change

This PR attempts to restate several lemmas using predicators such as cancel, (left|right)_(id|zero|inverse|distributive), idempotent, associative, and commutative. Some of them are probably too aggressive and I would like to have comments on this point.

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Jul 16 2020 at 05:21):

pi8027 updated PR #548 Use predicators even extensively from predicators to master:

Motivation for this change

This PR attempts to restate several lemmas using predicators such as cancel, (left|right)_(id|zero|inverse|distributive), idempotent, associative, and commutative. Some of them are probably too aggressive and I would like to have comments on this point.

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Jul 24 2020 at 13:10):

CohenCyril:

view this post on Zulip Mathcomp Github Bot (Jul 24 2020 at 13:18):

pi8027 edited PR #546 [DO NOT MERGE] Fix a coherence (ambiguous paths) issue of fieldExtType and a conversion issue of "regular" instances from fieldext-coherence to master:

Motivation for this change
Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Jul 29 2020 at 10:08):

pochinha opened Issue #549 The (if _ then _ else) pattern is not recognized when using ifN on a simple goal:

I'm not sure what the underlying problem is.

Example:

From mathcomp Require Import all_ssreflect.

Goal (if 1 < 0 then true else false) = false.
Proof.
  Fail rewrite ifN. (* The LHS of ifN (if _ then _ else _) does not match any subterm of the goal *)
  Fail apply: ifN. (* Cannot apply lemma ifN *)
  apply ifN (* works *)
Abort.

Using rewrite (@ifN _ (1 < 0)). also works.

Happens both with Coq 8.9.1 + mathcomp 1.9.0 and with Coq 8.11.2 + mathcomp 1.11.0, which are the versions I have installed.

view this post on Zulip Mathcomp Github Bot (Jul 29 2020 at 10:11):

pochinha edited Issue #549 The (if _ then _ else) pattern is not recognized when using ifN on a simple goal:

I'm not sure what the underlying problem is.

Example:

From mathcomp Require Import all_ssreflect.

Goal (if 1 < 0 then true else false) = false.
Proof.
  Fail rewrite ifN. (* The LHS of ifN (if _ then _ else _) does not match any subterm of the goal *)
  Fail apply: ifN. (* Cannot apply lemma ifN *)
  apply ifN. (* works *)
Abort.

Using rewrite (@ifN _ (1 < 0)). also works.

Happens both with Coq 8.9.1 + mathcomp 1.9.0 and with Coq 8.11.2 + mathcomp 1.11.0, which are the versions I have installed.

view this post on Zulip Mathcomp Github Bot (Jul 29 2020 at 11:08):

pochinha edited Issue #549 The (if _ then _ else) pattern is not recognized when using ifN on a simple goal:

I'm not sure what the underlying problem is.

Example:

From mathcomp Require Import all_ssreflect.

Goal (if 1 < 0 then true else false) = false.
Proof.
  Fail rewrite ifN. (* The LHS of ifN (if _ then _ else _) does not match any subterm of the goal *)
  Fail apply: ifN. (* Cannot apply lemma ifN *)
  apply ifN. (* works *)
Abort.

Using rewrite (@ifN _ (1 < 0)). also works.

EDIT: using rewrite (@ifN _ (1 < 0)). leaves a dangling bool. Furthermore, rewrite-> ifN works properly.

Happens both with Coq 8.9.1 + mathcomp 1.9.0 and with Coq 8.11.2 + mathcomp 1.11.0, which are the versions I have installed.

view this post on Zulip Mathcomp Github Bot (Jul 29 2020 at 17:40):

jashug opened PR #550 Be robust to a change in the default argument naming algorithm. from dont-refresh-argument-names-overlay to master:

Motivation for this change

Overlay for coq/coq#12756, in which the default argument name changes to just S from S0. This change preserves the old name; switching instead to use S may be preferable but introduces a potential impact on downstream users of mathcomp.
Should be entirely backwards compatible.

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Aug 11 2020 at 00:25):

CohenCyril merged PR #536 Fix some hierarchy.ml related issues.

view this post on Zulip Mathcomp Github Bot (Aug 11 2020 at 00:25):

CohenCyril pushed 3 commits to branch master. Commits by pi8027 (2) and CohenCyril (1).

view this post on Zulip Mathcomp Github Bot (Aug 11 2020 at 00:25):

CohenCyril milestoned Issue #536 Fix some hierarchy.ml related issues (assigned to CohenCyril):

Motivation for this change
Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Aug 11 2020 at 00:26):

CohenCyril milestoned Issue #517 Extra theorems about subn minn and maxn:

Motivation for this change

<!-- please explain your reason for doing this change -->

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

The theorems are missing but I am not very happy about their proofs

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Aug 11 2020 at 00:26):

CohenCyril edited PR #517 Extra theorems about subn minn and maxn from minn to master:

Motivation for this change

<!-- please explain your reason for doing this change -->

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

The theorems are missing but I am not very happy about their proofs

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Aug 11 2020 at 00:27):

CohenCyril submitted PR Review for #517 Extra theorems about subn minn and maxn.

view this post on Zulip Mathcomp Github Bot (Aug 11 2020 at 00:27):

CohenCyril created PR Review Comment on #517 Extra theorems about subn minn and maxn:

       `subn_minr` `subn_maxr` in `ssrnat.v`

view this post on Zulip Mathcomp Github Bot (Aug 11 2020 at 00:27):

CohenCyril updated PR #517 Extra theorems about subn minn and maxn from minn to master:

Motivation for this change

<!-- please explain your reason for doing this change -->

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

The theorems are missing but I am not very happy about their proofs

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Aug 11 2020 at 00:27):

CohenCyril submitted PR Review for #517 Extra theorems about subn minn and maxn.

view this post on Zulip Mathcomp Github Bot (Aug 11 2020 at 00:29):

CohenCyril assigned PR #517 Extra theorems about subn minn and maxn to CohenCyril.

view this post on Zulip Mathcomp Github Bot (Aug 11 2020 at 00:41):

CohenCyril submitted PR Review for #521 In and on.

view this post on Zulip Mathcomp Github Bot (Aug 11 2020 at 00:41):

CohenCyril created PR Review Comment on #521 In and on:


view this post on Zulip Mathcomp Github Bot (Aug 11 2020 at 00:41):

CohenCyril submitted PR Review for #521 In and on.

view this post on Zulip Mathcomp Github Bot (Aug 11 2020 at 00:41):

CohenCyril created PR Review Comment on #521 In and on:


view this post on Zulip Mathcomp Github Bot (Aug 11 2020 at 00:41):

CohenCyril updated PR #521 In and on from in_on to master:

Motivation for this change

These new lemmas describe more precisely the possible interactions between in and on.

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Aug 11 2020 at 00:46):

CohenCyril updated PR #521 In and on from in_on to master:

Motivation for this change

These new lemmas describe more precisely the possible interactions between in and on.

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Aug 11 2020 at 00:48):

CohenCyril has marked PR #521 as ready for review.

view this post on Zulip Mathcomp Github Bot (Aug 11 2020 at 00:49):

CohenCyril closed Issue #512 lemma for proper and setC?

I noticed that there are quite a few lemmas combining _ \subset _ and ~: _ but none for
_ \proper _ and ~: _.

How about adding (possibly with a different name):

Lemma properC (T : finType) (A B : {set T}) : A \proper B = (~: B \proper ~: A).
Proof.
rewrite !properEneq setCS [~: _ == _]inj_eq 1?eq_sym //; exact/inv_inj/setCK.
Qed.

I think this is sufficient, since any introduced double complement can easily be eliminated with ?setCK.

view this post on Zulip Mathcomp Github Bot (Aug 11 2020 at 00:49):

CohenCyril merged PR #541 lemmas for proper and setC.

view this post on Zulip Mathcomp Github Bot (Aug 11 2020 at 00:49):

CohenCyril pushed 2 commits to branch master. Commits by CohenCyril (1) and chdoc (1).

view this post on Zulip Mathcomp Github Bot (Aug 11 2020 at 00:49):

CohenCyril milestoned Issue #541 lemmas for proper and setC:

Motivation for this change

This adds a few trivial lemmas on proper and setC

closes #512

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Aug 11 2020 at 01:56):

CohenCyril opened PR #551 Use union driver for CHANGELOG_UNRELEASED from merge-changelog-by-union to master:

Motivation for this change

<!-- please explain your reason for doing this change -->

End CHANGELOG_UNRELEASED merge conflicts locally!
(Github does not support this yet though)

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Aug 11 2020 at 01:56):

CohenCyril merged PR #551 Use union driver for CHANGELOG_UNRELEASED.

view this post on Zulip Mathcomp Github Bot (Aug 11 2020 at 01:56):

CohenCyril pushed 2 commits to branch master.

view this post on Zulip Mathcomp Github Bot (Aug 11 2020 at 01:57):

CohenCyril merged PR #542 fix "Nothing to inject" warnings.

view this post on Zulip Mathcomp Github Bot (Aug 11 2020 at 01:57):

CohenCyril pushed 2 commits to branch master. Commits by CohenCyril (1) and chdoc (1).

view this post on Zulip Mathcomp Github Bot (Aug 11 2020 at 01:57):

CohenCyril milestoned Issue #542 fix "Nothing to inject" warnings:

Motivation for this change

This fixes two "Noting to inject" warnings introduced by #509 :disappointed:

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Aug 11 2020 at 09:00):

thery updated PR #517 Extra theorems about subn minn and maxn (assigned to CohenCyril) from minn to master:

Motivation for this change

<!-- please explain your reason for doing this change -->

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

The theorems are missing but I am not very happy about their proofs

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Aug 11 2020 at 09:31):

CohenCyril merged PR #507 Add more test cases for higher-order recursive functions in seq.v w.r.t. the guard condition.

view this post on Zulip Mathcomp Github Bot (Aug 11 2020 at 09:31):

CohenCyril pushed 2 commits to branch master. Commits by CohenCyril (1) and pi8027 (1).

view this post on Zulip Mathcomp Github Bot (Aug 11 2020 at 12:37):

chdoc opened PR #552 fix notation-incompatible-format warnings from rel-format-warning to master:

Motivation for this change

notation-incompatible-format warnings are everywhere in 8.12 (Zulip conversation)

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Aug 11 2020 at 14:12):

chdoc opened PR #553 fix non-reversible-notation warnings from non-reversible-notation to master:

Motivation for this change

fix non-reversible-notation warnings in ssrAC.v caused by Ltac in notations.

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Aug 11 2020 at 14:53):

CohenCyril submitted PR Review for #552 fix notation-incompatible-format warnings.

view this post on Zulip Mathcomp Github Bot (Aug 11 2020 at 14:53):

CohenCyril merged PR #552 fix notation-incompatible-format warnings.

view this post on Zulip Mathcomp Github Bot (Aug 11 2020 at 14:53):

CohenCyril pushed 2 commits to branch master. Commits by CohenCyril (1) and chdoc (1).

view this post on Zulip Mathcomp Github Bot (Aug 12 2020 at 17:19):

pi8027 updated PR #458 [WIP] new interval library from interval to master:

Motivation for this change

This PR generalizes the results in interval.v using order structures. The main achievements are that intervals on a latticeType form a latticeType where join is the intersection and meet is the convex hull, and intervals on an orderType form a distrLatticeType as well.

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Aug 12 2020 at 17:19):

pi8027 updated PR #545 Make [fieldExtType F of L] work for abstract instances (assigned to CohenCyril) from fieldext to master:

Motivation for this change

If L is an abstract fieldType, this pack notation did not work as in https://github.com/math-comp/analysis/pull/205#discussion_r451832262. CC: @CohenCyril

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Aug 12 2020 at 17:19):

pi8027 updated PR #547 Qualify the dual_* notations with the Order module from qualified-dual-op to master:

Motivation for this change
Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Aug 12 2020 at 17:19):

pi8027 updated PR #548 Use predicators even extensively from predicators to master:

Motivation for this change

This PR attempts to restate several lemmas using predicators such as cancel, (left|right)_(id|zero|inverse|distributive), idempotent, associative, and commutative. Some of them are probably too aggressive and I would like to have comments on this point.

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Aug 12 2020 at 17:19):

pi8027 updated PR #494 Get rid of displays in class fields and mixin parameters (assigned to CohenCyril) from rm-displays-in-classes to master:

Motivation for this change

This PR removes displays from class fields and mixin parameters, and also refactor factories and builders, as preliminary work for PR #464.

<!-- please explain your reason for doing this change -->

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Aug 12 2020 at 17:19):

pi8027 updated PR #464 [WIP] meet semilattice structures from semilattices to master:

Motivation for this change

This PR adds the following structures:

cc: @strub

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Aug 12 2020 at 17:19):

pi8027 updated PR #546 [DO NOT MERGE] Fix a coherence (ambiguous paths) issue of fieldExtType and a conversion issue of "regular" instances from fieldext-coherence to master:

Motivation for this change
Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Aug 13 2020 at 08:57):

chdoc updated PR #553 fix non-reversible-notation warnings from non-reversible-notation to master:

Motivation for this change

fix non-reversible-notation warnings in ssrAC.v caused by Ltac in notations.

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Aug 13 2020 at 15:09):

CohenCyril submitted PR Review for #494 Get rid of displays in class fields and mixin parameters.

view this post on Zulip Mathcomp Github Bot (Aug 13 2020 at 15:13):

CohenCyril:

view this post on Zulip Mathcomp Github Bot (Aug 13 2020 at 15:16):

CohenCyril merged PR #494 Get rid of displays in class fields and mixin parameters.

view this post on Zulip Mathcomp Github Bot (Aug 13 2020 at 15:16):

CohenCyril pushed 2 commits to branch master. Commits by CohenCyril (1) and pi8027 (1).

view this post on Zulip Mathcomp Github Bot (Aug 13 2020 at 15:18):

pi8027 edited PR #547 Qualify the dual_* notations with the Order module from qualified-dual-op to master:

Motivation for this change
Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Aug 13 2020 at 15:19):

CohenCyril merged PR #553 fix non-reversible-notation warnings.

view this post on Zulip Mathcomp Github Bot (Aug 13 2020 at 15:19):

CohenCyril pushed 2 commits to branch master. Commits by CohenCyril (1) and chdoc (1).

view this post on Zulip Mathcomp Github Bot (Aug 13 2020 at 15:19):

CohenCyril milestoned Issue #553 fix non-reversible-notation warnings:

Motivation for this change

fix non-reversible-notation warnings in ssrAC.v caused by Ltac in notations.

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Aug 13 2020 at 15:20):

CohenCyril milestoned Issue #552 fix notation-incompatible-format warnings:

Motivation for this change

notation-incompatible-format warnings are everywhere in 8.12 (Zulip conversation)

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Aug 13 2020 at 15:20):

CohenCyril milestoned Issue #551 Use union driver for CHANGELOG_UNRELEASED:

Motivation for this change

<!-- please explain your reason for doing this change -->

End CHANGELOG_UNRELEASED merge conflicts locally!
(Github does not support this yet though)

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Aug 13 2020 at 15:21):

CohenCyril demilestoned Issue #551 Use union driver for CHANGELOG_UNRELEASED:

Motivation for this change

<!-- please explain your reason for doing this change -->

End CHANGELOG_UNRELEASED merge conflicts locally!
(Github does not support this yet though)

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Aug 13 2020 at 15:22):

CohenCyril milestoned Issue #545 Make [fieldExtType F of L] work for abstract instances (assigned to CohenCyril):

Motivation for this change

If L is an abstract fieldType, this pack notation did not work as in https://github.com/math-comp/analysis/pull/205#discussion_r451832262. CC: @CohenCyril

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Aug 13 2020 at 15:22):

CohenCyril merged PR #545 Make [fieldExtType F of L] work for abstract instances.

view this post on Zulip Mathcomp Github Bot (Aug 13 2020 at 15:22):

CohenCyril pushed 2 commits to branch master. Commits by CohenCyril (1) and pi8027 (1).

view this post on Zulip Mathcomp Github Bot (Aug 13 2020 at 15:25):

jashug updated PR #550 Be robust to a change in the default argument naming algorithm. from dont-refresh-argument-names-overlay to master:

Motivation for this change

Overlay for coq/coq#12756, in which the default argument name changes to just S from S0. This change preserves the old name; switching instead to use S may be preferable but introduces a potential impact on downstream users of mathcomp.
Should be entirely backwards compatible.

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Aug 13 2020 at 15:31):

pi8027 updated PR #547 Qualify the dual_* notations with the Order module from qualified-dual-op to master:

Motivation for this change
Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Aug 13 2020 at 15:31):

pi8027 edited PR #547 Qualify the dual_* notations with the Order module from qualified-dual-op to master:

Motivation for this change
Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Aug 13 2020 at 16:17):

pi8027 updated PR #458 [WIP] new interval library from interval to master:

Motivation for this change

This PR generalizes the results in interval.v using order structures. The main achievements are that intervals on a latticeType form a latticeType where join is the intersection and meet is the convex hull, and intervals on an orderType form a distrLatticeType as well.

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Aug 13 2020 at 16:17):

pi8027 updated PR #464 [WIP] meet semilattice structures from semilattices to master:

Motivation for this change

This PR adds the following structures:

cc: @strub

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Aug 13 2020 at 16:17):

pi8027 updated PR #548 Use predicators even extensively from predicators to master:

Motivation for this change

This PR attempts to restate several lemmas using predicators such as cancel, (left|right)_(id|zero|inverse|distributive), idempotent, associative, and commutative. Some of them are probably too aggressive and I would like to have comments on this point.

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Aug 13 2020 at 16:58):

pi8027 submitted PR Review for #517 Extra theorems about subn minn and maxn.

view this post on Zulip Mathcomp Github Bot (Aug 13 2020 at 16:58):

pi8027 submitted PR Review for #517 Extra theorems about subn minn and maxn.

view this post on Zulip Mathcomp Github Bot (Aug 13 2020 at 16:58):

pi8027 created PR Review Comment on #517 Extra theorems about subn minn and maxn:

If suffixes l and r stand for left and right distributivity, this should be named subn_maxl.

view this post on Zulip Mathcomp Github Bot (Aug 13 2020 at 16:58):

pi8027 created PR Review Comment on #517 Extra theorems about subn minn and maxn:

subn_minl ?

view this post on Zulip Mathcomp Github Bot (Aug 13 2020 at 16:58):

pi8027 created PR Review Comment on #517 Extra theorems about subn minn and maxn:

leqP has been relocated in #429 after maxn/minn lemmas, so this does not work. I guess we should use leq_total instead here.

view this post on Zulip Mathcomp Github Bot (Aug 13 2020 at 17:07):

pi8027 updated PR #546 [DO NOT MERGE] Fix a coherence (ambiguous paths) issue of fieldExtType and a conversion issue of "regular" instances from fieldext-coherence to master:

Motivation for this change
Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Aug 13 2020 at 20:16):

thery updated PR #517 Extra theorems about subn minn and maxn (assigned to CohenCyril) from minn to master:

Motivation for this change

<!-- please explain your reason for doing this change -->

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

The theorems are missing but I am not very happy about their proofs

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Aug 13 2020 at 20:19):

thery updated PR #517 Extra theorems about subn minn and maxn (assigned to CohenCyril) from minn to master:

Motivation for this change

<!-- please explain your reason for doing this change -->

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

The theorems are missing but I am not very happy about their proofs

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Aug 13 2020 at 20:21):

thery updated PR #517 Extra theorems about subn minn and maxn (assigned to CohenCyril) from minn to master:

Motivation for this change

<!-- please explain your reason for doing this change -->

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

The theorems are missing but I am not very happy about their proofs

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Aug 13 2020 at 21:03):

pi8027 submitted PR Review for #517 Extra theorems about subn minn and maxn.

view this post on Zulip Mathcomp Github Bot (Aug 13 2020 at 21:03):

pi8027 submitted PR Review for #517 Extra theorems about subn minn and maxn.

view this post on Zulip Mathcomp Github Bot (Aug 13 2020 at 21:03):

pi8027 created PR Review Comment on #517 Extra theorems about subn minn and maxn:

move=> m n p; apply/eqP.
rewrite eqn_leq !geq_max !leq_sub2r leq_max ?leqnn ?andbT ?orbT // /maxn.
by case: (_ < _); rewrite leqnn // orbT.

view this post on Zulip Mathcomp Github Bot (Aug 13 2020 at 21:03):

pi8027 created PR Review Comment on #517 Extra theorems about subn minn and maxn:

move=> m n p; apply/eqP.
rewrite eqn_leq !leq_min !leq_sub2r geq_min ?leqnn ?orbT //= /minn.
by case: (_ < _); rewrite leqnn // orbT.

view this post on Zulip Mathcomp Github Bot (Aug 13 2020 at 21:51):

CohenCyril requested CohenCyril for a review on PR #517 Extra theorems about subn minn and maxn.

view this post on Zulip Mathcomp Github Bot (Aug 13 2020 at 22:50):

thery updated PR #517 Extra theorems about subn minn and maxn (assigned to CohenCyril) from minn to master:

Motivation for this change

<!-- please explain your reason for doing this change -->

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

The theorems are missing but I am not very happy about their proofs

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Aug 13 2020 at 22:51):

thery updated PR #517 Extra theorems about subn minn and maxn (assigned to CohenCyril) from minn to master:

Motivation for this change

<!-- please explain your reason for doing this change -->

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

The theorems are missing but I am not very happy about their proofs

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Aug 14 2020 at 09:38):

CohenCyril requested pi8027 and CohenCyril for a review on PR #517 Extra theorems about subn minn and maxn.

view this post on Zulip Mathcomp Github Bot (Aug 14 2020 at 09:38):

CohenCyril submitted PR Review for #517 Extra theorems about subn minn and maxn.

view this post on Zulip Mathcomp Github Bot (Aug 14 2020 at 10:25):

CohenCyril labeled Issue #467 Incompatibility with Ltac2:

Hi,

the following sample doesn't work :

`
From Ltac2 Require Import Ltac2.
From Ltac2 Require Option.

Ltac2 hello_world () := Message.print (Message.of_string "Hello, world!").

From mathcomp Require Import ssreflect ssrnat eqtype ssrbool ssrnum ssralg.

Variable R: fieldType.

Variable saturation:R.

Open Scope ring_scope.

Import GRing.Theory.

Definition NakaRushon x coeff :=
x / (1%:R + x * (1 - coeff) / saturation).

Lemma tmp:
forall x y:R, ~~(y == 0) -> x = x * y / y.
Proof.
move => x y H.
`

It fails with the error message : Syntax error: [tactic:q_ident] expected after 'move' (in [tactic:tac2expr]).

Coq is at version 8.11, mathcomp at 1.10.

view this post on Zulip Mathcomp Github Bot (Aug 15 2020 at 06:47):

pi8027 submitted PR Review for #517 Extra theorems about subn minn and maxn.

view this post on Zulip Mathcomp Github Bot (Aug 15 2020 at 06:47):

pi8027 created PR Review Comment on #517 Extra theorems about subn minn and maxn:

- Added theorems about subtraction and min and max :
       `subn_minl` and `subn_maxl` in `ssrnat.v`

view this post on Zulip Mathcomp Github Bot (Aug 15 2020 at 09:40):

thery updated PR #517 Extra theorems about subn minn and maxn (assigned to CohenCyril) from minn to master:

Motivation for this change

<!-- please explain your reason for doing this change -->

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

The theorems are missing but I am not very happy about their proofs

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Aug 15 2020 at 09:41):

thery updated PR #517 Extra theorems about subn minn and maxn (assigned to CohenCyril) from minn to master:

Motivation for this change

<!-- please explain your reason for doing this change -->

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

The theorems are missing but I am not very happy about their proofs

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Aug 15 2020 at 09:43):

thery submitted PR Review for #517 Extra theorems about subn minn and maxn.

view this post on Zulip Mathcomp Github Bot (Aug 15 2020 at 09:43):

thery created PR Review Comment on #517 Extra theorems about subn minn and maxn:

:see_no_evil: Thanks!

view this post on Zulip Mathcomp Github Bot (Aug 15 2020 at 09:50):

pi8027 submitted PR Review for #517 Extra theorems about subn minn and maxn.

view this post on Zulip Mathcomp Github Bot (Aug 16 2020 at 18:59):

CohenCyril merged PR #517 Extra theorems about subn minn and maxn.

view this post on Zulip Mathcomp Github Bot (Aug 16 2020 at 18:59):

CohenCyril pushed 2 commits to branch master. Commits by CohenCyril (1) and thery (1).

view this post on Zulip Mathcomp Github Bot (Aug 17 2020 at 04:03):

pi8027 updated PR #547 Qualify the dual_* notations with the Order module from qualified-dual-op to master:

Motivation for this change
Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Aug 17 2020 at 11:46):

CohenCyril closed Issue #467 Incompatibility with Ltac2:

Hi,

the following sample doesn't work :

`
From Ltac2 Require Import Ltac2.
From Ltac2 Require Option.

Ltac2 hello_world () := Message.print (Message.of_string "Hello, world!").

From mathcomp Require Import ssreflect ssrnat eqtype ssrbool ssrnum ssralg.

Variable R: fieldType.

Variable saturation:R.

Open Scope ring_scope.

Import GRing.Theory.

Definition NakaRushon x coeff :=
x / (1%:R + x * (1 - coeff) / saturation).

Lemma tmp:
forall x y:R, ~~(y == 0) -> x = x * y / y.
Proof.
move => x y H.
`

It fails with the error message : Syntax error: [tactic:q_ident] expected after 'move' (in [tactic:tac2expr]).

Coq is at version 8.11, mathcomp at 1.10.

view this post on Zulip Mathcomp Github Bot (Aug 17 2020 at 14:46):

CohenCyril closed Issue #538 Notations dual_(bottom|top|join|meet|max|min) should be qualified by the Order module:

https://github.com/math-comp/math-comp/blob/f25ef67ad2f58a30f1e700da89811b193755d84e/mathcomp/ssreflect/order.v#L2541-L2546

Since Order.bottom, etc. are qualified, I thought they should, but actually they are not. @CohenCyril

view this post on Zulip Mathcomp Github Bot (Aug 17 2020 at 14:46):

CohenCyril merged PR #547 Qualify the dual_* notations with the Order module.

view this post on Zulip Mathcomp Github Bot (Aug 17 2020 at 14:46):

CohenCyril pushed 2 commits to branch master. Commits by CohenCyril (1) and pi8027 (1).

view this post on Zulip Mathcomp Github Bot (Aug 17 2020 at 14:46):

CohenCyril milestoned Issue #547 Qualify the dual_* notations with the Order module:

Motivation for this change
Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Aug 17 2020 at 15:29):

pi8027 edited PR #464 [WIP] meet semilattice structures from semilattices to master:

Motivation for this change

This PR adds the following structures:

cc: @strub

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Aug 17 2020 at 23:46):

pi8027 updated PR #458 [WIP] new interval library from interval to master:

Motivation for this change

This PR generalizes the results in interval.v using order structures. The main achievements are that intervals on a latticeType form a latticeType where join is the intersection and meet is the convex hull, and intervals on an orderType form a distrLatticeType as well.

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Aug 17 2020 at 23:46):

pi8027 edited PR #458 The new interval library from interval to master:

Motivation for this change

This PR generalizes the results in interval.v using order structures. The main achievements are that intervals on a latticeType form a latticeType where join is the intersection and meet is the convex hull, and intervals on an orderType form a distrLatticeType as well.

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Aug 17 2020 at 23:47):

pi8027 has marked PR #458 as ready for review.

view this post on Zulip Mathcomp Github Bot (Aug 18 2020 at 00:58):

pi8027 updated PR #458 The new interval library from interval to master:

Motivation for this change

This PR generalizes the results in interval.v using order structures. The main achievements are that intervals on a latticeType form a latticeType where join is the intersection and meet is the convex hull, and intervals on an orderType form a distrLatticeType as well.

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Aug 18 2020 at 00:59):

pi8027 edited PR #458 The new interval library from interval to master:

Motivation for this change

This PR generalizes the results in interval.v using order structures.

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Aug 18 2020 at 01:09):

pi8027 edited PR #458 The new interval library from interval to master:

Motivation for this change

This PR generalizes the results in interval.v using order structures.

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Aug 18 2020 at 01:10):

pi8027 edited PR #458 The new interval library from interval to master:

Motivation for this change

This PR generalizes the results in interval.v using order structures.

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Aug 19 2020 at 13:18):

chdoc opened Issue #554 More lemmas on subseq, next, arc, findes, etc.

I just proved a number of additional results on subseq, next, arc, and findex. It's a bit long to post here in it's entirety, but maybe some of these could (should) find their way into the corresponding files in mathcomp.

Here is the file: arc.v.

For now the proofs do not conform to the mathcomp guidelines. Comments on what to PR or how to simplify are very much appreciated.

view this post on Zulip Mathcomp Github Bot (Aug 20 2020 at 09:01):

chdoc opened PR #555 some lemmas for disjoint from disjoint-lemmas to master:

Motivation for this change

Some more lemmas to facilitate reasoning about [disjoint _ & _].

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Aug 20 2020 at 15:35):

gares merged PR #550 Be robust to a change in the default argument naming algorithm.

view this post on Zulip Mathcomp Github Bot (Aug 20 2020 at 15:35):

gares pushed 2 commits to branch master. Commits by gares (1) and jashug (1).

view this post on Zulip Mathcomp Github Bot (Aug 20 2020 at 15:36):

gares milestoned Issue #550 Be robust to a change in the default argument naming algorithm.

Motivation for this change

Overlay for coq/coq#12756, in which the default argument name changes to just S from S0. This change preserves the old name; switching instead to use S may be preferable but introduces a potential impact on downstream users of mathcomp.
Should be entirely backwards compatible.

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Aug 24 2020 at 22:47):

CohenCyril pushed 19 commits to branch experiment/forms.

view this post on Zulip Mathcomp Github Bot (Aug 24 2020 at 22:47):

CohenCyril updated PR #207 Work In Progress: adding forms and spectral theorems from experiment/forms to master:

Content:

TODO:

TODO update after @LaurenceRideau tried on the odd-order repo (https://github.com/math-comp/odd-order/pull/2)

view this post on Zulip Mathcomp Github Bot (Aug 24 2020 at 22:47):

CohenCyril edited PR #207 Work In Progress: adding forms and spectral theorems from experiment/forms to master:

Content:

TODO:

TODO update after @LaurenceRideau tried on the odd-order repo (https://github.com/math-comp/odd-order/pull/2)

view this post on Zulip Mathcomp Github Bot (Aug 24 2020 at 22:50):

CohenCyril edited PR #207 Work In Progress: adding forms and spectral theorems from experiment/forms to master:

Content:

TODO:

TODO update after @LaurenceRideau tried on the odd-order repo (https://github.com/math-comp/odd-order/pull/2)

view this post on Zulip Mathcomp Github Bot (Aug 25 2020 at 04:29):

pi8027:

view this post on Zulip Mathcomp Github Bot (Aug 25 2020 at 09:10):

gares:

view this post on Zulip Mathcomp Github Bot (Aug 25 2020 at 09:11):

gares:

view this post on Zulip Mathcomp Github Bot (Aug 25 2020 at 09:12):

CohenCyril:

view this post on Zulip Mathcomp Github Bot (Aug 25 2020 at 09:29):

CohenCyril:

view this post on Zulip Mathcomp Github Bot (Aug 25 2020 at 09:32):

gares:

view this post on Zulip Mathcomp Github Bot (Aug 25 2020 at 09:35):

CohenCyril:

view this post on Zulip Mathcomp Github Bot (Aug 25 2020 at 09:46):

affeldt-aist:

view this post on Zulip Mathcomp Github Bot (Aug 25 2020 at 09:47):

affeldt-aist:

view this post on Zulip Mathcomp Github Bot (Aug 25 2020 at 09:47):

gares:

view this post on Zulip Mathcomp Github Bot (Aug 25 2020 at 10:07):

gares:

view this post on Zulip Mathcomp Github Bot (Aug 25 2020 at 10:07):

gares:

view this post on Zulip Mathcomp Github Bot (Aug 25 2020 at 10:13):

CohenCyril:

view this post on Zulip Mathcomp Github Bot (Aug 25 2020 at 11:03):

CohenCyril updated PR #501 Intro pattern extensions for rewrite, dup, swap and apply (assigned to gares) from intro_rw to master:

Motivation for this change

Intro pattern ltac views (rewrite, dup, swap, apply) in order not to break intro patterns for silly rewrites.

- calling rewrite from an intro pattern, use with parsimony
=> /[1! rules] does rewrite rules
=> /[! rules] does rewrite !rules

- top of the stack actions:
=> /apply does => hyp {}/hyp
=> /swap does => x y; move: y x (also swap and perserves let bindings)
=> /dup does => x; have copy := x; move: copy x (also copies and preserves let bindings)

This is a part of #372, simplified, rewritten and rebased.

Things done/to do

<!-- please fill in the following checklist -->

<!-- Cross-out the above items using ~crossed out item~ if they happen not to be relevent -->
<!-- You may also add more items to explain what you did and what remains to do -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Aug 25 2020 at 12:15):

CohenCyril labeled Issue #310 clean up using printing only notations:

Grep for:

view this post on Zulip Mathcomp Github Bot (Aug 25 2020 at 12:16):

CohenCyril labeled Issue #310 clean up using printing only notations:

Grep for:

view this post on Zulip Mathcomp Github Bot (Aug 25 2020 at 12:18):

CohenCyril labeled Issue #349 build the doc using CI:

One thing I don't know is then how to commit back the result, if wanted (the doc is committed in docs/htmldoc).

view this post on Zulip Mathcomp Github Bot (Aug 25 2020 at 12:30):

CohenCyril assigned Issue #480 Switching suffixes of more distributivity lemmas (assigned to CohenCyril):

It might be better to have short suffixes D and B rather than _add and _sub in the following lemmas.

algebra/fraction.v:158:Lemma pi_add : {morph \pi : x y / addf x y >-> add x y}.

algebra/matrix.v:1232:Lemma map_mx_sub A B : (A - B)^f = A^f - B^f.

algebra/mxalgebra.v:2380:Lemma mulsmx_addr m1 m2 m3 n
algebra/mxalgebra.v-2381-                  (R1 : 'A_(m1, n)) (R2 : 'A_(m2, n)) (R3 : 'A_(m3, n)) :
algebra/mxalgebra.v-2382-  (R1 * (R2 + R3) = R1 * R2 + R1 * R3)%MS.

algebra/poly.v:431:Lemma polyC_add : {morph polyC : a b / a + b}.

algebra/poly.v:437:Lemma polyC_sub : {morph polyC : a b / a - b}.

algebra/poly.v:1525:Lemma derivn_sub n : {morph derivn n : p q / p - q}.

algebra/polydiv.v:563:Lemma rdivp_addr q r : rdvdp d r -> rdivp (q + r) d = rdivp q d + rdivp r d.

algebra/polydiv.v:584:Lemma rmodp_add p q : rmodp (p + q) d = rmodp p d + rmodp q d.

algebra/polydiv.v:2504:Lemma modp_add p q : (p + q) %% d = p %% d + q %% d.

algebra/polydiv.v:2513:Lemma divp_add p q : (p + q) %/ d = p %/ d + q %/ d.

algebra/polydiv.v:2826:Lemma modp_add d p q : (p + q) %% d = p %% d + q %% d.

algebra/polydiv.v:2837:Lemma divp_add d p q : (p + q) %/ d = p %/ d + q %/ d.

algebra/ring_quotient.v:175:Lemma pi_addr zqT : {morph \pi_zqT : x y / addT x y >-> x + y}.

algebra/ring_quotient.v:537:Lemma pi_add : {morph \pi : x y / x + y >-> add x y}.

algebra/ssrint.v:140:Lemma oppz_add : {morph oppz : m n / m + n}.

algebra/vector.v:1494:Lemma limg_add f : {morph lfun_img f : U V / U + V}%VS.

algebra/zmodp.v:125:Lemma Zp_mul_addr : right_distributive Zp_mul Zp_add.

ssreflect/bigop.v:453:Lemma mulm_addr : right_distributive mul add.

ssreflect/seq.v:2422:Lemma iota_add m n1 n2 : iota m (n1 + n2) = iota m n1 ++ iota (m + n1) n2.

ssreflect/ssrnat.v:921:Lemma iter_add n m f x : iter (n + m) f x = iter n f (iter m f x).

Since I did this mechanically with grep and did not check the meaning of them entirely, I need some input to prepare a PR.

view this post on Zulip Mathcomp Github Bot (Aug 25 2020 at 12:31):

CohenCyril labeled Issue #480 Switching suffixes of more distributivity lemmas (assigned to CohenCyril):

It might be better to have short suffixes D and B rather than _add and _sub in the following lemmas.

algebra/fraction.v:158:Lemma pi_add : {morph \pi : x y / addf x y >-> add x y}.

algebra/matrix.v:1232:Lemma map_mx_sub A B : (A - B)^f = A^f - B^f.

algebra/mxalgebra.v:2380:Lemma mulsmx_addr m1 m2 m3 n
algebra/mxalgebra.v-2381-                  (R1 : 'A_(m1, n)) (R2 : 'A_(m2, n)) (R3 : 'A_(m3, n)) :
algebra/mxalgebra.v-2382-  (R1 * (R2 + R3) = R1 * R2 + R1 * R3)%MS.

algebra/poly.v:431:Lemma polyC_add : {morph polyC : a b / a + b}.

algebra/poly.v:437:Lemma polyC_sub : {morph polyC : a b / a - b}.

algebra/poly.v:1525:Lemma derivn_sub n : {morph derivn n : p q / p - q}.

algebra/polydiv.v:563:Lemma rdivp_addr q r : rdvdp d r -> rdivp (q + r) d = rdivp q d + rdivp r d.

algebra/polydiv.v:584:Lemma rmodp_add p q : rmodp (p + q) d = rmodp p d + rmodp q d.

algebra/polydiv.v:2504:Lemma modp_add p q : (p + q) %% d = p %% d + q %% d.

algebra/polydiv.v:2513:Lemma divp_add p q : (p + q) %/ d = p %/ d + q %/ d.

algebra/polydiv.v:2826:Lemma modp_add d p q : (p + q) %% d = p %% d + q %% d.

algebra/polydiv.v:2837:Lemma divp_add d p q : (p + q) %/ d = p %/ d + q %/ d.

algebra/ring_quotient.v:175:Lemma pi_addr zqT : {morph \pi_zqT : x y / addT x y >-> x + y}.

algebra/ring_quotient.v:537:Lemma pi_add : {morph \pi : x y / x + y >-> add x y}.

algebra/ssrint.v:140:Lemma oppz_add : {morph oppz : m n / m + n}.

algebra/vector.v:1494:Lemma limg_add f : {morph lfun_img f : U V / U + V}%VS.

algebra/zmodp.v:125:Lemma Zp_mul_addr : right_distributive Zp_mul Zp_add.

ssreflect/bigop.v:453:Lemma mulm_addr : right_distributive mul add.

ssreflect/seq.v:2422:Lemma iota_add m n1 n2 : iota m (n1 + n2) = iota m n1 ++ iota (m + n1) n2.

ssreflect/ssrnat.v:921:Lemma iter_add n m f x : iter (n + m) f x = iter n f (iter m f x).

Since I did this mechanically with grep and did not check the meaning of them entirely, I need some input to prepare a PR.

view this post on Zulip Mathcomp Github Bot (Aug 25 2020 at 12:52):

CohenCyril opened PR #556 Adding lemma oddS from oddS to master:

Motivation for this change

fixes #500

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Aug 25 2020 at 16:24):

maximedenes assigned PR #433 [test suite] infrastructure to test how some statements are printed to maximedenes.

view this post on Zulip Mathcomp Github Bot (Aug 26 2020 at 05:51):

pi8027 submitted PR Review for #556 Adding lemma oddS

view this post on Zulip Mathcomp Github Bot (Aug 26 2020 at 05:51):

pi8027 created PR Review Comment on #556 Adding lemma oddS

Isn't it better to merge these two items?

view this post on Zulip Mathcomp Github Bot (Aug 26 2020 at 09:54):

thery demilestoned Issue #357 Algebraic structure of dioid (assigned to thery):

Dear mathcomp developers,

This is a formalization of the algebraic structure of dioid and associated lemmas (including the Nerode lemma).

I am using this for formalizing proofs in network calculus: a theory used in certification of some embedded networks like AFDX in airplanes. This is a work done @proux01

Do you think it can be of interest for mathcomp? A separate library?

A few questions:

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Aug 26 2020 at 10:26):

thery closed without merge PR #357 Algebraic structure of dioid.

view this post on Zulip Mathcomp Github Bot (Aug 26 2020 at 12:54):

CohenCyril submitted PR Review for #556 Adding lemma oddS

view this post on Zulip Mathcomp Github Bot (Aug 26 2020 at 12:54):

CohenCyril created PR Review Comment on #556 Adding lemma oddS

I prefer this is done in the release phase, to minimize possible faulty merge union

view this post on Zulip Mathcomp Github Bot (Aug 26 2020 at 12:55):

CohenCyril pushed 1 commit to branch master.

view this post on Zulip Mathcomp Github Bot (Aug 26 2020 at 12:56):

CohenCyril:

view this post on Zulip Mathcomp Github Bot (Aug 26 2020 at 13:28):

gares submitted PR Review for #316 [build] Preliminary support for building with Dune.

view this post on Zulip Mathcomp Github Bot (Aug 26 2020 at 13:28):

gares created PR Review Comment on #316 [build] Preliminary support for building with Dune.

Do we really need an unreleased version of Dune?

view this post on Zulip Mathcomp Github Bot (Aug 26 2020 at 14:03):

ejgallego submitted PR Review for #316 [build] Preliminary support for building with Dune.

view this post on Zulip Mathcomp Github Bot (Aug 26 2020 at 14:03):

ejgallego created PR Review Comment on #316 [build] Preliminary support for building with Dune.

It should work fine with recent versions, but the PR needs updating.

view this post on Zulip Mathcomp Github Bot (Aug 26 2020 at 14:15):

ejgallego updated PR #316 [build] Preliminary support for building with Dune. (assigned to gares) from dune to master:

This PR provides preliminary support for building math-comp with Dune
[support in Dune's master currently]

As of today we do consider math-comp as a monolithic library due to
Dune's Coq support being unable to compose libraries yet, this will be
fixed in the future.

view this post on Zulip Mathcomp Github Bot (Aug 26 2020 at 14:21):

ejgallego submitted PR Review for #316 [build] Preliminary support for building with Dune.

view this post on Zulip Mathcomp Github Bot (Aug 26 2020 at 14:21):

ejgallego created PR Review Comment on #316 [build] Preliminary support for building with Dune.

Updated.

view this post on Zulip Mathcomp Github Bot (Aug 26 2020 at 15:31):

pi8027 submitted PR Review for #556 Adding lemma oddS

view this post on Zulip Mathcomp Github Bot (Aug 28 2020 at 08:47):

pi8027 updated PR #458 The new interval library from interval to master:

Motivation for this change

This PR generalizes the results in interval.v using order structures.

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Aug 28 2020 at 08:47):

pi8027 edited PR #458 The new interval library from interval to master:

Motivation for this change

This PR generalizes the results in interval.v using order structures.

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Aug 28 2020 at 08:47):

pi8027 edited PR #458 The new interval library from interval to master:

Motivation for this change

This PR generalizes the results in interval.v using order structures.

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Aug 28 2020 at 09:00):

pi8027 updated PR #458 The new interval library from interval to master:

Motivation for this change

This PR generalizes the results in interval.v using order structures.

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Aug 28 2020 at 14:02):

CohenCyril assigned PR #458 The new interval library to CohenCyril.

view this post on Zulip Mathcomp Github Bot (Aug 28 2020 at 14:02):

CohenCyril requested CohenCyril for a review on PR #458 The new interval library.

view this post on Zulip Mathcomp Github Bot (Aug 28 2020 at 14:16):

CohenCyril milestoned Issue #556 Adding lemma oddS

Motivation for this change

fixes #500

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Aug 28 2020 at 14:17):

CohenCyril closed Issue #500 [ssrnat] Suggestion of additional lemma: oddS:

Hi,

I was reading the book, and for one of the exercices (16 in 5.1.1), I missed a simple lemma on the odd predicate ; I propose to add it:

Lemma oddS n: odd n.+1 = ~~ odd n.
Proof.
  elim: n => [|n Hn] ; first by easy.
  by rewrite Hn.
Qed.

which gave me:

Lemma sum_odd n : \sum_ (0 <= i < n.*2 | odd i) i = n^2.
Proof.
 elim: n => [|n Hn] ; first by rewrite unlock.
 rewrite doubleS.
 rewrite big_mkcond.
 rewrite big_nat_recr //.
 rewrite big_nat_recr //.
 rewrite odd_double oddS odd_double //=.
 rewrite -big_mkcond {}Hn.
 rewrite addn0 -!mulnn -addnn mulnS mulnC mulnS.
 ring.
Qed.

I must admit I'm not satisfied by either proof, but as a beginner, getting a correct proof is already an achievement. [I find the last part about the (m.+1)^2=... especially awful].

view this post on Zulip Mathcomp Github Bot (Aug 28 2020 at 14:17):

CohenCyril merged PR #556 Adding lemma oddS

view this post on Zulip Mathcomp Github Bot (Aug 28 2020 at 14:17):

CohenCyril pushed 2 commits to branch master.

view this post on Zulip Mathcomp Github Bot (Aug 28 2020 at 15:12):

pi8027 updated PR #458 The new interval library (assigned to CohenCyril) from interval to master:

Motivation for this change

This PR generalizes the results in interval.v using order structures.

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Aug 28 2020 at 17:41):

pi8027 edited PR #458 The new interval library (assigned to CohenCyril) from interval to master:

Motivation for this change

This PR generalizes the results in interval.v using order structures.

Things done/to do

<!-- please fill in the following checklist -->

PR overlays

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Aug 28 2020 at 22:35):

erikmd opened PR #557 chore: refactor GitLab CI config a bit to lighten nightly builds from lighten-nightly-build to master:

Motivation for this change
Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Aug 29 2020 at 10:28):

pi8027 submitted PR Review for #458 The new interval library.

view this post on Zulip Mathcomp Github Bot (Aug 29 2020 at 10:28):

pi8027 created PR Review Comment on #458 The new interval library:

I think this result can be generalized by introducing the notion of the dimension of a lattice. I would say a lattice L is n-dimensional if "∀x_0 ... x_n ∈ L. ∃i ∈ {0, ..., n}. ⋀_(0 ≦ j ≦ n) x_j = ⋀_(0 ≦ j ≦ n ∧ j ≠ i) x_j" holds. As a result, a totally ordered set is a 1-dimensional lattice, and the product of n- and m-dimensional lattices forms an (n + m)-dimensional lattice. The problem is that this wording is confusing with lattice points.

view this post on Zulip Mathcomp Github Bot (Aug 29 2020 at 10:30):

pi8027 edited PR Review Comment on #458 The new interval library.

view this post on Zulip Mathcomp Github Bot (Aug 29 2020 at 20:56):

pi8027 edited PR Review Comment on #458 The new interval library.

view this post on Zulip Mathcomp Github Bot (Aug 30 2020 at 19:43):

pi8027 edited PR Review Comment on #458 The new interval library.

view this post on Zulip Mathcomp Github Bot (Sep 01 2020 at 11:20):

CohenCyril opened PR #558 Adding are_allpairs predicate from are_allpairs to master:

Motivation for this change

<!-- please explain your reason for doing this change -->

This predicate is useful in stating that a sequence of matrices all commute.
This is a part of #207.

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Sep 01 2020 at 11:21):

CohenCyril updated PR #558 Adding are_allpairs predicate from are_allpairs to master:

Motivation for this change

<!-- please explain your reason for doing this change -->

This predicate is useful in stating that a sequence of matrices all commute.
This is a part of #207.

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Sep 01 2020 at 11:21):

CohenCyril requested chdoc for a review on PR #558 Adding are_allpairs predicate.

view this post on Zulip Mathcomp Github Bot (Sep 01 2020 at 11:22):

CohenCyril milestoned Issue #558 Adding are_allpairs predicate:

Motivation for this change

<!-- please explain your reason for doing this change -->

This predicate is useful in stating that a sequence of matrices all commute.
This is a part of #207.

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Sep 01 2020 at 11:51):

gares assigned PR #558 Adding are_allpairs predicate to gares.

view this post on Zulip Mathcomp Github Bot (Sep 01 2020 at 12:06):

CohenCyril opened PR #559 Adding sig_big_dep lemma from sig_big_dep to master:

Motivation for this change

Useful tooling lemma with nested dependent bigops.
Part of #207.

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Sep 01 2020 at 12:08):

CohenCyril requested gares for a review on PR #559 Adding sig_big_dep lemma.

view this post on Zulip Mathcomp Github Bot (Sep 01 2020 at 12:10):

CohenCyril opened PR #560 Adding commr_horner lemma from commr_horner to master:

Motivation for this change

Missing lemma between GRing.comm, comm_coef and horner.

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Sep 01 2020 at 12:12):

CohenCyril updated PR #560 Adding commr_horner lemma from commr_horner to master:

Motivation for this change

Missing lemma between GRing.comm, comm_coef and horner.

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Sep 01 2020 at 12:12):

CohenCyril requested ybertot for a review on PR #560 Adding commr_horner lemma.

view this post on Zulip Mathcomp Github Bot (Sep 01 2020 at 12:22):

CohenCyril opened PR #561 Adding commr_horner lemma from rowcol_dlrsubmx to master:

Motivation for this change

<!-- please explain your reason for doing this change -->

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Sep 01 2020 at 12:22):

CohenCyril closed without merge PR #561 Adding commr_horner lemma.

view this post on Zulip Mathcomp Github Bot (Sep 01 2020 at 12:23):

CohenCyril edited PR #560 Adding commr_horner lemma from commr_horner to master:

Motivation for this change

Missing lemma between GRing.comm, comm_coef and horner.
Part of #207.

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Sep 01 2020 at 12:25):

CohenCyril opened PR #562 Adding [row|col]_[udlr]submx lemmas from rowcol_dlrsubmx to master:

Motivation for this change

Combining row and col with block submatrices.
Part of #207.

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Sep 01 2020 at 12:26):

CohenCyril updated PR #562 Adding [row|col]_[udlr]submx lemmas from rowcol_dlrsubmx to master:

Motivation for this change

Combining row and col with block submatrices.
Part of #207.

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Sep 01 2020 at 12:26):

CohenCyril edited PR #562 Adding [row|col]_[udlr]submx lemmas from rowcol_dlrsubmx to master:

Motivation for this change

Combining row and col with block submatrices.
Part of #207.

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Sep 01 2020 at 12:26):

CohenCyril edited PR #562 Adding [row|col]_[udlr]submx lemmas from rowcol_dlrsubmx to master:

Motivation for this change

Combining row and col with block submatrices.
Part of #207.

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Sep 01 2020 at 12:27):

CohenCyril edited PR #559 Adding sig_big_dep lemma from sig_big_dep to master:

Motivation for this change

Useful tooling lemma with nested dependent bigops.
Part of #207.

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Sep 01 2020 at 12:27):

CohenCyril edited PR #560 Adding commr_horner lemma from commr_horner to master:

Motivation for this change

Missing lemma between GRing.comm, comm_coef and horner.
Part of #207.

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Sep 01 2020 at 12:28):

CohenCyril updated PR #559 Adding sig_big_dep lemma from sig_big_dep to master:

Motivation for this change

Useful tooling lemma with nested dependent bigops.
Part of #207.

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Sep 01 2020 at 12:33):

chdoc submitted PR Review for #558 Adding are_allpairs predicate.

view this post on Zulip Mathcomp Github Bot (Sep 01 2020 at 12:33):

chdoc submitted PR Review for #558 Adding are_allpairs predicate.

view this post on Zulip Mathcomp Github Bot (Sep 01 2020 at 12:33):

chdoc created PR Review Comment on #558 Adding are_allpairs predicate:

I agree with @gares in not being happy with this name.

view this post on Zulip Mathcomp Github Bot (Sep 01 2020 at 12:33):

chdoc created PR Review Comment on #558 Adding are_allpairs predicate:

This line has 83 characters, I suggest splitting it at the semicolon :grin:

view this post on Zulip Mathcomp Github Bot (Sep 01 2020 at 12:33):

chdoc created PR Review Comment on #558 Adding are_allpairs predicate:

The more natural generalization would probably be _.+1 rather than size xs

view this post on Zulip Mathcomp Github Bot (Sep 01 2020 at 12:35):

gares submitted PR Review for #559 Adding sig_big_dep lemma.

view this post on Zulip Mathcomp Github Bot (Sep 01 2020 at 12:36):

gares submitted PR Review for #558 Adding are_allpairs predicate.

view this post on Zulip Mathcomp Github Bot (Sep 01 2020 at 12:36):

gares created PR Review Comment on #558 Adding are_allpairs predicate:

@CohenCyril probably took my vscode configuration...

view this post on Zulip Mathcomp Github Bot (Sep 01 2020 at 12:37):

CohenCyril opened PR #563 Lemmas mxminpoly_minP and dvd_mxminpoly from minpolymx_minP to master:

Motivation for this change

Equivalence between horner_mx A p being zero and divisibility by the
minimal polynomial mxminpoly A. (Only one way was proven)
Part of #207.

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Sep 01 2020 at 12:37):

CohenCyril requested thery for a review on PR #563 Lemmas mxminpoly_minP and dvd_mxminpoly.

view this post on Zulip Mathcomp Github Bot (Sep 01 2020 at 12:43):

CohenCyril submitted PR Review for #558 Adding are_allpairs predicate.

view this post on Zulip Mathcomp Github Bot (Sep 01 2020 at 12:43):

CohenCyril created PR Review Comment on #558 Adding are_allpairs predicate:

Also, is it useful to have T : nonPropType rather than T : eqType while requiring r : rel T to be a boolean relation? I mean, the proof of are_allpairs_cons is nifty, but I would have expected a simpler proof based in are_allpairsP.

It may happen that a relation is decidable even on some non discrete types (e.g. a pair of an ordered type with a no discrete type), and I would like to preserve the full generality of the theorem on such occurences.

view this post on Zulip Mathcomp Github Bot (Sep 01 2020 at 12:43):

CohenCyril deleted PR Review Comment on #558 Adding are_allpairs predicate.

view this post on Zulip Mathcomp Github Bot (Sep 01 2020 at 12:53):

CohenCyril opened PR #564 More pinvmx theory from pinvmx to master:

Motivation for this change

Adding lemma making pinvmx usable in a broader context, and
equality with invmx when in unitmx.

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Sep 01 2020 at 12:53):

CohenCyril requested ybertot for a review on PR #564 More pinvmx theory.

view this post on Zulip Mathcomp Github Bot (Sep 01 2020 at 12:53):

CohenCyril edited PR #564 More pinvmx theory from pinvmx to master:

Motivation for this change

Adding lemma making pinvmx usable in a broader context, and
equality with invmx when in unitmx.
Part of #207.

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Sep 01 2020 at 12:54):

CohenCyril edited PR #207 Work In Progress: adding forms and spectral theorems from experiment/forms to master:

Content:

TODO:

TODO update after @LaurenceRideau tried on the odd-order repo (https://github.com/math-comp/odd-order/pull/2)

view this post on Zulip Mathcomp Github Bot (Sep 01 2020 at 13:07):

CohenCyril opened PR #565 Expliciting relation between split and [lr]shift from split_ordP to master:

Motivation for this change

Adds lemma split_ordP, a variant of splitP which introduces
ordinal equalities between the index and lshift/rshift, rather
than equalities in nat, which in some proofs makes the reasoning
easier (cf matrix.v), especially together with the new lemmas
eq_shift and eq_lshift, eq_rshift, eq_lrshift, eq_rlshift,
lrshiftP, and rlshiftP.
Part of #207.

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Sep 01 2020 at 13:07):

CohenCyril requested thery for a review on PR #565 Expliciting relation between split and [lr]shift.

view this post on Zulip Mathcomp Github Bot (Sep 01 2020 at 13:18):

CohenCyril opened PR #566 Lemma sub_sums_genmxP (generalizes sub_sumsmxP) from sub_sums_genmxP to master:

Motivation for this change

Part of #207.

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Sep 01 2020 at 13:19):

CohenCyril updated PR #566 Lemma sub_sums_genmxP (generalizes sub_sumsmxP) from sub_sums_genmxP to master:

Motivation for this change

Part of #207.

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Sep 01 2020 at 14:19):

gares assigned PR #565 Expliciting relation between split and [lr]shift to gares.

view this post on Zulip Mathcomp Github Bot (Sep 01 2020 at 17:55):

thery assigned PR #559 Adding sig_big_dep lemma to thery.

view this post on Zulip Mathcomp Github Bot (Sep 01 2020 at 17:57):

thery milestoned Issue #559 Adding sig_big_dep lemma (assigned to thery):

Motivation for this change

Useful tooling lemma with nested dependent bigops.
Part of #207.

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Sep 01 2020 at 17:58):

thery merged PR #559 Adding sig_big_dep lemma.

view this post on Zulip Mathcomp Github Bot (Sep 01 2020 at 17:58):

thery pushed 3 commits to branch master. Commits by CohenCyril (2) and thery (1).

view this post on Zulip Mathcomp Github Bot (Sep 01 2020 at 17:59):

thery assigned PR #560 Adding commr_horner lemma to thery.

view this post on Zulip Mathcomp Github Bot (Sep 01 2020 at 18:01):

thery milestoned Issue #560 Adding commr_horner lemma (assigned to thery):

Motivation for this change

Missing lemma between GRing.comm, comm_coef and horner.
Part of #207.

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Sep 01 2020 at 18:02):

thery requested ybertot and affeldt-aist for a review on PR #560 Adding commr_horner lemma.

view this post on Zulip Mathcomp Github Bot (Sep 01 2020 at 18:04):

thery submitted PR Review for #563 Lemmas mxminpoly_minP and dvd_mxminpoly.

view this post on Zulip Mathcomp Github Bot (Sep 01 2020 at 18:05):

thery assigned PR #564 More pinvmx theory.

view this post on Zulip Mathcomp Github Bot (Sep 01 2020 at 18:06):

thery milestoned Issue #564 More pinvmx theory (assigned to thery):

Motivation for this change

Adding lemma making pinvmx usable in a broader context, and
equality with invmx when in unitmx.
Part of #207.

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Sep 01 2020 at 18:07):

thery requested amahboubi and ybertot for a review on PR #564 More pinvmx theory.

view this post on Zulip Mathcomp Github Bot (Sep 01 2020 at 18:20):

thery submitted PR Review for #565 Expliciting relation between split and [lr]shift.

view this post on Zulip Mathcomp Github Bot (Sep 01 2020 at 18:20):

thery submitted PR Review for #565 Expliciting relation between split and [lr]shift.

view this post on Zulip Mathcomp Github Bot (Sep 01 2020 at 18:20):

thery created PR Review Comment on #565 Expliciting relation between split and [lr]shift:

I would never have guessed the name of this theorem P?

view this post on Zulip Mathcomp Github Bot (Sep 01 2020 at 18:20):

thery created PR Review Comment on #565 Expliciting relation between split and [lr]shift:

why not simple apply/eqP/lrshiftP.

view this post on Zulip Mathcomp Github Bot (Sep 01 2020 at 18:20):

thery created PR Review Comment on #565 Expliciting relation between split and [lr]shift:

same as after

view this post on Zulip Mathcomp Github Bot (Sep 01 2020 at 18:20):

thery created PR Review Comment on #565 Expliciting relation between split and [lr]shift:

same as before

view this post on Zulip Mathcomp Github Bot (Sep 02 2020 at 05:42):

pi8027 updated PR #458 The new interval library (assigned to CohenCyril) from interval to master:

Motivation for this change

This PR generalizes the results in interval.v using order structures.

Things done/to do

<!-- please fill in the following checklist -->

PR overlays

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Sep 02 2020 at 06:35):

pi8027 updated PR #546 [DO NOT MERGE] Fix a coherence (ambiguous paths) issue of fieldExtType and a conversion issue of "regular" instances from fieldext-coherence to master:

Motivation for this change
Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Sep 02 2020 at 06:35):

pi8027 updated PR #464 [WIP] meet semilattice structures from semilattices to master:

Motivation for this change

This PR adds the following structures:

cc: @strub

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Sep 02 2020 at 06:35):

pi8027 updated PR #548 Use predicators even extensively from predicators to master:

Motivation for this change

This PR attempts to restate several lemmas using predicators such as cancel, (left|right)_(id|zero|inverse|distributive), idempotent, associative, and commutative. Some of them are probably too aggressive and I would like to have comments on this point.

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Sep 02 2020 at 10:04):

CohenCyril updated PR #565 Expliciting relation between split and [lr]shift (assigned to gares) from split_ordP to master:

Motivation for this change

Adds lemma split_ordP, a variant of splitP which introduces
ordinal equalities between the index and lshift/rshift, rather
than equalities in nat, which in some proofs makes the reasoning
easier (cf matrix.v), especially together with the new lemmas
eq_shift and eq_lshift, eq_rshift, eq_lrshift, eq_rlshift,
lrshiftP, and rlshiftP.
Part of #207.

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to reviewers -->

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

view this post on Zulip Mathcomp Github Bot (Sep 02 2020 at 10:04):

CohenCyril updated PR #558 Adding are_allpairs predicate (assigned to gares) from are_allpairs to master:

Motivation for this change

<!-- please explain your reason for doing this change -->

This predicate is useful in stating that a sequence of matrices all commute.
This is a part of #207.

Things done/to do

<!-- please fill in the following checklist -->

<!-- leave this note as a reminder to