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
|
# 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
- Lemmas `ltnNleqif`, `eq_leqif`, `eqTleqif` in `ssrnat`
- Lemmas `eqEtupe`, `tnthS` and `tnth_nseq` in `tuple`
- Ported `order.v` from the finmap library, which provides structures of ordered
sets (`porderType`, `distrLatticeType`, `orderType`, etc.) and its theory.
### Changed
- Reorganized the algebraic hierarchy and the theory of `ssrnum.v`.
+ `numDomainType` and `realDomainType` get inheritances respectively from
`porderType` and `orderType`.
+ `normedZmodType` is a new structure for `numDomainType` indexed normed
additive abelian groups.
+ `[arg minr_( i < n | P ) F]` and `[arg maxr_( i < n | P ) F]` notations are
removed. Now `[arg min_( i < n | P ) F]` and `[arg max_( i < n | P ) F]`
notations are defined in `nat_scope` (specialized for `nat`), `order_scope`
(general one), and `ring_scope` (specialized for `ring_display`). Lemma
`fintype.arg_minP` is aliased to `arg_minnP` and the same for `arg_maxnP`.
+ The following lemmas are generalized, renamed, and relocated to `order.v`:
* `ltr_def` -> `lt_def`
* `(ger|gtr)E` -> `(ge|gt)E`
* `(le|lt|lte)rr` -> `(le|lt|lte)xx`
* `ltrW` -> `ltW`
* `ltr_neqAle` -> `lt_neqAle`
* `ler_eqVlt` -> `le_eqVlt`
* `(gtr|ltr)_eqF` -> `(gt|lt)_eqF`
* `ler_anti`, `ler_asym` -> `le_anti`
* `eqr_le` -> `eq_le`
* `(ltr|ler_lt|ltr_le|ler)_trans` -> `(lt|le_lt|lt_le|le)_trans`
* `lerifP` -> `leifP`
* `(ltr|ltr_le|ler_lt)_asym` -> `(lt|lt_le|le_lt)_asym`
* `lter_anti` -> `lte_anti`
* `ltr_geF` -> `lt_geF`
* `ler_gtF` -> `le_gtF`
* `ltr_gtF` -> `lt_gtF`
* `lt(r|nr|rn)W_(n)homo(_in)` -> `ltW_(n)homo(_in)`
* `inj_(n)homo_lt(r|nr|rn)(_in)` -> `inj_(n)homo_lt(_in)`
* `(inc|dec)(r|nr|rn)_inj(_in)` -> `(inc_dec)_inj(_in)`
* `le(r|nr|rn)W_(n)mono(_in)` -> `leW_(n)mono(_in)`
* `lenr_(n)mono(_in)` -> `le_(n)mono(_in)`
* `lerif_(refl|trans|le|eq)` -> `leif_(refl|trans|le|eq)`
* `(ger|ltr)_lerif` -> `(ge|lt)_leif`
* `(n)mono(_in)_lerif` -> `(n)mono(_in)_leif`
* `(ler|ltr)_total` -> `(le|lt)_total`
* `wlog_(ler|ltr)` -> `wlog_(le|lt)`
* `ltrNge` -> `ltNge`
* `lerNgt` -> `leNgt`
* `neqr_lt` -> `neq_lt`
* `eqr_(le|lt)(LR|RL)` -> `eq_(le|lt)(LR|RL)`
* `eqr_(min|max)(l|r)` -> `eq_(meet|join)(l|r)`
* `ler_minr` -> `lexI`
* `ler_minl` -> `leIx`
* `ler_maxr` -> `lexU`
* `ler_maxl` -> `leUx`
* `lt(e)r_min(r|l)` -> `lt(e)(xI|Ix)`
* `lt(e)r_max(r|l)` -> `lt(e)(xU|Ux)`
* `minrK` -> `meetUKC`
* `minKr` -> `joinKIC`
* `maxr_min(l|r)` -> `joinI(l|r)`
* `minr_max(l|r)` -> `meetU(l|r)`
* `minrP`, `maxrP` -> `leP`, `ltP`
* `(minr|maxr)(r|C|A|CA|AC)` -> `(meet|join)(xx|C|A|CA|AC)`
* `minr_(l|r)` -> `meet_(l|r)`
* `maxr_(l|r)` -> `join_(l|r)`
* `arg_minrP` -> `arg_minP`
* `arg_maxrP` -> `arg_maxP`
+ Generalized the following lemmas as properties of `normedDomainType`:
`normr0`, `normr0P`, `normr_eq0`, `distrC`, `normr_id`, `normr_ge0`,
`normr_le0`, `normr_lt0`, `normr_gt0`, `normrE`, `normr_real`,
`ler_norm_sum`, `ler_norm_sub`, `ler_dist_add`, `ler_sub_norm_add`,
`ler_sub_dist`, `ler_dist_dist`, `ler_dist_norm_add`, `ler_nnorml`,
`ltr_nnorml`, `lter_nnormr`.
+ The compatibility layer for the version 1.9 is provided as the
`ssrnum.mc_1_9` module. One may compile proofs compatible with the version
1.9 in newer versions by using the `mc_1_9.Num` module instead of the `Num`
module. However, instances of the number structures may require changes.
### Renamed
- `real_lerP` -> `real_leP`
- `real_ltrP` -> `real_ltP`
- `real_ltrNge` -> `real_ltNge`
- `real_lerNgt` -> `real_leNgt`
- `real_ltrgtP` -> `real_ltgtP`
- `real_ger0P` -> `real_ge0P`
- `real_ltrgt0P` -> `real_ltgt0P`
- `lerif_nat` -> `leif_nat_r`
- Replaced `lerif` with `leif` in the following names of lemmas:
+ `lerif_subLR`, `lerif_subRL`, `lerif_add`, `lerif_sum`, `lerif_0_sum`,
`real_lerif_norm`, `lerif_pmul`, `lerif_nmul`, `lerif_pprod`,
`real_lerif_mean_square_scaled`, `real_lerif_AGM2_scaled`,
`lerif_AGM_scaled`, `real_lerif_mean_square`, `real_lerif_AGM2`,
`lerif_AGM`, `relif_mean_square_scaled`, `lerif_AGM2_scaled`,
`lerif_mean_square`, `lerif_AGM2`, `lerif_normC_Re_Creal`, `lerif_Re_Creal`,
`lerif_rootC_AGM`.
- The following naming inconsistencies have been fixed in `ssrnat.v`:
+ `homo_inj_lt(_in)` -> `inj_homo_ltn(in)`
+ `(inc|dec)r(_in)` -> `(inc|dev)n(_in)`
### Removed
### Infrastructure
### Misc
|
