group.lean

/-
Copyright (c) 2020. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Patrick Massot
-/
import tactic

/-!
# `group`

Normalizes expressions in the language of groups.

## Tags

group_theory
-/

lemma mul_gpow_neg_one {G : Type*} [group G] (a b : G) : (a*b)^(-(1:ℤ)) = b^(-(1:ℤ))*a^(-(1:ℤ)) :=
by simp only [mul_inv_rev, gpow_one, gpow_neg]

lemma gpow_trick {G : Type*} [group G] (a b : G) (n m : ℤ) : a*b^n*b^m = a*b^(n+m) :=
by rw [mul_assoc, ← gpow_add]

lemma mul_self_gpow {G : Type*} [group G] (b : G) (m : ℤ) : b*b^m = b^(m+1) :=
by { conv_lhs {congr, rw ← gpow_one b }, rw [← gpow_add, add_comm] }

lemma mul_gpow_self {G : Type*} [group G] (b : G) (m : ℤ) : b^m*b = b^(m+1) :=
by { conv_lhs {congr, skip, rw ← gpow_one b }, rw [← gpow_add, add_comm] }

lemma gpow_trick_one {G : Type*} [group G] (a b : G) (m : ℤ) : a*b*b^m = a*b^(m+1) :=
by rw [mul_assoc, mul_self_gpow]

lemma gpow_trick_one' {G : Type*} [group G] (a b : G) (n : ℤ) : a*b^n*b = a*b^(n+1) :=
by rw [mul_assoc, mul_gpow_self]

lemma gpow_trick_sub {G : Type*} [group G] (a b : G) (n m : ℤ) : a*b^n*b^(-m) = a*b^(n-m) :=
by rw [mul_assoc, ← gpow_add] ; refl

namespace tactic
open tactic.simp_arg_type tactic.interactive interactive

meta def aux_group₁ (locat : loc) : tactic unit :=
  simp_core {} skip tt [
  expr ``(mul_one),
  expr ``(one_mul),
  expr ``(sub_self),
  expr ``(add_neg_self),
  expr ``(neg_add_self),
  expr ``(neg_neg),
  expr ``(nat.sub_self),
  expr ``(int.coe_nat_add),
  expr ``(int.coe_nat_mul),
  expr ``(int.coe_nat_zero),
  expr ``(int.coe_nat_one),
  expr ``(int.coe_nat_bit0),
  expr ``(int.coe_nat_bit1),
  expr ``(int.mul_neg_eq_neg_mul_symm),
  expr ``(int.neg_mul_eq_neg_mul_symm),
  symm_expr ``(gpow_coe_nat),
  symm_expr ``(gpow_neg_one),
  symm_expr ``(gpow_mul),
  symm_expr ``(gpow_add_one),
  symm_expr ``(gpow_one_add),
  symm_expr ``(gpow_add),
  expr ``(mul_gpow_neg_one ),
  expr ``(gpow_zero),
  expr ``(mul_gpow),
  symm_expr ``(mul_assoc),
  expr ``(gpow_trick),
  expr ``(gpow_trick_one),
  expr ``(gpow_trick_one'),
  expr ``(gpow_trick_sub)]
  [] locat

meta def aux_group₂ (locat : loc) : tactic unit :=
ring none tactic.ring.normalize_mode.raw locat
end tactic

namespace tactic.interactive
setup_tactic_parser
open tactic

meta def group (locat : parse location) : tactic unit :=
do when locat.include_goal `[rw ← mul_inv_eq_one],
   repeat (aux_group₁ locat ; aux_group₂ locat),
   repeat (aux_group₂ locat ; aux_group₁ locat)
end tactic.interactive

example {G : Type} [group G] (a b c d : G) : c *(a*b)*(b⁻¹*a⁻¹)*c = c*c :=
by { group,  }

example {G : Type} [group G] (a b c d : G) : (b*c⁻¹)*c *(a*b)*(b⁻¹*a⁻¹)*c = b*c :=
by { group, }

example {G : Type} [group G] (a b c d : G) : c⁻¹*(b*c⁻¹)*c *(a*b)*(b⁻¹*a⁻¹*b⁻¹)*c = 1 :=
by {group, }


def commutator {G} [group G] : G → G → G := λ g h, g * h * g⁻¹ * h⁻¹

def commutator3 {G} [group G] : G → G → G → G := λ g h k, commutator (commutator g h) k

-- The following is known as the Hall-Witt identity, see e.g. https://en.wikipedia.org/wiki/Three_subgroups_lemma#Proof_and_the_Hall%E2%80%93Witt_identity
example {G} [group G] (g h k : G) : g * (commutator3 g⁻¹ h k) * g⁻¹ * k * (commutator3 k⁻¹ g h) * k⁻¹ * h * (commutator3 h⁻¹ k g) * h⁻¹ = 1 :=
by { dsimp [commutator3, commutator], group }

example {G : Type} [group G] (a : G) : a^2*a = a^3 :=
by group

example {G : Type} [group G] (n m : ℕ) (a : G) : a^n*a^m = a^(n+m) :=
by group

example {G : Type} [group G] (a b c d : G) : c *(a*b^2)*((b*b)⁻¹*a⁻¹)*c = c*c :=
by group

example {G : Type} [group G] (n m : ℕ) (a : G) : a^n*(a⁻¹)^n = 1 :=
by group

example {G : Type} [group G] (n m : ℕ) (a : G) : a^2*a⁻¹*a⁻¹ = 1 :=
by group

example {G : Type} [group G] (n m : ℕ) (a : G) : a^n*a^m = a^(m+n) :=
by group

example {G : Type} [group G] (n : ℕ) (a : G) : a^(n-n) = 1 :=
by group

example {G : Type} [group G] (n : ℤ) (a : G) : a^(n-n) = 1 :=
by group

example {G : Type} [group G] (n : ℤ) (a : G) (h : a^(n*(n+1)-n -n^2) = a) : a = 1 :=
begin
 group at h,
 exact h.symm,
 end

example {G : Type} [group G] (a b c d : G) (h : c = (a*b^2)*((b*b)⁻¹*a⁻¹)*d) : a*c*d⁻¹ = a :=
begin
  group at h,
  rw h,
  group,
end