annotate Solvable.agda @ 12:d960f2ea902f

...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 17 Aug 2020 15:12:17 +0900 (2020-08-17)
parents 9dae7ef74342
children e0d16960d10d
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
0
dc677bac3c54 Permutation group
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
1 open import Level hiding ( suc ; zero )
dc677bac3c54 Permutation group
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
2 open import Algebra
4
121213cfc85a add Solvable
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 3
diff changeset
3 module Solvable {n m : Level} (G : Group n m ) where
0
dc677bac3c54 Permutation group
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
4
4
121213cfc85a add Solvable
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 3
diff changeset
5 open import Data.Unit
121213cfc85a add Solvable
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 3
diff changeset
6 open import Function.Inverse as Inverse using (_↔_; Inverse; _InverseOf_)
6
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 5
diff changeset
7 open import Function
7
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 6
diff changeset
8 open import Data.Nat hiding (_⊔_) -- using (ℕ; suc; zero)
4
121213cfc85a add Solvable
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 3
diff changeset
9 open import Relation.Nullary
121213cfc85a add Solvable
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 3
diff changeset
10 open import Data.Empty
5
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
11 open import Data.Product
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
12 open import Relation.Binary.PropositionalEquality hiding ( [_] )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
13
0
dc677bac3c54 Permutation group
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
14
4
121213cfc85a add Solvable
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 3
diff changeset
15 open Group G
0
dc677bac3c54 Permutation group
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
16
4
121213cfc85a add Solvable
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 3
diff changeset
17 [_,_] : Carrier → Carrier → Carrier
121213cfc85a add Solvable
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 3
diff changeset
18 [ g , h ] = g ⁻¹ ∙ h ⁻¹ ∙ g ∙ h
0
dc677bac3c54 Permutation group
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
19
5
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
20 data Commutator (P : Carrier → Set (Level.suc n ⊔ m)) : (f : Carrier) → Set (Level.suc n ⊔ m) where
6
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 5
diff changeset
21 uni : Commutator P ε
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 5
diff changeset
22 comm : {g h : Carrier} → P g → P h → Commutator P [ g , h ]
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 5
diff changeset
23 gen : {f g : Carrier} → Commutator P f → Commutator P g → Commutator P ( f ∙ g )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 5
diff changeset
24 ccong : {f g : Carrier} → f ≈ g → Commutator P f → Commutator P g
5
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
25
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
26 deriving : ( i : ℕ ) → Carrier → Set (Level.suc n ⊔ m)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
27 deriving 0 x = Lift (Level.suc n ⊔ m) ⊤
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
28 deriving (suc i) x = Commutator (deriving i) x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
29
4
121213cfc85a add Solvable
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 3
diff changeset
30 record Solvable : Set (Level.suc n ⊔ m) where
121213cfc85a add Solvable
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 3
diff changeset
31 field
121213cfc85a add Solvable
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 3
diff changeset
32 dervied-length : ℕ
121213cfc85a add Solvable
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 3
diff changeset
33 end : (x : Carrier ) → deriving dervied-length x → x ≈ ε
6
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 5
diff changeset
34
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 5
diff changeset
35 -- deriving stage is closed on multiplication and inversion
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 5
diff changeset
36
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 5
diff changeset
37 import Relation.Binary.Reasoning.Setoid as EqReasoning
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 5
diff changeset
38
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 5
diff changeset
39 gsym = Algebra.Group.sym G
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 5
diff changeset
40 grefl = Algebra.Group.refl G
11
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
41 gtrans = Algebra.Group.trans G
8
4e275f918e63 deriving-inv done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 7
diff changeset
42
6
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 5
diff changeset
43 lemma3 : ε ≈ ε ⁻¹
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 5
diff changeset
44 lemma3 = begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 5
diff changeset
45 ε ≈⟨ gsym (proj₁ inverse _) ⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 5
diff changeset
46 ε ⁻¹ ∙ ε ≈⟨ proj₂ identity _ ⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 5
diff changeset
47 ε ⁻¹
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 5
diff changeset
48 ∎ where open EqReasoning (Algebra.Group.setoid G)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 5
diff changeset
49
8
4e275f918e63 deriving-inv done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 7
diff changeset
50 lemma6 : {f : Carrier } → ( f ⁻¹ ) ⁻¹ ≈ f
4e275f918e63 deriving-inv done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 7
diff changeset
51 lemma6 {f} = begin
4e275f918e63 deriving-inv done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 7
diff changeset
52 ( f ⁻¹ ) ⁻¹ ≈⟨ gsym ( proj₁ identity _) ⟩
4e275f918e63 deriving-inv done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 7
diff changeset
53 ε ∙ ( f ⁻¹ ) ⁻¹ ≈⟨ ∙-cong (gsym ( proj₂ inverse _ )) grefl ⟩
4e275f918e63 deriving-inv done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 7
diff changeset
54 (f ∙ f ⁻¹ ) ∙ ( f ⁻¹ ) ⁻¹ ≈⟨ assoc _ _ _ ⟩
4e275f918e63 deriving-inv done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 7
diff changeset
55 f ∙ ( f ⁻¹ ∙ ( f ⁻¹ ) ⁻¹ ) ≈⟨ ∙-cong grefl (proj₂ inverse _) ⟩
4e275f918e63 deriving-inv done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 7
diff changeset
56 f ∙ ε ≈⟨ proj₂ identity _ ⟩
4e275f918e63 deriving-inv done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 7
diff changeset
57 f
4e275f918e63 deriving-inv done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 7
diff changeset
58 ∎ where open EqReasoning (Algebra.Group.setoid G)
6
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 5
diff changeset
59
11
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
60 ≡→≈ : {f g : Carrier } → f ≡ g → f ≈ g
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
61 ≡→≈ refl = grefl
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
62
9
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
63 data MP : Carrier → Set (Level.suc n) where
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
64 am : (x : Carrier ) → MP x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
65 _o_ : {x y : Carrier } → MP x → MP y → MP ( x ∙ y )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
66
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
67 mpf : {x : Carrier } → (m : MP x ) → Carrier → Carrier
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
68 mpf {x} (am x) y = x ∙ y
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
69 mpf (m o m₁) y = mpf m ( mpf m₁ y )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
70
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
71 mp-flatten : {x : Carrier } → (m : MP x ) → Carrier
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
72 mp-flatten {x} m = mpf {x} m ε
11
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
73
9
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
74 ∙-flatten : {x : Carrier } → (m : MP x ) → x ≈ mp-flatten m
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
75 ∙-flatten {x} (am x) = gsym (proj₂ identity _)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
76 ∙-flatten {_} (am x o q) = ∙-cong grefl ( ∙-flatten q )
11
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
77 ∙-flatten (_o_ {_} {z} (_o_ {x} {y} p q) r) = lemma9 _ _ _ ( ∙-flatten {x ∙ y } (p o q )) ( ∙-flatten {z} r ) where
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
78 mp-cong : {p q r : Carrier} → (P : MP p) → q ≈ r → mpf P q ≈ mpf P r
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
79 mp-cong (am x) q=r = ∙-cong grefl q=r
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
80 mp-cong (P o P₁) q=r = mp-cong P ( mp-cong P₁ q=r )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
81 mp-assoc : {p q r : Carrier} → (P : MP p) → mpf P q ∙ r ≈ mpf P (q ∙ r )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
82 mp-assoc (am x) = assoc _ _ _
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
83 mp-assoc {p} {q} {r} (P o P₁) = begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
84 mpf P (mpf P₁ q) ∙ r ≈⟨ mp-assoc P ⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
85 mpf P (mpf P₁ q ∙ r) ≈⟨ mp-cong P (mp-assoc P₁) ⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
86 mpf P ((mpf P₁) (q ∙ r))
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
87 ∎ where open EqReasoning (Algebra.Group.setoid G)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
88 lemma9 : (x y z : Carrier) → x ∙ y ≈ mpf p (mpf q ε) → z ≈ mpf r ε → x ∙ y ∙ z ≈ mp-flatten ((p o q) o r)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
89 lemma9 x y z t s = begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
90 x ∙ y ∙ z ≈⟨ ∙-cong t grefl ⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
91 mpf p (mpf q ε) ∙ z ≈⟨ mp-assoc p ⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
92 mpf p (mpf q ε ∙ z) ≈⟨ mp-cong p (mp-assoc q ) ⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
93 mpf p (mpf q (ε ∙ z)) ≈⟨ mp-cong p (mp-cong q (proj₁ identity _ )) ⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
94 mpf p (mpf q z) ≈⟨ mp-cong p (mp-cong q s) ⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
95 mpf p (mpf q (mpf r ε))
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
96 ∎ where open EqReasoning (Algebra.Group.setoid G)
9
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
97
12
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 11
diff changeset
98 mpg : {x : Carrier } → (m : MP x ) → Carrier → Carrier
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 11
diff changeset
99 mpg {x} (am x) y = y ∙ x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 11
diff changeset
100 mpg (m o m₁) y = mpf m₁ ( mpf m y )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 11
diff changeset
101
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 11
diff changeset
102 mp-flatten-g : {x : Carrier } → (m : MP x ) → Carrier
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 11
diff changeset
103 mp-flatten-g {x} m = mpg {x} m ε
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 11
diff changeset
104
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 11
diff changeset
105 ∙-flatten-g : {x : Carrier } → (m : MP x ) → x ≈ mp-flatten-g m
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 11
diff changeset
106 ∙-flatten-g {x} (am x) = gsym (proj₁ identity _)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 11
diff changeset
107 ∙-flatten-g {_} (am x o q) = {!!} -- ∙-cong ( ∙-flatten-g q ) grefl
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 11
diff changeset
108 ∙-flatten-g (_o_ {_} {z} (_o_ {x} {y} p q) r) = lemma9 _ _ _ {!!} ( ∙-flatten-g {z} r ) where
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 11
diff changeset
109 mp-cong : {p q r : Carrier} → (P : MP p) → q ≈ r → mpg P q ≈ mpg P r
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 11
diff changeset
110 mp-cong (am x) q=r = {!!} -- ∙-cong grefl q=r
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 11
diff changeset
111 mp-cong (P o P₁) q=r = {!!} -- mp-cong P ( mp-cong P₁ q=r )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 11
diff changeset
112 mp-assoc : {p q r : Carrier} → (P : MP p) → mpg P q ∙ r ≈ mpg P (q ∙ r )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 11
diff changeset
113 mp-assoc (am x) = {!!} -- assoc _ _ _
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 11
diff changeset
114 mp-assoc {p} {q} {r} (P o P₁) = begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 11
diff changeset
115 {!!} ≈⟨ {!!} ⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 11
diff changeset
116 {!!}
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 11
diff changeset
117 ∎ where open EqReasoning (Algebra.Group.setoid G)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 11
diff changeset
118 lemma9 : (x y z : Carrier) → x ∙ y ≈ mpg p (mpg q ε) → z ≈ mpg r ε → x ∙ y ∙ z ≈ mp-flatten-g ((p o q) o r)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 11
diff changeset
119 lemma9 x y z t s = begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 11
diff changeset
120 {!!} ≈⟨ {!!} ⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 11
diff changeset
121 {!!}
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 11
diff changeset
122 ∎ where open EqReasoning (Algebra.Group.setoid G)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 11
diff changeset
123
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 11
diff changeset
124 tet1 : (f g : Carrier ) → {!!}
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 11
diff changeset
125 tet1 f g = mp-flatten-g ((am (g ⁻¹) o am (f ⁻¹) ) o ( (am f o am g) o am ((f ∙ g) ⁻¹ )))
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 11
diff changeset
126
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 11
diff changeset
127 tet2 : (f g : Carrier ) → {!!}
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 11
diff changeset
128 tet2 f g = mp-flatten ((am (g ⁻¹) o am (f ⁻¹) ) o ( (am f o am g) o am ((f ∙ g) ⁻¹ )))
9
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
129
8
4e275f918e63 deriving-inv done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 7
diff changeset
130 lemma5 : (f g : Carrier ) → g ⁻¹ ∙ f ⁻¹ ≈ (f ∙ g) ⁻¹
4e275f918e63 deriving-inv done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 7
diff changeset
131 lemma5 f g = begin
12
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 11
diff changeset
132 g ⁻¹ ∙ f ⁻¹ ≈⟨ gsym (proj₂ identity _) ⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 11
diff changeset
133 g ⁻¹ ∙ f ⁻¹ ∙ ε ≈⟨ gsym (∙-cong grefl (proj₂ inverse _ )) ⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 11
diff changeset
134 g ⁻¹ ∙ f ⁻¹ ∙ ( (f ∙ g) ∙ (f ∙ g) ⁻¹ ) ≈⟨ ∙-flatten ((am (g ⁻¹) o am (f ⁻¹) ) o ( (am f o am g) o am ((f ∙ g) ⁻¹ ))) ⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 11
diff changeset
135 g ⁻¹ ∙ (f ⁻¹ ∙ (f ∙ (g ∙ ((f ∙ g) ⁻¹ ∙ ε)))) ≈⟨ ∙-cong grefl (gsym (assoc _ _ _ )) ⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 11
diff changeset
136 g ⁻¹ ∙ ((f ⁻¹ ∙ f) ∙ (g ∙ ((f ∙ g) ⁻¹ ∙ ε))) ≈⟨ ∙-cong grefl (gtrans (∙-cong (proj₁ inverse _ ) grefl) (proj₁ identity _)) ⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 11
diff changeset
137 g ⁻¹ ∙ (g ∙ ((f ∙ g) ⁻¹ ∙ ε)) ≈⟨ gsym (assoc _ _ _) ⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 11
diff changeset
138 (g ⁻¹ ∙ g ) ∙ ((f ∙ g) ⁻¹ ∙ ε) ≈⟨ gtrans (∙-cong (proj₁ inverse _ ) grefl) (proj₁ identity _) ⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 11
diff changeset
139 (f ∙ g) ⁻¹ ∙ ε ≈⟨ proj₂ identity _ ⟩
8
4e275f918e63 deriving-inv done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 7
diff changeset
140 (f ∙ g) ⁻¹
4e275f918e63 deriving-inv done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 7
diff changeset
141 ∎ where open EqReasoning (Algebra.Group.setoid G)
6
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 5
diff changeset
142
8
4e275f918e63 deriving-inv done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 7
diff changeset
143 lemma4 : (g h : Carrier ) → [ h , g ] ≈ [ g , h ] ⁻¹
4e275f918e63 deriving-inv done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 7
diff changeset
144 lemma4 g h = begin
4e275f918e63 deriving-inv done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 7
diff changeset
145 [ h , g ] ≈⟨ grefl ⟩
4e275f918e63 deriving-inv done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 7
diff changeset
146 (h ⁻¹ ∙ g ⁻¹ ∙ h ) ∙ g ≈⟨ assoc _ _ _ ⟩
4e275f918e63 deriving-inv done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 7
diff changeset
147 h ⁻¹ ∙ g ⁻¹ ∙ (h ∙ g) ≈⟨ ∙-cong grefl (gsym (∙-cong lemma6 lemma6)) ⟩
4e275f918e63 deriving-inv done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 7
diff changeset
148 h ⁻¹ ∙ g ⁻¹ ∙ ((h ⁻¹) ⁻¹ ∙ (g ⁻¹) ⁻¹) ≈⟨ ∙-cong grefl (lemma5 _ _ ) ⟩
4e275f918e63 deriving-inv done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 7
diff changeset
149 h ⁻¹ ∙ g ⁻¹ ∙ (g ⁻¹ ∙ h ⁻¹) ⁻¹ ≈⟨ assoc _ _ _ ⟩
4e275f918e63 deriving-inv done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 7
diff changeset
150 h ⁻¹ ∙ (g ⁻¹ ∙ (g ⁻¹ ∙ h ⁻¹) ⁻¹) ≈⟨ ∙-cong grefl (lemma5 (g ⁻¹ ∙ h ⁻¹ ) g ) ⟩
4e275f918e63 deriving-inv done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 7
diff changeset
151 h ⁻¹ ∙ (g ⁻¹ ∙ h ⁻¹ ∙ g) ⁻¹ ≈⟨ lemma5 (g ⁻¹ ∙ h ⁻¹ ∙ g) h ⟩
4e275f918e63 deriving-inv done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 7
diff changeset
152 (g ⁻¹ ∙ h ⁻¹ ∙ g ∙ h) ⁻¹ ≈⟨ grefl ⟩
4e275f918e63 deriving-inv done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 7
diff changeset
153 [ g , h ] ⁻¹
4e275f918e63 deriving-inv done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 7
diff changeset
154 ∎ where open EqReasoning (Algebra.Group.setoid G)
6
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 5
diff changeset
155
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 5
diff changeset
156 deriving-mul : { i : ℕ } → { x y : Carrier } → deriving i x → deriving i y → deriving i ( x ∙ y )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 5
diff changeset
157 deriving-mul {zero} {x} {y} _ _ = lift tt
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 5
diff changeset
158 deriving-mul {suc i} {x} {y} ix iy = gen ix iy
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 5
diff changeset
159
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 5
diff changeset
160 deriving-inv : { i : ℕ } → { x : Carrier } → deriving i x → deriving i ( x ⁻¹ )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 5
diff changeset
161 deriving-inv {zero} {x} (lift tt) = lift tt
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 5
diff changeset
162 deriving-inv {suc i} {ε} uni = ccong lemma3 uni
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 5
diff changeset
163 deriving-inv {suc i} {_} (comm x x₁ ) = ccong (lemma4 _ _) (comm x₁ x) where
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 5
diff changeset
164 deriving-inv {suc i} {_} (gen x x₁ ) = ccong (lemma5 _ _ ) ( gen (deriving-inv x₁) (deriving-inv x)) where
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 5
diff changeset
165 deriving-inv {suc i} {x} (ccong eq ix ) = ccong (⁻¹-cong eq) ( deriving-inv ix )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 5
diff changeset
166