Initial check-in

diff --git a/FreeGroups.agda b/FreeGroups.agda
new file mode 100644 (file)
index 0000000..83363d1
--- /dev/null
+++ b/FreeGroups.agda
@@ -0,0 +1,179 @@
+open import Relation.Binary
+open import Level
+
+module FreeGroups {c ℓ} (S : Setoid c ℓ) where
+
+open import Relation.Binary.PropositionalEquality as P
+  using (_≡_; _≢_; refl; inspect)
+import Relation.Binary.List.Pointwise as LP
+import Relation.Binary.EqReasoning
+open import Data.Product hiding (map)
+open import Function
+open import Relation.Binary
+import Data.Bool
+open import Data.List
+open import Data.List.Properties
+open import Relation.Nullary
+open import Relation.Nullary.Negation
+open import Data.Empty
+import Algebra.FunctionProperties as FP
+open import Algebra
+
+open import Generators
+
+-- 
+-- G is the set of generators (and their inverses)
+-- Word are the elements of the free group
+--
+
+G : Set c
+G = Setoid.Carrier (setoid S)
+
+Word : Set c
+Word = List G
+
+--
+-- We define a reduction relation, representing the cancellation
+-- of two adjacent elements in a word.
+--
+
+data RedTo : Rel Word c where
+   reds : (xs : Word) → (x : G) → (ys : Word) → RedTo (xs ++ invert₁ x ∷ x ∷ ys) (xs ++ ys)
+
+--
+-- This cancellation is respected by list concatenation.
+--
+
+lem-++-red1 : (zs : Word) → RedTo =[ (λ xs → xs ++ zs) ]⇒ RedTo
+lem-++-red1 zs (reds xs x ys) = P.subst₂ RedTo
+  (P.sym (Monoid.assoc (monoid G) xs (invert₁ x ∷ x ∷ ys) zs))
+  (P.sym (Monoid.assoc (monoid G) xs ys zs))
+  (reds xs x (ys ++ zs))
+
+lem-++-red2 : (zs : Word) → RedTo =[ (λ xs → zs ++ xs) ]⇒ RedTo
+lem-++-red2 zs (reds xs x ys) = P.subst₂ RedTo
+  (Monoid.assoc (monoid G) zs xs (invert₁ x ∷ x ∷ ys))
+  (Monoid.assoc (monoid G) zs xs ys)
+  (reds (zs ++ xs) x ys)
+
+--
+-- The equivalence relation that the free groups are based on is
+-- the equivalence hull of the reduction relation.
+--
+
+_≈f_ : Rel (Word) _
+_≈f_ = EqCl RedTo
+
+--
+-- Inverting a word, which is involutive, commutes with append
+-- and respected the reduction relation
+--
+
+inv : Word → Word
+inv x = reverse (Data.List.map invert₁ x)
+
+inv-inv : FP.Involutive _≡_ inv
+inv-inv x = begin
+  inv (inv x)
+      ≡⟨ P.cong reverse (reverse-map-commute invert₁ (map invert₁ x)) ⟩
+  reverse (reverse (map invert₁ (map invert₁ x)))
+      ≡⟨ reverse-inv (map invert₁ (map invert₁ x)) ⟩
+  map invert₁ (map invert₁ x)
+      ≡⟨ P.sym (map-compose x) ⟩
+  map (invert₁ ∘ invert₁) x
+      ≡⟨ map-cong invert₁-inv x ⟩
+  map id x
+      ≡⟨ map-id x ⟩
+  x ∎
+  where open P.≡-Reasoning
+
+inv-++-commute : (xs ys : Word) → (inv ys ++ inv xs ≡ inv (xs ++ ys))
+inv-++-commute xs ys = begin
+  inv ys ++ inv xs
+    ≡⟨ P.sym (reverse-++-commute (map invert₁ xs) (map invert₁ ys)) ⟩
+  reverse (map invert₁ xs ++ map invert₁ ys)
+    ≡⟨ P.sym (P.cong reverse (map-++-commute invert₁ xs ys)) ⟩ 
+  inv (xs ++ ys) ∎
+  where open P.≡-Reasoning
+
+lem-inv-red : RedTo =[ inv ]⇒ RedTo
+lem-inv-red (reds xs x ys) = P.subst₂ RedTo p1 p2 (reds (inv ys) x (inv xs))
+  where
+    open P.≡-Reasoning
+    p1 = begin
+      inv ys ++ invert₁ x ∷ x ∷ inv xs
+        ≡⟨ P.sym $ P.cong (λ y → inv ys ++ invert₁ x ∷ y ∷ inv xs) $ invert₁-inv x ⟩
+      inv ys ++ invert₁ x ∷ invert₁ (invert₁ x) ∷ inv xs
+        ≡⟨ P.sym $ Monoid.assoc (monoid G) (inv ys) [ invert₁ x ] $ invert₁ (invert₁ x) ∷ inv xs ⟩
+      (inv ys ++ [ invert₁ x ]) ++ invert₁ (invert₁ x) ∷ inv xs
+        ≡⟨ P.cong (λ y → y ++ invert₁ (invert₁ x) ∷ inv xs) $ inv-++-commute [ x ] ys ⟩
+      inv (x ∷ ys) ++ invert₁ (invert₁ x) ∷ inv xs
+        ≡⟨ P.sym $ Monoid.assoc (monoid G) (inv (x ∷ ys)) [ invert₁ (invert₁ x)] (inv xs) ⟩
+      (inv (x ∷ ys) ++ [ invert₁ (invert₁ x) ]) ++ inv xs
+        ≡⟨ P.cong (λ y → y ++ inv xs) $ inv-++-commute [ invert₁ x ] (x ∷ ys) ⟩
+      inv (invert₁ x ∷ x ∷ ys) ++ inv xs
+        ≡⟨ inv-++-commute xs (invert₁ x ∷ x ∷ ys) ⟩
+      inv (xs ++ invert₁ x ∷ x ∷ ys)
+        ∎
+    p2 = inv-++-commute xs ys
+
+--
+-- Here, we define the actual group and check the group axioms
+--
+
+group : Group _ _ 
+group = record {
+  Carrier = Word;
+  _≈_ = _≈f_;
+  _∙_ = _++_;
+  ε = [];
+  _⁻¹ = inv;
+  isGroup = record {
+    isMonoid = record {
+      isSemigroup = record {
+        isEquivalence = L.isEquivalence;
+        assoc = λ x y z → L.reflexive (Monoid.assoc (monoid G) x y z);
+        ∙-cong = cong1
+      };
+      identity = (λ x → L.refl) , (λ x → L.reflexive (proj₂ (Monoid.identity (monoid G)) x))
+    };
+    inverse = linv , rinv;
+    ⁻¹-cong = mapEq lem-inv-red
+    }
+  }
+  where
+  module L = Setoid (eqSetoid RedTo)
+
+  cong1 : {x y u v : Word} → x ≈f y → u ≈f v → (x ++ u) ≈f (y ++ v)
+  cong1 {x} {y} {u} {v} p1 p2 = begin
+    x ++ u
+      ≈⟨ mapEq (lem-++-red1 u) p1 ⟩
+    y ++ u
+      ≈⟨ mapEq (lem-++-red2 y) p2 ⟩
+    y ++ v
+      ∎
+    where
+      open Relation.Binary.EqReasoning (eqSetoid RedTo)
+
+  linv : FP.LeftInverse _≈f_ [] inv _++_
+  linv [] = reflEq
+  linv (x ∷ xs) = begin
+    inv (x ∷ xs) ++ x ∷ xs
+      ≡⟨ P.sym (P.cong (λ y → y ++ x ∷ xs) (inv-++-commute [ x ] xs)) ⟩
+    (inv xs ++ [ invert₁ x ]) ++ x ∷ xs
+      ≡⟨ Monoid.assoc (monoid G) (inv xs) [ invert₁ x ] (x ∷ xs) ⟩
+    inv xs ++ invert₁ x ∷ x ∷ xs
+      ≈⟨ impEq (reds (inv xs) x xs) ⟩
+    inv xs ++ xs
+      ≈⟨ linv xs ⟩
+    [] ∎
+    where open Relation.Binary.EqReasoning (eqSetoid RedTo)
+
+  rinv : FP.RightInverse _≈f_ [] inv _++_
+  rinv x = begin
+    x ++ inv x
+      ≡⟨ P.cong (λ y → y ++ inv x) (P.sym (inv-inv x)) ⟩
+    inv (inv x) ++ inv x
+      ≈⟨ linv (inv x) ⟩
+    [] ∎
+    where open  Relation.Binary.EqReasoning (eqSetoid RedTo)

diff --git a/Generators.agda b/Generators.agda
new file mode 100644 (file)
index 0000000..88cefd6
--- /dev/null
+++ b/Generators.agda
@@ -0,0 +1,160 @@
+module Generators where
+
+open import Level
+open import Relation.Binary.PropositionalEquality as P
+  using (_≡_; _≢_; refl; inspect)
+import Relation.Binary.List.Pointwise as LP
+open import Function
+open import Relation.Binary
+open import Data.List
+open import Data.List.Properties
+open import Relation.Nullary
+import Algebra.FunctionProperties as FP
+
+-- Free Groups are built upon sets of generators. These can occur directly
+-- or as their abstract inverse:
+
+data Gen {c} (A : Set c) : Set c where
+  gen : A → Gen A
+  gen-inv : A → Gen A
+
+-- Inverting one generator is an involutive operation.
+
+invert₁ : ∀{a} → {A : Set a} → Gen A → Gen A
+invert₁ (gen x) = (gen-inv x)
+invert₁ (gen-inv x) = (gen x)
+
+invert₁-inv : ∀{a} {A : Set a} → FP.Involutive _≡_ (invert₁ {a} {A})
+invert₁-inv (gen x) = refl
+invert₁-inv (gen-inv x) = refl
+
+-- An equivalence relation (setoid, decidable setoid) of the underlying
+-- setinduces an equivalence relation (setoid, decidable setoid) on the generators.
+
+data LiftGen {a ℓ} {A : Set a} (_~_ : Rel A ℓ) : Gen A → Gen A → Set (a ⊔ ℓ)  where
+  gen : {x y : A} → (x ~ y) → LiftGen _~_ (gen x) (gen y)
+  gen-inv : {x y : A } → (x ~ y) → LiftGen _~_ (gen-inv x) (gen-inv y)
+
+unLiftGen : ∀{a ℓ} {A : Set a} {_~_ : Rel A ℓ} {a b : _} →
+  LiftGen _~_ (gen a) (gen b) → a ~ b
+unLiftGen (gen y) = y
+
+unLiftGenInv : ∀{a ℓ} {A : Set a} {_~_ : Rel A ℓ} {a b : _} →
+  LiftGen _~_ (gen-inv a) (gen-inv b) → a ~ b
+unLiftGenInv (gen-inv y) = y
+
+genIsDec : ∀{a ℓ} {A : Set a} { _~_ : Rel A ℓ} → Decidable _~_ →
+  Decidable (LiftGen _~_)
+genIsDec d (gen a) (gen b) with d a b 
+... | yes p = yes (gen p)
+... | no p = no (p ∘ unLiftGen)
+genIsDec d (gen a) (gen-inv b) = no (λ ())
+genIsDec d (gen-inv a) (gen b) = no (λ ())
+genIsDec d (gen-inv a) (gen-inv b) with d a b
+... | yes p = yes (gen-inv p)
+... | no p = no (p ∘ unLiftGenInv)
+
+genIsEquivalence : ∀{a ℓ} {A : Set a} { _~_ : Rel A ℓ} → IsEquivalence _~_ →
+  IsEquivalence (LiftGen _~_)
+genIsEquivalence {_} {_} {A} {_~_} e =
+  record  { refl = r ; sym = sym ; trans = trans }
+  where module E = IsEquivalence e
+        _≈_ = LiftGen _~_ 
+    
+        r : {x : Gen A} → LiftGen _~_ x x
+        r {gen y} = gen E.refl
+        r {gen-inv y} = gen-inv E.refl
+  
+        sym : ∀ {x y} → LiftGen _~_ x y → LiftGen _~_ y x
+        sym (gen p) = gen (E.sym p)
+        sym (gen-inv p) = gen-inv (E.sym p)
+
+        trans : ∀ {x y z} → x ≈ y → y ≈ z → x ≈ z
+        trans (gen p1) (gen p2) = gen (E.trans p1 p2)
+        trans (gen-inv p1) (gen-inv p2) = gen-inv (E.trans p1 p2)
+
+
+genIsDecEquivalence : ∀{a ℓ} {A : Set a} {_≈_ : Rel A ℓ} → IsDecEquivalence _≈_ →
+  IsDecEquivalence (LiftGen _≈_)
+genIsDecEquivalence d = record {
+  isEquivalence = genIsEquivalence (IsDecEquivalence.isEquivalence d);
+  _≟_ = genIsDec (IsDecEquivalence._≟_ d)
+  }
+
+setoid : ∀{a ℓ} → Setoid a ℓ → Setoid _ _
+setoid s = record {
+  isEquivalence = genIsEquivalence (Setoid.isEquivalence s)
+  }
+
+decSetoid : ∀{a ℓ} → DecSetoid a ℓ → DecSetoid _ _
+decSetoid d = record {
+  isDecEquivalence = genIsDecEquivalence (DecSetoid.isDecEquivalence d)
+  }
+
+--
+-- Transitive reflexive symmetric hull of a relation. Ought to go to some standard library
+--
+
+data EqCl {c ℓ} {A : Set c} (R : Rel {c} A ℓ) : Rel A ℓ where
+  impEq : R ⇒ EqCl R
+  symEq : Symmetric (EqCl R)
+  reflEq : Reflexive (EqCl R)
+  transEq : Trans (EqCl R) (EqCl R) (EqCl R)
+
+eqSetoid : ∀{ℓ} → {A : Set ℓ} → (_⟶_ : Rel A ℓ) → Setoid _ _
+eqSetoid  _⟶_ = record {
+  _≈_ = EqCl _⟶_;
+  isEquivalence = record { refl = reflEq ; sym = symEq ; trans = transEq}
+  }
+
+--
+-- A function that respects the underlying relation also respects its transitive
+-- reflexive symmetric hull.
+--
+
+mapEq : ∀{ℓ} → {A : Set ℓ} → {T : Rel A ℓ} → {f : A → A } →
+      T =[ f ]⇒ T → EqCl T =[ f ]⇒ EqCl T
+mapEq p (impEq y) = impEq (p y)
+mapEq p (symEq y) = symEq (mapEq p y)
+mapEq p reflEq = reflEq
+mapEq p (transEq y' y0) = transEq (mapEq p y') (mapEq p y0)
+
+
+--
+-- Utility lemmata that went into the standard library, but has not released yet.
+--
+
+reverse-map-commute :
+  ∀ {a b} {A : Set a} {B : Set b} (f : A → B) → (xs : List A) →
+  map f (reverse xs) ≡ reverse (map f xs)
+reverse-map-commute f [] = refl
+reverse-map-commute f (x ∷ xs) = begin
+  map f (reverse (x ∷ xs))
+    ≡⟨ P.cong (map f) (unfold-reverse x xs) ⟩
+  map f (reverse xs ∷ʳ x)
+    ≡⟨ map-++-commute f (reverse xs) (x ∷ []) ⟩
+  map f (reverse xs) ∷ʳ f x
+    ≡⟨ P.cong (λ y → y ∷ʳ f x) (reverse-map-commute f xs) ⟩
+  reverse (map f xs) ∷ʳ f x
+    ≡⟨ P.sym (unfold-reverse (f x) (map f xs)) ⟩
+  reverse (map f (x ∷ xs))
+    ∎
+  where
+    open P.≡-Reasoning
+
+reverse-inv : ∀{a} {A : Set a} → FP.Involutive {_} {_} {List A} _≡_ reverse
+reverse-inv [] = refl
+reverse-inv (x ∷ xs) = begin
+  reverse (reverse (x ∷ xs))
+    ≡⟨ P.cong reverse (unfold-reverse x xs) ⟩
+  reverse (reverse xs ∷ʳ x)
+    ≡⟨ reverse-++-commute (reverse xs) (x ∷ []) ⟩
+  x ∷ reverse (reverse (xs))
+    ≡⟨ P.cong (λ y → x ∷ y) (reverse-inv xs) ⟩
+  x ∷ xs
+    ∎
+  where
+    open P.≡-Reasoning
+
+
+

diff --git a/NormalForm.agda b/NormalForm.agda
new file mode 100644 (file)
index 0000000..9c8bb69
--- /dev/null
+++ b/NormalForm.agda
@@ -0,0 +1,79 @@
+--
+-- 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)