1 module Generators where
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
14 -- Free Groups are built upon sets of generators. These can occur directly
15 -- or as their abstract inverse:
17 data Gen {c} (A : Set c) : Set c where
18   gen : A → Gen A
19   gen-inv : A → Gen A
21 -- Inverting one generator is an involutive operation.
23 invert₁ : ∀{a} → {A : Set a} → Gen A → Gen A
24 invert₁ (gen x) = (gen-inv x)
25 invert₁ (gen-inv x) = (gen x)
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
31 -- An equivalence relation (setoid, decidable setoid) of the underlying
32 -- setinduces an equivalence relation (setoid, decidable setoid) on the generators.
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)
38 unLiftGen : ∀{a ℓ} {A : Set a} {_~_ : Rel A ℓ} {a b : _} →
39   LiftGen _~_ (gen a) (gen b) → a ~ b
40 unLiftGen (gen y) = y
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
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)
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 _~_
64         r : {x : Gen A} → LiftGen _~_ x x
65         r {gen y} = gen E.refl
66         r {gen-inv y} = gen-inv E.refl
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)
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)
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   }
84 setoid : ∀{a ℓ} → Setoid a ℓ → Setoid _ _
85 setoid s = record {
86   isEquivalence = genIsEquivalence (Setoid.isEquivalence s)
87   }
89 decSetoid : ∀{a ℓ} → DecSetoid a ℓ → DecSetoid _ _
90 decSetoid d = record {
91   isDecEquivalence = genIsDecEquivalence (DecSetoid.isDecEquivalence d)
92   }
94 --
95 -- Transitive reflexive symmetric hull of a relation. Ought to go to some standard library
96 --
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)
104 eqSetoid : ∀{ℓ} → {A : Set ℓ} → (_⟶_ : Rel A ℓ) → Setoid _ _
105 eqSetoid  _⟶_ = record {
106   _≈_ = EqCl _⟶_;
107   isEquivalence = record { refl = reflEq ; sym = symEq ; trans = transEq}
108   }
110 --
111 -- A function that respects the underlying relation also respects its transitive
112 -- reflexive symmetric hull.
113 --
115 liftEqCl : ∀{c d ℓ ℓ2} → {A : Set c} → {B : Setoid d ℓ} → {T : Rel A ℓ2} → {f : A → Setoid.Carrier B } → T =[ f ]⇒ Setoid._≈_ B → EqCl T =[ f ]⇒ Setoid._≈_ B
116 liftEqCl p (impEq y) = p y
117 liftEqCl {B = B} p (symEq y) = Setoid.sym B (liftEqCl {B = B} p y)
118 liftEqCl {B = B} p reflEq = Setoid.refl B
119 liftEqCl {B = B} p (transEq y y') = Setoid.trans B (liftEqCl {B = B} p y) (liftEqCl {B = B} p y')
121 mapEq : ∀{ℓ} → {A : Set ℓ} → {T : Rel A ℓ} → {f : A → A } →
122       T =[ f ]⇒ T → EqCl T =[ f ]⇒ EqCl T
123 mapEq {T = T} p = liftEqCl {B = eqSetoid T} (impEq ∘ p)
125 --
126 -- Utility lemmata that went into the standard library, but has not released yet.
127 --
129 reverse-map-commute :
130   ∀ {a b} {A : Set a} {B : Set b} (f : A → B) → (xs : List A) →
131   map f (reverse xs) ≡ reverse (map f xs)
132 reverse-map-commute f [] = refl
133 reverse-map-commute f (x ∷ xs) = begin
134   map f (reverse (x ∷ xs))
135     ≡⟨ P.cong (map f) (unfold-reverse x xs) ⟩
136   map f (reverse xs ∷ʳ x)
137     ≡⟨ map-++-commute f (reverse xs) (x ∷ []) ⟩
138   map f (reverse xs) ∷ʳ f x
139     ≡⟨ P.cong (λ y → y ∷ʳ f x) (reverse-map-commute f xs) ⟩
140   reverse (map f xs) ∷ʳ f x
141     ≡⟨ P.sym (unfold-reverse (f x) (map f xs)) ⟩
142   reverse (map f (x ∷ xs))
143     ∎
144   where
145     open P.≡-Reasoning
147 reverse-inv : ∀{a} {A : Set a} → FP.Involutive {_} {_} {List A} _≡_ reverse
148 reverse-inv [] = refl
149 reverse-inv (x ∷ xs) = begin
150   reverse (reverse (x ∷ xs))
151     ≡⟨ P.cong reverse (unfold-reverse x xs) ⟩
152   reverse (reverse xs ∷ʳ x)
153     ≡⟨ reverse-++-commute (reverse xs) (x ∷ []) ⟩
154   x ∷ reverse (reverse (xs))
155     ≡⟨ P.cong (λ y → x ∷ y) (reverse-inv xs) ⟩
156   x ∷ xs
157     ∎
158   where
159     open P.≡-Reasoning