|
0
|
1 open import Level hiding ( suc ; zero )
|
|
|
2 open import Algebra
|
|
14
|
3 module Gutil {n m : Level} (G : Group n m ) where
|
|
0
|
4
|
|
4
|
5 open import Data.Unit
|
|
|
6 open import Function.Inverse as Inverse using (_↔_; Inverse; _InverseOf_)
|
|
6
|
7 open import Function
|
|
7
|
8 open import Data.Nat hiding (_⊔_) -- using (ℕ; suc; zero)
|
|
4
|
9 open import Relation.Nullary
|
|
|
10 open import Data.Empty
|
|
5
|
11 open import Data.Product
|
|
|
12 open import Relation.Binary.PropositionalEquality hiding ( [_] )
|
|
|
13
|
|
0
|
14
|
|
4
|
15 open Group G
|
|
0
|
16
|
|
6
|
17 import Relation.Binary.Reasoning.Setoid as EqReasoning
|
|
|
18
|
|
|
19 gsym = Algebra.Group.sym G
|
|
|
20 grefl = Algebra.Group.refl G
|
|
11
|
21 gtrans = Algebra.Group.trans G
|
|
8
|
22
|
|
6
|
23 lemma3 : ε ≈ ε ⁻¹
|
|
|
24 lemma3 = begin
|
|
|
25 ε ≈⟨ gsym (proj₁ inverse _) ⟩
|
|
|
26 ε ⁻¹ ∙ ε ≈⟨ proj₂ identity _ ⟩
|
|
|
27 ε ⁻¹
|
|
|
28 ∎ where open EqReasoning (Algebra.Group.setoid G)
|
|
|
29
|
|
8
|
30 lemma6 : {f : Carrier } → ( f ⁻¹ ) ⁻¹ ≈ f
|
|
|
31 lemma6 {f} = begin
|
|
|
32 ( f ⁻¹ ) ⁻¹ ≈⟨ gsym ( proj₁ identity _) ⟩
|
|
|
33 ε ∙ ( f ⁻¹ ) ⁻¹ ≈⟨ ∙-cong (gsym ( proj₂ inverse _ )) grefl ⟩
|
|
|
34 (f ∙ f ⁻¹ ) ∙ ( f ⁻¹ ) ⁻¹ ≈⟨ assoc _ _ _ ⟩
|
|
|
35 f ∙ ( f ⁻¹ ∙ ( f ⁻¹ ) ⁻¹ ) ≈⟨ ∙-cong grefl (proj₂ inverse _) ⟩
|
|
|
36 f ∙ ε ≈⟨ proj₂ identity _ ⟩
|
|
|
37 f
|
|
|
38 ∎ where open EqReasoning (Algebra.Group.setoid G)
|
|
6
|
39
|
|
11
|
40 ≡→≈ : {f g : Carrier } → f ≡ g → f ≈ g
|
|
|
41 ≡→≈ refl = grefl
|
|
|
42
|
|
14
|
43 ---
|
|
|
44 -- to avoid assoc storm, flatten multiplication according to the template
|
|
|
45 --
|
|
|
46
|
|
9
|
47 data MP : Carrier → Set (Level.suc n) where
|
|
|
48 am : (x : Carrier ) → MP x
|
|
|
49 _o_ : {x y : Carrier } → MP x → MP y → MP ( x ∙ y )
|
|
|
50
|
|
|
51 mpf : {x : Carrier } → (m : MP x ) → Carrier → Carrier
|
|
15
|
52 mpf (am x) y = x ∙ y
|
|
9
|
53 mpf (m o m₁) y = mpf m ( mpf m₁ y )
|
|
|
54
|
|
|
55 mp-flatten : {x : Carrier } → (m : MP x ) → Carrier
|
|
15
|
56 mp-flatten m = mpf m ε
|
|
|
57
|
|
|
58 mpl1 : Carrier → {x : Carrier } → MP x → Carrier
|
|
|
59 mpl1 x (am y) = x ∙ y
|
|
|
60 mpl1 x (y o y1) = mpl1 ( mpl1 x y ) y1
|
|
|
61
|
|
|
62 mpl : {x z : Carrier } → MP x → MP z → Carrier
|
|
|
63 mpl (am x) m = mpl1 x m
|
|
|
64 mpl (m o m1) m2 = mpl m (m1 o m2)
|
|
|
65
|
|
|
66 mp-flattenl : {x : Carrier } → (m : MP x ) → Carrier
|
|
|
67 mp-flattenl m = mpl m (am ε)
|
|
|
68
|
|
|
69 test1 : ( f g : Carrier ) → Carrier
|
|
|
70 test1 f g = mp-flattenl ((am (g ⁻¹) o am (f ⁻¹) ) o ( (am f o am g) o am ((f ∙ g) ⁻¹ )))
|
|
|
71
|
|
|
72 test2 : ( f g : Carrier ) → test1 f g ≡ g ⁻¹ ∙ f ⁻¹ ∙ f ∙ g ∙ (f ∙ g) ⁻¹ ∙ ε
|
|
|
73 test2 f g = _≡_.refl
|
|
|
74
|
|
|
75 test3 : ( f g : Carrier ) → Carrier
|
|
|
76 test3 f g = mp-flatten ((am (g ⁻¹) o am (f ⁻¹) ) o ( (am f o am g) o am ((f ∙ g) ⁻¹ )))
|
|
|
77
|
|
|
78 test4 : ( f g : Carrier ) → test3 f g ≡ g ⁻¹ ∙ (f ⁻¹ ∙ (f ∙ (g ∙ ((f ∙ g) ⁻¹ ∙ ε))))
|
|
|
79 test4 f g = _≡_.refl
|
|
|
80
|
|
11
|
81
|
|
9
|
82 ∙-flatten : {x : Carrier } → (m : MP x ) → x ≈ mp-flatten m
|
|
|
83 ∙-flatten {x} (am x) = gsym (proj₂ identity _)
|
|
|
84 ∙-flatten {_} (am x o q) = ∙-cong grefl ( ∙-flatten q )
|
|
11
|
85 ∙-flatten (_o_ {_} {z} (_o_ {x} {y} p q) r) = lemma9 _ _ _ ( ∙-flatten {x ∙ y } (p o q )) ( ∙-flatten {z} r ) where
|
|
|
86 mp-cong : {p q r : Carrier} → (P : MP p) → q ≈ r → mpf P q ≈ mpf P r
|
|
|
87 mp-cong (am x) q=r = ∙-cong grefl q=r
|
|
|
88 mp-cong (P o P₁) q=r = mp-cong P ( mp-cong P₁ q=r )
|
|
|
89 mp-assoc : {p q r : Carrier} → (P : MP p) → mpf P q ∙ r ≈ mpf P (q ∙ r )
|
|
|
90 mp-assoc (am x) = assoc _ _ _
|
|
|
91 mp-assoc {p} {q} {r} (P o P₁) = begin
|
|
|
92 mpf P (mpf P₁ q) ∙ r ≈⟨ mp-assoc P ⟩
|
|
15
|
93 mpf P (mpf P₁ q ∙ r) ≈⟨ mp-cong P (mp-assoc P₁) ⟩ mpf P ((mpf P₁) (q ∙ r))
|
|
11
|
94 ∎ where open EqReasoning (Algebra.Group.setoid G)
|
|
|
95 lemma9 : (x y z : Carrier) → x ∙ y ≈ mpf p (mpf q ε) → z ≈ mpf r ε → x ∙ y ∙ z ≈ mp-flatten ((p o q) o r)
|
|
|
96 lemma9 x y z t s = begin
|
|
|
97 x ∙ y ∙ z ≈⟨ ∙-cong t grefl ⟩
|
|
|
98 mpf p (mpf q ε) ∙ z ≈⟨ mp-assoc p ⟩
|
|
|
99 mpf p (mpf q ε ∙ z) ≈⟨ mp-cong p (mp-assoc q ) ⟩
|
|
|
100 mpf p (mpf q (ε ∙ z)) ≈⟨ mp-cong p (mp-cong q (proj₁ identity _ )) ⟩
|
|
|
101 mpf p (mpf q z) ≈⟨ mp-cong p (mp-cong q s) ⟩
|
|
|
102 mpf p (mpf q (mpf r ε))
|
|
|
103 ∎ where open EqReasoning (Algebra.Group.setoid G)
|
|
9
|
104
|
|
87
|
105 grepl : { x y0 y1 z : Carrier } → x ∙ y0 ≈ y1 → x ∙ ( y0 ∙ z ) ≈ y1 ∙ z
|
|
|
106 grepl eq = gtrans (gsym (assoc _ _ _ )) (∙-cong eq grefl )
|
|
|
107
|
|
|
108 grm : { x y0 y1 z : Carrier } → x ∙ y0 ≈ ε → x ∙ ( y0 ∙ z ) ≈ z
|
|
|
109 grm eq = gtrans ( gtrans (gsym (assoc _ _ _ )) (∙-cong eq grefl )) ( proj₁ identity _ )
|
|
|
110
|
|
15
|
111 -- ∙-flattenl : {x : Carrier } → (m : MP x ) → x ≈ mp-flattenl m
|
|
|
112 -- ∙-flattenl (am x) = gsym (proj₂ identity _)
|
|
|
113 -- ∙-flattenl (q o am x) with ∙-flattenl q -- x₁ ∙ x ≈ mpl q (am x o am ε) , t : x₁ ≈ mpl q (am ε)
|
|
|
114 -- ... | t = {!!}
|
|
|
115 -- ∙-flattenl (q o (x o y )) with ∙-flattenl q
|
|
|
116 -- ... | t = gtrans (gsym (assoc _ _ _ )) {!!}
|
|
|
117
|
|
8
|
118 lemma5 : (f g : Carrier ) → g ⁻¹ ∙ f ⁻¹ ≈ (f ∙ g) ⁻¹
|
|
|
119 lemma5 f g = begin
|
|
12
|
120 g ⁻¹ ∙ f ⁻¹ ≈⟨ gsym (proj₂ identity _) ⟩
|
|
|
121 g ⁻¹ ∙ f ⁻¹ ∙ ε ≈⟨ gsym (∙-cong grefl (proj₂ inverse _ )) ⟩
|
|
|
122 g ⁻¹ ∙ f ⁻¹ ∙ ( (f ∙ g) ∙ (f ∙ g) ⁻¹ ) ≈⟨ ∙-flatten ((am (g ⁻¹) o am (f ⁻¹) ) o ( (am f o am g) o am ((f ∙ g) ⁻¹ ))) ⟩
|
|
|
123 g ⁻¹ ∙ (f ⁻¹ ∙ (f ∙ (g ∙ ((f ∙ g) ⁻¹ ∙ ε)))) ≈⟨ ∙-cong grefl (gsym (assoc _ _ _ )) ⟩
|
|
|
124 g ⁻¹ ∙ ((f ⁻¹ ∙ f) ∙ (g ∙ ((f ∙ g) ⁻¹ ∙ ε))) ≈⟨ ∙-cong grefl (gtrans (∙-cong (proj₁ inverse _ ) grefl) (proj₁ identity _)) ⟩
|
|
|
125 g ⁻¹ ∙ (g ∙ ((f ∙ g) ⁻¹ ∙ ε)) ≈⟨ gsym (assoc _ _ _) ⟩
|
|
|
126 (g ⁻¹ ∙ g ) ∙ ((f ∙ g) ⁻¹ ∙ ε) ≈⟨ gtrans (∙-cong (proj₁ inverse _ ) grefl) (proj₁ identity _) ⟩
|
|
|
127 (f ∙ g) ⁻¹ ∙ ε ≈⟨ proj₂ identity _ ⟩
|
|
8
|
128 (f ∙ g) ⁻¹
|
|
|
129 ∎ where open EqReasoning (Algebra.Group.setoid G)
|
|
6
|
130
|
