FreeGroups.agda

   1 open import Relation.Binary
   2
   3 module FreeGroups {c ℓ} (S : Setoid c ℓ) where
   4
   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
  20
  21 open import Generators
  22
  23 --
  24 -- G is the set of generators (and their inverses)
  25 -- Word are the elements of the free group
  26 --
  27
  28 G : Set c
  29 G = Setoid.Carrier (setoid S)
  30
  31 Word : Set c
  32 Word = List G
  33
  34 --
  35 -- We define a reduction relation, representing the cancellation
  36 -- of two adjacent elements in a word.
  37 --
  38
  39 data RedTo : Rel Word c where
  40    reds : (xs : Word) → (x : G) → (ys : Word) → RedTo (xs ++ invert₁ x ∷ x ∷ ys) (xs ++ ys)
  41
  42 --
  43 -- This cancellation is respected by list concatenation.
  44 --
  45
  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))
  51
  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)
  57
  58 --
  59 -- The equivalence relation that the free groups are based on is
  60 -- the equivalence hull of the reduction relation.
  61 --
  62
  63 _≈f_ : Rel (Word) _
  64 _≈f_ = EqCl RedTo
  65
  66 --
  67 -- Inverting a word, which is involutive, commutes with append
  68 -- and respected the reduction relation
  69 --
  70
  71 inv : Word → Word
  72 inv x = reverse (Data.List.map invert₁ x)
  73
  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
  88
  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
  97
  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
 118
 119 --
 120 -- Here, we define the actual group and check the group axioms
 121 --
 122
 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)
 145
 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)
 156
 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)
 170
 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)