From c0254eaba338a4d308b4e2f200841ff76e6b4b9a Mon Sep 17 00:00:00 2001 From: Georges Gonthier Date: Sun, 31 Mar 2019 03:52:29 +0200 Subject: Permutations and other extensions to seq; fintype documentation - Added `permutations` and some `perm_eq` lemmas suggested by @MrSet in #299 (except the link to the coq lib `Permutation` predicate). Use insertions to construct permutations. This definition is closer to the one proposed by @MrSet, than one using rotations (it adds one line to the definition of `permutations` but the proofs become a little simpler.) - Added support for casts on `map` comprehension general terms. - Added `allpairs_map[lr]` suggested by @pi8027 in #314, but with equational proofs; changed `allpairs_comp` to its converse `map_allpairs` for consistency. - Add three `allpairs` extensionality lemmas: for the non-localised, dependent localised and non-dependent localised cases; as per `eq_in_map`, the latter two are equivalences. - Documented the `all2` predicate added in #224, and the view combinators added in #202. - Renamed `seq2_ind` to `seq_ind2`, and weakened the induction hypothesis, adding a `size` equality assumption. - Corrected the header to use `<=>` for `bool` predicate documentation, and `<->` for `Prop` predicates, following the library’s general convention. - Replaced the `nosimpl` in `rev` with a `Arguments simpl never` directive, making it possible to merge the `Rev` section into the main `Sequences` section. - Miscellaneous improvements to proof scripts and file organisation. - Correct maximal implicits of `constant`. - Fixes omitted `Prenex Implicit` declaration. - Other implicits fixes. - Fix apparent `done` regression It appears `done` now does a weaker form of intros, and this broke the `dtuple_onP` proof. Updated the proof to eliminate the issue. (Commit log edited by @CohenCyril during the squash.) --- CHANGELOG.md | 48 ++++++++++++++++++++++++++++++++++++++---------- 1 file changed, 38 insertions(+), 10 deletions(-) (limited to 'CHANGELOG.md') diff --git a/CHANGELOG.md b/CHANGELOG.md index 9a0559c..3ea6b8c 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -12,7 +12,7 @@ MathComp 1.8.0 is compatible with Coq 8.7, 8.8 and 8.9. - Companion matrix of a polynomial `companionmx p` and the theorems: `companionmxK`, `map_mx_companion` and `companion_map_poly` - + - `homoW_in`, `inj_homo_in`, `mono_inj_in`, `anti_mono_in`, `total_homo_mono_in`, `homoW`, `inj_homo`, `monoj`, `anti_mono`, `total_homo_mono` @@ -36,6 +36,18 @@ MathComp 1.8.0 is compatible with Coq 8.7, 8.8 and 8.9. circular implication `P0 -> P1 -> ... -> Pn -> P0`. Related theorems are `all_iffLR` and `all_iffP` +- support for casts in map comprehension notations, e.g., + `[seq E : T | s <- s]`. + +- a predicate `all2`, a parallel double `seq` version of `all`. + +- some `perm_eq` lemmas: `perm_cat[lr]`, `perm_eq_nilP`, + `perm_eq_consP`, `perm_eq_flatten`. + +- a function `permutations` that computes a duplicate-free list + of all permutations of a given sequence `s` over an `eqType`, along + whit its theory. + ### Changed - Theory of `lersif` and intervals: @@ -83,20 +95,34 @@ MathComp 1.8.0 is compatible with Coq 8.7, 8.8 and 8.9. where `t` may depend on `i`. The notation is now primitive and expressed using `flatten` and `map` (see documentation of seq). `allpairs` now expands to this notation when fully applied. - Added `allpairs_dep` and made it self-expanding as well. - Generalized some lemmas in a backward compatible way. - Some strictly more general lemmas now have suffix `_dep`. - -- Generalised `{ffun A -> R}` to handle dependent functions, and to be + + Added `allpairs_dep` and made it self-expanding as well. + + Generalized some lemmas in a backward compatible way. + + Some strictly more general lemmas now have suffix `_dep`. + + Replaced `allpairs_comp` with its converse `map_allpairs`. + + Added `allpairs` extensionality lemmas for the following cases: + non-localised (`eq_allpairs`), dependent localised + (`eq_in_allpairs_dep`) and non-dependent localised + (`eq_in_allpairs`); as per `eq_in_map`, the latter two are + equivalences. + +- Generalized `{ffun A -> R}` to handle dependent functions, and to be structurally positive so it can be used in recursive inductive type definitions. - + Minor backward incompatibilities: `fgraph f` is no longer a field accessor, and no longer equal to `val f` as `{ffun A -> R}` is no longer a `subType`; some instances of `finfun`, `ffunE`, `ffunK` may not unify - with a generic nondependent function type `A -> ?R` due to a bug in + with a generic non-dependent function type `A -> ?R` due to a bug in Coq version 8.9 or below. +- Renamed double `seq` induction lemma from `seq2_ind` to `seq_ind2`, + and weakened its induction hypothesis. + +- Replaced the `nosimpl` in `rev` with a `Arguments simpl never` + directive. + +- Many corrections in implicits declarations. + ### Renamed Renamings also involve the `_in` suffix counterpart when applicable @@ -132,6 +158,8 @@ Renamings also involve the `_in` suffix counterpart when applicable - Removed duplicated definitions of `tag`, `tagged` and `Tagged` from `eqtype.v`. They are already in `ssrfun.v`. +- Miscellaneous improvements to proof scripts and file organisation. + ## [1.7.0] - 2018-04-24 Compatibility with Coq 8.8 and lost compatibility with @@ -160,7 +188,7 @@ Coq <= 8.5. This release is compatible with Coq 8.6, 8.7 and 8.8. implicit, parameter of type `numClosedFieldType`. This could break some proofs. Every theorem from `ssrnum` that used to be in `algC` changed statement. - + - `ltngtP`, `contra_eq`, `contra_neq`, `odd_opp`, `nth_iota` ### Added @@ -193,7 +221,7 @@ Major reorganization of the archive. 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 -- cgit v1.2.3