Mercurial > hg > Members > kono > Proof > galois
changeset 116:6022d00a0690
check termination problem remains
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Thu, 03 Sep 2020 11:45:42 +0900 |
| parents | 32df4073746e |
| children | 540d109b599c |
| files | Solvable.agda sym5.agda |
| diffstat | 2 files changed, 41 insertions(+), 51 deletions(-) [+] |
line wrap: on
line diff
--- a/Solvable.agda Thu Sep 03 09:11:05 2020 +0900 +++ b/Solvable.agda Thu Sep 03 11:45:42 2020 +0900 @@ -28,6 +28,12 @@ deriving 0 x = Lift (Level.suc n ⊔ m) ⊤ deriving (suc i) x = Commutator (deriving i) x +open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) + +deriving-subst : { i : ℕ } → {x y : Carrier } → x ≈ y → (dx : deriving i x ) → deriving i y +deriving-subst {zero} {x} {y} x=y dx = lift tt +deriving-subst {suc i} {x} {y} x=y dx = ccong x=y dx + record solvable : Set (Level.suc n ⊔ m) where field dervied-length : ℕ
--- a/sym5.agda Thu Sep 03 09:11:05 2020 +0900 +++ b/sym5.agda Thu Sep 03 11:45:42 2020 +0900 @@ -18,7 +18,11 @@ open import Relation.Binary.PropositionalEquality hiding ( [_] ) open import Data.Fin hiding (_<_ ; _≤_ ; lift ) -open import Data.Fin.Permutation +open import Data.Fin.Permutation hiding (_∘ₚ_) + +infixr 200 _∘ₚ_ +_∘ₚ_ = Data.Fin.Permutation._∘ₚ_ + open import Data.List hiding ( [_] ) open import nat open import fin @@ -60,9 +64,9 @@ ins2 : {i j : ℕ } → Permutation 3 3 → (i ≤ 3 ) → ( j ≤ 4 ) → Permutation 5 5 ins2 abc i<3 j<4 = (save2 i<3 j<4 ∘ₚ (pprep (pprep abc))) ∘ₚ flip (save2 i<3 j<4 ) - -- 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 - -- 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 )} - -- (presp {5} {save2 i<3 j<4} prefl (pprep-cong (pprep-cong x=y)) ) prefl + 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 + 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 )} + (presp {5} {save2 i<3 j<4} prefl (pprep-cong (pprep-cong x=y)) ) prefl open _=p=_ @@ -79,7 +83,7 @@ dba1<4 : Fin 5 aec0<3 : Fin 4 aec1<4 : Fin 5 - abc= : ins2 rot i<3 j<4 =p= [ ins2 (rot ∘ₚ rot) (fin≤n {3} dba0<3) (fin≤n {4} dba1<4) , ins2 (pinv rot) (fin≤n {3} aec0<3) (fin≤n {4} aec1<4) ] + 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) ] open Triple triple : {i j : ℕ } → (i<3 : i ≤ 3) (j<4 : j ≤ 4) → Triple i<3 j<4 3rot @@ -172,66 +176,46 @@ dba-triple (s≤s (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 } - -3=33 : pinv 3rot =p= (3rot ∘ₚ 3rot ) -3=33 = pleq _ _ refl - -- so aec-triple ≡ dba-triple, cong-Triple is valid but difficutl to prove - -- - aec-triple : {i j : ℕ } → (i<3 : i ≤ 3 ) → (j<4 : j ≤ 4 ) → Triple i<3 j<4 (pinv 3rot ) - aec-triple z≤n z≤n = record { dba0<3 = # 0 ; dba1<4 = # 2 ; aec0<3 = # 2 ; aec1<4 = # 0 ; abc= = pleq _ _ refl } - aec-triple z≤n (s≤s z≤n) = record { dba0<3 = # 0 ; dba1<4 = # 2 ; aec0<3 = # 2 ; aec1<4 = # 0 ; abc= = pleq _ _ refl } - aec-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 } - aec-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 } - aec-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 } - aec-triple (s≤s z≤n) z≤n = record { dba0<3 = # 0 ; dba1<4 = # 0 ; aec0<3 = # 1 ; aec1<4 = # 3 ; abc= = pleq _ _ refl } - aec-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 } - aec-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 } - aec-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 } - aec-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 } - aec-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 } - aec-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 } - aec-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 } - aec-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 } - aec-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 } - aec-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 } - aec-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 } - aec-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 } - aec-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 } - aec-triple (s≤s (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 } - + 4=1 : (3rot ∘ₚ 3rot) ∘ₚ (3rot ∘ₚ 3rot ) =p= 3rot + 4=1 = pleq _ _ refl dervie-any-3rot0 : (n : ℕ ) → {i j : ℕ } → (i<3 : i ≤ 3 ) → (j<4 : j ≤ 4 ) → deriving n (abc i<3 j<4 ) dervie-any-3rot1 : (n : ℕ ) → {i j : ℕ } → (i<3 : i ≤ 3 ) → (j<4 : j ≤ 4 ) → deriving n (dba i<3 j<4 ) - dervie-any-3rot2 : (n : ℕ ) → {i j : ℕ } → (i<3 : i ≤ 3 ) → (j<4 : j ≤ 4 ) - → deriving n (aec i<3 j<4 ) + + commd : {n : ℕ } → (f g : Permutation 5 5) + → deriving n f + → deriving n g + → Commutator (deriving n) [ f , g ] + commd {n} f g df dg = comm {deriving n} {f} {g} df dg dervie-any-3rot0 0 i<3 j<4 = lift tt - dervie-any-3rot0 (suc i) i<3 j<4 = - ccong {deriving i} ( psym (abc= tc)) ( - comm {deriving i} {dba (fin≤n {3} (dba0<3 tc)) (fin≤n {4} (dba1<4 tc))} {aec (fin≤n {3} (aec0<3 tc)) (fin≤n {4} (aec1<4 tc))} - ( dervie-any-3rot1 i (fin≤n {3} (dba0<3 tc)) (fin≤n {4} (dba1<4 tc))) - ( dervie-any-3rot2 i (fin≤n {3} (aec0<3 tc)) (fin≤n {4} (aec1<4 tc)))) where + dervie-any-3rot0 (suc i) i<3 j<4 = ccong {deriving i} (psym ceq) (commd dba0 aec0 df dg )where tc = triple i<3 j<4 + dba0 = dba (fin≤n {3} (dba0<3 tc)) (fin≤n {4} (dba1<4 tc)) + aec0 = dba (fin≤n {3} (aec0<3 tc)) (fin≤n {4} (aec1<4 tc)) + ceq : abc i<3 j<4 =p= [ dba0 , aec0 ] + ceq = {!!} -- abc= tc + df = dervie-any-3rot1 i (fin≤n {3} (dba0<3 tc)) (fin≤n {4} (dba1<4 tc)) + dg = dervie-any-3rot1 i (fin≤n {3} (aec0<3 tc)) (fin≤n {4} (aec1<4 tc)) dervie-any-3rot1 0 i<3 j<4 = lift tt - dervie-any-3rot1 (suc i) i<3 j<4 = - ccong {deriving i} ( psym (abc= tdba )) ( - comm {deriving i} {aec (fin≤n {3} (dba0<3 tdba)) (fin≤n {4} (dba1<4 tdba))} {abc (fin≤n {3} (aec0<3 tdba)) (fin≤n {4} (aec1<4 tdba))} - (dervie-any-3rot2 i (fin≤n {3} (dba0<3 tdba)) (fin≤n {4} (dba1<4 tdba))) - (dervie-any-3rot0 i (fin≤n {3} (aec0<3 tdba)) (fin≤n {4} (aec1<4 tdba)))) where + dervie-any-3rot1 (suc n) {i} {j} i<3 j<4 = ccong {deriving n} ( psym ceq ) (commd aec0 abc0 df dg ) where tdba = dba-triple i<3 j<4 - - dervie-any-3rot2 0 i<3 j<4 = lift tt - dervie-any-3rot2 (suc i) i<3 j<4 = - ccong {deriving i} ( psym (abc= (aec-triple i<3 j<4) )) ( - comm {deriving i} {abc (fin≤n {3} (dba0<3 taec)) (fin≤n {4} (dba1<4 taec) )} {dba (fin≤n {3} (aec0<3 taec)) (fin≤n {4} (aec1<4 taec))} - ( dervie-any-3rot0 i (fin≤n {3} (dba0<3 taec)) (fin≤n {4} (dba1<4 taec))) - ( dervie-any-3rot1 i (fin≤n {3} (aec0<3 taec)) (fin≤n {4} (aec1<4 taec)))) where - taec = aec-triple i<3 j<4 + aec0 = ins2 ((3rot ∘ₚ 3rot) ∘ₚ (3rot ∘ₚ 3rot )) (fin≤n {3} (dba0<3 tdba)) (fin≤n {4} (dba1<4 tdba)) + abc0 = ins2 ((3rot ∘ₚ 3rot) ∘ₚ (3rot ∘ₚ 3rot )) (fin≤n {3} (aec0<3 tdba)) (fin≤n {4} (aec1<4 tdba)) + ceq : dba i<3 j<4 =p= [ aec0 , abc0 ] + ceq = abc= tdba + df : deriving n (ins2 ((3rot ∘ₚ 3rot) ∘ₚ (3rot ∘ₚ 3rot )) (fin≤n {3} (dba0<3 tdba)) (fin≤n {4} (dba1<4 tdba))) + 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 )) + (dervie-any-3rot0 n (fin≤n {3} (dba0<3 tdba)) (fin≤n {4} (dba1<4 tdba))) + dg : deriving n (ins2 ((3rot ∘ₚ 3rot) ∘ₚ (3rot ∘ₚ 3rot )) (fin≤n {3} (aec0<3 tdba)) (fin≤n {4} (aec1<4 tdba))) + 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 )) + (dervie-any-3rot0 n (fin≤n {3} (aec0<3 tdba)) (fin≤n {4} (aec1<4 tdba))) open _=p=_ counter-example : ¬ (abc 0<3 0<4 =p= pid )