free_group.lean

import data.list.basic data.quot algebra.group

universes u v

variables (α : Type u)

namespace free_group

inductive rel : list (α × bool) → list (α × bool) → Prop
| refl {L} : rel L L
| symm {L₁ L₂} : rel L₁ L₂ → rel L₂ L₁
| trans {L₁ L₂ L₃} : rel L₁ L₂ → rel L₂ L₃ → rel L₁ L₃
| append {L₁ L₂ L₃ L₄} : rel L₁ L₃ → rel L₂ L₄ → rel (L₁ ++ L₂) (L₃ ++ L₄)
| bnot {x b} : rel [(x, b), (x, bnot b)] []

instance setoid : setoid (list (α × bool)) :=
⟨rel α,
 λ L, rel.refl α,
 λ L₁ L₂, rel.symm,
 λ L₁ L₂ L₃, rel.trans⟩

end free_group

def free_group : Type u :=
quotient (free_group.setoid α)

namespace free_group

lemma reverse_map_bnot {L₁ L₂} (H : rel α L₁ L₂) :
  rel α (L₁.map $ λ (x : α × bool), (x.1, bnot x.2)).reverse
    (L₂.map $ λ (x : α × bool), (x.1, bnot x.2)).reverse :=
begin
  induction H with L1 L1 L2 H1 ih1 L1 L2 L3 H1 H2 ih1 ih2
    L1 L2 L3 L4 H1 H2 ih1 ih2 x b,
  case rel.refl
  { apply rel.refl },
  case rel.symm
  { apply rel.symm, assumption },
  case rel.trans
  { apply rel.trans, assumption, assumption },
  case rel.append
  { rw [list.map_append, list.map_append],
    rw [list.reverse_append, list.reverse_append],
    apply rel.append,
    assumption, assumption },
  case rel.bnot
  { dsimp [list.reverse, list.reverse_core],
    rw [bnot_bnot],
    apply rel.bnot }
end

lemma reverse_map_bnot_append {L : list (α × bool)} :
  (L.map $ λ (x : α × bool), (x.1, bnot x.2)).reverse ++ L ≈ list.nil :=
begin
  induction L with h t ih,
  case list.nil
  { refl },
  case list.cons
  { apply rel.trans _ ih,
    rw [list.map_cons, list.reverse_cons', list.append_assoc],
    apply rel.append,
    { apply rel.refl },
    { change rel α ([(h.fst, bnot (h.snd))] ++ [h] ++ t) ([] ++ t),
      apply rel.append,
      { cases h with x b,
        have H := @rel.bnot α x (bnot b),
        rwa bnot_bnot at H },
      { apply rel.refl } } }
end

instance group : group (free_group α) :=
{ mul := @quotient.lift₂ _ _ _ (free_group.setoid α) _ (λ L₁ L₂, ⟦L₁ ++ L₂⟧) $
    λ L₁ L₂ L₃ L₄ H13 H24, quotient.sound $ rel.append H13 H24,
  one := ⟦[]⟧,
  inv := @quotient.lift _ _ (free_group.setoid α) (λ L, ⟦(L.map $ λ (x : α × bool), (x.1, bnot x.2)).reverse⟧) $
    λ L₁ L₂ H, quotient.sound $ reverse_map_bnot α H,
  mul_assoc := λ x y z, quotient.induction_on₃ x y z $ λ m n p, quotient.sound $ by rw [list.append_assoc],
  one_mul := λ x, quotient.induction_on x $ λ L, quotient.sound $ by refl,
  mul_one := λ x, quotient.induction_on x $ λ L, quotient.sound $ by rw list.append_nil,
  mul_left_inv := λ x, quotient.induction_on x $ λ L, quotient.sound $
    reverse_map_bnot_append α }

def of_type : α → free_group α :=
λ x, ⟦[(x, tt)]⟧

section to_group

variables {α} {β : Type v} [group β] (f : α → β)

def to_group.aux : α × bool → β :=
λ x, bool.rec_on x.2 (f x.1)⁻¹ (f x.1)

def to_group : free_group α → β :=
λ x, quotient.lift_on x (λ L : list _, list.prod $ L.map $ to_group.aux f) $
begin
  intros L₁ L₂ H,
  induction H with L1 L1 L2 H1 ih1 L1 L2 L3 H1 H2 ih1 ih2
    L1 L2 L3 L4 H1 H2 ih1 ih2 x b,
  case rel.refl
  { refl },
  case rel.symm
  { symmetry, assumption },
  case rel.trans
  { transitivity, assumption, assumption },
  case rel.append
  { dsimp at ih1 ih2 ⊢,
    rw [list.map_append, list.map_append],
    rw [list.prod_append, list.prod_append],
    rw [ih1, ih2] },
  case rel.bnot
  { cases b;
    simp [to_group.aux, list.prod] }
end

instance to_group.is_group_hom : is_group_hom (to_group f) :=
λ x y, quotient.induction_on₂ x y $ λ L₁ L₂,
show to_group f (⟦L₁ ++ L₂⟧) = to_group f ⟦L₁⟧ * to_group f ⟦L₂⟧,
by simp [to_group]

theorem to_group.of_type (x) : to_group f (of_type α x) = f x :=
one_mul _

end to_group

end free_group