Library reducedwordsnoproofs

Proof that words in free groups have unique reduced form

Developed for Coq 8.3

Written by P. Christopher Staecker, updated November 2010.

We begin with a nonempty set of generators, which gives a set of Letters, each of which is either a generator or an "inverse" of a generator. A word is a list of letters, and a word is reduced when it contains no adjacent pair of a letter with its inverse. We show that every word can be related to a unique reduced word through a sequence of insertions or deletions of pairs of inverse letters.

The proof follows that found in O. Bogopolski, "Introduction to Group Theory", European Math. Soc., 2008.

We use the excluded middle three times: once explicitly, and twice via a lemma which states that every set of integers has a computable least element. Excluded middle is probably not necessary to obtain the result, but is pretty important in this proof.

See also the version with proofs.

Require Import Arith.
Require Import Omega.
Require Import List.

Load listlemmas.

Excluded middle is used

Parameter EM: forall P:Prop, P \/ ~ P.

By EM, every set of integers has a computable least element

Lemma nat_well_ordered: forall (P:nat -> Prop),
(exists n:nat, P n) -> (exists m:nat, P m /\
forall k:nat, P k -> k >= m).

Letters and inverses

V is the set of generators, assumed not empty

Variable V:Set.
Parameter V_not_empty: V.

Words are lists of letters

Inductive Letter:Type :=
  | L : V -> Letter
  | Li : V -> Letter.

Definition Letter_inv (l:Letter):Letter :=
  match l with
    L c => Li c
  | Li c => L c
end.

Lemma Letter_inv_involutive: forall l:Letter,
  Letter_inv (Letter_inv l) = l.

Words and letters

Definition Word:Type := list Letter.

inserts l * l^-1 at the given position

Definition Word_inv_letter_insert (w:Word) (l:Letter) (pos:nat):Word :=
  (sublist 0 pos w) ++ (l :: Letter_inv l :: nil) ++ (sublist pos (length w) w).

Lemma Word_ili_length: forall (u:Word) (l:Letter) (pos:nat),
  length (Word_inv_letter_insert u l pos) = length u + 2.

Lemma Word_ili_delete: forall (u v:Word) (l:Letter) (pos:nat),
  u = sublist 0 pos v ++ sublist (pos+2) (length v) v /\
        (nth pos v l = l /\ nth (pos+1) v l = Letter_inv l) /\
        pos + 1 < length v
     -> v = Word_inv_letter_insert u l pos.

Direct relation.

Two words are directly related when one is a inv_letter_insert of the other. dr is irreflexive and symmetric

Definition Word_direct_rel (u v:Word):Prop :=
  (exists l:Letter, exists n:nat, n <= length v /\ u = Word_inv_letter_insert v l n) \/
    (exists l:Letter, exists n:nat, n <= length u /\ v = Word_inv_letter_insert u l n).

Lemma Word_dr_irrefl: forall u:Word,
  ~ Word_direct_rel u u.

Lemma Word_dr_sym: forall u v:Word,
  Word_direct_rel u v <-> Word_direct_rel v u.

Indirect relation.

Words are indirectly related if there is a chain of directly related words connecting them, chain must be more than one word long. ir is an equivalence relation

Definition Word_ir_by (u v:Word) (ws:list Word):Prop :=
    (length ws > 1) /\
    (hd nil ws = u /\ last ws nil = v) /\
    list_prop_pairwise ws Word_direct_rel.

Definition Word_indirect_rel (u v:Word):Prop :=
  exists ws:list Word, Word_ir_by u v ws.

Lemma Word_ir_by_dr: forall (u v:Word) (l:list Word) (pos:nat),
  Word_ir_by u v l /\ pos < length l - 2 ->
    Word_direct_rel (nth pos l nil) (nth (pos+1) l nil).

Lemma Word_dr_ir: forall u v:Word,
  Word_direct_rel u v -> Word_indirect_rel u v.

Lemma Word_ir_refl: forall u:Word,
  Word_indirect_rel u u.

Lemma Word_ir_sym: forall u v,
  Word_indirect_rel u v <-> Word_indirect_rel v u.

Lemma Word_ir_trans: forall u v w,
  Word_indirect_rel u v -> Word_indirect_rel v w -> Word_indirect_rel u w.

Reduced words.

A word is reduced when it contains no adjacent inverse letters

Definition Word_reduced (u:Word):Prop :=
  ~ (exists v:Word, exists l:Letter, exists pos:nat,
      pos <= length v /\ u = Word_inv_letter_insert v l pos).

Lemma Word_short_red: forall w:Word, length w < 2 -> Word_reduced w.

Lemma Word_ir_exists_reduced: forall w:Word,
  exists v:Word, Word_reduced v /\ Word_indirect_rel w v.

Uniqueness of reduced words.

Proof that every word is ir to a unique reduced word

Idea of the proof: assume some word w has two reduced forms v and u. Then v and u are ir by some minimal chain of intermediate words. The lengths of these intermidiate words must increase and then decrease, since v and u are reduced. Thus there is a particular spot on the chain when the length increases from an insertion and then immediately decreases by a removal of a pair of inverse letters. An argument in cases shows that such a spot in the chain could be bypassed by doing the removal before the insertion, contradicting the assumed minimality of the chain.

Definition length_ir_chain (ws:list Word) :=
  fold_right plus 0 (map (length (A:=Letter)) ws).

Lemma length_ir_chain_app: forall l k:list Word,
  length_ir_chain (l++k) = length_ir_chain l + length_ir_chain k.

Lemma Word_ir_minimal_chain_exists: forall u v:Word,
  Word_indirect_rel u v ->
    (exists l:list Word,
      Word_ir_by u v l /\
      (forall k:list Word,
        Word_ir_by u v k -> length_ir_chain l <= length_ir_chain k)).

Lemma Word_ir_unique_reduced_lemma1:
  forall (a b c:Word) (abl bcl:Letter) (abpos bcpos:nat),
    abpos <= length a /\ bcpos <= length c /\
    b = Word_inv_letter_insert a abl abpos /\
    b = Word_inv_letter_insert c bcl bcpos /\
    (abpos = bcpos \/ abpos + 1 = bcpos)
      -> a = c.

Lemma Word_ir_unique_reduced_lemma2:
  forall (a b c:Word) (abl bcl:Letter) (abpos bcpos:nat),
    abpos <= length a /\ bcpos <= length c /\
    b = Word_inv_letter_insert a abl abpos /\
    b = Word_inv_letter_insert c bcl bcpos /\
    abpos + 1 < bcpos ->
      exists b':Word, (Word_direct_rel a b' /\ Word_direct_rel b' c) /\ length b' < length b.

Theorem Word_ir_unique_reduced: forall w:Word,
  exists ! v:Word, Word_reduced v /\ Word_indirect_rel w v.

Written by P. Christopher Staecker

This page has been generated by coqdoc