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