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
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
|
??/??/???? - version 1.7.1
* Removed `_ : Type` field from packed classes. This performance
optimization is not strictly necessary with modern Coq versions.
* Added companion matrix of a polynomial `companionmx p` and the
theorems: companionmxK, map_mx_companion and companion_map_poly.
* Extended generic theory about monotonocity (*mono* and *homo* lemmas).
* Added: homoW_in, inj_homo_in, mono_inj_in, anti_mono_in,
total_homo_mono_in, homoW, inj_homo, monoj, anti_mono,
total_homo_mono.
* Extended theory about homo and mono for leq/or and Num.le
* Renamed: (together with the _in suffix counterpart)
mono_inj -> incr_inj
nmono_inj -> decr_inj
leq_mono_inj -> incnr_inj
leq_nmono_inj -> decnr_inj
homo_inj_ltn_lt -> incnr_inj
nhomo_inj_ltn_lt -> decnr_inj
homo_inj_in_lt -> inj_homo_ltr_in
nhomo_inj_in_lt -> inj_nhomo_ltr_in
ltn_ltrW_homo -> ltnrW_homo
ltn_ltrW_nhomo -> ltnrW_nhomo
leq_lerW_mono -> lenrW_mono
leq_lerW_nmono -> lenrW_nmono
homo_leq_mono -> lenr_mono
nhomo_leq_mono -> lenr_nmono
homo_inj_lt -> inj_homo_ltr
nhomo_inj_lt -> inj_nhomo_ltr
homo_inj_ltn_lt -> inj_homo_ltnr
nhomo_inj_ltn_lt -> inj_nhomo_ltnr
homo_mono -> ler_mono
nhomo_mono -> ler_nmono
* Added sorted_lt_nth, ltn_index, sorted_le_nth, leq_index.
* Generalized extremum_spec and its theory, added extremum and
extremumP, generalizing arg_min for an arbitrary eqType with an
order relation on it (rather than nat). Redefined arg_min and
arg_max with it.
* Added [arg minr_( i < n | P ) F] and [arg maxr_( i < n | P ) F]
with all their variants, following the same convention as for nat.
* Added missing contra* lemma: contra_neqN, contra_neqF,
contra_neqT, contra_neq_eq, contra_eq_neq.
* Addded missing seq theorems: take_subseq, drop_subseq
* Reshuffled theorems inside files and packages:
* countalg goes from the field to the algebra package
* finalg now gets inheritance from countalg
* closed_field now contains the construction of algebraic closure
for countable fields that used to be in countalg.
* Rewritten proof of quantifier elimination for closed field in a
monadic style.
* Added all_iff, "the following are all equivalent"
with notation [<-> P0; P1; ..; Pn] and theorems
`all_iffLR` and coercion `all_iffP` (see header for doc)
proved by circular implication P0 -> P1 -> ... -> Pn -> P0
* Removed duplicated definitions of `tag` `tagged` and `Tagged`
from eqtype.v. They were already in ssrfun.v.
* Specialized `bool_irrelevance` so that the statement reflects
the name.
* Changed the shape of the type of FieldMixin to allow one-line
in-proof definition of bespoke fieldType structure.
* Refactored and extended Arguments directives to provide more
comprehensive signature information.
* Added maximal implicits to reflection, injectivity and cancellation
lemmas so that they are easier to pass to combinator lemmas such as
sameP, inj_eq or canLR.
* Added reindex_inj s shorthand for reindexing a bigop with a
permutation s.
* Added lemma `eqmxMunitP`: two matrices with the same shape
represent the same subspace iff they differ only by a change of
basis.
* Corrected implicits and documentation of MatrixGenField.
24/04/2018 - compatibility with Coq 8.8 and several small fixes - version 1.7
* Added compatibility with Coq 8.8 and lost compatibility with
Coq <= 8.5. This release is compatible with Coq 8.6, 8.7 and 8.8.
* Integration to Coq: ssrbool.v ssrfun.v and plugin.
ssrtest also moved to Coq test suite.
* Cleaning up the github repository: the math-comp repository is
now dedicated to the released material (as in the present
release). For instance, directories real-closed and odd-order now
have their own repository.
* Library refactoring: algC ssrnum: Library ssrnum.v now
provides an interface numClosedFieldType, which abstracts the
theory of algebraic numbers. In particular, Re, Im, 'i,
conjC, n.-root and sqrtC, previously defined in library algC.v,
are now part of this generic interface. In case of ambiguity,
a cast to type algC, of complex algebraic numbers, can be used to
disambiguate via typing constraints. Some theory was thus made
more generic, and the corresponding lemmas, previously defined in
library algC.v (e.g. conjCK) now feature an extra, non maximal
implicit, parameter of type numClosedFieldType. This could break
some proofs.
* Lemma dvdn_fact was moved from library prime.v to library div.v
* Structures, changes in interfaces:
numClosedFieldType
* New Theorems:
iter_in, finv_in, inv_f_in, finv_inj_in, fconnect_sym_in,
iter_order_in, iter_finv_in, cycle_orbit_in, fpath_finv_in,
fpath_finv_f_in, fpath_f_finv_in
big_allpairs
uniqP, uniqPn
dec_factor_theorem,
mul_bin_down, mul_bin_left
abstract_context (now merged in Coq)
* Renamed/generalized:
mul_Sm_binm -> mul_bin_diag
divn1 -> divz1 (in intdiv)
rootC -> nthroot
algRe -> Re
algIm -> Im
algCi -> imaginaryC
reshape_index_leq -> reshape_leq
Every theorem from ssrnum that used to be in algC
* Generalized or improved:
ltngtP, contra_eq, contra_neq, odd_opp, nth_iota
24/11/2015 - major reorganization of the archive - version 1.6
* Files split into sub-directories: ssreflect, algebra, fingroup,
solvable, field and character. In this way the user can decide
to compile only the subset of the Mathematical Components library
that is relevant to her. Note that this introduces a possible
incompatibility for users of the previous version. A replacement
scheme is suggested in the installation notes.
* The archive is now open and based on git. Public mirror at:
https://github.com/math-comp/math-comp
* Sources of the reference manual of the Ssreflect tactic language are
also open and available at:
https://github.com/math-comp/ssr-manual
Pull requests improving the documentation are welcome.
* Renaming or replacements:
conjC_closed -> cfConjC_closed
class_transr -> class_eqP
cfclass_transl -> cfclass_transr
nontrivial_ideal -> proper_ideal
zchar_orthonormalP -> vchar_orthonormalP
* Definitions that changed:
seq_sub
* Statements that changed:
orbit_in_transl, orbit_sym, orbit_trans, orbit_transl, orbit_transr,
cfAut_char, cfConjC_char, invg_lcosets, lcoset_transl,
lcoset_transr, rcoset_transl, rcoset_transr, mem2_last,
bind_unless, unless_contra, all_and2, all_and3, all_and4, all_and5,
ltr0_neq0, ltr_prod, Zisometry_of_iso
* New definitions:
adhoc_seq_sub_choiceMixin, adhoc_seq_sub_[choice|fin]Type
* New theorems:
orbit_in_eqP, cards_draws, cfAut_lin_char, cfConjC_lin_char,
extend_cfConjC_subset, isometry_of_free, cfAutK, cfAutVK,
lcoset_eqP, rcoset_eqP, class_eqP, gFsub_trans, gFnorms,
gFchar_trans, gFnormal_trans, gFnorm_trans, mem2_seq1,
dvdn_fact, prime_above, subKr, subrI, subIr, subr0_eq,
divrI, divIr, divKr, divfI, divIf, divKf, impliesP, impliesPn,
unlessL, unlessR, unless_sym, unlessP (coercion), classicW,
ltr_prod_nat
* New notation: "\unless C, P"
12/03/2014 - split the archive in SSReflect and MathComp - version 1.5
* With this release "ssreflect" has been split into two packages.
The Ssreflect one contains the proof language (plugin for Coq) and a
small set of core theory libraries about boolean, natural numbers,
sequences, decidable equality and finite types. The Mathematical
Components one contains advanced theory files covering a wider
spectrum of mathematics.
* With respect to version 1.4 the proof language got a few new
features related to forward reasoning and some bug fixes. The
Mathematical Components library features 16 new theory files and in
particular: some field and Galois theory, advanced character theory
and a construction of algebraic numbers.
05/09/2012 - ssreflect - version 1.4
* With this release the plugin code received many bug fixes and the
existing libraries relevant updates. This release also includes
some new libraries on the following topics: rational numbers,
divisibility of integers, F-algebras, finite dimensional field
extensions and Euclidean division for polynomials over a ring.
* The release includes a major code refactoring of the plugin for Coq
8.4. In particular a documented ML API to access the pattern matching
facilities of Ssreflect from third party plugins has been introduced.
14/03/2011 - ssreflect - version 1.3
* The tactic language has been extended with several new features,
inspired by the five years of intensive use in our project. However we
have kept the core of the language unchanged; the new library compiles
with Ssreflect 1.2. Users of a Coq 8.2 toplevel statically linked
with Ssreflect 1.2 need to comment the Declare ML Module "ssreflect"
line in ssreflect.v to properly compile the 1.3 library. We will
continue supporting new releases of Coq in due course.
* The new library adds general linear algebra (matrix rank, subspaces)
and all of the advanced finite group that was developed in the course
of completing the Local Analysis part of the Odd Order Theorem,
starting from the Sylow and Hall theorems and including full structure
theorems for abelian, extremal and extraspecial groups, and general
(modular) linear representation theory.
14/08/2009 - ssreflect - version 1.2
* No change log
18/03/2008 - ssreflect - version 1.1
* First public release
|
