Cleanup in Import

math-comp · Sep 12, 2015 · 75e83ab · 75e83ab
1 parent 1685a40
commit 75e83ab
Show file tree

Hide file tree

Showing 15 changed files with 27 additions and 50 deletions.
diff --git a/LRrule/Erdos_Szekeres.v b/LRrule/Erdos_Szekeres.v
@@ -15,7 +15,7 @@
 Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq fintype.
 Require Import tuple finfun finset bigop path.
 
-Require Import partition Schensted ordtype Greene Greene_inv stdplact.
+Require Import partition tableau Schensted ordtype Greene Greene_inv stdplact.
 
 Set Implicit Arguments.
 Unset Strict Implicit.

diff --git a/LRrule/Greene.v b/LRrule/Greene.v
@@ -14,7 +14,8 @@
 (******************************************************************************)
 Require Import ssreflect ssrbool ssrfun ssrnat eqtype finfun fintype choice seq tuple.
 Require Import finset perm tuple path bigop.
-Require Import tools subseq partition ordtype Schensted congr plactic ordcast.
+Require Import sorted tools subseq partition ordtype tableau.
+Require Import Schensted congr plactic ordcast.
 
 
 Set Implicit Arguments.
@@ -746,7 +747,6 @@ Proof.
     by rewrite rev_ordK.
 Qed.
 
-Require Import sorted.
 
 Lemma ksupp_inj_rev (leT : rel Alph) u k : ksupp_inj leT (fun y x => leT x y) k u (rev u).
 Proof.

diff --git a/LRrule/Greene_inv.v b/LRrule/Greene_inv.v
@@ -14,8 +14,8 @@
 (******************************************************************************)
 Require Import ssreflect ssrbool ssrfun ssrnat eqtype finfun fintype choice seq tuple.
 Require Import finset perm tuple path bigop.
-Require Import tools subseq partition Yamanouchi ordtype.
-Require Import Schensted congr plactic ordcast Greene.
+Require Import tools ordcast ordtype subseq partition tableau Yamanouchi stdtab.
+Require Import Schensted congr plactic Greene.
 
 Set Implicit Arguments.
 Unset Strict Implicit.
@@ -1544,8 +1544,6 @@ Proof.
 Qed.
 
 
-Require Import stdtab plactic.
-
 Section Rev.
 
 Variable T : ordType.

diff --git a/LRrule/Schensted.v b/LRrule/Schensted.v
@@ -13,9 +13,8 @@
 (*                  http://www.gnu.org/licenses/                              *)
 (******************************************************************************)
 Require Import ssreflect ssrbool ssrfun ssrnat eqtype fintype choice seq.
-Require Import path.
-Require Import tools partition Yamanouchi ordtype subseq.
-Require Export tableau.
+Require Import path bigop finset perm fingroup.
+Require Import tools partition Yamanouchi ordtype subseq tableau std stdtab.
 
 Set Implicit Arguments.
 Unset Strict Implicit.
@@ -397,8 +396,6 @@ Section Schensted.
 
 End Schensted.
 
-Require Import bigop.
-
 Theorem Sch_max_size w : size (Sch w) = \max_(s : subseqs w | is_row s) size s.
 Proof.
   apply/eqP; rewrite eqn_leq; apply/andP; split.
@@ -1223,9 +1220,6 @@ End Classes.
 End NonEmpty.
 
 
-Require Import finset perm fingroup.
-Require Import std stdtab.
-
 Lemma RSperm n (p : 'S_n) : is_stdtab (RS (wordperm p)).
 Proof.
   rewrite /is_stdtab; apply/andP; split; first by apply: is_tableau_RS.

diff --git a/LRrule/Schur.v b/LRrule/Schur.v
@@ -16,8 +16,8 @@ Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq fintype.
 Require Import tuple finfun finset bigop ssralg.
 Require Import poly.
 
-Require Import tools ordtype partition Yamanouchi std stdtab.
-Require Import Schensted stdplact Yam_plact Greene_inv shuffle.
+Require Import tools ordtype partition Yamanouchi std tableau stdtab.
+Require Import Schensted congr plactic stdplact Yam_plact Greene_inv shuffle.
 
 (******************************************************************************)
 (* The main goal of this file is to lift the multiplication of multivariate   *)
@@ -450,8 +450,6 @@ Proof.
   by rewrite unfold_in inE.
 Qed.
 
-Require Import plactic congr Yam_plact.
-
 Lemma size_RSmapinv2_yam d (Typ : ordType) (tab : seq (seq Typ)) (T : stdtabn d) :
   size (RSmapinv2 (tab, yam_of_stdtab T)) = d.
 Proof.

diff --git a/LRrule/Yam_plact.v b/LRrule/Yam_plact.v
@@ -15,7 +15,7 @@
 Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq fintype.
 Require Import tuple finfun finset path bigop.
 
-Require Import tools partition Yamanouchi ordtype std stdtab.
+Require Import tools partition Yamanouchi ordtype std tableau stdtab.
 Require Import Schensted congr plactic Greene_inv stdplact.
 
 Set Implicit Arguments.

diff --git a/LRrule/combclass.v b/LRrule/combclass.v
@@ -13,9 +13,7 @@
 (*                  http://www.gnu.org/licenses/                              *)
 (******************************************************************************)
 Require Import ssreflect ssrbool ssrfun ssrnat eqtype fintype choice seq.
-Require Import bigop.
-
-Require Import tools.
+Require Import bigop tools.
 
 Set Implicit Arguments.
 Unset Strict Implicit.

diff --git a/LRrule/congr.v b/LRrule/congr.v
@@ -13,8 +13,12 @@
 (*                  http://www.gnu.org/licenses/                              *)
 (******************************************************************************)
 Require Import ssreflect ssrbool ssrfun ssrnat eqtype seq.
-Require Import path.
-Require Import permuted.
+Require Import Recdef path.
+Require Import permuted vectNK.
+
+
+Set Implicit Arguments.
+Unset Strict Implicit.
 
 (******************************************************************************)
 (* Equivalence and congruence closure of a rewriting rule on words            *)
@@ -44,9 +48,6 @@ Require Import permuted.
 (*                  preserved along the rewriting rule holds for classes.     *)
 (******************************************************************************)
 
-Set Implicit Arguments.
-Unset Strict Implicit.
-
 (* Basic facts on congruences:                                                *)
 (* equivalence of various definitions and immediate consequences              *)
 Section CongruenceFacts.
@@ -118,8 +119,6 @@ End FullKnown.
 Variable bound : nat.
 Hypothesis Hbound: forall s : seq T, all invar s -> uniq s -> size s <= bound.
 
-Require Import Recdef.
-
 Lemma invar_undupE s : all invar (undup s) = all invar s.
 Proof.
   apply/(sameP idP); apply(iffP idP); move/allP => H; apply/allP => x Hx; apply: H;
@@ -392,7 +391,6 @@ Proof. by rewrite /congr /congr_class /rtrans. Qed.
 
 End CongruenceClosure.
 
-Require Import vectNK.
 
 Section CongruenceRule.
 

diff --git a/LRrule/plactic.v b/LRrule/plactic.v
@@ -13,8 +13,8 @@
 (*                  http://www.gnu.org/licenses/                              *)
 (******************************************************************************)
 Require Import ssreflect ssrbool ssrfun ssrnat eqtype finfun fintype choice seq tuple.
-Require Import finset perm.
-Require Import tools partition ordtype Schensted congr.
+Require Import finset perm path.
+Require Import tools partition ordtype tableau Schensted congr.
 
 
 Set Implicit Arguments.
@@ -204,8 +204,6 @@ Variable Alph : ordType.
 Let word := seq Alph.
 Implicit Type u v w : word.
 
-Require Import path.
-
 Lemma plact_row u v : is_row u -> u =Pl v -> u = v.
 Proof.
   move=> Hrowu; move: v; apply: gencongr_ind => [//= |] x y1 z y2 Hu /plactruleP [].

diff --git a/LRrule/shuffle.v b/LRrule/shuffle.v
@@ -13,8 +13,8 @@
 (*                  http://www.gnu.org/licenses/                              *)
 (******************************************************************************)
 Require Import ssreflect ssrbool ssrfun ssrnat eqtype finfun fintype choice seq tuple.
-Require Import finset perm binomial.
-Require Import tools subseq partition Yamanouchi ordtype std stdtab.
+Require Import finset perm binomial bigop.
+Require Import tools vectNK subseq partition Yamanouchi ordtype std tableau stdtab.
 Require Import Schensted plactic Greene_inv stdplact.
 
 
@@ -71,8 +71,6 @@ Proof.
 Qed.
 
 
-Require Import bigop vectNK.
-
 (* Tentative proof of associativity of shuffle *)
 
 Lemma shuffle_perm_eq u l1 l2 :

diff --git a/LRrule/stdplact.v b/LRrule/stdplact.v
@@ -15,7 +15,7 @@
 Require Import ssreflect ssrbool ssrfun ssrnat eqtype finfun fintype choice seq tuple.
 Require Import finset perm fingroup path.
 
-Require Import tools combclass ordcast partition Yamanouchi ordtype permuted std stdtab.
+Require Import tools combclass ordcast partition Yamanouchi ordtype std tableau stdtab.
 Require Import Schensted congr plactic Greene Greene_inv.
 
 Set Implicit Arguments.

diff --git a/LRrule/stdtab.v b/LRrule/stdtab.v
@@ -14,7 +14,7 @@
 (******************************************************************************)
 Require Import ssreflect ssrbool ssrfun ssrnat eqtype finfun fintype choice seq tuple.
 Require Import finset perm fingroup.
-Require Import tools combclass shape partition Yamanouchi permuted ordtype std tableau.
+Require Import tools combclass shape partition Yamanouchi ordtype std tableau.
 
 Import OrdNotations.
 

diff --git a/LRrule/subseq.v b/LRrule/subseq.v
@@ -13,6 +13,7 @@
 (*                  http://www.gnu.org/licenses/                              *)
 (******************************************************************************)
 Require Import ssreflect ssrbool ssrfun ssrnat eqtype choice fintype seq.
+Require Import path.
 Require Import tools combclass.
 
 Set Implicit Arguments.
@@ -156,8 +157,6 @@ Proof. case: s => s Ps /=; by apply: size_subseq. Qed.
 End Fintype.
 
 
-Require Import path.
-
 Lemma sorted_subseq_iota_rcons s n : subseq s (iota 0 n) = sorted ltn (rcons s n).
 Proof.
   apply (sameP idP); apply (iffP idP).

diff --git a/LRrule/tableau.v b/LRrule/tableau.v
@@ -13,7 +13,7 @@
 (*                  http://www.gnu.org/licenses/                              *)
 (******************************************************************************)
 Require Import ssreflect ssrbool ssrfun ssrnat eqtype fintype choice seq.
-Require Import path.
+Require Import path sorted.
 Require Import tools shape partition ordtype sorted.
 
 Set Implicit Arguments.
@@ -242,8 +242,6 @@ Section Tableau.
     apply/eqP; by apply (eq_from_nth (x0 := [::]) Hsz) => i _.
   Qed.
 
-  Require Import path sorted.
-
   Lemma is_tableau_sorted_dominate (t : seq (seq T)) :
     is_tableau t =
     [&& is_part (shape t), all (sorted (@leqX_op T)) t & sorted (fun x y => dominate y x) t].

diff --git a/LRrule/therule.v b/LRrule/therule.v
@@ -13,9 +13,9 @@
 (*                  http://www.gnu.org/licenses/                              *)
 (******************************************************************************)
 Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq fintype.
-Require Import tuple finfun finset bigop path.
+Require Import tuple finfun finset bigop path ssralg.
 
-Require Import tools ordcast combclass partition Yamanouchi ordtype std stdtab.
+Require Import tools ordcast combclass partition Yamanouchi ordtype std tableau stdtab.
 Require Import Schensted congr plactic Greene_inv stdplact Yam_plact skewtab.
 Require Import shuffle Schur.
 
@@ -527,8 +527,6 @@ Proof.
 Qed.
 
 
-Require Import ssralg.
-
 Local Open Scope ring_scope.
 Import GRing.Theory.