Mercurial > hg > Members > kono > Proof > galois

changeset 115:32df4073746e

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 03 Sep 2020 09:11:05 +0900
parents eb1dcba4752e
children 6022d00a0690
files sym5.agda
diffstat 1 files changed, 15 insertions(+), 9 deletions(-) [+]
line wrap: on
line diff
--- a/sym5.agda	Wed Sep 02 19:20:20 2020 +0900
+++ b/sym5.agda	Thu Sep 03 09:11:05 2020 +0900
@@ -27,7 +27,7 @@
 open _∧_
 
 ¬sym5solvable : ¬ ( solvable (Symmetric 5) )
-¬sym5solvable sol = counter-example (end5 (abc 0<3 0<4 ) (proj1 (dervie-any-3rot0 (dervied-length sol) 0<3 0<4 ) )) where
+¬sym5solvable sol = counter-example (end5 (abc 0<3 0<4 ) (dervie-any-3rot0 (dervied-length sol) 0<3 0<4 ) ) where
 
 --
 --    dba       1320      d → b → a → d
@@ -173,6 +173,11 @@
                                                     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 }
@@ -197,7 +202,6 @@
                                                     record { dba0<3 = # 2 ; dba1<4 = # 0 ; aec0<3 = # 3 ; aec1<4 = # 2 ; abc= = 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 )
@@ -206,25 +210,27 @@
           → deriving n (aec i<3 j<4 )
 
      dervie-any-3rot0 0 i<3 j<4 = lift tt 
-     dervie-any-3rot0 (suc i) i<3 j<4 =  
+     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
         tc = triple i<3 j<4
 
-     dervie-any-3rot1 (suc i) i<3 j<4 = {!!} 
+     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-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
         tdba = dba-triple i<3 j<4
 
-     dervie-any-3rot2 (suc i) 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
+              ( 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
 
      open _=p=_