Mercurial > hg > Members > kono > Proof > galois
annotate src/sym5.agda @ 316:d712d2a1f8bb stack-8.10.7
fix for new agda stdlib
author | kono |
---|---|
date | Sat, 16 Sep 2023 14:59:33 +0900 |
parents | 6d1619d9f880 |
children |
rev | line source |
---|---|
68 | 1 open import Level hiding ( suc ; zero ) |
2 open import Algebra | |
73 | 3 module sym5 where |
68 | 4 |
5 open import Symmetric | |
75 | 6 open import Data.Unit using (⊤ ; tt ) |
68 | 7 open import Function.Inverse as Inverse using (_↔_; Inverse; _InverseOf_) |
75 | 8 open import Function hiding (flip) |
68 | 9 open import Data.Nat hiding (_⊔_) -- using (ℕ; suc; zero) |
75 | 10 open import Data.Nat.Properties |
68 | 11 open import Relation.Nullary |
12 open import Data.Empty | |
13 open import Data.Product | |
14 | |
15 open import Gutil | |
16 open import Putil | |
316 | 17 open import Solvable (Symmetric 5) |
68 | 18 open import Relation.Binary.PropositionalEquality hiding ( [_] ) |
19 | |
75 | 20 open import Data.Fin hiding (_<_ ; _≤_ ; lift ) |
116
6022d00a0690
check termination problem remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
115
diff
changeset
|
21 open import Data.Fin.Permutation hiding (_∘ₚ_) |
6022d00a0690
check termination problem remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
115
diff
changeset
|
22 |
6022d00a0690
check termination problem remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
115
diff
changeset
|
23 infixr 200 _∘ₚ_ |
6022d00a0690
check termination problem remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
115
diff
changeset
|
24 _∘ₚ_ = Data.Fin.Permutation._∘ₚ_ |
6022d00a0690
check termination problem remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
115
diff
changeset
|
25 |
73 | 26 open import Data.List hiding ( [_] ) |
75 | 27 open import nat |
77 | 28 open import fin |
84 | 29 open import logic |
30 | |
31 open _∧_ | |
68 | 32 |
316 | 33 ¬sym5solvable : ¬ solvable |
115 | 34 ¬sym5solvable sol = counter-example (end5 (abc 0<3 0<4 ) (dervie-any-3rot0 (dervied-length sol) 0<3 0<4 ) ) where |
316 | 35 |
73 | 36 -- |
37 -- dba 1320 d → b → a → d | |
38 -- (dba)⁻¹ 3021 a → b → d → a | |
39 -- aec 21430 | |
40 -- (aec)⁻¹ 41032 | |
113
d8a21c5db0e0
sym5 done but agda won'y stop
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
112
diff
changeset
|
41 -- [ dba , aec ] = (abd)(cea)(dba)(aec) = abc |
d8a21c5db0e0
sym5 done but agda won'y stop
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
112
diff
changeset
|
42 -- so commutator always contains abc, dba and aec |
73 | 43 |
112 | 44 open ≡-Reasoning |
45 | |
73 | 46 open solvable |
47 end5 : (x : Permutation 5 5) → deriving (dervied-length sol) x → x =p= pid | |
48 end5 x der = end sol x der | |
49 | |
74 | 50 0<4 : 0 < 4 |
75 | 51 0<4 = s≤s z≤n |
74 | 52 |
53 0<3 : 0 < 3 | |
75 | 54 0<3 = s≤s z≤n |
74 | 55 |
79 | 56 --- 1 ∷ 2 ∷ 0 ∷ [] abc |
74 | 57 3rot : Permutation 3 3 |
79 | 58 3rot = pid {3} ∘ₚ pins (n≤ 2) |
59 | |
85 | 60 save2 : {i j : ℕ } → (i ≤ 3 ) → ( j ≤ 4 ) → Permutation 5 5 |
61 save2 i<3 j<4 = flip (pins (s≤s i<3)) ∘ₚ flip (pins j<4) | |
62 | |
79 | 63 ins2 : {i j : ℕ } → Permutation 3 3 → (i ≤ 3 ) → ( j ≤ 4 ) → Permutation 5 5 |
85 | 64 ins2 abc i<3 j<4 = (save2 i<3 j<4 ∘ₚ (pprep (pprep abc))) ∘ₚ flip (save2 i<3 j<4 ) |
74 | 65 |
116
6022d00a0690
check termination problem remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
115
diff
changeset
|
66 ins2cong : {i j : ℕ } → {x y : Permutation 3 3 } → {i<3 : i ≤ 3 } → {j<4 : j ≤ 4 } → x =p= y → ins2 x i<3 j<4 =p= ins2 y i<3 j<4 |
6022d00a0690
check termination problem remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
115
diff
changeset
|
67 ins2cong {i} {j} {x} {y} {i<3} {j<4} x=y = presp {5} {save2 i<3 j<4 ∘ₚ (pprep (pprep x))} {_} {flip (save2 i<3 j<4 )} |
6022d00a0690
check termination problem remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
115
diff
changeset
|
68 (presp {5} {save2 i<3 j<4} prefl (pprep-cong (pprep-cong x=y)) ) prefl |
112 | 69 |
70 open _=p=_ | |
71 | |
75 | 72 abc : {i j : ℕ } → (i ≤ 3 ) → ( j ≤ 4 ) → Permutation 5 5 |
79 | 73 abc i<3 j<4 = ins2 3rot i<3 j<4 |
74 dba : {i j : ℕ } → (i ≤ 3 ) → ( j ≤ 4 ) → Permutation 5 5 | |
75 dba i<3 j<4 = ins2 (3rot ∘ₚ 3rot) i<3 j<4 | |
74 | 76 |
184 | 77 counter-example : ¬ (abc 0<3 0<4 =p= pid ) |
78 counter-example eq with ←pleq _ _ eq | |
79 ... | () | |
80 | |
87 | 81 record Triple {i j : ℕ } (i<3 : i ≤ 3) (j<4 : j ≤ 4) (rot : Permutation 3 3) : Set where |
77 | 82 field |
82 | 83 dba0<3 : Fin 4 |
84 dba1<4 : Fin 5 | |
85 aec0<3 : Fin 4 | |
86 aec1<4 : Fin 5 | |
116
6022d00a0690
check termination problem remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
115
diff
changeset
|
87 abc= : ins2 rot i<3 j<4 =p= [ ins2 (rot ∘ₚ rot) (fin≤n {3} dba0<3) (fin≤n {4} dba1<4) , ins2 (rot ∘ₚ rot) (fin≤n {3} aec0<3) (fin≤n {4} aec1<4) ] |
83 | 88 |
85 | 89 open Triple |
87 | 90 triple : {i j : ℕ } → (i<3 : i ≤ 3) (j<4 : j ≤ 4) → Triple i<3 j<4 3rot |
84 | 91 triple z≤n z≤n = record { dba0<3 = # 0 ; dba1<4 = # 4 ; aec0<3 = # 2 ; aec1<4 = # 0 ; abc= = pleq _ _ refl } |
92 triple z≤n (s≤s z≤n) = record { dba0<3 = # 0 ; dba1<4 = # 4 ; aec0<3 = # 2 ; aec1<4 = # 0 ; abc= = pleq _ _ refl } | |
93 triple z≤n (s≤s (s≤s z≤n)) = record { dba0<3 = # 1 ; dba1<4 = # 0 ; aec0<3 = # 3 ; aec1<4 = # 2 ; abc= = pleq _ _ refl } | |
94 triple z≤n (s≤s (s≤s (s≤s z≤n))) = record { dba0<3 = # 1 ; dba1<4 = # 3 ; aec0<3 = # 0 ; aec1<4 = # 0 ; abc= = pleq _ _ refl } | |
95 triple z≤n (s≤s (s≤s (s≤s (s≤s z≤n)))) = record { dba0<3 = # 0 ; dba1<4 = # 0 ; aec0<3 = # 2 ; aec1<4 = # 4 ; abc= = pleq _ _ refl } | |
96 triple (s≤s z≤n) z≤n = record { dba0<3 = # 0 ; dba1<4 = # 2 ; aec0<3 = # 3 ; aec1<4 = # 1 ; abc= = pleq _ _ refl } | |
97 triple (s≤s z≤n) (s≤s z≤n) = record { dba0<3 = # 0 ; dba1<4 = # 2 ; aec0<3 = # 3 ; aec1<4 = # 1 ; abc= = pleq _ _ refl } | |
98 triple (s≤s z≤n) (s≤s (s≤s z≤n)) = record { dba0<3 = # 1 ; dba1<4 = # 0 ; aec0<3 = # 3 ; aec1<4 = # 2 ; abc= = pleq _ _ refl } | |
99 triple (s≤s z≤n) (s≤s (s≤s (s≤s z≤n))) = record { dba0<3 = # 0 ; dba1<4 = # 3 ; aec0<3 = # 1 ; aec1<4 = # 0 ; abc= = pleq _ _ refl } | |
100 triple (s≤s z≤n) (s≤s (s≤s (s≤s (s≤s z≤n)))) = record { dba0<3 = # 2 ; dba1<4 = # 4 ; aec0<3 = # 0 ; aec1<4 = # 2 ; abc= = pleq _ _ refl } | |
101 triple (s≤s (s≤s z≤n)) z≤n = record { dba0<3 = # 3 ; dba1<4 = # 0 ; aec0<3 = # 1 ; aec1<4 = # 3 ; abc= = pleq _ _ refl } | |
102 triple (s≤s (s≤s z≤n)) (s≤s z≤n) = record { dba0<3 = # 3 ; dba1<4 = # 0 ; aec0<3 = # 1 ; aec1<4 = # 3 ; abc= = pleq _ _ refl } | |
103 triple (s≤s (s≤s z≤n)) (s≤s (s≤s z≤n)) = record { dba0<3 = # 1 ; dba1<4 = # 3 ; aec0<3 = # 0 ; aec1<4 = # 0 ; abc= = pleq _ _ refl } | |
104 triple (s≤s (s≤s z≤n)) (s≤s (s≤s (s≤s z≤n))) = record { dba0<3 = # 0 ; dba1<4 = # 3 ; aec0<3 = # 1 ; aec1<4 = # 0 ; abc= = pleq _ _ refl } | |
105 triple (s≤s (s≤s z≤n)) (s≤s (s≤s (s≤s (s≤s z≤n)))) = record { dba0<3 = # 1 ; dba1<4 = # 4 ; aec0<3 = # 2 ; aec1<4 = # 2 ; abc= = pleq _ _ refl } | |
106 triple (s≤s (s≤s (s≤s z≤n))) z≤n = record { dba0<3 = # 2 ; dba1<4 = # 4 ; aec0<3 = # 1 ; aec1<4 = # 0 ; abc= = pleq _ _ refl } | |
107 triple (s≤s (s≤s (s≤s z≤n))) (s≤s z≤n) = record { dba0<3 = # 2 ; dba1<4 = # 4 ; aec0<3 = # 1 ; aec1<4 = # 0 ; abc= = pleq _ _ refl } | |
108 triple (s≤s (s≤s (s≤s z≤n))) (s≤s (s≤s z≤n)) = record { dba0<3 = # 0 ; dba1<4 = # 0 ; aec0<3 = # 2 ; aec1<4 = # 4 ; abc= = pleq _ _ refl } | |
109 triple (s≤s (s≤s (s≤s z≤n))) (s≤s (s≤s (s≤s z≤n))) = record { dba0<3 = # 2 ; dba1<4 = # 4 ; aec0<3 = # 0 ; aec1<4 = # 2 ; abc= = pleq _ _ refl } | |
80 | 110 triple (s≤s (s≤s (s≤s z≤n))) (s≤s (s≤s (s≤s (s≤s z≤n)))) = |
84 | 111 record { dba0<3 = # 1 ; dba1<4 = # 4 ; aec0<3 = # 0 ; aec1<4 = # 3 ; abc= = pleq _ _ refl } |
112 | 112 |
113 _⁻¹ : {n : ℕ } ( x : Permutation n n) → Permutation n n | |
114 _⁻¹ = pinv | |
79 | 115 |
113
d8a21c5db0e0
sym5 done but agda won'y stop
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
112
diff
changeset
|
116 -- tt5 : (i : Fin 4) (j : Fin 5) → (z : Fin 4) → (w : Fin 5) → (x : Fin 5) (y : Fin 4) → (rot : Permutation 3 3 ) → List (List ℕ) → List (List ℕ) |
d8a21c5db0e0
sym5 done but agda won'y stop
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
112
diff
changeset
|
117 -- tt5 i j z w x y rot t with is-=p= (ins2 rot (fin≤n i) (fin≤n j)) |
d8a21c5db0e0
sym5 done but agda won'y stop
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
112
diff
changeset
|
118 -- [ ins2 (rot ∘ₚ rot) (fin≤n z) (fin≤n x) , ins2 (pinv rot) (fin≤n y) (fin≤n w) ] |
d8a21c5db0e0
sym5 done but agda won'y stop
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
112
diff
changeset
|
119 -- ... | yes _ = ( toℕ i ∷ toℕ j ∷ 9 ∷ toℕ z ∷ toℕ x ∷ toℕ y ∷ toℕ w ∷ [] ) ∷ t |
d8a21c5db0e0
sym5 done but agda won'y stop
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
112
diff
changeset
|
120 -- ... | no _ = t |
112 | 121 |
113
d8a21c5db0e0
sym5 done but agda won'y stop
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
112
diff
changeset
|
122 -- open import Relation.Binary.Definitions |
112 | 123 |
113
d8a21c5db0e0
sym5 done but agda won'y stop
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
112
diff
changeset
|
124 -- tt2 : (i : Fin 4) (j : Fin 5) → (rot : Permutation 3 3 ) → List (List ℕ) |
d8a21c5db0e0
sym5 done but agda won'y stop
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
112
diff
changeset
|
125 -- tt2 i j rot = tt3 (# 4) (# 3) (# 3) (# 4) [] where |
d8a21c5db0e0
sym5 done but agda won'y stop
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
112
diff
changeset
|
126 -- tt3 : (w : Fin 5) (z : Fin 4) (x : Fin 4) (y : Fin 5) → List (List ℕ) → List (List ℕ) |
d8a21c5db0e0
sym5 done but agda won'y stop
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
112
diff
changeset
|
127 -- tt3 zero zero zero zero t = ( tt5 i j zero zero zero zero rot [] ) ++ t |
d8a21c5db0e0
sym5 done but agda won'y stop
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
112
diff
changeset
|
128 -- tt3 (suc w) zero zero zero t = tt3 (fin+1 w) (# 3) (# 3) (# 4) ((tt5 i j zero (suc w) zero zero rot [] ) ++ t) |
d8a21c5db0e0
sym5 done but agda won'y stop
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
112
diff
changeset
|
129 -- tt3 w z zero (suc y) t = tt3 w z (# 3) (fin+1 y) ((tt5 i j z w (suc y) zero rot [] ) ++ t) |
d8a21c5db0e0
sym5 done but agda won'y stop
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
112
diff
changeset
|
130 -- tt3 w z (suc x) y t = tt3 w z (fin+1 x) y ((tt5 i j z w y (suc x) rot [] ) ++ t) |
d8a21c5db0e0
sym5 done but agda won'y stop
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
112
diff
changeset
|
131 -- tt3 w (suc z) zero zero t = tt3 w (fin+1 z) (# 3) (# 4) ((tt5 i j (suc z) w zero zero rot [] ) ++ t) |
112 | 132 |
113
d8a21c5db0e0
sym5 done but agda won'y stop
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
112
diff
changeset
|
133 -- tt4 : List (List (List ℕ)) |
d8a21c5db0e0
sym5 done but agda won'y stop
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
112
diff
changeset
|
134 -- tt4 = tt2 (# 0) (# 0) (pinv 3rot) ∷ |
d8a21c5db0e0
sym5 done but agda won'y stop
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
112
diff
changeset
|
135 -- tt2 (# 1) (# 0) (pinv 3rot) ∷ |
d8a21c5db0e0
sym5 done but agda won'y stop
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
112
diff
changeset
|
136 -- tt2 (# 2) (# 0) (pinv 3rot) ∷ |
d8a21c5db0e0
sym5 done but agda won'y stop
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
112
diff
changeset
|
137 -- tt2 (# 3) (# 0) (pinv 3rot) ∷ |
d8a21c5db0e0
sym5 done but agda won'y stop
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
112
diff
changeset
|
138 -- tt2 (# 0) (# 1) (pinv 3rot) ∷ |
d8a21c5db0e0
sym5 done but agda won'y stop
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
112
diff
changeset
|
139 -- tt2 (# 1) (# 1) (pinv 3rot) ∷ |
d8a21c5db0e0
sym5 done but agda won'y stop
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
112
diff
changeset
|
140 -- tt2 (# 2) (# 1) (pinv 3rot) ∷ |
d8a21c5db0e0
sym5 done but agda won'y stop
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
112
diff
changeset
|
141 -- tt2 (# 3) (# 1) (pinv 3rot) ∷ |
d8a21c5db0e0
sym5 done but agda won'y stop
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
112
diff
changeset
|
142 -- tt2 (# 0) (# 2) (pinv 3rot) ∷ |
d8a21c5db0e0
sym5 done but agda won'y stop
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
112
diff
changeset
|
143 -- tt2 (# 1) (# 2) (pinv 3rot) ∷ |
d8a21c5db0e0
sym5 done but agda won'y stop
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
112
diff
changeset
|
144 -- tt2 (# 2) (# 2) (pinv 3rot) ∷ |
d8a21c5db0e0
sym5 done but agda won'y stop
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
112
diff
changeset
|
145 -- tt2 (# 3) (# 2) (pinv 3rot) ∷ |
d8a21c5db0e0
sym5 done but agda won'y stop
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
112
diff
changeset
|
146 -- tt2 (# 0) (# 3) (pinv 3rot) ∷ |
d8a21c5db0e0
sym5 done but agda won'y stop
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
112
diff
changeset
|
147 -- tt2 (# 1) (# 3) (pinv 3rot) ∷ |
d8a21c5db0e0
sym5 done but agda won'y stop
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
112
diff
changeset
|
148 -- tt2 (# 2) (# 3) (pinv 3rot) ∷ |
d8a21c5db0e0
sym5 done but agda won'y stop
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
112
diff
changeset
|
149 -- tt2 (# 3) (# 3) (pinv 3rot) ∷ |
d8a21c5db0e0
sym5 done but agda won'y stop
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
112
diff
changeset
|
150 -- tt2 (# 0) (# 4) (pinv 3rot) ∷ |
d8a21c5db0e0
sym5 done but agda won'y stop
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
112
diff
changeset
|
151 -- tt2 (# 1) (# 4) (pinv 3rot) ∷ |
d8a21c5db0e0
sym5 done but agda won'y stop
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
112
diff
changeset
|
152 -- tt2 (# 2) (# 4) (pinv 3rot) ∷ |
d8a21c5db0e0
sym5 done but agda won'y stop
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
112
diff
changeset
|
153 -- tt2 (# 3) (# 4) (pinv 3rot) ∷ |
112 | 154 -- [] |
155 | |
156 open Triple | |
87 | 157 dba-triple : {i j : ℕ } → (i<3 : i ≤ 3 ) → (j<4 : j ≤ 4 ) → Triple i<3 j<4 (3rot ∘ₚ 3rot ) |
113
d8a21c5db0e0
sym5 done but agda won'y stop
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
112
diff
changeset
|
158 dba-triple z≤n z≤n = record { dba0<3 = # 0 ; dba1<4 = # 2 ; aec0<3 = # 2 ; aec1<4 = # 0 ; abc= = pleq _ _ refl } |
d8a21c5db0e0
sym5 done but agda won'y stop
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
112
diff
changeset
|
159 dba-triple z≤n (s≤s z≤n) = record { dba0<3 = # 0 ; dba1<4 = # 2 ; aec0<3 = # 2 ; aec1<4 = # 0 ; abc= = pleq _ _ refl } |
d8a21c5db0e0
sym5 done but agda won'y stop
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
112
diff
changeset
|
160 dba-triple z≤n (s≤s (s≤s z≤n)) = record { dba0<3 = # 1 ; dba1<4 = # 3 ; aec0<3 = # 3 ; aec1<4 = # 2 ; abc= = pleq _ _ refl } |
d8a21c5db0e0
sym5 done but agda won'y stop
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
112
diff
changeset
|
161 dba-triple z≤n (s≤s (s≤s (s≤s z≤n))) = record { dba0<3 = # 0 ; dba1<4 = # 2 ; aec0<3 = # 2 ; aec1<4 = # 4 ; abc= = pleq _ _ refl } |
d8a21c5db0e0
sym5 done but agda won'y stop
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
112
diff
changeset
|
162 dba-triple z≤n (s≤s (s≤s (s≤s (s≤s z≤n)))) = record { dba0<3 = # 3 ; dba1<4 = # 0 ; aec0<3 = # 0 ; aec1<4 = # 2 ; abc= = pleq _ _ refl } |
d8a21c5db0e0
sym5 done but agda won'y stop
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
112
diff
changeset
|
163 dba-triple (s≤s z≤n) z≤n = record { dba0<3 = # 0 ; dba1<4 = # 0 ; aec0<3 = # 1 ; aec1<4 = # 3 ; abc= = pleq _ _ refl } |
d8a21c5db0e0
sym5 done but agda won'y stop
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
112
diff
changeset
|
164 dba-triple (s≤s z≤n) (s≤s z≤n) = record { dba0<3 = # 0 ; dba1<4 = # 0 ; aec0<3 = # 1 ; aec1<4 = # 3 ; abc= = pleq _ _ refl } |
d8a21c5db0e0
sym5 done but agda won'y stop
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
112
diff
changeset
|
165 dba-triple (s≤s z≤n) (s≤s (s≤s z≤n)) = record { dba0<3 = # 1 ; dba1<4 = # 3 ; aec0<3 = # 3 ; aec1<4 = # 2 ; abc= = pleq _ _ refl } |
d8a21c5db0e0
sym5 done but agda won'y stop
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
112
diff
changeset
|
166 dba-triple (s≤s z≤n) (s≤s (s≤s (s≤s z≤n))) = record { dba0<3 = # 1 ; dba1<4 = # 4 ; aec0<3 = # 2 ; aec1<4 = # 0 ; abc= = pleq _ _ refl } |
d8a21c5db0e0
sym5 done but agda won'y stop
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
112
diff
changeset
|
167 dba-triple (s≤s z≤n) (s≤s (s≤s (s≤s (s≤s z≤n)))) = record { dba0<3 = # 1 ; dba1<4 = # 3 ; aec0<3 = # 3 ; aec1<4 = # 0 ; abc= = pleq _ _ refl } |
d8a21c5db0e0
sym5 done but agda won'y stop
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
112
diff
changeset
|
168 dba-triple (s≤s (s≤s z≤n)) z≤n = record { dba0<3 = # 2 ; dba1<4 = # 4 ; aec0<3 = # 0 ; aec1<4 = # 0 ; abc= = pleq _ _ refl } |
d8a21c5db0e0
sym5 done but agda won'y stop
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
112
diff
changeset
|
169 dba-triple (s≤s (s≤s z≤n)) (s≤s z≤n) = record { dba0<3 = # 2 ; dba1<4 = # 4 ; aec0<3 = # 0 ; aec1<4 = # 0 ; abc= = pleq _ _ refl } |
d8a21c5db0e0
sym5 done but agda won'y stop
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
112
diff
changeset
|
170 dba-triple (s≤s (s≤s z≤n)) (s≤s (s≤s z≤n)) = record { dba0<3 = # 0 ; dba1<4 = # 2 ; aec0<3 = # 2 ; aec1<4 = # 4 ; abc= = pleq _ _ refl } |
d8a21c5db0e0
sym5 done but agda won'y stop
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
112
diff
changeset
|
171 dba-triple (s≤s (s≤s z≤n)) (s≤s (s≤s (s≤s z≤n))) = record { dba0<3 = # 1 ; dba1<4 = # 4 ; aec0<3 = # 2 ; aec1<4 = # 0 ; abc= = pleq _ _ refl } |
d8a21c5db0e0
sym5 done but agda won'y stop
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
112
diff
changeset
|
172 dba-triple (s≤s (s≤s z≤n)) (s≤s (s≤s (s≤s (s≤s z≤n)))) = record { dba0<3 = # 2 ; dba1<4 = # 0 ; aec0<3 = # 3 ; aec1<4 = # 2 ; abc= = pleq _ _ refl } |
d8a21c5db0e0
sym5 done but agda won'y stop
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
112
diff
changeset
|
173 dba-triple (s≤s (s≤s (s≤s z≤n))) z≤n = record { dba0<3 = # 0 ; dba1<4 = # 4 ; aec0<3 = # 1 ; aec1<4 = # 0 ; abc= = pleq _ _ refl } |
d8a21c5db0e0
sym5 done but agda won'y stop
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
112
diff
changeset
|
174 dba-triple (s≤s (s≤s (s≤s z≤n))) (s≤s z≤n) = record { dba0<3 = # 0 ; dba1<4 = # 4 ; aec0<3 = # 1 ; aec1<4 = # 0 ; abc= = pleq _ _ refl } |
d8a21c5db0e0
sym5 done but agda won'y stop
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
112
diff
changeset
|
175 dba-triple (s≤s (s≤s (s≤s z≤n))) (s≤s (s≤s z≤n)) = record { dba0<3 = # 3 ; dba1<4 = # 0 ; aec0<3 = # 0 ; aec1<4 = # 2 ; abc= = pleq _ _ refl } |
d8a21c5db0e0
sym5 done but agda won'y stop
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
112
diff
changeset
|
176 dba-triple (s≤s (s≤s (s≤s z≤n))) (s≤s (s≤s (s≤s z≤n))) = record { dba0<3 = # 1 ; dba1<4 = # 3 ; aec0<3 = # 3 ; aec1<4 = # 0 ; abc= = pleq _ _ refl } |
d8a21c5db0e0
sym5 done but agda won'y stop
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
112
diff
changeset
|
177 dba-triple (s≤s (s≤s (s≤s z≤n))) (s≤s (s≤s (s≤s (s≤s z≤n)))) = |
d8a21c5db0e0
sym5 done but agda won'y stop
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
112
diff
changeset
|
178 record { dba0<3 = # 2 ; dba1<4 = # 0 ; aec0<3 = # 3 ; aec1<4 = # 2 ; abc= = pleq _ _ refl } |
d8a21c5db0e0
sym5 done but agda won'y stop
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
112
diff
changeset
|
179 |
115 | 180 -3=33 : pinv 3rot =p= (3rot ∘ₚ 3rot ) |
181 -3=33 = pleq _ _ refl | |
182 | |
116
6022d00a0690
check termination problem remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
115
diff
changeset
|
183 4=1 : (3rot ∘ₚ 3rot) ∘ₚ (3rot ∘ₚ 3rot ) =p= 3rot |
6022d00a0690
check termination problem remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
115
diff
changeset
|
184 4=1 = pleq _ _ refl |
87 | 185 |
114 | 186 dervie-any-3rot0 : (n : ℕ ) → {i j : ℕ } → (i<3 : i ≤ 3 ) → (j<4 : j ≤ 4 ) |
187 → deriving n (abc i<3 j<4 ) | |
188 dervie-any-3rot1 : (n : ℕ ) → {i j : ℕ } → (i<3 : i ≤ 3 ) → (j<4 : j ≤ 4 ) | |
189 → deriving n (dba i<3 j<4 ) | |
116
6022d00a0690
check termination problem remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
115
diff
changeset
|
190 |
6022d00a0690
check termination problem remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
115
diff
changeset
|
191 commd : {n : ℕ } → (f g : Permutation 5 5) |
6022d00a0690
check termination problem remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
115
diff
changeset
|
192 → deriving n f |
6022d00a0690
check termination problem remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
115
diff
changeset
|
193 → deriving n g |
6022d00a0690
check termination problem remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
115
diff
changeset
|
194 → Commutator (deriving n) [ f , g ] |
6022d00a0690
check termination problem remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
115
diff
changeset
|
195 commd {n} f g df dg = comm {deriving n} {f} {g} df dg |
114 | 196 |
197 dervie-any-3rot0 0 i<3 j<4 = lift tt | |
116
6022d00a0690
check termination problem remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
115
diff
changeset
|
198 dervie-any-3rot0 (suc i) i<3 j<4 = ccong {deriving i} (psym ceq) (commd dba0 aec0 df dg )where |
113
d8a21c5db0e0
sym5 done but agda won'y stop
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
112
diff
changeset
|
199 tc = triple i<3 j<4 |
116
6022d00a0690
check termination problem remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
115
diff
changeset
|
200 dba0 = dba (fin≤n {3} (dba0<3 tc)) (fin≤n {4} (dba1<4 tc)) |
6022d00a0690
check termination problem remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
115
diff
changeset
|
201 aec0 = dba (fin≤n {3} (aec0<3 tc)) (fin≤n {4} (aec1<4 tc)) |
6022d00a0690
check termination problem remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
115
diff
changeset
|
202 ceq : abc i<3 j<4 =p= [ dba0 , aec0 ] |
118 | 203 ceq = record { peq = peq (abc= tc) } |
116
6022d00a0690
check termination problem remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
115
diff
changeset
|
204 df = dervie-any-3rot1 i (fin≤n {3} (dba0<3 tc)) (fin≤n {4} (dba1<4 tc)) |
6022d00a0690
check termination problem remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
115
diff
changeset
|
205 dg = dervie-any-3rot1 i (fin≤n {3} (aec0<3 tc)) (fin≤n {4} (aec1<4 tc)) |
114 | 206 |
115 | 207 dervie-any-3rot1 0 i<3 j<4 = lift tt |
116
6022d00a0690
check termination problem remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
115
diff
changeset
|
208 dervie-any-3rot1 (suc n) {i} {j} i<3 j<4 = ccong {deriving n} ( psym ceq ) (commd aec0 abc0 df dg ) where |
113
d8a21c5db0e0
sym5 done but agda won'y stop
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
112
diff
changeset
|
209 tdba = dba-triple i<3 j<4 |
116
6022d00a0690
check termination problem remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
115
diff
changeset
|
210 aec0 = ins2 ((3rot ∘ₚ 3rot) ∘ₚ (3rot ∘ₚ 3rot )) (fin≤n {3} (dba0<3 tdba)) (fin≤n {4} (dba1<4 tdba)) |
6022d00a0690
check termination problem remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
115
diff
changeset
|
211 abc0 = ins2 ((3rot ∘ₚ 3rot) ∘ₚ (3rot ∘ₚ 3rot )) (fin≤n {3} (aec0<3 tdba)) (fin≤n {4} (aec1<4 tdba)) |
6022d00a0690
check termination problem remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
115
diff
changeset
|
212 ceq : dba i<3 j<4 =p= [ aec0 , abc0 ] |
118 | 213 ceq = record { peq = peq (abc= tdba) } |
116
6022d00a0690
check termination problem remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
115
diff
changeset
|
214 df : deriving n (ins2 ((3rot ∘ₚ 3rot) ∘ₚ (3rot ∘ₚ 3rot )) (fin≤n {3} (dba0<3 tdba)) (fin≤n {4} (dba1<4 tdba))) |
6022d00a0690
check termination problem remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
115
diff
changeset
|
215 df = deriving-subst (psym (ins2cong {toℕ (dba0<3 (dba-triple i<3 j<4))} {toℕ (dba1<4 (dba-triple i<3 j<4))} 4=1 )) |
6022d00a0690
check termination problem remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
115
diff
changeset
|
216 (dervie-any-3rot0 n (fin≤n {3} (dba0<3 tdba)) (fin≤n {4} (dba1<4 tdba))) |
6022d00a0690
check termination problem remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
115
diff
changeset
|
217 dg : deriving n (ins2 ((3rot ∘ₚ 3rot) ∘ₚ (3rot ∘ₚ 3rot )) (fin≤n {3} (aec0<3 tdba)) (fin≤n {4} (aec1<4 tdba))) |
6022d00a0690
check termination problem remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
115
diff
changeset
|
218 dg = deriving-subst (psym (ins2cong {toℕ (aec0<3 (dba-triple i<3 j<4))} {toℕ (aec1<4 (dba-triple i<3 j<4))} 4=1 )) |
6022d00a0690
check termination problem remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
115
diff
changeset
|
219 (dervie-any-3rot0 n (fin≤n {3} (aec0<3 tdba)) (fin≤n {4} (aec1<4 tdba))) |
74 | 220 |