Grace/Cumulus/Algebra/Group/Words.g17

Open in Workbench Download source

Imports

List.Filter

Declarations

Source

1-- Words over the four letters a, a⁻¹, b, b⁻¹ as lists over 4: the inverse2-- letter, reduced words with no adjacent inverse pair, the reduction that3-- cancels adjacent inverse pairs, the inverse of a word, the laws of4-- reduction under concatenation, and the set of all lists over a carrier5-- Part of Cumulus, the Grace17 mathematics library.6-- Copyright (c) 2026 Grant Passmore.7-- Released under the Apache License 2.0. See LICENSE in the repository root.8-- Authors: Grant Passmore910module Grace.Cumulus.Algebra.Group.Words11import List.Filter1213-- The letters are 0, 1, 2, 3, read a, a⁻¹, b, b⁻¹; the inverse letter14-- swaps 0 with 1 and 2 with 3, and cancels(x, y) says y is the inverse15-- of x.16def evenTest (n : Nat) → Bool17  | zero => Bool.true18  | succ(k) => BoolOps.not(evenTest(k))1920def inverseLetter (ℓ : Nat) → Nat21  | zero => 122  | succ(k) => chooseNat(evenTest(k), k, succ(succ(k)))2324def cancels (x y : Nat) : Bool := equalNat(y, inverseLetter(x))2526-- fitsTest(x, w): x placed before w makes no adjacent inverse pair;27-- reducedTest(w): no two adjacent letters of w are inverse; Reduced(w)28-- is the latter as a property.29def fitsTest (x : Nat, w : List(4)) → Bool30  | x, [] => Bool.true31  | x, y :: ys => BoolOps.not(cancels(x, y))32  descends w3334def reducedTest (w : List(4)) → Bool35  | [] => Bool.true36  | x :: xs => BoolOps.and(fitsTest(x, xs), reducedTest(xs))3738predicate Reduced (w : Set) := reducedTest(w) = Bool.true3940-- pushLetter(x, r) places x before the word r, cancelling it against the41-- first letter of r when the two are inverse; reduce(w) cancels every42-- adjacent inverse pair of w, working from the end of the word.43def pushLetter (x : Nat, r : List(4)) → Set44  | x, [] => x :: []45  | x, y :: ys => boolChoice(cancels(x, y), ys, x :: y :: ys)46  descends r4748def reduce (w : List(4)) → Set49  | [] => []50  | x :: xs => pushLetter(x, reduce(xs))5152-- Concatenation of words: concat(u, v) is u followed by v.53def concat (u v : Set) : Set := append{A := 4}(v, u)5455-- The inverse of a word: the reversed word with every letter inverted.56def inverseWord (w : List(4)) → Set57  | [] => []58  | x :: xs => concat(inverseWord(xs), inverseLetter(x) :: [])5960-- The set of all lists over A: the union over n of the lists of length n.61def consAll (A L : Set) : Set := { fst(p) :: snd(p) | p ∈ A × L }6263def listsOfLength (A : Set, n : Nat) → Set64  | A, zero => {[]}65  | A, succ(k) => consAll(A, listsOfLength(A, k))6667def listStages (A : Set) : Set := { listsOfLength(A, n) | n ∈ ℕ }68def listsOver (A : Set) : Set := ⋃(listStages(A))6970-- The reduced words over the four letters.71def reducedWords : Set := { w ∈ listsOver(4) | Reduced(w) }7273-- Letters.74theorem letter.natural (ℓ : Set)75  requires member : ℓ ∈ 476  shows Nat(ℓ)77proof78  exact natural.member at 4 with ℓ, member7980theorem letter.of_lt (n : Nat)81  requires below : n < 482  shows n ∈ 483proof84  exact membership.of_Less at n, 4 with below8586-- The four letters.87theorem letter.zero_mem88  shows 0 ∈ 489proof90  have below : 0 < 4 by arith91  exact letter.of_lt with below9293theorem letter.one_mem94  shows 1 ∈ 495proof96  have below : 1 < 4 by arith97  exact letter.of_lt with below9899theorem letter.two_mem100  shows 2 ∈ 4101proof102  have below : 2 < 4 by arith103  exact letter.of_lt with below104105theorem letter.three_mem106  shows 3 ∈ 4107proof108  have below : 3 < 4 by arith109  exact letter.of_lt with below110111theorem letter.cases (ℓ : Set)112  requires member : ℓ ∈ 4113  shows ℓ = 0 ∨ ℓ = 1 ∨ ℓ = 2 ∨ ℓ = 3114proof115  have natural : Nat(ℓ) := letter.natural with member116  have below := Less.of_membership at ℓ, 4 with member117  have shape := natural.zero_or_successor at ℓ118  cases shape with zero | successor119  . left120    exact zero121  . obtain ⟨k, kNat, equal⟩ := successor122    rw equal at below123    rw equal124    have shapeK := natural.zero_or_successor at k125    cases shapeK with zeroK | successorK126    . right127      left128      rw zeroK129      arith130    . obtain ⟨j, jNat, equalK⟩ := successorK131      rw equalK at below132      rw equalK133      have shapeJ := natural.zero_or_successor at j134      cases shapeJ with zeroJ | successorJ135      . right136        right137        left138        rw zeroJ139        arith140      . obtain ⟨i, iNat, equalJ⟩ := successorJ141        rw equalJ at below142        rw equalJ143        have shapeI := natural.zero_or_successor at i144        cases shapeI with zeroI | successorI145        . right146          right147          right148          rw zeroI149          arith150        . obtain ⟨h, hNat, equalI⟩ := successorI151          rw equalI at below152          exfalso153          arith154155theorem inverseLetter.zero156  shows inverseLetter(0) = 1157proof158  compute159160theorem inverseLetter.one161  shows inverseLetter(1) = 0162proof163  compute164165theorem inverseLetter.two166  shows inverseLetter(2) = 3167proof168  compute169170theorem inverseLetter.three171  shows inverseLetter(3) = 2172proof173  compute174175theorem inverseLetter.letter (ℓ : Set)176  requires member : ℓ ∈ 4177  shows inverseLetter(ℓ) ∈ 4178proof179  have split := letter.cases with member180  rcases split with zero | one | two | three181  . rw [zero, inverseLetter.zero]182    have below : 1 < 4 by arith183    exact letter.of_lt with below184  . rw [one, inverseLetter.one]185    have below : 0 < 4 by arith186    exact letter.of_lt with below187  . rw [two, inverseLetter.two]188    have below : 3 < 4 by arith189    exact letter.of_lt with below190  . rw [three, inverseLetter.three]191    have below : 2 < 4 by arith192    exact letter.of_lt with below193194theorem inverseLetter.involutive (ℓ : Set)195  requires member : ℓ ∈ 4196  shows inverseLetter(inverseLetter(ℓ)) = ℓ197proof198  have split := letter.cases with member199  rcases split with zero | one | two | three200  . rw zero201    compute202  . rw one203    compute204  . rw two205    compute206  . rw three207    compute208209theorem cancels.true_iff (x y : Set)210  requires hx : x ∈ 4211  requires hy : y ∈ 4212  shows cancels(x, y) = Bool.true ↔ y = inverseLetter(x)213proof214  have criterion := equalNat.true_iff at y, inverseLetter(x)215  simp [cancels]216217theorem cancels.false_iff (x y : Set)218  requires hx : x ∈ 4219  requires hy : y ∈ 4220  shows cancels(x, y) = Bool.false ↔ y ≠ inverseLetter(x)221proof222  have criterion := equalNat.false_iff at y, inverseLetter(x)223  simp [cancels]224225theorem cancels.boolean (x y : Nat)226  shows Bool(cancels(x, y))227proof228  have boolean := equalNat.boolean at y, inverseLetter(x)229  simp [cancels]230231theorem cancels.self_inverse (x : Set)232  requires hx : x ∈ 4233  shows cancels(x, inverseLetter(x)) = Bool.true234proof235  have letter := inverseLetter.letter with hx236  have criterion := cancels.true_iff with hx, letter237  apply criterion.backward238  rfl239240theorem cancels.inverse_self (x : Set)241  requires hx : x ∈ 4242  shows cancels(inverseLetter(x), x) = Bool.true243proof244  have letter := inverseLetter.letter with hx245  have involutive := inverseLetter.involutive with hx246  have criterion := cancels.true_iff with letter, hx247  apply criterion.backward248  symm249  exact involutive250251-- Booleans.252theorem and.true_iff (a b : Bool)253  shows BoolOps.and(a, b) = Bool.true ↔ a = Bool.true ∧ b = Bool.true254proof255  have split : a = Bool.false ∨ a = Bool.true := boolean.cases with *256  have distinct := Bool.inductive.disjoint.false.true257  have reflexive : Bool.true = Bool.true by rfl258  cases split with falseA | trueA259  . rw falseA260    simp [BoolOps.and]261  . rw trueA262    simp [BoolOps.and]263264theorem and.boolean (a b : Bool)265  shows Bool(BoolOps.and(a, b))266proof267  typecheck268269theorem not.true_iff (b : Bool)270  shows BoolOps.not(b) = Bool.true ↔ b = Bool.false271proof272  have split : b = Bool.false ∨ b = Bool.true := boolean.cases with *273  have distinct := Bool.inductive.disjoint.false.true274  have distinctFlip : Bool.true ≠ Bool.false275    intro equal276    symm at equal277    exact distinct with equal278  have reflexive : Bool.true = Bool.true by rfl279  have reflexiveFalse : Bool.false = Bool.false by rfl280  have notFalse : BoolOps.not(Bool.false) = Bool.true by simp [BoolOps.not]281  have notTrue : BoolOps.not(Bool.true) = Bool.false by simp [BoolOps.not]282  cases split with falseB | trueB283  . rw [falseB, notFalse]284    tauto285  . rw [trueB, notTrue]286    tauto287288-- The tail of a list over A is a list over A.289theorem List.tail_list (A x xs : Set)290  requires list : List(A, x :: xs)291  shows List(A, xs)292proof293  have shape := List.cases with list294  cases shape with nil | cons295  . exfalso296    have distinct := List.inductive.disjoint.nil.cons at x, xs297    symm at nil298    exact distinct with nil299  . obtain ⟨y, hy, ys, ysList, consShape⟩ := cons300    have both := List.inductive.injective.cons with consShape301    rw both.right302    exact ysList303304-- Reduced words.305theorem fitsTest.nil (x : Set)306  requires hx : x ∈ 4307  shows fitsTest(x, []) = Bool.true308proof309  simp [fitsTest]310311theorem fitsTest.cons (x y : Set) (ys : List(4))312  requires hx : x ∈ 4313  requires hy : y ∈ 4314  shows fitsTest(x, y :: ys) = BoolOps.not(cancels(x, y))315proof316  simp [fitsTest]317318theorem reducedTest.nil319  shows reducedTest([]) = Bool.true320proof321  simp [reducedTest]322323theorem reducedTest.cons (x : Set) (xs : List(4))324  requires hx : x ∈ 4325  shows reducedTest(x :: xs) = BoolOps.and(fitsTest(x, xs), reducedTest(xs))326proof327  simp [reducedTest]328329theorem fitsTest.type (x : Nat) (w : List(4))330  shows Bool(fitsTest(x, w))331proof332  have shape := List.cases with *333  cases shape with nil | cons334  . rw nil335    simp [fitsTest]336    exact Bool.inductive.constructor.true337  . obtain ⟨y, hy, ys, tailList, equal⟩ := cons338    have boolean := cancels.boolean at x, y339    rw equal340    simp [fitsTest]341    exact not.boolean with boolean342343theorem reducedTest.type (w : List(4))344  shows Bool(reducedTest(w))345proof346  induction w347  | List.nil =>348    simp [reducedTest]349    exact Bool.inductive.constructor.true350  | List.cons(x, xs) using ih =>351    have hx : x ∈ 4 by assumption352    have fits := fitsTest.type at x, xs with *353    simp [reducedTest]354    exact and.boolean with fits, ih355356theorem Reduced.nil357  shows Reduced([])358proof359  unfold Reduced360  exact reducedTest.nil361362theorem Reduced.cons_iff (x : Set) (xs : List(4))363  requires hx : x ∈ 4364  shows Reduced(x :: xs) ↔ fitsTest(x, xs) = Bool.true ∧ Reduced(xs)365proof366  have fits := fitsTest.type at x, xs with *367  have tailTest := reducedTest.type at xs with *368  have criterion := and.true_iff with fits, tailTest369  constructor370  . intro reduced371    unfold Reduced at reduced372    rw reducedTest.cons at reduced373    obtain ⟨fitsHead, reducedTail⟩ := criterion.forward with reduced374    constructor375    . exact fitsHead376    . unfold Reduced377      exact reducedTail378  . intro parts379    obtain ⟨fitsHead, reducedTail⟩ := parts380    unfold Reduced at reducedTail381    unfold Reduced382    rw reducedTest.cons383    exact criterion.backward with ⟨fitsHead, reducedTail⟩384385theorem Reduced.tail (x : Set) (xs : List(4))386  requires hx : x ∈ 4387  requires reduced : Reduced(x :: xs)388  shows Reduced(xs)389proof390  have parts := Reduced.cons_iff.forward with reduced391  exact parts.right392393theorem Reduced.fits (x : Set) (xs : List(4))394  requires hx : x ∈ 4395  requires reduced : Reduced(x :: xs)396  shows fitsTest(x, xs) = Bool.true397proof398  have parts := Reduced.cons_iff.forward with reduced399  exact parts.left400401theorem Reduced.singleton (x : Set)402  requires hx : x ∈ 4403  shows Reduced(x :: [])404proof405  have fits := fitsTest.nil with hx406  exact Reduced.cons_iff.backward with ⟨fits, Reduced.nil⟩407408theorem Reduced.cons_cons (x y : Set) (ys : List(4))409  requires hx : x ∈ 4410  requires hy : y ∈ 4411  shows Reduced(x :: y :: ys) ↔ cancels(x, y) = Bool.false ∧ Reduced(y :: ys)412proof413  have criterion := Reduced.cons_iff at x, y :: ys with hx414  have fits := fitsTest.cons at x, y, ys with hx, hy415  have boolean := cancels.boolean at x, y416  have flip := not.true_iff with boolean417  rw fits at criterion418  constructor419  . intro reduced420    obtain ⟨notCancel, tail⟩ := criterion.forward with reduced421    exact ⟨flip.forward with notCancel, tail⟩422  . intro parts423    obtain ⟨keep, tail⟩ := parts424    exact criterion.backward with ⟨flip.backward with keep, tail⟩425426-- Pushing a letter onto a word.427theorem pushLetter.nil (x : Set)428  requires hx : x ∈ 4429  shows pushLetter(x, []) = x :: []430proof431  simp [pushLetter]432433theorem pushLetter.cancel (x y : Set) (ys : List(4))434  requires hx : x ∈ 4435  requires hy : y ∈ 4436  requires cancel : cancels(x, y) = Bool.true437  shows pushLetter(x, y :: ys) = ys438proof439  simp [pushLetter, cancel, boolChoice]440441theorem pushLetter.keep (x y : Set) (ys : List(4))442  requires hx : x ∈ 4443  requires hy : y ∈ 4444  requires keep : cancels(x, y) = Bool.false445  shows pushLetter(x, y :: ys) = x :: y :: ys446proof447  simp [pushLetter, keep, boolChoice]448449theorem pushLetter.closed (x : Set) (r : List(4))450  requires hx : x ∈ 4451  shows List(4, pushLetter(x, r))452proof453  have shape := List.cases with *454  cases shape with nil | cons455  . rw [nil, pushLetter.nil]456    typecheck457  . obtain ⟨y, hy, ys, tailList, equal⟩ := cons458    have boolean := cancels.boolean at x, y459    have split : cancels(x, y) = Bool.false ∨ cancels(x, y) = Bool.true :=460      boolean.cases with boolean461    cases split with keep | cancel462    . rw [equal, pushLetter.keep]463      typecheck464    . rw [equal, pushLetter.cancel]465      exact tailList466467theorem pushLetter.of_fits (x : Set) (r : List(4))468  requires hx : x ∈ 4469  requires fits : fitsTest(x, r) = Bool.true470  shows pushLetter(x, r) = x :: r471proof472  have shape := List.cases with *473  cases shape with nil | cons474  . rw [nil, pushLetter.nil]475    rfl476  . obtain ⟨y, hy, ys, tailList, equal⟩ := cons477    rw [equal, fitsTest.cons] at fits478    have keep := not.true_iff.forward with fits479    rw [equal, pushLetter.keep]480    rfl481482theorem pushLetter.reduced (x : Set) (r : List(4))483  requires hx : x ∈ 4484  requires reduced : Reduced(r)485  shows Reduced(pushLetter(x, r))486proof487  have shape := List.cases with *488  cases shape with nil | cons489  . rw [nil, pushLetter.nil]490    exact Reduced.singleton with hx491  . obtain ⟨y, hy, ys, tailList, equal⟩ := cons492    rw equal at reduced493    have boolean := cancels.boolean at x, y494    have split : cancels(x, y) = Bool.false ∨ cancels(x, y) = Bool.true :=495      boolean.cases with boolean496    cases split with keep | cancel497    . rw [equal, pushLetter.keep]498      exact Reduced.cons_cons.backward with ⟨keep, reduced⟩499    . rw [equal, pushLetter.cancel]500      exact Reduced.tail with hy, reduced501502-- Cancelling twice restores a reduced word: the key law of reduction.503theorem pushLetter.cancel_cancel (x y : Set) (s : List(4))504  requires hx : x ∈ 4505  requires hy : y ∈ 4506  requires reduced : Reduced(s)507  requires cancel : cancels(x, y) = Bool.true508  shows pushLetter(x, pushLetter(y, s)) = s509proof510  have yInverse := cancels.true_iff.forward with hx, hy, cancel511  have shape := List.cases with *512  cases shape with nil | cons513  . have empty : List(4, []) by typecheck514    have single := pushLetter.cancel at x, y, [] with hx, hy, cancel515    rw [nil, pushLetter.nil, single]516    rfl517  . obtain ⟨z, hz, zs, tailList, equal⟩ := cons518    rw equal at reduced519    have boolean := cancels.boolean at y, z520    have split : cancels(y, z) = Bool.false ∨ cancels(y, z) = Bool.true :=521      boolean.cases with boolean522    cases split with keep | cancelZ523    . have keepStep := pushLetter.keep at y, z, zs with hy, hz, keep524      have tailCons : List(4, z :: zs) by typecheck525      have cancelStep := pushLetter.cancel at x, y, z :: zs with hx, hy, cancel526      rw [equal, keepStep, cancelStep]527      rfl528    . have zInverse := cancels.true_iff.forward with hy, hz, cancelZ529      have zIsX : z = x530        rw [zInverse, yInverse]531        exact inverseLetter.involutive with hx532      rw zIsX at reduced533      have fits := Reduced.fits with hx, reduced534      have cancelStep := pushLetter.cancel at y, z, zs with hy, hz, cancelZ535      have fitsStep := pushLetter.of_fits at x, zs with hx, fits536      rw [equal, cancelStep, fitsStep, zIsX]537      rfl538539-- Reduction.540theorem reduce.nil541  shows reduce([]) = []542proof543  simp [reduce]544545theorem reduce.cons (x : Set) (xs : List(4))546  requires hx : x ∈ 4547  shows reduce(x :: xs) = pushLetter(x, reduce(xs))548proof549  simp [reduce]550551theorem reduce.closed (w : List(4))552  shows List(4, reduce(w))553proof554  induction w555  | List.nil =>556    rw reduce.nil557    typecheck558  | List.cons(x, xs) using ih =>559    have hx : x ∈ 4 by assumption560    rw reduce.cons561    exact pushLetter.closed with hx, ih562563theorem reduce.reduced (w : List(4))564  shows Reduced(reduce(w))565proof566  induction w567  | List.nil =>568    rw reduce.nil569    exact Reduced.nil570  | List.cons(x, xs) using ih =>571    have hx : x ∈ 4 by assumption572    have closed := reduce.closed at xs with *573    rw reduce.cons574    exact pushLetter.reduced with hx, closed, ih575576theorem reduce.of_reduced (w : List(4))577  requires reduced : Reduced(w)578  shows reduce(w) = w579proof580  induction w581  | List.nil =>582    intro reduced583    exact reduce.nil584  | List.cons(x, xs) using ih =>585    intro reduced586    have hx : x ∈ 4 by assumption587    have fits := Reduced.fits with hx, reduced588    have tail := Reduced.tail with hx, reduced589    have fixed := ih with tail590    rw [reduce.cons, fixed, pushLetter.of_fits]591    rfl592593theorem reduce.idempotent (w : List(4))594  shows reduce(reduce(w)) = reduce(w)595proof596  have closed := reduce.closed at w with *597  have reduced := reduce.reduced at w with *598  exact reduce.of_reduced with closed, reduced599600theorem Reduced.iff_fixed (w : List(4))601  shows Reduced(w) ↔ reduce(w) = w602proof603  constructor604  . intro reduced605    exact reduce.of_reduced with reduced606  . intro fixed607    have reduced := reduce.reduced at w with *608    rwa fixed at reduced609610-- Concatenation.611instance concat.closed (u v : List(4))612  shows List(4, concat(u, v))613proof614  unfold concat615  typecheck616617theorem concat.nil_left (v : List(4))618  shows concat([], v) = v619proof620  unfold concat621  exact append.nil at 4, v with *622623theorem concat.nil_right (u : List(4))624  shows concat(u, []) = u625proof626  unfold concat627  exact append.right_unit at u with *628629theorem concat.cons (x : Set) (u v : List(4))630  requires hx : x ∈ 4631  shows concat(x :: u, v) = x :: concat(u, v)632proof633  unfold concat634  exact append.cons with *635636theorem concat.associative (u v w : List(4))637  shows concat(concat(u, v), w) = concat(u, concat(v, w))638proof639  unfold concat640  exact append.associative at w, v, u with *641642theorem concat.singleton (x : Set) (v : List(4))643  requires hx : x ∈ 4644  shows concat(x :: [], v) = x :: v645proof646  have empty : List(4, []) by typecheck647  have step := concat.cons at x, [], v with hx648  rw [step, concat.nil_left]649  rfl650651-- Reduction and concatenation: reducing either part first does not652-- change the reduction of the whole.653theorem reduce.concat_right (u v : List(4))654  shows reduce(concat(u, v)) = reduce(concat(u, reduce(v)))655proof656  induction u657  | List.nil =>658    have closed := reduce.closed at v with *659    have left := concat.nil_left at v with *660    have right := concat.nil_left at reduce(v) with *661    rw [left, right, reduce.idempotent]662    rfl663  | List.cons(x, xs) using ih =>664    have hx : x ∈ 4 by assumption665    have closed := reduce.closed at v with *666    have left := concat.cons at x, xs, v with hx667    have right := concat.cons at x, xs, reduce(v) with hx668    have reduceLeft := reduce.cons at x, concat(xs, v) with hx669    have reduceRight := reduce.cons at x, concat(xs, reduce(v)) with hx670    rw [left, right, reduceLeft, reduceRight, ih]671    rfl672673theorem reduce.concat_left (u v : List(4))674  shows reduce(concat(u, v)) = reduce(concat(reduce(u), v))675proof676  induction u677  | List.nil =>678    rw reduce.nil679    rfl680  | List.cons(x, xs) using ih =>681    have hx : x ∈ 4 by assumption682    have closed := reduce.closed at xs with *683    have reduced := reduce.reduced at xs with *684    have left := concat.cons at x, xs, v with hx685    have reduceLeft := reduce.cons at x, concat(xs, v) with hx686    have reduceHead := reduce.cons at x, xs with hx687    rw [left, reduceLeft, ih, reduceHead]688    have shape := List.cases with closed689    cases shape with nil | cons690    . have single := concat.singleton at x, v with hx691      rw [nil, pushLetter.nil, concat.nil_left, single, reduce.cons]692      rfl693    . obtain ⟨y, hy, ys, tailList, equal⟩ := cons694      rw equal at reduced695      have reducedTail := reduce.reduced at concat(ys, v) with *696      have consY := concat.cons at y, ys, v with hy697      have reduceY := reduce.cons at y, concat(ys, v) with hy698      have boolean := cancels.boolean at x, y699      have split : cancels(x, y) = Bool.false ∨ cancels(x, y) = Bool.true :=700        boolean.cases with boolean701      cases split with keep | cancel702      . have consX := concat.cons at x, y :: ys, v with hx703        have reduceX := reduce.cons at x, concat(y :: ys, v) with hx704        rw [equal, pushLetter.keep, consX, reduceX, consY, reduceY]705        rfl706      . have closedTail := reduce.closed at concat(ys, v) with *707        have cancelStep := pushLetter.cancel at x, y, ys with hx, hy, cancel708        have collapse := pushLetter.cancel_cancel at x, y, reduce(concat(ys, v)) with709          hx, hy, reducedTail, cancel710        rw [equal, cancelStep, consY, reduceY, collapse]711        rfl712713theorem reduce.concat (u v : List(4))714  shows reduce(concat(u, v)) = reduce(concat(reduce(u), reduce(v)))715proof716  have closedU := reduce.closed at u with *717  have first := reduce.concat_left at u, v with *718  have second := reduce.concat_right at reduce(u), v with *719  rw [first, second]720  rfl721722-- The inverse word.723theorem inverseWord.nil724  shows inverseWord([]) = []725proof726  simp [inverseWord]727728theorem inverseWord.cons (x : Set) (xs : List(4))729  requires hx : x ∈ 4730  shows inverseWord(x :: xs) = concat(inverseWord(xs), inverseLetter(x) :: [])731proof732  simp [inverseWord]733734instance inverseWord.closed (w : List(4))735  shows List(4, inverseWord(w))736proof737  induction w738  | List.nil =>739    rw inverseWord.nil740    typecheck741  | List.cons(x, xs) using ih =>742    have hx : x ∈ 4 by assumption743    have letter := inverseLetter.letter with hx744    rw inverseWord.cons745    typecheck746747theorem reduce.inverse_left (w : List(4))748  shows reduce(concat(inverseWord(w), w)) = []749proof750  induction w751  | List.nil =>752    have empty : List(4, []) by typecheck753    rw [inverseWord.nil, concat.nil_left, reduce.nil]754    rfl755  | List.cons(x, xs) using ih =>756    have hx : x ∈ 4 by assumption757    have letter := inverseLetter.letter with hx758    have closedInverse := inverseWord.closed at xs with *759    have closed := reduce.closed at xs with *760    have reduced := reduce.reduced at xs with *761    have single : List(4, inverseLetter(x) :: []) by typecheck762    have cancel := cancels.inverse_self with hx763    have cancelled : reduce(inverseLetter(x) :: x :: xs) = reduce(xs)764      have outer := reduce.cons at inverseLetter(x), x :: xs with letter765      have inner := reduce.cons at x, xs with hx766      have collapse := pushLetter.cancel_cancel at inverseLetter(x), x, reduce(xs) with767        letter, hx, reduced, cancel768      rw [outer, inner, collapse]769      rfl770    have pair : List(4, inverseLetter(x) :: x :: xs) by typecheck771    have assoc := concat.associative at inverseWord(xs), inverseLetter(x) :: [], x :: xs772      with *773    have singleton := concat.singleton at inverseLetter(x), x :: xs with letter774    have front := reduce.concat_right at inverseWord(xs), inverseLetter(x) :: x :: xs775      with *776    have back := reduce.concat_right at inverseWord(xs), xs with *777    rw [inverseWord.cons, assoc, singleton, front, cancelled, ← back]778    exact ih779780theorem reduce.inverse_right (w : List(4))781  shows reduce(concat(w, inverseWord(w))) = []782proof783  induction w784  | List.nil =>785    have empty : List(4, []) by typecheck786    rw [inverseWord.nil, concat.nil_left, reduce.nil]787    rfl788  | List.cons(x, xs) using ih =>789    have hx : x ∈ 4 by assumption790    have letter := inverseLetter.letter with hx791    have closedInverse := inverseWord.closed at xs with *792    have single : List(4, inverseLetter(x) :: []) by typecheck793    have cancel := cancels.self_inverse with hx794    have tailPart : List(4, concat(inverseWord(xs), inverseLetter(x) :: [])) by typecheck795    have both : List(4, concat(xs, inverseWord(xs))) by typecheck796    have whole : List(4, concat(concat(xs, inverseWord(xs)), inverseLetter(x) :: []))797      typecheck798    have outer := concat.cons at x, xs, concat(inverseWord(xs), inverseLetter(x) :: [])799      with *800    have assoc := concat.associative at xs, inverseWord(xs), inverseLetter(x) :: [] with *801    have reduceOuter := reduce.cons at x,802      concat(concat(xs, inverseWord(xs)), inverseLetter(x) :: []) with *803    have inner := reduce.concat_left at concat(xs, inverseWord(xs)), inverseLetter(x) :: []804      with *805    have empty : List(4, []) by typecheck806    have nilLeft := concat.nil_left at inverseLetter(x) :: [] with single807    have reduceSingle := reduce.cons at inverseLetter(x), [] with letter808    have pushSingle := pushLetter.nil at inverseLetter(x) with letter809    have final := pushLetter.cancel at x, inverseLetter(x), [] with hx, letter, cancel810    rw [inverseWord.cons, outer, ← assoc, reduceOuter, inner, ih, nilLeft, reduceSingle,811      reduce.nil, pushSingle, final]812    rfl813814-- The lists over a carrier.815theorem listsOfLength.zero (A : Set)816  shows listsOfLength(A, 0) = {[]}817proof818  simp [listsOfLength]819820theorem listsOfLength.succ (A : Set) (k : Nat)821  shows listsOfLength(A, succ(k)) = consAll(A, listsOfLength(A, k))822proof823  simp [listsOfLength]824825theorem listsOfLength.list (A : Set) (n : Nat)826  shows ∀ w ∈ listsOfLength(A, n), List(A, w)827proof828  induction n829  | zero =>830    intros w hw831    rw listsOfLength.zero at hw832    have equal := singleton.membership.forward with hw833    rw equal834    typecheck835  | succ(k) using ih =>836    intros w hw837    rw listsOfLength.succ at hw838    obtain ⟨p, hp, equal⟩ := consAll.membership.forward with hw839    obtain ⟨bound, x, hx, t, ht, shape⟩ := product.membership.forward with hp840    have tail := ih with t, ht841    rw [shape, fst.pair, snd.pair] at equal842    rw ← equal843    typecheck844845theorem listsOver.list (A w : Set)846  requires member : w ∈ listsOver(A)847  shows List(A, w)848proof849  unfold listsOver at member850  obtain ⟨L, hL, hwL⟩ := union.membership.forward with member851  obtain ⟨n, hn, equal⟩ := listStages.membership.forward with hL852  have natural := nat.omega.backward with hn853  rw ← equal at hwL854  have all := listsOfLength.list at A, n with *855  exact all with w, hwL856857theorem listsOfLength.of_list (A : Set) (w : List(A))858  shows ∃ n ∈ ℕ, w ∈ listsOfLength(A, n)859proof860  induction w861  | List.nil =>862    witness 0863    constructor864    . typecheck865    . rw listsOfLength.zero866      exact singleton.self867  | List.cons(x, xs) using ih =>868    have hx : x ∈ A by assumption869    obtain ⟨n, hn, member⟩ := ih870    have natural := nat.omega.backward with hn871    witness succ(n)872    constructor873    . typecheck874    . rw listsOfLength.succ875      have pair := product.pair at x, xs, A, listsOfLength(A, n) with *876      apply consAll.membership.backward877      witness (x, xs)878      constructor879      . exact pair880      . rw [fst.pair, snd.pair]881        rfl882883theorem listsOver.of_list (A : Set) (w : List(A))884  shows w ∈ listsOver(A)885proof886  obtain ⟨n, hn, member⟩ := listsOfLength.of_list with *887  have stage := listStages.membership.backward at A, listsOfLength(A, n) with ⟨n, hn, rfl⟩888  unfold listsOver889  exact union.membership.backward with ⟨listsOfLength(A, n), stage, member⟩890891theorem listsOver.membership (A w : Set)892  shows w ∈ listsOver(A) ↔ List(A, w)893proof894  constructor895  . intro member896    exact listsOver.list with member897  . intro list898    exact listsOver.of_list with list899900-- The reduced words.901theorem reducedWords.mem_iff (w : Set)902  shows w ∈ reducedWords ↔ List(4, w) ∧ Reduced(w)903proof904  constructor905  . intro member906    obtain ⟨inLists, reduced⟩ := reducedWords.membership.forward with member907    exact ⟨listsOver.list with inLists, reduced⟩908  . intro parts909    obtain ⟨list, reduced⟩ := parts910    have inLists := listsOver.of_list with list911    exact reducedWords.membership.backward with ⟨inLists, reduced⟩912913theorem reducedWords.list (w : Set)914  requires member : w ∈ reducedWords915  shows List(4, w)916proof917  have parts := reducedWords.mem_iff.forward with member918  exact parts.left919920theorem reducedWords.reduced (w : Set)921  requires member : w ∈ reducedWords922  shows Reduced(w)923proof924  have parts := reducedWords.mem_iff.forward with member925  exact parts.right926927theorem reducedWords.of_reduced (w : List(4))928  requires reduced : Reduced(w)929  shows w ∈ reducedWords930proof931  have list : List(4, w) by assumption932  exact reducedWords.mem_iff.backward with ⟨list, reduced⟩933934theorem reduce.mem (w : List(4))935  shows reduce(w) ∈ reducedWords936proof937  have closed := reduce.closed at w with *938  have reduced := reduce.reduced at w with *939  exact reducedWords.of_reduced with closed, reduced940941theorem reducedWords.nil_mem942  shows [] ∈ reducedWords943proof944  have list : List(4, []) by typecheck945  exact reducedWords.of_reduced with list, Reduced.nil946947theorem reducedWords.fixed (w : Set)948  requires member : w ∈ reducedWords949  shows reduce(w) = w950proof951  have list := reducedWords.list with member952  have reduced := reducedWords.reduced with member953  exact reduce.of_reduced with list, reduced954