-- Words over the four letters a, a⁻¹, b, b⁻¹ as lists over 4: the inverse
-- letter, reduced words with no adjacent inverse pair, the reduction that
-- cancels adjacent inverse pairs, the inverse of a word, the laws of
-- reduction under concatenation, and the set of all lists over a carrier
-- 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.Words
import List.Filter

-- The letters are 0, 1, 2, 3, read a, a⁻¹, b, b⁻¹; the inverse letter
-- swaps 0 with 1 and 2 with 3, and cancels(x, y) says y is the inverse
-- of x.
def evenTest (n : Nat) → Bool
  | zero => Bool.true
  | succ(k) => BoolOps.not(evenTest(k))

def inverseLetter (ℓ : Nat) → Nat
  | zero => 1
  | succ(k) => chooseNat(evenTest(k), k, succ(succ(k)))

def cancels (x y : Nat) : Bool := equalNat(y, inverseLetter(x))

-- fitsTest(x, w): x placed before w makes no adjacent inverse pair;
-- reducedTest(w): no two adjacent letters of w are inverse; Reduced(w)
-- is the latter as a property.
def fitsTest (x : Nat, w : List(4)) → Bool
  | x, [] => Bool.true
  | x, y :: ys => BoolOps.not(cancels(x, y))
  descends w

def reducedTest (w : List(4)) → Bool
  | [] => Bool.true
  | x :: xs => BoolOps.and(fitsTest(x, xs), reducedTest(xs))

predicate Reduced (w : Set) := reducedTest(w) = Bool.true

-- pushLetter(x, r) places x before the word r, cancelling it against the
-- first letter of r when the two are inverse; reduce(w) cancels every
-- adjacent inverse pair of w, working from the end of the word.
def pushLetter (x : Nat, r : List(4)) → Set
  | x, [] => x :: []
  | x, y :: ys => boolChoice(cancels(x, y), ys, x :: y :: ys)
  descends r

def reduce (w : List(4)) → Set
  | [] => []
  | x :: xs => pushLetter(x, reduce(xs))

-- Concatenation of words: concat(u, v) is u followed by v.
def concat (u v : Set) : Set := append{A := 4}(v, u)

-- The inverse of a word: the reversed word with every letter inverted.
def inverseWord (w : List(4)) → Set
  | [] => []
  | x :: xs => concat(inverseWord(xs), inverseLetter(x) :: [])

-- The set of all lists over A: the union over n of the lists of length n.
def consAll (A L : Set) : Set := { fst(p) :: snd(p) | p ∈ A × L }

def listsOfLength (A : Set, n : Nat) → Set
  | A, zero => {[]}
  | A, succ(k) => consAll(A, listsOfLength(A, k))

def listStages (A : Set) : Set := { listsOfLength(A, n) | n ∈ ℕ }
def listsOver (A : Set) : Set := ⋃(listStages(A))

-- The reduced words over the four letters.
def reducedWords : Set := { w ∈ listsOver(4) | Reduced(w) }

-- Letters.
theorem letter.natural (ℓ : Set)
  requires member : ℓ ∈ 4
  shows Nat(ℓ)
proof
  exact natural.member at 4 with ℓ, member

theorem letter.of_lt (n : Nat)
  requires below : n < 4
  shows n ∈ 4
proof
  exact membership.of_Less at n, 4 with below

-- The four letters.
theorem letter.zero_mem
  shows 0 ∈ 4
proof
  have below : 0 < 4 by arith
  exact letter.of_lt with below

theorem letter.one_mem
  shows 1 ∈ 4
proof
  have below : 1 < 4 by arith
  exact letter.of_lt with below

theorem letter.two_mem
  shows 2 ∈ 4
proof
  have below : 2 < 4 by arith
  exact letter.of_lt with below

theorem letter.three_mem
  shows 3 ∈ 4
proof
  have below : 3 < 4 by arith
  exact letter.of_lt with below

theorem letter.cases (ℓ : Set)
  requires member : ℓ ∈ 4
  shows ℓ = 0 ∨ ℓ = 1 ∨ ℓ = 2 ∨ ℓ = 3
proof
  have natural : Nat(ℓ) := letter.natural with member
  have below := Less.of_membership at ℓ, 4 with member
  have shape := natural.zero_or_successor at ℓ
  cases shape with zero | successor
  . left
    exact zero
  . obtain ⟨k, kNat, equal⟩ := successor
    rw equal at below
    rw equal
    have shapeK := natural.zero_or_successor at k
    cases shapeK with zeroK | successorK
    . right
      left
      rw zeroK
      arith
    . obtain ⟨j, jNat, equalK⟩ := successorK
      rw equalK at below
      rw equalK
      have shapeJ := natural.zero_or_successor at j
      cases shapeJ with zeroJ | successorJ
      . right
        right
        left
        rw zeroJ
        arith
      . obtain ⟨i, iNat, equalJ⟩ := successorJ
        rw equalJ at below
        rw equalJ
        have shapeI := natural.zero_or_successor at i
        cases shapeI with zeroI | successorI
        . right
          right
          right
          rw zeroI
          arith
        . obtain ⟨h, hNat, equalI⟩ := successorI
          rw equalI at below
          exfalso
          arith

theorem inverseLetter.zero
  shows inverseLetter(0) = 1
proof
  compute

theorem inverseLetter.one
  shows inverseLetter(1) = 0
proof
  compute

theorem inverseLetter.two
  shows inverseLetter(2) = 3
proof
  compute

theorem inverseLetter.three
  shows inverseLetter(3) = 2
proof
  compute

theorem inverseLetter.letter (ℓ : Set)
  requires member : ℓ ∈ 4
  shows inverseLetter(ℓ) ∈ 4
proof
  have split := letter.cases with member
  rcases split with zero | one | two | three
  . rw [zero, inverseLetter.zero]
    have below : 1 < 4 by arith
    exact letter.of_lt with below
  . rw [one, inverseLetter.one]
    have below : 0 < 4 by arith
    exact letter.of_lt with below
  . rw [two, inverseLetter.two]
    have below : 3 < 4 by arith
    exact letter.of_lt with below
  . rw [three, inverseLetter.three]
    have below : 2 < 4 by arith
    exact letter.of_lt with below

theorem inverseLetter.involutive (ℓ : Set)
  requires member : ℓ ∈ 4
  shows inverseLetter(inverseLetter(ℓ)) = ℓ
proof
  have split := letter.cases with member
  rcases split with zero | one | two | three
  . rw zero
    compute
  . rw one
    compute
  . rw two
    compute
  . rw three
    compute

theorem cancels.true_iff (x y : Set)
  requires hx : x ∈ 4
  requires hy : y ∈ 4
  shows cancels(x, y) = Bool.true ↔ y = inverseLetter(x)
proof
  have criterion := equalNat.true_iff at y, inverseLetter(x)
  simp [cancels]

theorem cancels.false_iff (x y : Set)
  requires hx : x ∈ 4
  requires hy : y ∈ 4
  shows cancels(x, y) = Bool.false ↔ y ≠ inverseLetter(x)
proof
  have criterion := equalNat.false_iff at y, inverseLetter(x)
  simp [cancels]

theorem cancels.boolean (x y : Nat)
  shows Bool(cancels(x, y))
proof
  have boolean := equalNat.boolean at y, inverseLetter(x)
  simp [cancels]

theorem cancels.self_inverse (x : Set)
  requires hx : x ∈ 4
  shows cancels(x, inverseLetter(x)) = Bool.true
proof
  have letter := inverseLetter.letter with hx
  have criterion := cancels.true_iff with hx, letter
  apply criterion.backward
  rfl

theorem cancels.inverse_self (x : Set)
  requires hx : x ∈ 4
  shows cancels(inverseLetter(x), x) = Bool.true
proof
  have letter := inverseLetter.letter with hx
  have involutive := inverseLetter.involutive with hx
  have criterion := cancels.true_iff with letter, hx
  apply criterion.backward
  symm
  exact involutive

-- Booleans.
theorem and.true_iff (a b : Bool)
  shows BoolOps.and(a, b) = Bool.true ↔ a = Bool.true ∧ b = Bool.true
proof
  have split : a = Bool.false ∨ a = Bool.true := boolean.cases with *
  have distinct := Bool.inductive.disjoint.false.true
  have reflexive : Bool.true = Bool.true by rfl
  cases split with falseA | trueA
  . rw falseA
    simp [BoolOps.and]
  . rw trueA
    simp [BoolOps.and]

theorem and.boolean (a b : Bool)
  shows Bool(BoolOps.and(a, b))
proof
  typecheck

theorem not.true_iff (b : Bool)
  shows BoolOps.not(b) = Bool.true ↔ b = Bool.false
proof
  have split : b = Bool.false ∨ b = Bool.true := boolean.cases with *
  have distinct := Bool.inductive.disjoint.false.true
  have distinctFlip : Bool.true ≠ Bool.false
    intro equal
    symm at equal
    exact distinct with equal
  have reflexive : Bool.true = Bool.true by rfl
  have reflexiveFalse : Bool.false = Bool.false by rfl
  have notFalse : BoolOps.not(Bool.false) = Bool.true by simp [BoolOps.not]
  have notTrue : BoolOps.not(Bool.true) = Bool.false by simp [BoolOps.not]
  cases split with falseB | trueB
  . rw [falseB, notFalse]
    tauto
  . rw [trueB, notTrue]
    tauto

-- The tail of a list over A is a list over A.
theorem List.tail_list (A x xs : Set)
  requires list : List(A, x :: xs)
  shows List(A, xs)
proof
  have shape := List.cases with list
  cases shape with nil | cons
  . exfalso
    have distinct := List.inductive.disjoint.nil.cons at x, xs
    symm at nil
    exact distinct with nil
  . obtain ⟨y, hy, ys, ysList, consShape⟩ := cons
    have both := List.inductive.injective.cons with consShape
    rw both.right
    exact ysList

-- Reduced words.
theorem fitsTest.nil (x : Set)
  requires hx : x ∈ 4
  shows fitsTest(x, []) = Bool.true
proof
  simp [fitsTest]

theorem fitsTest.cons (x y : Set) (ys : List(4))
  requires hx : x ∈ 4
  requires hy : y ∈ 4
  shows fitsTest(x, y :: ys) = BoolOps.not(cancels(x, y))
proof
  simp [fitsTest]

theorem reducedTest.nil
  shows reducedTest([]) = Bool.true
proof
  simp [reducedTest]

theorem reducedTest.cons (x : Set) (xs : List(4))
  requires hx : x ∈ 4
  shows reducedTest(x :: xs) = BoolOps.and(fitsTest(x, xs), reducedTest(xs))
proof
  simp [reducedTest]

theorem fitsTest.type (x : Nat) (w : List(4))
  shows Bool(fitsTest(x, w))
proof
  have shape := List.cases with *
  cases shape with nil | cons
  . rw nil
    simp [fitsTest]
    exact Bool.inductive.constructor.true
  . obtain ⟨y, hy, ys, tailList, equal⟩ := cons
    have boolean := cancels.boolean at x, y
    rw equal
    simp [fitsTest]
    exact not.boolean with boolean

theorem reducedTest.type (w : List(4))
  shows Bool(reducedTest(w))
proof
  induction w
  | List.nil =>
    simp [reducedTest]
    exact Bool.inductive.constructor.true
  | List.cons(x, xs) using ih =>
    have hx : x ∈ 4 by assumption
    have fits := fitsTest.type at x, xs with *
    simp [reducedTest]
    exact and.boolean with fits, ih

theorem Reduced.nil
  shows Reduced([])
proof
  unfold Reduced
  exact reducedTest.nil

theorem Reduced.cons_iff (x : Set) (xs : List(4))
  requires hx : x ∈ 4
  shows Reduced(x :: xs) ↔ fitsTest(x, xs) = Bool.true ∧ Reduced(xs)
proof
  have fits := fitsTest.type at x, xs with *
  have tailTest := reducedTest.type at xs with *
  have criterion := and.true_iff with fits, tailTest
  constructor
  . intro reduced
    unfold Reduced at reduced
    rw reducedTest.cons at reduced
    obtain ⟨fitsHead, reducedTail⟩ := criterion.forward with reduced
    constructor
    . exact fitsHead
    . unfold Reduced
      exact reducedTail
  . intro parts
    obtain ⟨fitsHead, reducedTail⟩ := parts
    unfold Reduced at reducedTail
    unfold Reduced
    rw reducedTest.cons
    exact criterion.backward with ⟨fitsHead, reducedTail⟩

theorem Reduced.tail (x : Set) (xs : List(4))
  requires hx : x ∈ 4
  requires reduced : Reduced(x :: xs)
  shows Reduced(xs)
proof
  have parts := Reduced.cons_iff.forward with reduced
  exact parts.right

theorem Reduced.fits (x : Set) (xs : List(4))
  requires hx : x ∈ 4
  requires reduced : Reduced(x :: xs)
  shows fitsTest(x, xs) = Bool.true
proof
  have parts := Reduced.cons_iff.forward with reduced
  exact parts.left

theorem Reduced.singleton (x : Set)
  requires hx : x ∈ 4
  shows Reduced(x :: [])
proof
  have fits := fitsTest.nil with hx
  exact Reduced.cons_iff.backward with ⟨fits, Reduced.nil⟩

theorem Reduced.cons_cons (x y : Set) (ys : List(4))
  requires hx : x ∈ 4
  requires hy : y ∈ 4
  shows Reduced(x :: y :: ys) ↔ cancels(x, y) = Bool.false ∧ Reduced(y :: ys)
proof
  have criterion := Reduced.cons_iff at x, y :: ys with hx
  have fits := fitsTest.cons at x, y, ys with hx, hy
  have boolean := cancels.boolean at x, y
  have flip := not.true_iff with boolean
  rw fits at criterion
  constructor
  . intro reduced
    obtain ⟨notCancel, tail⟩ := criterion.forward with reduced
    exact ⟨flip.forward with notCancel, tail⟩
  . intro parts
    obtain ⟨keep, tail⟩ := parts
    exact criterion.backward with ⟨flip.backward with keep, tail⟩

-- Pushing a letter onto a word.
theorem pushLetter.nil (x : Set)
  requires hx : x ∈ 4
  shows pushLetter(x, []) = x :: []
proof
  simp [pushLetter]

theorem pushLetter.cancel (x y : Set) (ys : List(4))
  requires hx : x ∈ 4
  requires hy : y ∈ 4
  requires cancel : cancels(x, y) = Bool.true
  shows pushLetter(x, y :: ys) = ys
proof
  simp [pushLetter, cancel, boolChoice]

theorem pushLetter.keep (x y : Set) (ys : List(4))
  requires hx : x ∈ 4
  requires hy : y ∈ 4
  requires keep : cancels(x, y) = Bool.false
  shows pushLetter(x, y :: ys) = x :: y :: ys
proof
  simp [pushLetter, keep, boolChoice]

theorem pushLetter.closed (x : Set) (r : List(4))
  requires hx : x ∈ 4
  shows List(4, pushLetter(x, r))
proof
  have shape := List.cases with *
  cases shape with nil | cons
  . rw [nil, pushLetter.nil]
    typecheck
  . obtain ⟨y, hy, ys, tailList, equal⟩ := cons
    have boolean := cancels.boolean at x, y
    have split : cancels(x, y) = Bool.false ∨ cancels(x, y) = Bool.true :=
      boolean.cases with boolean
    cases split with keep | cancel
    . rw [equal, pushLetter.keep]
      typecheck
    . rw [equal, pushLetter.cancel]
      exact tailList

theorem pushLetter.of_fits (x : Set) (r : List(4))
  requires hx : x ∈ 4
  requires fits : fitsTest(x, r) = Bool.true
  shows pushLetter(x, r) = x :: r
proof
  have shape := List.cases with *
  cases shape with nil | cons
  . rw [nil, pushLetter.nil]
    rfl
  . obtain ⟨y, hy, ys, tailList, equal⟩ := cons
    rw [equal, fitsTest.cons] at fits
    have keep := not.true_iff.forward with fits
    rw [equal, pushLetter.keep]
    rfl

theorem pushLetter.reduced (x : Set) (r : List(4))
  requires hx : x ∈ 4
  requires reduced : Reduced(r)
  shows Reduced(pushLetter(x, r))
proof
  have shape := List.cases with *
  cases shape with nil | cons
  . rw [nil, pushLetter.nil]
    exact Reduced.singleton with hx
  . obtain ⟨y, hy, ys, tailList, equal⟩ := cons
    rw equal at reduced
    have boolean := cancels.boolean at x, y
    have split : cancels(x, y) = Bool.false ∨ cancels(x, y) = Bool.true :=
      boolean.cases with boolean
    cases split with keep | cancel
    . rw [equal, pushLetter.keep]
      exact Reduced.cons_cons.backward with ⟨keep, reduced⟩
    . rw [equal, pushLetter.cancel]
      exact Reduced.tail with hy, reduced

-- Cancelling twice restores a reduced word: the key law of reduction.
theorem pushLetter.cancel_cancel (x y : Set) (s : List(4))
  requires hx : x ∈ 4
  requires hy : y ∈ 4
  requires reduced : Reduced(s)
  requires cancel : cancels(x, y) = Bool.true
  shows pushLetter(x, pushLetter(y, s)) = s
proof
  have yInverse := cancels.true_iff.forward with hx, hy, cancel
  have shape := List.cases with *
  cases shape with nil | cons
  . have empty : List(4, []) by typecheck
    have single := pushLetter.cancel at x, y, [] with hx, hy, cancel
    rw [nil, pushLetter.nil, single]
    rfl
  . obtain ⟨z, hz, zs, tailList, equal⟩ := cons
    rw equal at reduced
    have boolean := cancels.boolean at y, z
    have split : cancels(y, z) = Bool.false ∨ cancels(y, z) = Bool.true :=
      boolean.cases with boolean
    cases split with keep | cancelZ
    . have keepStep := pushLetter.keep at y, z, zs with hy, hz, keep
      have tailCons : List(4, z :: zs) by typecheck
      have cancelStep := pushLetter.cancel at x, y, z :: zs with hx, hy, cancel
      rw [equal, keepStep, cancelStep]
      rfl
    . have zInverse := cancels.true_iff.forward with hy, hz, cancelZ
      have zIsX : z = x
        rw [zInverse, yInverse]
        exact inverseLetter.involutive with hx
      rw zIsX at reduced
      have fits := Reduced.fits with hx, reduced
      have cancelStep := pushLetter.cancel at y, z, zs with hy, hz, cancelZ
      have fitsStep := pushLetter.of_fits at x, zs with hx, fits
      rw [equal, cancelStep, fitsStep, zIsX]
      rfl

-- Reduction.
theorem reduce.nil
  shows reduce([]) = []
proof
  simp [reduce]

theorem reduce.cons (x : Set) (xs : List(4))
  requires hx : x ∈ 4
  shows reduce(x :: xs) = pushLetter(x, reduce(xs))
proof
  simp [reduce]

theorem reduce.closed (w : List(4))
  shows List(4, reduce(w))
proof
  induction w
  | List.nil =>
    rw reduce.nil
    typecheck
  | List.cons(x, xs) using ih =>
    have hx : x ∈ 4 by assumption
    rw reduce.cons
    exact pushLetter.closed with hx, ih

theorem reduce.reduced (w : List(4))
  shows Reduced(reduce(w))
proof
  induction w
  | List.nil =>
    rw reduce.nil
    exact Reduced.nil
  | List.cons(x, xs) using ih =>
    have hx : x ∈ 4 by assumption
    have closed := reduce.closed at xs with *
    rw reduce.cons
    exact pushLetter.reduced with hx, closed, ih

theorem reduce.of_reduced (w : List(4))
  requires reduced : Reduced(w)
  shows reduce(w) = w
proof
  induction w
  | List.nil =>
    intro reduced
    exact reduce.nil
  | List.cons(x, xs) using ih =>
    intro reduced
    have hx : x ∈ 4 by assumption
    have fits := Reduced.fits with hx, reduced
    have tail := Reduced.tail with hx, reduced
    have fixed := ih with tail
    rw [reduce.cons, fixed, pushLetter.of_fits]
    rfl

theorem reduce.idempotent (w : List(4))
  shows reduce(reduce(w)) = reduce(w)
proof
  have closed := reduce.closed at w with *
  have reduced := reduce.reduced at w with *
  exact reduce.of_reduced with closed, reduced

theorem Reduced.iff_fixed (w : List(4))
  shows Reduced(w) ↔ reduce(w) = w
proof
  constructor
  . intro reduced
    exact reduce.of_reduced with reduced
  . intro fixed
    have reduced := reduce.reduced at w with *
    rwa fixed at reduced

-- Concatenation.
instance concat.closed (u v : List(4))
  shows List(4, concat(u, v))
proof
  unfold concat
  typecheck

theorem concat.nil_left (v : List(4))
  shows concat([], v) = v
proof
  unfold concat
  exact append.nil at 4, v with *

theorem concat.nil_right (u : List(4))
  shows concat(u, []) = u
proof
  unfold concat
  exact append.right_unit at u with *

theorem concat.cons (x : Set) (u v : List(4))
  requires hx : x ∈ 4
  shows concat(x :: u, v) = x :: concat(u, v)
proof
  unfold concat
  exact append.cons with *

theorem concat.associative (u v w : List(4))
  shows concat(concat(u, v), w) = concat(u, concat(v, w))
proof
  unfold concat
  exact append.associative at w, v, u with *

theorem concat.singleton (x : Set) (v : List(4))
  requires hx : x ∈ 4
  shows concat(x :: [], v) = x :: v
proof
  have empty : List(4, []) by typecheck
  have step := concat.cons at x, [], v with hx
  rw [step, concat.nil_left]
  rfl

-- Reduction and concatenation: reducing either part first does not
-- change the reduction of the whole.
theorem reduce.concat_right (u v : List(4))
  shows reduce(concat(u, v)) = reduce(concat(u, reduce(v)))
proof
  induction u
  | List.nil =>
    have closed := reduce.closed at v with *
    have left := concat.nil_left at v with *
    have right := concat.nil_left at reduce(v) with *
    rw [left, right, reduce.idempotent]
    rfl
  | List.cons(x, xs) using ih =>
    have hx : x ∈ 4 by assumption
    have closed := reduce.closed at v with *
    have left := concat.cons at x, xs, v with hx
    have right := concat.cons at x, xs, reduce(v) with hx
    have reduceLeft := reduce.cons at x, concat(xs, v) with hx
    have reduceRight := reduce.cons at x, concat(xs, reduce(v)) with hx
    rw [left, right, reduceLeft, reduceRight, ih]
    rfl

theorem reduce.concat_left (u v : List(4))
  shows reduce(concat(u, v)) = reduce(concat(reduce(u), v))
proof
  induction u
  | List.nil =>
    rw reduce.nil
    rfl
  | List.cons(x, xs) using ih =>
    have hx : x ∈ 4 by assumption
    have closed := reduce.closed at xs with *
    have reduced := reduce.reduced at xs with *
    have left := concat.cons at x, xs, v with hx
    have reduceLeft := reduce.cons at x, concat(xs, v) with hx
    have reduceHead := reduce.cons at x, xs with hx
    rw [left, reduceLeft, ih, reduceHead]
    have shape := List.cases with closed
    cases shape with nil | cons
    . have single := concat.singleton at x, v with hx
      rw [nil, pushLetter.nil, concat.nil_left, single, reduce.cons]
      rfl
    . obtain ⟨y, hy, ys, tailList, equal⟩ := cons
      rw equal at reduced
      have reducedTail := reduce.reduced at concat(ys, v) with *
      have consY := concat.cons at y, ys, v with hy
      have reduceY := reduce.cons at y, concat(ys, v) with hy
      have boolean := cancels.boolean at x, y
      have split : cancels(x, y) = Bool.false ∨ cancels(x, y) = Bool.true :=
        boolean.cases with boolean
      cases split with keep | cancel
      . have consX := concat.cons at x, y :: ys, v with hx
        have reduceX := reduce.cons at x, concat(y :: ys, v) with hx
        rw [equal, pushLetter.keep, consX, reduceX, consY, reduceY]
        rfl
      . have closedTail := reduce.closed at concat(ys, v) with *
        have cancelStep := pushLetter.cancel at x, y, ys with hx, hy, cancel
        have collapse := pushLetter.cancel_cancel at x, y, reduce(concat(ys, v)) with
          hx, hy, reducedTail, cancel
        rw [equal, cancelStep, consY, reduceY, collapse]
        rfl

theorem reduce.concat (u v : List(4))
  shows reduce(concat(u, v)) = reduce(concat(reduce(u), reduce(v)))
proof
  have closedU := reduce.closed at u with *
  have first := reduce.concat_left at u, v with *
  have second := reduce.concat_right at reduce(u), v with *
  rw [first, second]
  rfl

-- The inverse word.
theorem inverseWord.nil
  shows inverseWord([]) = []
proof
  simp [inverseWord]

theorem inverseWord.cons (x : Set) (xs : List(4))
  requires hx : x ∈ 4
  shows inverseWord(x :: xs) = concat(inverseWord(xs), inverseLetter(x) :: [])
proof
  simp [inverseWord]

instance inverseWord.closed (w : List(4))
  shows List(4, inverseWord(w))
proof
  induction w
  | List.nil =>
    rw inverseWord.nil
    typecheck
  | List.cons(x, xs) using ih =>
    have hx : x ∈ 4 by assumption
    have letter := inverseLetter.letter with hx
    rw inverseWord.cons
    typecheck

theorem reduce.inverse_left (w : List(4))
  shows reduce(concat(inverseWord(w), w)) = []
proof
  induction w
  | List.nil =>
    have empty : List(4, []) by typecheck
    rw [inverseWord.nil, concat.nil_left, reduce.nil]
    rfl
  | List.cons(x, xs) using ih =>
    have hx : x ∈ 4 by assumption
    have letter := inverseLetter.letter with hx
    have closedInverse := inverseWord.closed at xs with *
    have closed := reduce.closed at xs with *
    have reduced := reduce.reduced at xs with *
    have single : List(4, inverseLetter(x) :: []) by typecheck
    have cancel := cancels.inverse_self with hx
    have cancelled : reduce(inverseLetter(x) :: x :: xs) = reduce(xs)
      have outer := reduce.cons at inverseLetter(x), x :: xs with letter
      have inner := reduce.cons at x, xs with hx
      have collapse := pushLetter.cancel_cancel at inverseLetter(x), x, reduce(xs) with
        letter, hx, reduced, cancel
      rw [outer, inner, collapse]
      rfl
    have pair : List(4, inverseLetter(x) :: x :: xs) by typecheck
    have assoc := concat.associative at inverseWord(xs), inverseLetter(x) :: [], x :: xs
      with *
    have singleton := concat.singleton at inverseLetter(x), x :: xs with letter
    have front := reduce.concat_right at inverseWord(xs), inverseLetter(x) :: x :: xs
      with *
    have back := reduce.concat_right at inverseWord(xs), xs with *
    rw [inverseWord.cons, assoc, singleton, front, cancelled, ← back]
    exact ih

theorem reduce.inverse_right (w : List(4))
  shows reduce(concat(w, inverseWord(w))) = []
proof
  induction w
  | List.nil =>
    have empty : List(4, []) by typecheck
    rw [inverseWord.nil, concat.nil_left, reduce.nil]
    rfl
  | List.cons(x, xs) using ih =>
    have hx : x ∈ 4 by assumption
    have letter := inverseLetter.letter with hx
    have closedInverse := inverseWord.closed at xs with *
    have single : List(4, inverseLetter(x) :: []) by typecheck
    have cancel := cancels.self_inverse with hx
    have tailPart : List(4, concat(inverseWord(xs), inverseLetter(x) :: [])) by typecheck
    have both : List(4, concat(xs, inverseWord(xs))) by typecheck
    have whole : List(4, concat(concat(xs, inverseWord(xs)), inverseLetter(x) :: []))
      typecheck
    have outer := concat.cons at x, xs, concat(inverseWord(xs), inverseLetter(x) :: [])
      with *
    have assoc := concat.associative at xs, inverseWord(xs), inverseLetter(x) :: [] with *
    have reduceOuter := reduce.cons at x,
      concat(concat(xs, inverseWord(xs)), inverseLetter(x) :: []) with *
    have inner := reduce.concat_left at concat(xs, inverseWord(xs)), inverseLetter(x) :: []
      with *
    have empty : List(4, []) by typecheck
    have nilLeft := concat.nil_left at inverseLetter(x) :: [] with single
    have reduceSingle := reduce.cons at inverseLetter(x), [] with letter
    have pushSingle := pushLetter.nil at inverseLetter(x) with letter
    have final := pushLetter.cancel at x, inverseLetter(x), [] with hx, letter, cancel
    rw [inverseWord.cons, outer, ← assoc, reduceOuter, inner, ih, nilLeft, reduceSingle,
      reduce.nil, pushSingle, final]
    rfl

-- The lists over a carrier.
theorem listsOfLength.zero (A : Set)
  shows listsOfLength(A, 0) = {[]}
proof
  simp [listsOfLength]

theorem listsOfLength.succ (A : Set) (k : Nat)
  shows listsOfLength(A, succ(k)) = consAll(A, listsOfLength(A, k))
proof
  simp [listsOfLength]

theorem listsOfLength.list (A : Set) (n : Nat)
  shows ∀ w ∈ listsOfLength(A, n), List(A, w)
proof
  induction n
  | zero =>
    intros w hw
    rw listsOfLength.zero at hw
    have equal := singleton.membership.forward with hw
    rw equal
    typecheck
  | succ(k) using ih =>
    intros w hw
    rw listsOfLength.succ at hw
    obtain ⟨p, hp, equal⟩ := consAll.membership.forward with hw
    obtain ⟨bound, x, hx, t, ht, shape⟩ := product.membership.forward with hp
    have tail := ih with t, ht
    rw [shape, fst.pair, snd.pair] at equal
    rw ← equal
    typecheck

theorem listsOver.list (A w : Set)
  requires member : w ∈ listsOver(A)
  shows List(A, w)
proof
  unfold listsOver at member
  obtain ⟨L, hL, hwL⟩ := union.membership.forward with member
  obtain ⟨n, hn, equal⟩ := listStages.membership.forward with hL
  have natural := nat.omega.backward with hn
  rw ← equal at hwL
  have all := listsOfLength.list at A, n with *
  exact all with w, hwL

theorem listsOfLength.of_list (A : Set) (w : List(A))
  shows ∃ n ∈ ℕ, w ∈ listsOfLength(A, n)
proof
  induction w
  | List.nil =>
    witness 0
    constructor
    . typecheck
    . rw listsOfLength.zero
      exact singleton.self
  | List.cons(x, xs) using ih =>
    have hx : x ∈ A by assumption
    obtain ⟨n, hn, member⟩ := ih
    have natural := nat.omega.backward with hn
    witness succ(n)
    constructor
    . typecheck
    . rw listsOfLength.succ
      have pair := product.pair at x, xs, A, listsOfLength(A, n) with *
      apply consAll.membership.backward
      witness (x, xs)
      constructor
      . exact pair
      . rw [fst.pair, snd.pair]
        rfl

theorem listsOver.of_list (A : Set) (w : List(A))
  shows w ∈ listsOver(A)
proof
  obtain ⟨n, hn, member⟩ := listsOfLength.of_list with *
  have stage := listStages.membership.backward at A, listsOfLength(A, n) with ⟨n, hn, rfl⟩
  unfold listsOver
  exact union.membership.backward with ⟨listsOfLength(A, n), stage, member⟩

theorem listsOver.membership (A w : Set)
  shows w ∈ listsOver(A) ↔ List(A, w)
proof
  constructor
  . intro member
    exact listsOver.list with member
  . intro list
    exact listsOver.of_list with list

-- The reduced words.
theorem reducedWords.mem_iff (w : Set)
  shows w ∈ reducedWords ↔ List(4, w) ∧ Reduced(w)
proof
  constructor
  . intro member
    obtain ⟨inLists, reduced⟩ := reducedWords.membership.forward with member
    exact ⟨listsOver.list with inLists, reduced⟩
  . intro parts
    obtain ⟨list, reduced⟩ := parts
    have inLists := listsOver.of_list with list
    exact reducedWords.membership.backward with ⟨inLists, reduced⟩

theorem reducedWords.list (w : Set)
  requires member : w ∈ reducedWords
  shows List(4, w)
proof
  have parts := reducedWords.mem_iff.forward with member
  exact parts.left

theorem reducedWords.reduced (w : Set)
  requires member : w ∈ reducedWords
  shows Reduced(w)
proof
  have parts := reducedWords.mem_iff.forward with member
  exact parts.right

theorem reducedWords.of_reduced (w : List(4))
  requires reduced : Reduced(w)
  shows w ∈ reducedWords
proof
  have list : List(4, w) by assumption
  exact reducedWords.mem_iff.backward with ⟨list, reduced⟩

theorem reduce.mem (w : List(4))
  shows reduce(w) ∈ reducedWords
proof
  have closed := reduce.closed at w with *
  have reduced := reduce.reduced at w with *
  exact reducedWords.of_reduced with closed, reduced

theorem reducedWords.nil_mem
  shows [] ∈ reducedWords
proof
  have list : List(4, []) by typecheck
  exact reducedWords.of_reduced with list, Reduced.nil

theorem reducedWords.fixed (w : Set)
  requires member : w ∈ reducedWords
  shows reduce(w) = w
proof
  have list := reducedWords.list with member
  have reduced := reducedWords.reduced with member
  exact reduce.of_reduced with list, reduced