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.)

1 files changed, 38 insertions, 10 deletions

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