Initial check-in
[darcs-mirror-agda-free-groups.git] / Generators.agda
1 module Generators where
2
3 open import Level
4 open import Relation.Binary.PropositionalEquality as P
5   using (_≡_; _≢_; refl; inspect)
6 import Relation.Binary.List.Pointwise as LP
7 open import Function
8 open import Relation.Binary
9 open import Data.List
10 open import Data.List.Properties
11 open import Relation.Nullary
12 import Algebra.FunctionProperties as FP
13
14 -- Free Groups are built upon sets of generators. These can occur directly
15 -- or as their abstract inverse:
16
17 data Gen {c} (A : Set c) : Set c where
18   gen : A → Gen A
19   gen-inv : A → Gen A
20
21 -- Inverting one generator is an involutive operation.
22
23 invert₁ : ∀{a} → {A : Set a} → Gen A → Gen A
24 invert₁ (gen x) = (gen-inv x)
25 invert₁ (gen-inv x) = (gen x)
26
27 invert₁-inv : ∀{a} {A : Set a} → FP.Involutive _≡_ (invert₁ {a} {A})
28 invert₁-inv (gen x) = refl
29 invert₁-inv (gen-inv x) = refl
30
31 -- An equivalence relation (setoid, decidable setoid) of the underlying
32 -- setinduces an equivalence relation (setoid, decidable setoid) on the generators.
33
34 data LiftGen {a ℓ} {A : Set a} (_~_ : Rel A ℓ) : Gen A → Gen A → Set (a ⊔ ℓ)  where
35   gen : {x y : A} → (x ~ y) → LiftGen _~_ (gen x) (gen y)
36   gen-inv : {x y : A } → (x ~ y) → LiftGen _~_ (gen-inv x) (gen-inv y)
37
38 unLiftGen : ∀{a ℓ} {A : Set a} {_~_ : Rel A ℓ} {a b : _} →
39   LiftGen _~_ (gen a) (gen b) → a ~ b
40 unLiftGen (gen y) = y
41
42 unLiftGenInv : ∀{a ℓ} {A : Set a} {_~_ : Rel A ℓ} {a b : _} →
43   LiftGen _~_ (gen-inv a) (gen-inv b) → a ~ b
44 unLiftGenInv (gen-inv y) = y
45
46 genIsDec : ∀{a ℓ} {A : Set a} { _~_ : Rel A ℓ} → Decidable _~_ →
47   Decidable (LiftGen _~_)
48 genIsDec d (gen a) (gen b) with d a b 
49 ... | yes p = yes (gen p)
50 ... | no p = no (p ∘ unLiftGen)
51 genIsDec d (gen a) (gen-inv b) = no (λ ())
52 genIsDec d (gen-inv a) (gen b) = no (λ ())
53 genIsDec d (gen-inv a) (gen-inv b) with d a b
54 ... | yes p = yes (gen-inv p)
55 ... | no p = no (p ∘ unLiftGenInv)
56
57 genIsEquivalence : ∀{a ℓ} {A : Set a} { _~_ : Rel A ℓ} → IsEquivalence _~_ →
58   IsEquivalence (LiftGen _~_)
59 genIsEquivalence {_} {_} {A} {_~_} e =
60   record  { refl = r ; sym = sym ; trans = trans }
61   where module E = IsEquivalence e
62         _≈_ = LiftGen _~_ 
63     
64         r : {x : Gen A} → LiftGen _~_ x x
65         r {gen y} = gen E.refl
66         r {gen-inv y} = gen-inv E.refl
67   
68         sym : ∀ {x y} → LiftGen _~_ x y → LiftGen _~_ y x
69         sym (gen p) = gen (E.sym p)
70         sym (gen-inv p) = gen-inv (E.sym p)
71
72         trans : ∀ {x y z} → x ≈ y → y ≈ z → x ≈ z
73         trans (gen p1) (gen p2) = gen (E.trans p1 p2)
74         trans (gen-inv p1) (gen-inv p2) = gen-inv (E.trans p1 p2)
75
76
77 genIsDecEquivalence : ∀{a ℓ} {A : Set a} {_≈_ : Rel A ℓ} → IsDecEquivalence _≈_ →
78   IsDecEquivalence (LiftGen _≈_)
79 genIsDecEquivalence d = record {
80   isEquivalence = genIsEquivalence (IsDecEquivalence.isEquivalence d);
81   _≟_ = genIsDec (IsDecEquivalence._≟_ d)
82   }
83
84 setoid : ∀{a ℓ} → Setoid a ℓ → Setoid _ _
85 setoid s = record {
86   isEquivalence = genIsEquivalence (Setoid.isEquivalence s)
87   }
88
89 decSetoid : ∀{a ℓ} → DecSetoid a ℓ → DecSetoid _ _
90 decSetoid d = record {
91   isDecEquivalence = genIsDecEquivalence (DecSetoid.isDecEquivalence d)
92   }
93
94 --
95 -- Transitive reflexive symmetric hull of a relation. Ought to go to some standard library
96 --
97
98 data EqCl {c ℓ} {A : Set c} (R : Rel {c} A ℓ) : Rel A ℓ where
99   impEq : R ⇒ EqCl R
100   symEq : Symmetric (EqCl R)
101   reflEq : Reflexive (EqCl R)
102   transEq : Trans (EqCl R) (EqCl R) (EqCl R)
103
104 eqSetoid : ∀{ℓ} → {A : Set ℓ} → (_⟶_ : Rel A ℓ) → Setoid _ _
105 eqSetoid  _⟶_ = record {
106   _≈_ = EqCl _⟶_;
107   isEquivalence = record { refl = reflEq ; sym = symEq ; trans = transEq}
108   }
109
110 --
111 -- A function that respects the underlying relation also respects its transitive
112 -- reflexive symmetric hull.
113 --
114
115 mapEq : ∀{ℓ} → {A : Set ℓ} → {T : Rel A ℓ} → {f : A → A } →
116       T =[ f ]⇒ T → EqCl T =[ f ]⇒ EqCl T
117 mapEq p (impEq y) = impEq (p y)
118 mapEq p (symEq y) = symEq (mapEq p y)
119 mapEq p reflEq = reflEq
120 mapEq p (transEq y' y0) = transEq (mapEq p y') (mapEq p y0)
121
122
123 --
124 -- Utility lemmata that went into the standard library, but has not released yet.
125 --
126
127 reverse-map-commute :
128   ∀ {a b} {A : Set a} {B : Set b} (f : A → B) → (xs : List A) →
129   map f (reverse xs) ≡ reverse (map f xs)
130 reverse-map-commute f [] = refl
131 reverse-map-commute f (x ∷ xs) = begin
132   map f (reverse (x ∷ xs))
133     ≡⟨ P.cong (map f) (unfold-reverse x xs) ⟩
134   map f (reverse xs ∷ʳ x)
135     ≡⟨ map-++-commute f (reverse xs) (x ∷ []) ⟩
136   map f (reverse xs) ∷ʳ f x
137     ≡⟨ P.cong (λ y → y ∷ʳ f x) (reverse-map-commute f xs) ⟩
138   reverse (map f xs) ∷ʳ f x
139     ≡⟨ P.sym (unfold-reverse (f x) (map f xs)) ⟩
140   reverse (map f (x ∷ xs))
141     ∎
142   where
143     open P.≡-Reasoning
144
145 reverse-inv : ∀{a} {A : Set a} → FP.Involutive {_} {_} {List A} _≡_ reverse
146 reverse-inv [] = refl
147 reverse-inv (x ∷ xs) = begin
148   reverse (reverse (x ∷ xs))
149     ≡⟨ P.cong reverse (unfold-reverse x xs) ⟩
150   reverse (reverse xs ∷ʳ x)
151     ≡⟨ reverse-++-commute (reverse xs) (x ∷ []) ⟩
152   x ∷ reverse (reverse (xs))
153     ≡⟨ P.cong (λ y → x ∷ y) (reverse-inv xs) ⟩
154   x ∷ xs
155     ∎
156   where
157     open P.≡-Reasoning
158
159
160