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.)
---
 mathcomp/solvable/primitive_action.v | 6 ++----
 1 file changed, 2 insertions(+), 4 deletions(-)

(limited to 'mathcomp/solvable')

diff --git a/mathcomp/solvable/primitive_action.v b/mathcomp/solvable/primitive_action.v
index fa27e75..73e397d 100644
--- a/mathcomp/solvable/primitive_action.v
+++ b/mathcomp/solvable/primitive_action.v
@@ -165,10 +165,8 @@ Definition ntransitive := [transitive A, on dtuple_on | to * n].
 Lemma dtuple_onP t :
   reflect (injective (tnth t) /\ forall i, tnth t i \in S) (t \in dtuple_on).
 Proof.
-rewrite inE subset_all -map_tnth_enum.
-case: (uniq _) / (injectiveP (tnth t)) => f_inj; last by right; case.
-rewrite -[all _ _]negbK -has_predC has_map has_predC negbK /=.
-by apply: (iffP allP) => [Sf|[]//]; split=> // i; rewrite Sf ?mem_enum.
+rewrite inE subset_all -forallb_tnth -[in uniq t]map_tnth_enum /=.
+by apply: (iffP andP) => -[/injectiveP-f_inj /forallP].
 Qed.
 
 Lemma n_act_dtuple t a :
-- 
cgit v1.2.3