Kazuhiko Sakaguchi

New order structures and definitionally involutive duals

19

##### Motivation for this change This PR adds the following structures and implements definitionally involutive duals (except for complemented lattice structures): - `(b|t|tb)POrderType`, - `(|b|t|tb|fin|finB)MeetSemilatticeType`: meet-semilattice, - `(|b|t|tb|fin|finT)JoinSemilatticeType`: join-semilattice, -...

Rework of PR #281: Archimedean structures on top of num/real domain/field/closedField

27

##### Motivation for this change This PR renames the `archiFieldType` structure to `archiRealFieldType` and introduces 5 new Archimedean ring/field structures. These structures are currently defined in `ssrnum.v`, but will be...

##### Motivation for this change This is an experimental feature of the order hierarchy based on #464. I open this PR just to run CI. ##### Things done/to do -...

Old comments mentioning unsupported versions of Coq

5

Should we review, simplify, and/or remove them? https://github.com/math-comp/math-comp/blob/9bfc9834b46c1e492aaaf257cfa811d1e5e39065/mathcomp/ssreflect/ssrAC.v#L70-L72 https://github.com/math-comp/math-comp/blob/9bfc9834b46c1e492aaaf257cfa811d1e5e39065/mathcomp/ssreflect/finfun.v#L18-L21 https://github.com/math-comp/math-comp/blob/9bfc9834b46c1e492aaaf257cfa811d1e5e39065/mathcomp/algebra/ssralg.v#L1856-L1858 https://github.com/math-comp/math-comp/blob/9bfc9834b46c1e492aaaf257cfa811d1e5e39065/mathcomp/algebra/ssralg.v#L3551-L3552 https://github.com/math-comp/math-comp/blob/9bfc9834b46c1e492aaaf257cfa811d1e5e39065/mathcomp/algebra/vector.v#L1384-L1386 https://github.com/math-comp/math-comp/blob/9bfc9834b46c1e492aaaf257cfa811d1e5e39065/mathcomp/field/fieldext.v#L1584-L1592

I saw at least two use cases of order.v that open `order_scope`. I think that the header documentation should strongly recommend users not to open `order_scope` and explain its reason.

Make the finType structure equipped with indexing functions

2

This PR redefine the `finType` structure by adding the following bijection to `Finite.mixin_of T`. ``` fin_encode : T -> 'I_#|T|, fin_decode : 'I_#|T| -> T. ``` I have used this...

Missing subset lemmas

3

```coq Lemma subset_trans {T : eqType} (s1 s2 s3 : seq T) : {subset s1 {subset s2 {subset s1 all p s1. Lemma subset_cons {T : eqType} (s: seq T)...

> BTW, having `minn` and `maxn` in the arguments of `leqP`, `ltnP`, and `ltngtP` could be nice. But we need to reorder definitions and lemmas in ssrnat. (In this case,...

Coq PG doesn't recognize the new quotation mechanism of coq/coq#9733

8

For example, with the coq-elpi plugin, we can write the following Vernacular command. But PG doesn't recognize the proper end of the command when we do `C-c C-n`. https://github.com/LPCIC/coq-elpi/blob/6d21fa61fb59a555c5075ba3e3c89844a5d14bee/theories/tutorial/elpi_lang.v#L53-L58 ```...

See math-comp/math-comp#682.