1 --
2 -- Reduced words. Every equivalence class in the free group has a unique fully reduced word.
3 --
4 -- Findind this fully reduced word is possibe, but needs the underlying Setoid to have decidable equalit
6 open import Relation.Binary
7 open import Level
9 module NormalForm {c ℓ} (S : DecSetoid c ℓ) where
11 open import Relation.Binary.PropositionalEquality as P
12   using (_≡_; _≢_; refl; inspect)
13 import Relation.Binary.EqReasoning
14 open import Data.Product hiding (map)
15 open import Function
16 open import Data.List
17 open import Data.List.Properties
18 open import Relation.Nullary
20 open import Generators
21 import FreeGroups
22 open module F = FreeGroups (DecSetoid.setoid S)
24 -- Decidable equality on generators
25 open DecSetoid (Generators.decSetoid S) using (_≟_; _≈_)
27 Reduced : Word → Set _
28 Reduced x = ∄ (λ y → RedTo x y)
30 _∷f_ : G → Word → Word
31 _∷f_ g [] = g ∷ []
32 _∷f_ g (x ∷ xs) with g ≟ invert₁ x
33 ... | yes p = xs
34 ... | no ¬p = g ∷ x ∷ xs
36 tailReduced : ∀{x xs} → Reduced (x ∷ xs) → Reduced xs
37 tailReduced {x} p (.(xs ++ ys) , reds xs x' ys) = p ((x ∷ xs ++ ys) , (reds (x ∷ xs) x' ys))
39 consReduced : ∀{x y ys l} → ¬ x ≈ invert₁ y → Reduced (y ∷ ys) → l ≡ x ∷ y ∷ ys → Reduced l
40 consReduced {x} {y} ¬e _ eq (.ys' , reds [] x' ys') = ¬e \$
41   begin x ≡⟨ P.sym eq1 ⟩ invert₁ x' ≡⟨ P.cong _ eq2 ⟩ invert₁ y ∎
42   where eq1 = proj₁ (∷-injective eq)
43         eq2 = proj₁ (∷-injective (proj₂ (∷-injective eq)))
44         open Relation.Binary.EqReasoning (Generators.setoid (DecSetoid.setoid S))
45 consReduced ¬e ¬r eq (.(x' ∷ xs ++ ys) , reds (x' ∷ xs) x0 ys) with ∷-injective eq
46 ... | (eq1 , eq2) =  ¬r (xs ++ ys , (
47                P.subst (λ y → RedTo y (xs ++ ys)) eq2 \$
48                P.subst (λ y → RedTo (xs ++ invert₁ x0 ∷ x0 ∷ ys) (xs ++ ys)) eq1 \$
49                reds xs x0 ys))
51 lem-[]-red' : ∀{xs} → xs ≡ [] → Reduced xs
52 lem-[]-red' () (.ys , reds [] x ys)
53 lem-[]-red' () (.(x ∷ xs ++ ys) , reds (x ∷ xs) x' ys)
55 lem-[]-red : Reduced []
56 lem-[]-red = lem-[]-red' refl
58 lem-[x]-red' : ∀{xs} (x : G) → xs ≡ [ x ] → Reduced xs
59 lem-[x]-red' _ () (.ys , reds [] x' ys)
60 lem-[x]-red' _ () (.(x' ∷ ys) , reds (x' ∷ []) x0 ys)
61 lem-[x]-red' _ () (.(x' ∷ x0 ∷ xs ++ ys) , reds (x' ∷ x0 ∷ xs) x1 ys)
63 lem-[x]-red : (x : G) → Reduced [ x ]
64 lem-[x]-red x = lem-[x]-red' x refl
67 lem-∷f : ∀{x xs} → Reduced xs → Reduced (x ∷f xs)
68 lem-∷f {xs = []} _ = lem-[x]-red _
69 lem-∷f {x} {xs = y ∷ ys} r with x ≟ invert₁ y
70 ... | yes _ = tailReduced r
71 ... | no ¬p  = consReduced ¬p r P.refl
74 normalize : Word → Word
75 normalize l = foldr _∷f_ [] l
77 lem-normalized : (xs : List G) → Reduced (normalize xs)
78 lem-normalized [] = lem-[]-red
79 lem-normalized (x ∷ xs) = lem-∷f (lem-normalized xs)