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, 13 insertions, 11 deletions

diff --git a/mathcomp/ssreflect/fintype.v b/mathcomp/ssreflect/fintype.v
index 93810ca..c06238c 100644
--- a/mathcomp/ssreflect/fintype.v
+++ b/mathcomp/ssreflect/fintype.v
@@ -92,9 +92,9 @@ Require Import ssrfun ssrbool eqtype ssrnat seq choice path.
 (*      enum_rank x == the i : 'I_(#|T|) such that enum_val i = x.            *)
 (* enum_rank_in Ax0 x == some i : 'I_(#|A|) such that enum_val i = x if       *)
 (*                     x \in A, given Ax0 : x0 \in A.                         *)
-(*      A \subset B == all x \in A satisfy x \in B.                           *)
-(*      A \proper B == all x \in A satisfy x \in B but not the converse.      *)
-(* [disjoint A & B] == no x \in A satisfies x \in B.                          *)
+(*      A \subset B <=> all x \in A satisfy x \in B.                          *)
+(*      A \proper B <=> all x \in A satisfy x \in B but not the converse.     *)
+(* [disjoint A & B] <=> no x \in A satisfies x \in B.                         *)
 (*        image f A == the sequence of f x for all x : T such that x \in A    *)
 (*                     (where a is an applicative predicate), of length #|P|. *)
 (*                     The codomain of F can be any type, but image f A can   *)
@@ -108,13 +108,13 @@ Require Import ssrfun ssrbool eqtype ssrnat seq choice path.
 (*                     im_y : y \in image f P.                                *)
 (*     invF inj_f y == the x such that f x = y, for inj_j : injective f with  *)
 (*                     f : T -> T.                                            *)
-(*  dinjectiveb A f == the restriction of f : T -> R to A is injective        *)
+(*  dinjectiveb A f <=> the restriction of f : T -> R to A is injective       *)
 (*                     (this is a bolean predicate, R must be an eqType).     *)
-(*     injectiveb f == f : T -> R is injective (boolean predicate).           *)
-(*         pred0b A == no x : T satisfies x \in A.                            *)
-(*    [forall x, P] == P (in which x can appear) is true for all values of x; *)
+(*     injectiveb f <=> f : T -> R is injective (boolean predicate).          *)
+(*         pred0b A <=> no x : T satisfies x \in A.                           *)
+(*    [forall x, P] <=> P (in which x can appear) is true for all values of x *)
 (*                     x must range over a finType.                           *)
-(*    [exists x, P] == P is true for some value of x.                         *)
+(*    [exists x, P] <=> P is true for some value of x.                        *)
 (*      [forall (x | C), P] := [forall x, C ==> P].                           *)
 (*       [forall x in A, P] := [forall (x | x \in A), P].                     *)
 (*      [exists (x | C), P] := [exists x, C && P].                            *)
@@ -123,13 +123,15 @@ Require Import ssrfun ssrbool eqtype ssrnat seq choice path.
 (*   [exists x : T, P], [exists x : T in A, P], etc.                          *)
 (* -> The outer brackets can be omitted when nesting finitary quantifiers,    *)
 (*    e.g., [forall i in I, forall j in J, exists a, f i j == a].             *)
-(*       'forall_pP == view for [forall x, p _], for pP : reflect .. (p _).   *)
-(*       'exists_pP == view for [exists x, p _], for pP : reflect .. (p _).   *)
+(*       'forall_pP <-> view for [forall x, p _], for pP : reflect .. (p _).  *)
+(*       'exists_pP <-> view for [exists x, p _], for pP : reflect .. (p _).  *)
+(*    'forall_in_pP <-> view for [forall x in .., p _], for pP as above.      *)
+(*    'exists_in_pP <-> view for [exists x in .., p _], for pP as above.      *)
 (*     [pick x | P] == Some x, for an x such that P holds, or None if there   *)
 (*                     is no such x.                                          *)
 (*     [pick x : T] == Some x with x : T, provided T is nonempty, else None.  *)
 (*    [pick x in A] == Some x, with x \in A, or None if A is empty.           *)
-(* [pick x in A | P] == Some x, with x \in A s.t. P holds, else None.         *)
+(* [pick x in A | P] == Some x, with x \in A such that P holds, else None.    *)
 (*   [pick x | P & Q] := [pick x | P & Q].                                    *)
 (* [pick x in A | P & Q] := [pick x | P & Q].                                 *)
 (* and (un)typed variants [pick x : T | P], [pick x : T in A], [pick x], etc. *)