1 open import Relation.Binary
3 module FreeGroups {c ℓ} (S : Setoid c ℓ) where
5 open import Relation.Binary.PropositionalEquality as P
6   using (_≡_; _≢_; refl; inspect)
7 import Relation.Binary.List.Pointwise as LP
8 import Relation.Binary.EqReasoning
9 open import Data.Product hiding (map)
10 open import Function
11 open import Relation.Binary
12 import Data.Bool
13 open import Data.List
14 open import Data.List.Properties
15 open import Relation.Nullary
16 open import Relation.Nullary.Negation
17 open import Data.Empty
18 import Algebra.FunctionProperties as FP
19 open import Algebra
21 open import Generators
23 --
24 -- G is the set of generators (and their inverses)
25 -- Word are the elements of the free group
26 --
28 G : Set c
29 G = Setoid.Carrier (setoid S)
31 Word : Set c
32 Word = List G
34 --
35 -- We define a reduction relation, representing the cancellation
36 -- of two adjacent elements in a word.
37 --
39 data RedTo : Rel Word c where
40    reds : (xs : Word) → (x : G) → (ys : Word) → RedTo (xs ++ invert₁ x ∷ x ∷ ys) (xs ++ ys)
42 --
43 -- This cancellation is respected by list concatenation.
44 --
46 lem-++-red1 : (zs : Word) → RedTo =[ (λ xs → xs ++ zs) ]⇒ RedTo
47 lem-++-red1 zs (reds xs x ys) = P.subst₂ RedTo
48   (P.sym (Monoid.assoc (monoid G) xs (invert₁ x ∷ x ∷ ys) zs))
49   (P.sym (Monoid.assoc (monoid G) xs ys zs))
50   (reds xs x (ys ++ zs))
52 lem-++-red2 : (zs : Word) → RedTo =[ (λ xs → zs ++ xs) ]⇒ RedTo
53 lem-++-red2 zs (reds xs x ys) = P.subst₂ RedTo
54   (Monoid.assoc (monoid G) zs xs (invert₁ x ∷ x ∷ ys))
55   (Monoid.assoc (monoid G) zs xs ys)
56   (reds (zs ++ xs) x ys)
58 --
59 -- The equivalence relation that the free groups are based on is
60 -- the equivalence hull of the reduction relation.
61 --
63 _≈f_ : Rel (Word) _
64 _≈f_ = EqCl RedTo
66 --
67 -- Inverting a word, which is involutive, commutes with append
68 -- and respected the reduction relation
69 --
71 inv : Word → Word
72 inv x = reverse (Data.List.map invert₁ x)
74 inv-inv : FP.Involutive _≡_ inv
75 inv-inv x = begin
76   inv (inv x)
77       ≡⟨ P.cong reverse (reverse-map-commute invert₁ (map invert₁ x)) ⟩
78   reverse (reverse (map invert₁ (map invert₁ x)))
79       ≡⟨ reverse-inv (map invert₁ (map invert₁ x)) ⟩
80   map invert₁ (map invert₁ x)
81       ≡⟨ P.sym (map-compose x) ⟩
82   map (invert₁ ∘ invert₁) x
83       ≡⟨ map-cong invert₁-inv x ⟩
84   map id x
85       ≡⟨ map-id x ⟩
86   x ∎
87   where open P.≡-Reasoning
89 inv-++-commute : (xs ys : Word) → (inv ys ++ inv xs ≡ inv (xs ++ ys))
90 inv-++-commute xs ys = begin
91   inv ys ++ inv xs
92     ≡⟨ P.sym (reverse-++-commute (map invert₁ xs) (map invert₁ ys)) ⟩
93   reverse (map invert₁ xs ++ map invert₁ ys)
94     ≡⟨ P.sym (P.cong reverse (map-++-commute invert₁ xs ys)) ⟩
95   inv (xs ++ ys) ∎
96   where open P.≡-Reasoning
98 lem-inv-red : RedTo =[ inv ]⇒ RedTo
99 lem-inv-red (reds xs x ys) = P.subst₂ RedTo p1 p2 (reds (inv ys) x (inv xs))
100   where
101     open P.≡-Reasoning
102     p1 = begin
103       inv ys ++ invert₁ x ∷ x ∷ inv xs
104         ≡⟨ P.sym \$ P.cong (λ y → inv ys ++ invert₁ x ∷ y ∷ inv xs) \$ invert₁-inv x ⟩
105       inv ys ++ invert₁ x ∷ invert₁ (invert₁ x) ∷ inv xs
106         ≡⟨ P.sym \$ Monoid.assoc (monoid G) (inv ys) [ invert₁ x ] \$ invert₁ (invert₁ x) ∷ inv xs ⟩
107       (inv ys ++ [ invert₁ x ]) ++ invert₁ (invert₁ x) ∷ inv xs
108         ≡⟨ P.cong (λ y → y ++ invert₁ (invert₁ x) ∷ inv xs) \$ inv-++-commute [ x ] ys ⟩
109       inv (x ∷ ys) ++ invert₁ (invert₁ x) ∷ inv xs
110         ≡⟨ P.sym \$ Monoid.assoc (monoid G) (inv (x ∷ ys)) [ invert₁ (invert₁ x)] (inv xs) ⟩
111       (inv (x ∷ ys) ++ [ invert₁ (invert₁ x) ]) ++ inv xs
112         ≡⟨ P.cong (λ y → y ++ inv xs) \$ inv-++-commute [ invert₁ x ] (x ∷ ys) ⟩
113       inv (invert₁ x ∷ x ∷ ys) ++ inv xs
114         ≡⟨ inv-++-commute xs (invert₁ x ∷ x ∷ ys) ⟩
115       inv (xs ++ invert₁ x ∷ x ∷ ys)
116         ∎
117     p2 = inv-++-commute xs ys
119 --
120 -- Here, we define the actual group and check the group axioms
121 --
123 group : Group _ _
124 group = record {
125   Carrier = Word;
126   _≈_ = _≈f_;
127   _∙_ = _++_;
128   ε = [];
129   _⁻¹ = inv;
130   isGroup = record {
131     isMonoid = record {
132       isSemigroup = record {
133         isEquivalence = L.isEquivalence;
134         assoc = λ x y z → L.reflexive (Monoid.assoc (monoid G) x y z);
135         ∙-cong = cong1
136       };
137       identity = (λ x → L.refl) , (λ x → L.reflexive (proj₂ (Monoid.identity (monoid G)) x))
138     };
139     inverse = linv , rinv;
140     ⁻¹-cong = mapEq lem-inv-red
141     }
142   }
143   where
144   module L = Setoid (eqSetoid RedTo)
146   cong1 : {x y u v : Word} → x ≈f y → u ≈f v → (x ++ u) ≈f (y ++ v)
147   cong1 {x} {y} {u} {v} p1 p2 = begin
148     x ++ u
149       ≈⟨ mapEq (lem-++-red1 u) p1 ⟩
150     y ++ u
151       ≈⟨ mapEq (lem-++-red2 y) p2 ⟩
152     y ++ v
153       ∎
154     where
155       open Relation.Binary.EqReasoning (eqSetoid RedTo)
157   linv : FP.LeftInverse _≈f_ [] inv _++_
158   linv [] = reflEq
159   linv (x ∷ xs) = begin
160     inv (x ∷ xs) ++ x ∷ xs
161       ≡⟨ P.sym (P.cong (λ y → y ++ x ∷ xs) (inv-++-commute [ x ] xs)) ⟩
162     (inv xs ++ [ invert₁ x ]) ++ x ∷ xs
163       ≡⟨ Monoid.assoc (monoid G) (inv xs) [ invert₁ x ] (x ∷ xs) ⟩
164     inv xs ++ invert₁ x ∷ x ∷ xs
165       ≈⟨ impEq (reds (inv xs) x xs) ⟩
166     inv xs ++ xs
167       ≈⟨ linv xs ⟩
168     [] ∎
169     where open Relation.Binary.EqReasoning (eqSetoid RedTo)
171   rinv : FP.RightInverse _≈f_ [] inv _++_
172   rinv x = begin
173     x ++ inv x
174       ≡⟨ P.cong (λ y → y ++ inv x) (P.sym (inv-inv x)) ⟩
175     inv (inv x) ++ inv x
176       ≈⟨ linv (inv x) ⟩
177     [] ∎
178     where open  Relation.Binary.EqReasoning (eqSetoid RedTo)