-- The free group on two generators as a structure value: the reduced
-- words under the reduction of their concatenation, the generators freeA
-- and freeB, the reduced words starting with a given letter, and the
-- paradoxical decomposition of the free group into those sets
-- Part of Cumulus, the Grace17 mathematics library.
-- Copyright (c) 2026 Grant Passmore.
-- Released under the Apache License 2.0. See LICENSE in the repository root.
-- Authors: Grant Passmore

module Grace.Cumulus.Algebra.Group.FreeGroup
import Words
import Coset

-- The product of two reduced words reduces their concatenation, and the
-- inverse of a reduced word reduces its inverse word; both are graphs on
-- the reduced words.
defgraph freeMul (p ∈ reducedWords × reducedWords) : reducedWords :=
  reduce(concat(fst(p), snd(p)))
proof
  obtain ⟨bound, u, hu, v, hv, shape⟩ := product.membership.forward with member
  have listU := reducedWords.list with hu
  have listV := reducedWords.list with hv
  rw [shape, fst.pair, snd.pair]
  exact reduce.mem with *

defgraph freeInv (w ∈ reducedWords) : reducedWords := reduce(inverseWord(w))
proof
  have list := reducedWords.list with member
  have inverse := inverseWord.closed with list
  exact reduce.mem with inverse

-- The free group on the two generators freeA = [0] and freeB = [2].
def freeGroup : Set := Group.mk(reducedWords, freeMul, [], freeInv)
def freeA : Set := 0 :: []
def freeB : Set := 2 :: []

-- The reduced words whose first letter is ℓ.
def startsWith (ℓ : Set) : Set := { w ∈ reducedWords | ∃ u, w = ℓ :: u }

theorem freeGroup.carrierOf
  shows Group.carrier(freeGroup) = reducedWords
proof
  simp [freeGroup, Group.mk.carrier]

theorem freeGroup.operation
  shows Group.mul(freeGroup) = freeMul
proof
  simp [freeGroup, Group.mk.mul]

theorem freeGroup.unit
  shows Group.one(freeGroup) = []
proof
  simp [freeGroup, Group.mk.one]

theorem freeGroup.inverse
  shows Group.inv(freeGroup) = freeInv
proof
  simp [freeGroup, Group.mk.inv]

-- The product and the inverse on reduced words.
theorem freeMul.apply (u v : Set)
  requires hu : u ∈ reducedWords
  requires hv : v ∈ reducedWords
  shows freeMul(u, v) = reduce(concat(u, v))
proof
  have pair := product.pair at u, v, reducedWords, reducedWords with *
  have value := freeMul.value at (u, v) with pair
  simp [call2]
  rw [fst.pair, snd.pair]
  rfl

theorem freeMul.mem (u v : Set)
  requires hu : u ∈ reducedWords
  requires hv : v ∈ reducedWords
  shows freeMul(u, v) ∈ reducedWords
proof
  have listU := reducedWords.list with hu
  have listV := reducedWords.list with hv
  rw freeMul.apply
  exact reduce.mem with *

theorem freeInv.apply (w : Set)
  requires hw : w ∈ reducedWords
  shows freeInv(w) = reduce(inverseWord(w))
proof
  exact freeInv.value at w with hw

theorem freeInv.mem (w : Set)
  requires hw : w ∈ reducedWords
  shows freeInv(w) ∈ reducedWords
proof
  have list := reducedWords.list with hw
  have inverse := inverseWord.closed with list
  rw freeInv.apply
  exact reduce.mem with inverse

-- The free group is a group.
theorem freeGroup.group
  shows Group(freeGroup)
proof
  have mulFunction := freeMul.function
  have invFunction := freeInv.function
  have unitIn := reducedWords.nil_mem
  unfold freeGroup
  apply Group.intro with mulFunction, unitIn, invFunction
  . intros a ha b hb c hc
    have listA := reducedWords.list with ha
    have listB := reducedWords.list with hb
    have listC := reducedWords.list with hc
    have abIn := freeMul.mem with ha, hb
    have bcIn := freeMul.mem with hb, hc
    have ab := freeMul.apply with ha, hb
    have bc := freeMul.apply with hb, hc
    have left := freeMul.apply with abIn, hc
    have right := freeMul.apply with ha, bcIn
    have leftLaw := reduce.concat_left at concat(a, b), c with *
    have rightLaw := reduce.concat_right at a, concat(b, c) with *
    have assoc := concat.associative at a, b, c with *
    rw [left, right, ab, bc, ← leftLaw, ← rightLaw, assoc]
    rfl
  . intros a ha
    have listA := reducedWords.list with ha
    have value := freeMul.apply with unitIn, ha
    rw [value, concat.nil_left]
    exact reducedWords.fixed with ha
  . intros a ha
    have listA := reducedWords.list with ha
    have value := freeMul.apply with ha, unitIn
    rw [value, concat.nil_right]
    exact reducedWords.fixed with ha
  . intros a ha
    have listA := reducedWords.list with ha
    have invIn := freeInv.mem with ha
    have value := freeMul.apply with invIn, ha
    have invValue := freeInv.apply with ha
    have law := reduce.concat_left at inverseWord(a), a with *
    rw [value, invValue, ← law]
    exact reduce.inverse_left with listA
  . intros a ha
    have listA := reducedWords.list with ha
    have invIn := freeInv.mem with ha
    have value := freeMul.apply with ha, invIn
    have invValue := freeInv.apply with ha
    have law := reduce.concat_right at a, inverseWord(a) with *
    rw [value, invValue, ← law]
    exact reduce.inverse_right with listA

theorem freeA.mem
  shows freeA ∈ reducedWords
proof
  have letter := letter.zero_mem
  have reduced := Reduced.singleton with letter
  have list : List(4, 0 :: []) by typecheck
  unfold freeA
  exact reducedWords.of_reduced with list, reduced

theorem freeB.mem
  shows freeB ∈ reducedWords
proof
  have letter := letter.two_mem
  have reduced := Reduced.singleton with letter
  have list : List(4, 2 :: []) by typecheck
  unfold freeB
  exact reducedWords.of_reduced with list, reduced

-- Multiplying by a single letter pushes it onto the word.
theorem freeMul.letter (ℓ w : Set)
  requires hℓ : ℓ ∈ 4
  requires hw : w ∈ reducedWords
  shows freeMul(ℓ :: [], w) = pushLetter(ℓ, w)
proof
  have list := reducedWords.list with hw
  have single : List(4, ℓ :: []) by typecheck
  have singleIn := reducedWords.of_reduced with single, (Reduced.singleton with hℓ)
  have value := freeMul.apply with singleIn, hw
  have fixed := reducedWords.fixed with hw
  rw [value, concat.singleton, reduce.cons, fixed]
  rfl

-- The words starting with a letter.
theorem startsWith.subset (ℓ : Set)
  shows startsWith(ℓ) ⊆ reducedWords
proof
  intros w hw
  have parts := startsWith.membership.forward with hw
  exact parts.left

theorem startsWith.of_reduced (ℓ : Set) (u : List(4))
  requires hℓ : ℓ ∈ 4
  requires reduced : Reduced(ℓ :: u)
  shows ℓ :: u ∈ startsWith(ℓ)
proof
  have list : List(4, ℓ :: u) by typecheck
  have member := reducedWords.of_reduced with list, reduced
  exact startsWith.membership.backward with ⟨member, u, rfl⟩

theorem startsWith.nil_not_mem (ℓ : Set)
  shows ¬([] ∈ startsWith(ℓ))
proof
  intro member
  obtain ⟨bound, u, equal⟩ := startsWith.membership.forward with member
  have distinct := List.inductive.disjoint.nil.cons at ℓ, u
  exact distinct with equal

theorem startsWith.head (ℓ m : Set) (u : List(4))
  requires hℓ : ℓ ∈ 4
  requires hm : m ∈ 4
  requires member : m :: u ∈ startsWith(ℓ)
  shows m = ℓ
proof
  obtain ⟨bound, v, equal⟩ := startsWith.membership.forward with member
  have both := List.inductive.injective.cons with equal
  exact both.left

theorem startsWith.disjoint (ℓ m : Set)
  requires hℓ : ℓ ∈ 4
  requires hm : m ∈ 4
  requires different : ℓ ≠ m
  shows Disjoint(startsWith(ℓ), startsWith(m))
proof
  apply Disjoint.iff.backward
  intros w hwℓ hwm
  obtain ⟨boundℓ, u, equalℓ⟩ := startsWith.membership.forward with hwℓ
  obtain ⟨boundm, v, equalm⟩ := startsWith.membership.forward with hwm
  have same : ℓ :: u = m :: v by cc
  have both := List.inductive.injective.cons with same
  exact different with both.left

-- Every reduced word is empty or starts with one of the four letters.
theorem reducedWords.cases (w : Set)
  requires hw : w ∈ reducedWords
  shows w = [] ∨ ∃ ℓ ∈ 4, w ∈ startsWith(ℓ)
proof
  have list := reducedWords.list with hw
  have shape := List.cases with list
  cases shape with nil | cons
  . left
    exact nil
  . right
    obtain ⟨ℓ, hℓ, u, tailList, equal⟩ := cons
    rw equal at hw
    refine ⟨ℓ, hℓ, ?_⟩
    rw equal
    exact startsWith.membership.backward with ⟨hw, u, rfl⟩

-- The five pieces: the empty word and the words starting with each letter.
theorem reducedWords.decomposition
  shows reducedWords =
    {[]} ∪ startsWith(0) ∪ startsWith(1) ∪ startsWith(2) ∪ startsWith(3)
proof
  ext w
  constructor
  . intro hw
    have split := reducedWords.cases with hw
    cases split with nil | cons
    . rw nil
      simp [union2.membership, singleton.membership]
    . obtain ⟨ℓ, hℓ, member⟩ := cons
      have letters := letter.cases with hℓ
      rcases letters with zero | one | two | three
      . rw zero at member
        simp [union2.membership, member]
      . rw one at member
        simp [union2.membership, member]
      . rw two at member
        simp [union2.membership, member]
      . rw three at member
        simp [union2.membership, member]
  . intro hw
    have nilSubset : {[]} ⊆ reducedWords
      intros z hz
      have equal := singleton.membership.forward with hz
      rw equal
      exact reducedWords.nil_mem
    have first := union2.subset with nilSubset, (startsWith.subset at 0)
    have second := union2.subset with first, (startsWith.subset at 1)
    have third := union2.subset with second, (startsWith.subset at 2)
    have fourth := union2.subset with third, (startsWith.subset at 3)
    exact fourth with w, hw

-- Translating the words starting with the inverse of ℓ by the letter ℓ
-- gives exactly the reduced words not starting with ℓ.
theorem leftCoset.letter (ℓ m : Set)
  requires hℓ : ℓ ∈ 4
  requires hm : m ∈ 4
  requires inverse : m = inverseLetter(ℓ)
  shows leftCoset(freeGroup, ℓ :: [], startsWith(m)) = reducedWords ∖ startsWith(ℓ)
proof
  have cancel : cancels(ℓ, m) = Bool.true
    rw inverse
    exact cancels.self_inverse with hℓ
  have cancelBack : cancels(m, ℓ) = Bool.true
    rw inverse
    exact cancels.inverse_self with hℓ
  ext w
  constructor
  . intro hw
    obtain ⟨bound, h, hh, equal⟩ := leftCoset.membership.forward with hw
    rw freeGroup.operation at equal
    have hIn := startsWith.subset at m with h, hh
    obtain ⟨boundH, u, hShape⟩ := startsWith.membership.forward with hh
    have listH := reducedWords.list with hIn
    rw hShape at listH
    have tailList := List.tail_list with listH
    have reducedH := reducedWords.reduced with hIn
    rw hShape at reducedH
    have reducedU := Reduced.tail with hm, reducedH
    have pushed := freeMul.letter with hℓ, hIn
    rw [hShape, pushLetter.cancel] at pushed
    rw [equal, hShape, pushed]
    apply difference.membership.backward
    constructor
    . exact reducedWords.of_reduced with tailList, reducedU
    . intro inLetter
      obtain ⟨boundU, v, uShape⟩ := startsWith.membership.forward with inLetter
      rw uShape at reducedH
      rw uShape at tailList
      have listV := List.tail_list with tailList
      have parts := Reduced.cons_cons.forward with hm, hℓ, reducedH
      have distinct := Bool.inductive.disjoint.false.true
      have mixed : Bool.false = Bool.true by cc
      exact distinct with mixed
  . intro hw
    obtain ⟨hwIn, notℓ⟩ := difference.membership.forward with hw
    have listW := reducedWords.list with hwIn
    have reducedW := reducedWords.reduced with hwIn
    have fits : fitsTest(m, w) = Bool.true
      have shape := List.cases with listW
      cases shape with nil | cons
      . rw nil
        exact fitsTest.nil with hm
      . obtain ⟨y, hy, ys, ysList, consShape⟩ := cons
        have headDifferent : y ≠ ℓ
          intro same
          apply notℓ
          rw [consShape, same]
          rw [consShape, same] at reducedW
          exact startsWith.of_reduced with hℓ, reducedW
        have keep : cancels(m, y) = Bool.false
          apply cancels.false_iff.backward with hm, hy
          rw inverse
          rw inverseLetter.involutive
          exact headDifferent
        have boolean := cancels.boolean at m, y
        rw [consShape, fitsTest.cons]
        exact not.true_iff.backward with boolean, keep
    have reducedH := Reduced.cons_iff.backward with hm, ⟨fits, reducedW⟩
    have hIn := startsWith.of_reduced with hm, reducedH
    have listH : List(4, m :: w) by typecheck
    have hCarrier := reducedWords.of_reduced with listH, reducedH
    have pushed := freeMul.letter with hℓ, hCarrier
    rw pushLetter.cancel at pushed
    apply leftCoset.membership.backward
    rw freeGroup.carrierOf
    refine ⟨hwIn, m :: w, hIn, ?_⟩
    rw freeGroup.operation
    symm
    exact pushed

-- The paradoxical decomposition of the free group: the words starting
-- with a together with the translate by a of the words starting with a⁻¹
-- exhaust the group, and likewise for b.
theorem freeGroup.decomposition_a
  shows startsWith(0) ∪ leftCoset(freeGroup, freeA, startsWith(1)) = reducedWords ∧
    Disjoint(startsWith(0), leftCoset(freeGroup, freeA, startsWith(1)))
proof
  have zero := letter.zero_mem
  have one := letter.one_mem
  have inverse : 1 = inverseLetter(0)
    symm
    exact inverseLetter.zero
  have translate := leftCoset.letter with zero, one, inverse
  have value : freeA = 0 :: [] by simp [freeA]
  rw [value, translate]
  constructor
  . exact difference.union2_of_subset with (startsWith.subset at 0)
  . have disjoint := difference.disjoint at reducedWords, startsWith(0)
    exact Disjoint.symmetric with disjoint

theorem freeGroup.decomposition_b
  shows startsWith(2) ∪ leftCoset(freeGroup, freeB, startsWith(3)) = reducedWords ∧
    Disjoint(startsWith(2), leftCoset(freeGroup, freeB, startsWith(3)))
proof
  have two := letter.two_mem
  have three := letter.three_mem
  have inverse : 3 = inverseLetter(2)
    symm
    exact inverseLetter.two
  have translate := leftCoset.letter with two, three, inverse
  have value : freeB = 2 :: [] by simp [freeB]
  rw [value, translate]
  constructor
  . exact difference.union2_of_subset with (startsWith.subset at 2)
  . have disjoint := difference.disjoint at reducedWords, startsWith(2)
    exact Disjoint.symmetric with disjoint