From 49eae56db439958b9c107c739dbbd1ffccc9e54e Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 13 Dec 2015 13:40:54 -0800
Subject: [PATCH] test(library/theories/group_theory): test auto-include in the
 group theory library

---
 library/algebra/group.lean                 | 29 +++++++---------
 library/theories/group_theory/action.lean  | 40 ++++++----------------
 library/theories/group_theory/finsubg.lean | 16 +++------
 library/theories/group_theory/perm.lean    | 15 +++-----
 4 files changed, 31 insertions(+), 69 deletions(-)

diff --git a/library/algebra/group.lean b/library/algebra/group.lean
index 183a4c660..21d01781a 100644
--- a/library/algebra/group.lean
+++ b/library/algebra/group.lean
@@ -129,8 +129,7 @@ definition add_comm_monoid.to_comm_monoid {A : Type} [add_comm_monoid A] : comm_
 ⦄
 
 section add_comm_monoid
-  variables [s : add_comm_monoid A]
-  include s
+  variables [add_comm_monoid A]
 
   theorem add_comm_three  (a b c : A) : a + b + c = c + b + a :=
     by rewrite [{a + _}add.comm, {_ + c}add.comm, -*add.assoc]
@@ -147,9 +146,7 @@ structure group [class] (A : Type) extends monoid A, has_inv A :=
 -- Note: with more work, we could derive the axiom one_mul
 
 section group
-
-  variable [s : group A]
-  include s
+  variable [group A]
 
   theorem mul.left_inv (a : A) : a⁻¹ * a = 1 := !group.mul_left_inv
 
@@ -306,19 +303,18 @@ section group
       x*y ∘c c = x ∘c y ∘c c : conj_compose
       ... = x ∘c b : Py
       ... = a : Px)
-
-  definition group.to_left_cancel_semigroup [trans_instance] [reducible] :
-    left_cancel_semigroup A :=
-  ⦃ left_cancel_semigroup, s,
-    mul_left_cancel := @mul_left_cancel A s ⦄
-
-  definition group.to_right_cancel_semigroup [trans_instance] [reducible] :
-    right_cancel_semigroup A :=
-  ⦃ right_cancel_semigroup, s,
-    mul_right_cancel := @mul_right_cancel A s ⦄
-
 end group
 
+definition group.to_left_cancel_semigroup [trans_instance] [reducible] [s : group A] :
+    left_cancel_semigroup A :=
+⦃ left_cancel_semigroup, s,
+  mul_left_cancel := @mul_left_cancel A s ⦄
+
+definition group.to_right_cancel_semigroup [trans_instance] [reducible] [s : group A] :
+    right_cancel_semigroup A :=
+⦃ right_cancel_semigroup, s,
+  mul_right_cancel := @mul_right_cancel A s ⦄
+
 structure comm_group [class] (A : Type) extends group A, comm_monoid A
 
 /- additive group -/
@@ -332,7 +328,6 @@ definition add_group.to_group {A : Type} [add_group A] : group A :=
 
 
 section add_group
-
   variables [s : add_group A]
   include s
 
diff --git a/library/theories/group_theory/action.lean b/library/theories/group_theory/action.lean
index 36deaf31d..cf67ea627 100644
--- a/library/theories/group_theory/action.lean
+++ b/library/theories/group_theory/action.lean
@@ -15,13 +15,12 @@ private lemma and_left_true {a b : Prop} (Pa : a) : a ∧ b ↔ b :=
 by rewrite [iff_true_intro Pa, true_and]
 
 section def
-variables {G S : Type} [ambientG : group G] [finS : fintype S] [deceqS : decidable_eq S]
-include ambientG finS
+variables {G S : Type} [group G] [fintype S]
 
 definition is_fixed_point (hom : G → perm S) (H : finset G) (a : S) : Prop :=
 ∀ h, h ∈ H → hom h a = a
 
-include deceqS
+variables [decidable_eq S]
 
 definition orbit (hom : G → perm S) (H : finset G) (a : S) : finset S :=
            image (move_by a) (image hom H)
@@ -29,8 +28,7 @@ definition orbit (hom : G → perm S) (H : finset G) (a : S) : finset S :=
 definition fixed_points [reducible] (hom : G → perm S) (H : finset G) : finset S :=
 {a ∈ univ | orbit hom H a = singleton a}
 
-variable [deceqG : decidable_eq G]
-include deceqG -- required by {x ∈ H |p x} filtering
+variable [decidable_eq G] -- required by {x ∈ H |p x} filtering
 
 definition moverset (hom : G → perm S) (H : finset G) (a b : S) : finset G :=
            {f ∈ H | hom f a = b}
@@ -42,13 +40,7 @@ end def
 
 section orbit_stabilizer
 
-variables {G S : Type}
-variable [ambientG : group G]
-include ambientG
-variable [finS : fintype S]
-include finS
-variable [deceqS : decidable_eq S]
-include deceqS
+variables {G S : Type} [group G] [fintype S] [decidable_eq S]
 
 section
 
@@ -108,8 +100,7 @@ by rewrite [fixed_points_of_one]
 
 end
 
-variable [deceqG : decidable_eq G]
-include deceqG
+variable [decidable_eq G]
 
 -- these are already specified by stab hom H a
 variables {hom : G → perm S} {H : finset G} {a : S}
@@ -152,8 +143,7 @@ lemma moverset_inj_on_orbit : set.inj_on (moverset hom H a) (ts (orbit hom H a))
         apply of_mem_sep Ph1b1
       end
 
-variable [subgH : is_finsubg H]
-include subgH
+variable [is_finsubg H]
 
 lemma subg_stab_of_move {h g : G} :
       h ∈ H → g ∈ moverset hom H a (hom h a) → h⁻¹*g ∈ stab hom H a :=
@@ -244,7 +234,7 @@ lemma subg_moversets_of_orbit_eq_stab_lcosets :
       existsi h, subst Pb₂, assumption
       end)
       (assume Pr, obtain h Ph₁ Ph₂, from exists_of_mem_image Pr,
-      obtain b Pb, from @subg_lcoset_of_stab_is_moverset_of_orbit G S ambientG finS deceqS deceqG hom H a Hom subgH h Ph₁, begin
+      obtain b Pb, from @subg_lcoset_of_stab_is_moverset_of_orbit G S _ _ _ _ hom H a Hom _ h Ph₁, begin
       rewrite [mem_image_eq],
       existsi b, subst Ph₂, assumption
       end))
@@ -260,9 +250,7 @@ end orbit_stabilizer
 
 section orbit_partition
 
-variables {G S : Type} [ambientG : group G] [finS : fintype S]
-variables [deceqS : decidable_eq S]
-include ambientG finS deceqS
+variables {G S : Type} [group G] [fintype S] [decidable_eq S]
 variables {hom : G → perm S} [Hom : is_hom_class hom] {H : finset G} [subgH : is_finsubg H]
 include Hom subgH
 
@@ -377,17 +365,12 @@ calc card S = Sum (orbits hom H) finset.card
 end orbit_partition
 
 section cayley
-variables {G : Type}
-variable [ambientG : group G]
-include ambientG
-variable [finG : fintype G]
-include finG
+variables {G : Type} [group G] [fintype G]
 
 definition action_by_lmul : G → perm G :=
 take g, perm.mk (lmul_by g) (lmul_inj g)
 
-variable [deceqG : decidable_eq G]
-include deceqG
+variable [decidable_eq G]
 
 lemma action_by_lmul_hom : homomorphic (@action_by_lmul G _ _) :=
 take g₁ (g₂ : G), eq.symm (calc
@@ -411,8 +394,7 @@ end cayley
 section lcosets
 open fintype subtype
 
-variables {G : Type} [ambientG : group G] [finG : fintype G] [deceqG : decidable_eq G]
-include ambientG deceqG finG
+variables {G : Type} [group G] [fintype G] [decidable_eq G]
 
 variables H : finset G
 
diff --git a/library/theories/group_theory/finsubg.lean b/library/theories/group_theory/finsubg.lean
index b7f480d2c..e99aca437 100644
--- a/library/theories/group_theory/finsubg.lean
+++ b/library/theories/group_theory/finsubg.lean
@@ -18,9 +18,7 @@ open ops
 
 section subg
 -- we should be able to prove properties using finsets directly
-variable {G : Type}
-variable [ambientG : group G]
-include ambientG
+variables {G : Type} [group G]
 
 definition finset_mul_closed_on [reducible] (H : finset G) : Prop :=
            ∀ x y : G, x ∈ H → y ∈ H → x * y ∈ H
@@ -47,8 +45,7 @@ lemma finsubg_mul_closed (H : finset G) [h : is_finsubg H] {x y : G} : x ∈ H 
 lemma finsubg_has_inv (H : finset G) [h : is_finsubg H] {a : G} :  a ∈ H → a⁻¹ ∈ H :=
       @is_finsubg.has_inv G _ H h a
 
-variable [deceqG : decidable_eq G]
-include deceqG
+variable [decidable_eq G]
 
 definition finsubg_to_subg [instance] {H : finset G} [h : is_finsubg H]
          : is_subgroup (ts H) :=
@@ -72,11 +69,7 @@ section fin_lcoset
 
 open set
 
-variable {A : Type}
-variable [deceq : decidable_eq A]
-include deceq
-variable [s : group A]
-include s
+variables {A : Type} [decidable_eq A] [group A]
 
 definition fin_lcoset (H : finset A) (a : A) := finset.image (lmul_by a) H
 
@@ -195,8 +188,7 @@ end
 section lcoset_fintype
 open fintype list subtype
 
-variables {A : Type} [ambientA : group A] [finA : fintype A] [deceqA : decidable_eq A]
-include ambientA deceqA finA
+variables {A : Type} [group A] [fintype A] [decidable_eq A]
 
 variables G H : finset A
 
diff --git a/library/theories/group_theory/perm.lean b/library/theories/group_theory/perm.lean
index 28c370317..4ff686b6e 100644
--- a/library/theories/group_theory/perm.lean
+++ b/library/theories/group_theory/perm.lean
@@ -12,12 +12,8 @@ namespace group_theory
 open fintype
 
 section perm
-variable {A : Type}
-variable [finA : fintype A]
-include finA
-variable [deceqA : decidable_eq A]
-include deceqA
-variable {f : A → A}
+variables {A : Type} [fintype A] [decidable_eq A]
+variable  {f : A → A}
 
 lemma perm_surj : injective f → surjective f :=
       surj_of_inj_eq_card (eq.refl (card A))
@@ -44,9 +40,7 @@ structure perm (A : Type) [h : fintype A] : Type :=
 local attribute perm.f [coercion]
 
 section perm
-variable {A : Type}
-variable [finA : fintype A]
-include finA
+variables {A : Type} [fintype A]
 
 lemma eq_of_feq : ∀ {p₁ p₂ : perm A}, (perm.f p₁) = p₂ → p₁ = p₂
 | (perm.mk f₁ P₁) (perm.mk f₂ P₂) := assume (feq : f₁ = f₂), by congruence; assumption
@@ -62,8 +56,7 @@ lemma perm.f_mk {f : A → A} {Pinj : injective f} : perm.f (perm.mk f Pinj) = f
 
 definition move_by [reducible] (a : A) (f : perm A) : A := f a
 
-variable [deceqA : decidable_eq A]
-include deceqA
+variable [decidable_eq A]
 
 lemma perm.has_decidable_eq [instance] : decidable_eq (perm A) :=
       take f g,