Merge pull request #1440 from Alizter/group_auto

auto for groups

theories/Algebra/Groups/Group.v

@@ -31,8 +31,8 @@ Arguments group_sgop {_}.
 Arguments group_unit {_}.
 Arguments group_inverse {_}.
 Arguments group_isgroup {_}.
-(** We never need to unfold the proof that something is a group *)
-Opaque group_isgroup.
+(** We should never need to unfold the proof that something is a group. *)
+Global Opaque group_isgroup.
 
 (** We coerce groups back to types. *)
 Coercion group_type : Group >-> Sortclass.
@@ -41,6 +41,33 @@ Global Existing Instances group_sgop group_unit group_inverse group_isgroup.
 Definition issig_group : _ <~> Group
   := ltac:(issig).
 
+(** * Proof automation *)
+(** Many times in group theoretic proofs we want some form of automation for obvious identities. Here we implement such a behaviour. *)
+
+(** We create a database of hints for the group theory library *)
+Create HintDb group_db.
+
+(** Our group laws can be proven easily with tactics such as [rapply associativity]. However this requires a typeclass search on more general algebraic structures. Therefore we explicitly list many groups laws here so that coq can use them. We also create hints for each law in our groups database. *)
+Local Definition grp_law_associativity {G : Group} (x y z : G) := associativity x y z.
+#[export] Hint Immediate grp_law_associativity : group_db.
+Local Definition grp_law_left_identity {G : Group} (x : G) := left_identity x.
+#[export] Hint Immediate grp_law_left_identity : group_db.
+Local Definition grp_law_right_identity {G : Group} (x : G) := right_identity x.
+#[export] Hint Immediate grp_law_right_identity : group_db.
+Local Definition grp_law_left_inverse {G : Group} (x : G) := left_inverse x.
+#[export] Hint Immediate grp_law_left_inverse : group_db.
+Local Definition grp_law_right_inverse {G : Group} (x : G) := right_inverse x.
+#[export] Hint Immediate grp_law_right_inverse : group_db.
+
+(** Given path types in a product we may want to decompose. *)
+#[export] Hint Extern 5 (@paths (_ * _) _ _) => (rapply path_prod) : group_db.
+(** Given path types in a sigma type of a hprop family (i.e. a subset) we may want to decompose. *)
+#[export] Hint Extern 6 (@paths (sig _) _ _) => (rapply path_sigma_hprop) : group_db.
+
+(** We also declare a tactic (notation) for automatically solving group laws *)
+(** TODO: improve this tactic so that it also rewrites and is able to solve basic group lemmas. *)
+Tactic Notation "grp_auto" := hnf; intros; eauto with group_db.
+
 (** Groups are pointed sets with point the identity. *)
 Global Instance ispointed_group (G : Group)
   : IsPointed G := @mon_unit G _.
@@ -196,13 +223,15 @@ Definition grp_homo_unit {G H} (f : GroupHomomorphism G H)
 Proof.
   apply monmor_unitmor.
 Defined.
+#[export] Hint Immediate grp_homo_unit : group_db.
 
 (** Group homomorphisms preserve group operations *)
 Definition grp_homo_op {G H} (f : GroupHomomorphism G H)
   : forall x y : G, f (x * y) = f x * f y.
 Proof.
   apply monmor_sgmor.
 Defined.
+#[export] Hint Immediate grp_homo_op : group_db.
 
 (** Group homomorphisms preserve inverses *)
 Definition grp_homo_inv {G H} (f : GroupHomomorphism G H)
@@ -216,6 +245,7 @@ Proof.
     apply left_inverse.
   + apply right_inverse.
 Defined.
+#[export] Hint Immediate grp_homo_inv : group_db.
 
 (** When building a group homomorphism we only need that it preserves the group operation, since we can prove that the identity is preserved. *)
 Definition Build_GroupHomomorphism {G H : Group}
@@ -471,32 +501,9 @@ Proof.
   (** Inverse *)
   { intros [g h].
     exact (-g, -h). }
-  (** Group laws *)
-  srapply Build_IsGroup.
-  (** Monoid laws *)
-  { srapply Build_IsMonoid.
-    (** Semigroup lawss *)
-    { srapply Build_IsSemiGroup.
-      (** Associativity *)
-      intros [g1 h1] [g2 h2] [g3 h3].
-      apply path_prod; cbn.
-      1,2: apply associativity. }
-    (** Left identity *)
-    { intros [g h].
-      apply path_prod; cbn.
-      1,2: apply left_identity. }
-    (** Right identity *)
-    { intros [g h].
-      apply path_prod; cbn.
-      1,2: apply right_identity. } }
-  (** Left inverse *)
-  { intros [g h].
-    apply path_prod; cbn.
-    1,2: apply left_inverse. }
-  (** Right inverse *)
-  { intros [g h].
-    apply path_prod; cbn.
-    1,2: apply right_inverse. }
+  repeat split.
+  1: exact _.
+  all: grp_auto.
 Defined.
 
 Proposition grp_prod_corec {G H K : Group}