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
|
07/09/2016 - compatibility with Coq 8.7 and several small fixes -
upcoming version 1.7
* Compatibility with Coq 8.7
* Lost compatibility with Coq 8.4
* Library refactoring: algC, complex, ssrnum: Library ssrnum.v now
provides an interface numClosedFieldType, which factors some
theory from both complex and algC. In particular, Re, Im, 'i,
conjC, n.-root and sqrtC are now part of this generic
interface. In case of ambiguity, they can be casted to the type
algC, of complex algebraic numbers, 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
(C : numClosedFieldType). This could break some
proofs. Additionally, a few ad hoc constructions in library
complex.v, e.g. -*+ or complex.Re, are now deprecated and should
be replaced by the corresponding ones provided by the
numClosedFieldType interface. The next revision might definitely
hide those constructions under a module.
* Structures, changes in interfaces:
numClosedFieldType
* New Theorems:
dec_factor_theorem, abstract_context,
mul_bin_down, mul_bin_left
* Renamed/generalized:
mul_Sm_binm -> mul_bin_diag
divn1 -> divz1 (in intdiv)
rootC -> nthroot
algRe -> Re
algIm -> Im
algCi -> imaginaryC
Every theorem from ssrnum that used to be in algC
* Generalized or improved:
ltngtP, contra_eq, contra_neq, odd_opp
* Plugin:
ssrpattern: compatibility with Tactic Notation
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
|
