Mercurial > hg > Members > kono > Proof > galois

changeset 76:cef943dcd18c

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
rot3 corret?
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 26 Aug 2020 01:41:52 +0900
parents 4b17a4daf2df
children fba304a25c36
files sym5.agda
diffstat 1 files changed, 17 insertions(+), 18 deletions(-) [+]
line wrap: on
line diff
--- a/sym5.agda	Wed Aug 26 00:53:33 2020 +0900
+++ b/sym5.agda	Wed Aug 26 01:41:52 2020 +0900
@@ -23,7 +23,7 @@
 open import nat
 
 ¬sym5solvable : ¬ ( solvable (Symmetric 5) )
-¬sym5solvable sol = counter-example (end5 (abc 0<3 0<4 ) (dervie-any-3rot (dervied-length sol) 0<3 0<4 ) ) where
+¬sym5solvable sol = counter-example {!!} where -- (end5 (abc ? 0<4 ) (dervie-any-3rot (dervied-length sol) 0<3 0<4 ) ) where
 
 --
 --    dba       1320      d → b → a → d
@@ -51,7 +51,7 @@
      abc : {i j : ℕ }  → (i ≤ 3 ) → ( j ≤ 4 ) → Permutation  5 5
      abc i<3 j<4 = (save2 ∘ₚ (pprep (pprep 3rot))) ∘ₚ flip save2  where
           save2 : Permutation  5 5
-          save2 = ( (pprep ( pid {4} ∘ₚ flip (pins i<3 ) )) ∘ₚ flip (pins j<4)) 
+          save2 = ( (( pid {5} ∘ₚ flip (pins (s≤s i<3) ) )) ∘ₚ flip (pins j<4)) 
 
      dba-0 : {i j : ℕ } → (i < 4 ) → ( j < 3 ) → ( j < 4 ) 
      dba-0 = {!!}
@@ -59,7 +59,7 @@
      dba-1 = {!!}
 
      dba : {i j : ℕ }  → (i < 3 ) → ( j < 4 ) → Permutation  5 5
-     dba i<3 j<4 = abc (dba-1 j<4 i<3 ) (dba-0 j<4 i<3 )
+     dba i<3 j<4 = abc {!!} (dba-0 j<4 i<3 )
 
      aec-0 : {i j : ℕ } → (i < 4 ) → ( j < 3 ) → ( j < 4 ) 
      aec-0 = {!!}
@@ -67,23 +67,22 @@
      aec-1 = {!!}
 
      aec : {i j : ℕ }  → (i < 3 ) → ( j < 4 ) → Permutation  5 5
-     aec i<3 j<4 = abc (aec-1 j<4 i<3 ) (aec-0 j<4 i<3 )
+     aec i<3 j<4 = abc {!!} (aec-0 j<4 i<3 )
 
-     [dba,aec]=abc : {i j : ℕ }  → (i<4 : i < 4 ) → (j<3 : j < 3 ) → [ dba j<3 i<4 , aec j<3 i<4 ] =p= abc j<3 i<4
+     [dba,aec]=abc : {i j : ℕ }  → (i<4 : i < 4 ) → (j<3 : j < 3 ) → [ dba j<3 i<4 , aec j<3 i<4 ] =p= abc {!!} i<4
      [dba,aec]=abc = {!!}
 
      --- 2 ∷ 0 ∷ 1 ∷ []      abc
      t10 : List (List ℕ )
-     t10 =   t101 (n≤ 4) (n≤ 5)  [] where
-          t101 : { i j : ℕ } → i ≤ 4 → j ≤ 5  → List (List ℕ ) → List (List ℕ )
+     t10 =   t101 (n≤ 3) (n≤ 4)  [] where
+          t101 : { i j : ℕ } → i ≤ 3 → j ≤ 4  → List (List ℕ ) → List (List ℕ )
           t101 z≤n z≤n t =  plist (abc z≤n z≤n) ∷ t 
-          t101 z≤n (s≤s y) t = t101 y (≤-trans y refl-≤s) ( plist (abc z≤n (y)) ∷ t )
-          t101 (s≤s x) z≤n t = t101 (≤-trans x refl-≤s)  z≤n  ( plist (abc (x) z≤n) ∷ t )
-          t101 (s≤s x) (s≤s y) t = t101 (≤-trans x refl-≤s)  (s≤s y) ( plist (abc (x) y) ∷ t )
+          t101 z≤n (s≤s y) t = t101 (n≤ 3) (≤-trans y refl-≤s) ( plist (abc z≤n (s≤s y)) ∷ t )
+          t101 (s≤s x) z≤n t = t101 (≤-trans x refl-≤s) z≤n ( plist (abc (s≤s x) z≤n) ∷ t )
+          t101 (s≤s x) (s≤s y) t = t101 (≤-trans x refl-≤s)  (s≤s y) ( plist (abc (s≤s x) (s≤s y)) ∷ t )
           -- t101 (s≤s x) z≤n t = t101 (≤-trans x ?) x ( abc (s≤s x) z≤n ∷ t )
           -- t101 (s≤s x) (s≤s y) t = {!!}
      t12 = {!!}
-     
      --- 0 ∷ 1 ∷ 2 ∷ 3 ∷ 4 ∷ [] 
      --- 1 ∷ 0 ∷ 2 ∷ 3 ∷ 4 ∷ [] 
      --- 1 ∷ 2 ∷ 0 ∷ 3 ∷ 4 ∷ [] 
@@ -101,16 +100,16 @@
      --- 1 ∷ 3 ∷ 2 ∷ 0 ∷ 4 ∷ []     abd 
      --  2 ∷ 1 ∷ 4 ∷ 3 ∷ 0 ∷ []     cea
 
-     dervie-any-3rot : (n : ℕ ) → {i j : ℕ }  → (i<3 : i < 3 ) → (j<4 : j < 4 ) → deriving n (abc i<3 j<4 )
+     dervie-any-3rot : (n : ℕ ) → {i j : ℕ }  → (i<3 : i < 3 ) → (j<4 : j < 4 ) → deriving n (abc {!!} j<4 )
      dervie-any-3rot 0 i<3 j<4 = lift tt
-     dervie-any-3rot (suc i) i<3 j<4 = 
-         ccong ( [dba,aec]=abc j<4 i<3 ) (
-         comm {{!!}} {dba i<3 j<4} {aec i<3 j<4 } 
-             ( dervie-any-3rot i (dba-1 j<4 i<3) (dba-0 j<4 i<3 ) ) 
-             ( dervie-any-3rot i (aec-1 j<4 i<3) (aec-0 j<4 i<3 ) ))
+     dervie-any-3rot (suc i) i<3 j<4 =  {!!}
+         -- ccong ( [dba,aec]=abc j<4 i<3 ) (
+         -- comm {{!!}} {dba i<3 j<4} {aec i<3 j<4 } 
+         --     ( dervie-any-3rot i (dba-1 j<4 i<3) (dba-0 j<4 i<3 ) ) 
+         --     ( dervie-any-3rot i (aec-1 j<4 i<3) (aec-0 j<4 i<3 ) ))
 
      open _=p=_
-     counter-example :  ¬ (abc 0<3 0<4  =p= pid )
+     counter-example :  ¬ (abc {!!} 0<4  =p= pid )
      counter-example = {!!}