1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
|
# Changelog (unreleased)
To avoid having old PRs put changes into the wrong section of the CHANGELOG,
new entries now go to the present file as discussed
[here](https://github.com/math-comp/math-comp/wiki/Agenda-of-the-April-23rd-2019-meeting-9h30-to-12h30#avoiding-issues-with-changelog).
The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/).
## [Unreleased]
### Added
- Added a `void` notation for the `Empty_set` type of the standard library, the
canonical injection `of_void` and its cancellation lemma `of_voidK`, and
`eq`, `choice`, `count` and `fin` instances.
- Added fixpoint and cofixpoint constructions to `finset`: `fixset`,
`cofixset` and `fix_order`, with a few theorems about them
- Added functions `tuple_of_finfun`, `finfun_of_tuple`, and their
"cancellation" lemmas.
- Added theorems `totient_prime` and `Euclid_dvd_prod` in `prime.v`
- Added theorems `ffact_prod`, `prime_modn_expSn` and `fermat_little`
in `binomial.v`
- Added theorems `flatten_map1`, `allpairs_consr`, and `mask_filter` in `seq.v`.
- Fintype theorems: `fintype0`, `card_le1P`, `mem_card1`,
`card1P`, `fintype_le1P`, `fintype1`, `fintype1P`,
`existsPn`, `exists_inPn`, `forallPn`, `forall_inPn`.
- Bigop theorems: `big_rmcond`, `bigD1_seq`,
`big_enum_val_cond`, `big_enum_rank_cond`,
`big_enum_val`, `big_enum_rank`, `big_set`.
- Arithmetic theorems in ssrnat and div:
- some trivial results in ssrnat: `ltn_predl`, `ltn_predr`,
`ltn_subr` and `predn_sub`,
- theorems about `n <=/< p +/- m` and `m +/- n <=/< p`:
`leq_psubRL`, `ltn_psubLR`, `leq_subRL`, `ltn_subLR`, `leq_subCl`,
`leq_psubCr`, `leq_subCr`, `ltn_subCr`, `ltn_psubCl` and
`ltn_subCl`,
- some commutations between modulo and division: `modn_divl` and
`divn_modl`,
- theorems about the euclidean division of additions and subtraction,
+ without preconditions of divisibility: `edivnD`, `edivnB`,
`divnD`, `divnB`, `modnD`, `modnB`,
+ with divisibility of one argument: `divnDMl`, `divnMBl`,
`divnBMl`, `divnBl` and `divnBr`,
+ specialization of the former theorems for .+1 and .-1:
`edivnS`, `divnS`, `modnS`, `edivn_pred`, `divn_pred` and
`modn_pred`.
- Added map/parametricity theorems about `path`, `sort` and `sorted`:
- Added `mem2E` in `path.v`.
- Added `sort_rec1` and `sortE` to help inductive reasoning on `sort`.
- Added map/parametricity theorems about `path`, `sort`, and `sorted`:
`homo_path`, `mono_path`, `homo_path_in`, `mono_path_in`,
`homo_sorted`, `mono_sorted`, `map_merge`, `merge_map`, `map_sort`,
`sort_map`, `sorted_map`, `homo_sorted_in`, `mono_sorted_in`.
- Added the theorem `perm_iota_sort` to express that the sorting of
any sequence `s` is equal to a mapping of `iota 0 (size s)` to the
nth elements of `s`, so that one can still reason on `nat`, even
though the elements of `s` are not in an `eqType`.
- Added stability theorems about `merge` and `sort`: `sorted_merge`,
`merge_stable_path`, `merge_stable_sorted`, `sorted_sort`, `sort_stable`,
`filter_sort`, `mask_sort`, `sorted_mask_sort`, `subseq_sort`,
`sorted_subseq_sort`, and `mem2_sort`.
- New algebraic interfaces : comAlgebra and comUnitAlgebra for
commutative and commutative-unitary algebras.
- Initial property for polynomials in algebras:
New canonical lrMoprphism `horner_alg` evaluating a polynomial in an element
of an algebra. The theory include the lemmas `in_alg_comm`, `horner_algC`,
`horner_algX`, `poly_alg_initial`.
### Changed
- `eqVneq` lemma is changed from `{x = y} + {x != y}` to
`eq_xor_neq x y (y == x) (x == y)`, on which a case analysis performs
simultaneous replacement of expressions of the form `x == y` and `y == x`
by `true` or `false`, while keeping the ability to use it in the way
it was used before.
- Generalized the `allpairs_catr` lemma to the case where the types of `s`,
`t1`, and `t2` are non-`eqType`s in `[seq E | i <- s, j <- t1 ++ t2]`.
- Generalized `muln_modr` and `muln_modl` removing hypothesis `0 < p`.
- Generalized `sort` to non-`eqType`s (as well as `merge`,
`merge_sort_push`, `merge_sort_pop`), together with all the lemmas
that did not really rely on an `eqType`: `size_merge`, `size_sort`,
`merge_path`, `merge_sorted`, `sort_sorted`, `path_min_sorted`
(which statement was modified to remove the dependency in `eqType`),
and `order_path_min`.
- `compare_nat` type family and `ltngtP` comparison predicate are changed
from `compare_nat m n (m <= n) (n <= m) (m < n) (n < m) (n == m) (m == n)`
to `compare_nat m n (n == m) (m == n) (n <= m) (m <= n) (n < m) (m < n)`,
to make it tries to match subterms with `m < n` first, `m <= n`, then
`m == n`.
+ The compatibility layer for the version 1.9 is provided as the
`ssrnat.mc_1_9` module. One may compile proofs compatible with the version
1.9 in newer versions by using this module.
### Infrastructure
- `Makefile` now supports the `test-suite` and `only` targets. Currently,
`make test-suite` will verify the implementation of mathematical structures
and their inheritances of MathComp automatically, by using the `hierarchy.ml`
utility. One can use the `only` target to build the sub-libraries of MathComp
specified by the `TGTS` variable, e.g.,
`make only TGTS="ssreflect/all_ssreflect.vo fingroup/all_fingroup.vo"`.
|
