# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1598332549 -32400
# Node ID 69ed81f8e2126614e6ac193f7ee946d89b812752
# Parent  9bd1d7cd432c74f9f02efeb895e26f07c374224e
...

diff -r 9bd1d7cd432c -r 69ed81f8e212 Putil.agda
--- a/Putil.agda	Tue Aug 25 11:07:39 2020 +0900
+++ b/Putil.agda	Tue Aug 25 14:15:49 2020 +0900
@@ -132,8 +132,8 @@
 plist {suc j} perm = rev (plist1 j a<sa) where
     n = suc j
     plist1 : (i : ℕ ) → i < n → List ℕ
-    plist1  zero _           = toℕ ( perm ⟨$⟩ˡ (fromℕ≤ {zero} (s≤s z≤n))) ∷ []
-    plist1  (suc i) (s≤s lt) = toℕ ( perm ⟨$⟩ˡ (fromℕ≤ (s≤s lt)))         ∷ plist1  i (<-trans lt a<sa) 
+    plist1  zero _           = toℕ ( perm ⟨$⟩ˡ (fromℕ< {zero} (s≤s z≤n))) ∷ []
+    plist1  (suc i) (s≤s lt) = toℕ ( perm ⟨$⟩ˡ (fromℕ< (s≤s lt)))         ∷ plist1  i (<-trans lt a<sa) 
 
 data  FL : (n : ℕ )→ Set where
    f0 :  FL 0 
@@ -261,7 +261,7 @@
 
 -- t5 = plist t4 ∷ plist ( t4  ∘ₚ flip (pins ( n≤  3 ) ))
 t5 = plist (t4) ∷ plist (flip t4)
-    ∷ ( toℕ (t4 ⟨$⟩ˡ fromℕ≤ a<sa) ∷ [] )
+    ∷ ( toℕ (t4 ⟨$⟩ˡ fromℕ< a<sa) ∷ [] )
     ∷ ( toℕ (t4 ⟨$⟩ʳ (# 0)) ∷ [] )
     -- ∷  plist ( t4  ∘ₚ flip (pins ( n≤  1 ) ))
     ∷  plist (remove (# 0) t4  )
@@ -289,7 +289,7 @@
 ∀-FL  x  = fls6 x  where
    fls4 :  ( i n : ℕ ) → (i<n : i ≤ n ) → FL  n → List (FL  (suc n))  → List (FL  (suc n)) 
    fls4 zero n i≤n perm x = (zero :: perm ) ∷ x
-   fls4 (suc i) n i≤n  perm x = fls4 i n (≤-trans refl-≤s i≤n ) perm ((fromℕ≤ (s≤s i≤n) :: perm ) ∷ x)
+   fls4 (suc i) n i≤n  perm x = fls4 i n (≤-trans refl-≤s i≤n ) perm ((fromℕ< (s≤s i≤n) :: perm ) ∷ x)
    fls5 :  ( n : ℕ ) → List (FL n) → List (FL  (suc n))  → List (FL (suc n)) 
    fls5 n [] x = x
    fls5 n (h ∷ x) y = fls5  n x (fls4 n n lem0 h y)
diff -r 9bd1d7cd432c -r 69ed81f8e212 fin.agda
--- a/fin.agda	Tue Aug 25 11:07:39 2020 +0900
+++ b/fin.agda	Tue Aug 25 14:15:49 2020 +0900
@@ -40,7 +40,7 @@
 
 open import Data.Nat.Properties as NatP  hiding ( _≟_ )
 
-fin+1≤ : { i n : ℕ } → (a : i < n)  → fin+1 (fromℕ≤ a) ≡ fromℕ≤ (<-trans a a<sa)
+fin+1≤ : { i n : ℕ } → (a : i < n)  → fin+1 (fromℕ< a) ≡ fromℕ< (<-trans a a<sa)
 fin+1≤ {0} {suc i} (s≤s z≤n) = refl
 fin+1≤ {suc n} {suc (suc i)} (s≤s (s≤s a)) = cong (λ k → suc k ) ( fin+1≤ {n} {suc i} (s≤s a) )
 
@@ -66,9 +66,9 @@
 -- suc-eq : {n : ℕ } {x y : Fin n} → Fin.suc x ≡ Fin.suc y  → x ≡ y
 -- suc-eq {n} {x} {y} eq = subst₂ (λ j k → j ≡ k ) {!!} {!!} (cong (λ k → Data.Fin.pred k ) eq )
 
-lemma3 : {a b : ℕ } → (lt : a < b ) → fromℕ≤ (s≤s lt) ≡ suc (fromℕ≤ lt)
+lemma3 : {a b : ℕ } → (lt : a < b ) → fromℕ< (s≤s lt) ≡ suc (fromℕ< lt)
 lemma3 (s≤s lt) = refl
-lemma12 : {n m : ℕ } → (n<m : n < m ) → (f : Fin m )  → toℕ f ≡ n → f ≡ fromℕ≤ n<m 
+lemma12 : {n m : ℕ } → (n<m : n < m ) → (f : Fin m )  → toℕ f ≡ n → f ≡ fromℕ< n<m 
 lemma12 {zero} {suc m} (s≤s z≤n) zero refl = refl
 lemma12 {suc n} {suc m} (s≤s n<m) (suc f) refl = subst ( λ k → suc f ≡ k ) (sym (lemma3 n<m) ) ( cong ( λ k → suc k ) ( lemma12 {n} {m} n<m f refl  ) )
 
@@ -78,14 +78,14 @@
 lemma8 : {i j n : ℕ } → ( i ≡ j ) → {i<n : i < n } → {j<n : j < n } → i<n ≅ j<n  
 lemma8 {zero} {zero} {suc n} refl {s≤s z≤n} {s≤s z≤n} = HE.refl
 lemma8 {suc i} {suc i} {suc n} refl {s≤s i<n} {s≤s j<n} = HE.cong (λ k → s≤s k ) ( lemma8 {i} {i} {n} refl  )
-lemma10 : {n i j  : ℕ } → ( i ≡ j ) → {i<n : i < n } → {j<n : j < n }  → fromℕ≤ i<n ≡ fromℕ≤ j<n
-lemma10 {n} refl  = HE.≅-to-≡ (HE.cong (λ k → fromℕ≤ k ) (lemma8 refl  ))
+lemma10 : {n i j  : ℕ } → ( i ≡ j ) → {i<n : i < n } → {j<n : j < n }  → fromℕ< i<n ≡ fromℕ< j<n
+lemma10 {n} refl  = HE.≅-to-≡ (HE.cong (λ k → fromℕ< k ) (lemma8 refl  ))
 lemma31 : {a b c : ℕ } → { a<b : a < b } { b<c : b < c } { a<c : a < c } → NatP.<-trans a<b b<c ≡ a<c
 lemma31 {a} {b} {c} {a<b} {b<c} {a<c} = HE.≅-to-≡ (lemma8 refl) 
-lemma11 : {n m : ℕ } {x : Fin n } → (n<m : n < m ) → toℕ (fromℕ≤ (NatP.<-trans (toℕ<n x) n<m)) ≡ toℕ x
+lemma11 : {n m : ℕ } {x : Fin n } → (n<m : n < m ) → toℕ (fromℕ< (NatP.<-trans (toℕ<n x) n<m)) ≡ toℕ x
 lemma11 {n} {m} {x} n<m  = begin
-              toℕ (fromℕ≤ (NatP.<-trans (toℕ<n x) n<m))
-           ≡⟨ toℕ-fromℕ≤ _ ⟩
+              toℕ (fromℕ< (NatP.<-trans (toℕ<n x) n<m))
+           ≡⟨ toℕ-fromℕ< _ ⟩
               toℕ x
            ∎  where
                open ≡-Reasoning
diff -r 9bd1d7cd432c -r 69ed81f8e212 logic.agda
--- a/logic.agda	Tue Aug 25 11:07:39 2020 +0900
+++ b/logic.agda	Tue Aug 25 14:15:49 2020 +0900
@@ -2,7 +2,7 @@
 
 open import Level
 open import Relation.Nullary
-open import Relation.Binary
+open import Relation.Binary hiding (_⇔_ )
 open import Data.Empty
 
 
diff -r 9bd1d7cd432c -r 69ed81f8e212 nat.agda
--- a/nat.agda	Tue Aug 25 11:07:39 2020 +0900
+++ b/nat.agda	Tue Aug 25 14:15:49 2020 +0900
@@ -7,6 +7,7 @@
 open import Relation.Nullary
 open import  Relation.Binary.PropositionalEquality
 open import  Relation.Binary.Core
+open import Relation.Binary.Definitions
 open import  logic
 
 
diff -r 9bd1d7cd432c -r 69ed81f8e212 sym5.agda
--- a/sym5.agda	Tue Aug 25 11:07:39 2020 +0900
+++ b/sym5.agda	Tue Aug 25 14:15:49 2020 +0900
@@ -16,12 +16,12 @@
 open import Solvable using (solvable)
 open import  Relation.Binary.PropositionalEquality hiding ( [_] )
 
-open import Data.Fin
+open import Data.Fin hiding (_<_ ; lift )
 open import Data.Fin.Permutation
 open import Data.List  hiding ( [_] )
 
 ¬sym5solvable : ¬ ( solvable (Symmetric 5) )
-¬sym5solvable sol = counter-example (end5  [ dba , aec ] d ) where
+¬sym5solvable sol = counter-example (end5 (abc 0<4 0<3 ) (dervie-any-3rot (dervied-length sol) 0<4 0<3 ) ) where
 
 --
 --    dba       1320      d → b → a → d
@@ -36,32 +36,63 @@
      end5 : (x : Permutation 5 5) → deriving (dervied-length sol) x →  x =p= pid  
      end5 x der = end sol x der
 
+     0<4 : 0 < 4
+     0<4 = {!!}
+
+     0<3 : 0 < 3
+     0<3 = {!!}
+
+     --- 2 ∷ 0 ∷ 1 ∷ []
+     3rot : Permutation 3 3
+     3rot = {!!} -- pswap (pid {0}) ∘ₚ pins (n≤ 1)
+
+     abc : {i j : ℕ }  → (i < 4 ) → ( j < 3 ) → Permutation  5 5
+     abc i<4 j<3 = {!!} -- (3rot ∘ₚ pins i<4 )  ∘ₚ pins j<3
+
+     dba-0 : {i j : ℕ } → (i < 4 ) → ( j < 3 ) → ( j < 4 ) 
+     dba-0 = {!!}
+     dba-1 : {i j : ℕ } → (i < 4 ) → ( j < 3 ) → ( j < 3 )
+     dba-1 = {!!}
+
+     dba : {i j : ℕ }  → (i < 4 ) → ( j < 3 ) → Permutation  5 5
+     dba i<4 j<3 = abc (dba-0 i<4 j<3 ) (dba-1 i<4 j<3 )
+
+     aec-0 : {i j : ℕ } → (i < 4 ) → ( j < 3 ) → ( j < 4 ) 
+     aec-0 = {!!}
+     aec-1 : {i j : ℕ } → (i < 4 ) → ( j < 3 ) → ( j < 3 )
+     aec-1 = {!!}
+
+     aec : {i j : ℕ }  → (i < 4 ) → ( j < 3 ) → Permutation  5 5
+     aec i<4 j<3 = abc (aec-0 i<4 j<3 ) (aec-1 i<4 j<3 )
+
+     [dba,aec]=abc : {i j : ℕ }  → (i<4 : i < 4 ) → (j<3 : j < 3 ) → [ dba i<4 j<3 , aec i<4 j<3 ] =p= abc i<4 j<3
+     [dba,aec]=abc = {!!}
+
+     dervie-any-3rot : (n : ℕ ) → {i j : ℕ }  → (i<4 : i < 4 ) → (j<3 : j < 3 ) → deriving n (abc i<4 j<3 )
+     dervie-any-3rot 0 i<4 j<3 = lift tt
+     dervie-any-3rot (suc i) i<4 j<3 = 
+         ccong ( [dba,aec]=abc i<4 j<3 ) (
+         comm {{!!}} {dba i<4 j<3} {aec i<4 j<3 } 
+             ( dervie-any-3rot i (dba-0 i<4 j<3) (dba-1 i<4 j<3) ) 
+             ( dervie-any-3rot i (aec-0 i<4 j<3) (aec-1 i<4 j<3) ))
+
+     open _=p=_
+     counter-example :  ¬ (abc 0<4 0<3  =p= pid )
+     counter-example = {!!}
+
+
      --- 1 ∷ 0 ∷ 2 ∷ []
      --- 0 ∷ 2 ∷ 1 ∷ 3 ∷ []
      --- 1 ∷ 3 ∷ 2 ∷ 0 ∷ 4 ∷ []
      --  2 ∷ 1 ∷ 3 ∷ 0 ∷ 4 ∷ []  (dba)⁻¹ = abd
-     dba : Permutation 5 5
-     dba = pprep (pprep (pswap (pid {1}))) ∘ₚ pins (n≤ 3)
-     t1 = plist dba ∷ plist (pinv dba) ∷ []
+     dba99  : Permutation 5 5
+     dba99 = pprep (pprep (pswap (pid {1}))) ∘ₚ pins (n≤ 3)
+     t1 = plist dba99 ∷ plist (pinv dba99) ∷ []
      --  1 ∷ 0 ∷ []  
      --  0 ∷ 2 ∷ 1 ∷ []  
      --  1 ∷ 0 ∷ 3 ∷ 2 ∷ []  
      --  2 ∷ 1 ∷ 4 ∷ 3 ∷ 0 ∷ []  
      --  4 ∷ 1 ∷ 0 ∷ 3 ∷ 2 ∷ []  (aec)⁻¹ = cea
-     aec : Permutation 5 5
-     aec = pprep (pprep (pprep (pswap (pid {0}))) ∘ₚ pins (n≤ 1)) ∘ₚ pins (n≤ 4)
-     tt2 = plist aec ∷ plist (pinv aec) ∷ []
-
-     open _=p=_
-     postulate counter-example : ¬ ( [ dba , aec ] =p= pid )
-     -- counter-example eq with peq eq zero
-     -- counter-example eq | ()
-
-     d : deriving (dervied-length sol) [ dba , aec ] 
-     d = {!!}
-     -- d with dervied-length sol
-     -- ... | zero = Lift.lift tt
-     -- ... | suc i = comm {?} {dba} {aec} ? ?
-
-
-
+     aec99 : Permutation 5 5
+     aec99 = pprep (pprep (pprep (pswap (pid {0}))) ∘ₚ pins (n≤ 1)) ∘ₚ pins (n≤ 4)
+     tt2 = plist aec99 ∷ plist (pinv aec99) ∷ []