-- -- Reduced words. Every equivalence class in the free group has a unique fully reduced word. -- -- Findind this fully reduced word is possibe, but needs the underlying Setoid to have decidable equalit open import Relation.Binary open import Level module NormalForm {c ℓ} (S : DecSetoid c ℓ) where open import Relation.Binary.PropositionalEquality as P using (_≡_; _≢_; refl; inspect) import Relation.Binary.EqReasoning open import Data.Product hiding (map) open import Function open import Data.List open import Data.List.Properties open import Relation.Nullary open import Generators import FreeGroups open module F = FreeGroups (DecSetoid.setoid S) -- Decidable equality on generators open DecSetoid (Generators.decSetoid S) using (_≟_; _≈_) Reduced : Word → Set _ Reduced x = ∄ (λ y → RedTo x y) _∷f_ : G → Word → Word _∷f_ g [] = g ∷ [] _∷f_ g (x ∷ xs) with g ≟ invert₁ x ... | yes p = xs ... | no ¬p = g ∷ x ∷ xs tailReduced : ∀{x xs} → Reduced (x ∷ xs) → Reduced xs tailReduced {x} p (.(xs ++ ys) , reds xs x' ys) = p ((x ∷ xs ++ ys) , (reds (x ∷ xs) x' ys)) consReduced : ∀{x y ys l} → ¬ x ≈ invert₁ y → Reduced (y ∷ ys) → l ≡ x ∷ y ∷ ys → Reduced l consReduced {x} {y} ¬e _ eq (.ys' , reds [] x' ys') = ¬e \$ begin x ≡⟨ P.sym eq1 ⟩ invert₁ x' ≡⟨ P.cong _ eq2 ⟩ invert₁ y ∎ where eq1 = proj₁ (∷-injective eq) eq2 = proj₁ (∷-injective (proj₂ (∷-injective eq))) open Relation.Binary.EqReasoning (Generators.setoid (DecSetoid.setoid S)) consReduced ¬e ¬r eq (.(x' ∷ xs ++ ys) , reds (x' ∷ xs) x0 ys) with ∷-injective eq ... | (eq1 , eq2) = ¬r (xs ++ ys , ( P.subst (λ y → RedTo y (xs ++ ys)) eq2 \$ P.subst (λ y → RedTo (xs ++ invert₁ x0 ∷ x0 ∷ ys) (xs ++ ys)) eq1 \$ reds xs x0 ys)) lem-[]-red' : ∀{xs} → xs ≡ [] → Reduced xs lem-[]-red' () (.ys , reds [] x ys) lem-[]-red' () (.(x ∷ xs ++ ys) , reds (x ∷ xs) x' ys) lem-[]-red : Reduced [] lem-[]-red = lem-[]-red' refl lem-[x]-red' : ∀{xs} (x : G) → xs ≡ [ x ] → Reduced xs lem-[x]-red' _ () (.ys , reds [] x' ys) lem-[x]-red' _ () (.(x' ∷ ys) , reds (x' ∷ []) x0 ys) lem-[x]-red' _ () (.(x' ∷ x0 ∷ xs ++ ys) , reds (x' ∷ x0 ∷ xs) x1 ys) lem-[x]-red : (x : G) → Reduced [ x ] lem-[x]-red x = lem-[x]-red' x refl lem-∷f : ∀{x xs} → Reduced xs → Reduced (x ∷f xs) lem-∷f {xs = []} _ = lem-[x]-red _ lem-∷f {x} {xs = y ∷ ys} r with x ≟ invert₁ y ... | yes _ = tailReduced r ... | no ¬p = consReduced ¬p r P.refl normalize : Word → Word normalize l = foldr _∷f_ [] l lem-normalized : (xs : List G) → Reduced (normalize xs) lem-normalized [] = lem-[]-red lem-normalized (x ∷ xs) = lem-∷f (lem-normalized xs)