# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1598458772 -32400
# Node ID 2d79a2c06c6cfd94b69d4e6a9dbf7daa03a8d0aa
# Parent  7e36bd8916a9d19cece7661787306d93caf6ab54
...

diff -r 7e36bd8916a9 -r 2d79a2c06c6c Putil.agda
--- a/Putil.agda	Wed Aug 26 23:53:40 2020 +0900
+++ b/Putil.agda	Thu Aug 27 01:19:32 2020 +0900
@@ -144,6 +144,14 @@
 plist0 {0} perm = []
 plist0 {suc n} perm = plist2 perm n a<sa
 
+open _=p=_
+
+←pleq  : {n  : ℕ} → (x y : Permutation n n ) → x =p= y → plist0 x ≡ plist0 y 
+←pleq {zero} x y eq = refl
+←pleq {suc n} x y eq =  ←pleq1  n a<sa where
+   ←pleq1  :   (i : ℕ ) → (i<sn : i < suc n ) →  plist2 x i i<sn ≡ plist2 y i i<sn
+   ←pleq1  zero _           = cong ( λ k → toℕ k ∷ [] ) ( peq eq (fromℕ< {zero} (s≤s z≤n)))
+   ←pleq1  (suc i) (s≤s lt) = cong₂ ( λ j k → toℕ j ∷ k ) ( peq eq (fromℕ< (s≤s lt)))  ( ←pleq1  i (<-trans lt a<sa) )
 
 headeq : {A : Set } →  {x y : A } → {xt yt : List A } → (x ∷ xt)  ≡ (y ∷ yt)  →  x ≡ y
 headeq refl = refl
diff -r 7e36bd8916a9 -r 2d79a2c06c6c sym5.agda
--- a/sym5.agda	Wed Aug 26 23:53:40 2020 +0900
+++ b/sym5.agda	Thu Aug 27 01:19:32 2020 +0900
@@ -52,10 +52,11 @@
      3rot : Permutation 3 3
      3rot = pid {3} ∘ₚ pins (n≤ 2)
 
+     save2 : {i j : ℕ }  → (i ≤ 3 ) → ( j ≤ 4 ) →  Permutation  5 5 
+     save2 i<3 j<4 = flip (pins (s≤s i<3)) ∘ₚ flip (pins j<4) 
+
      ins2 : {i j : ℕ }  → Permutation 3 3  → (i ≤ 3 ) → ( j ≤ 4 ) → Permutation  5 5
-     ins2 abc i<3 j<4 = (save2 ∘ₚ (pprep (pprep abc))) ∘ₚ flip save2  where
-          save2 : Permutation  5 5
-          save2 = ( (( pid {5} ∘ₚ flip (pins (s≤s i<3) ) )) ∘ₚ flip (pins j<4)) 
+     ins2 abc i<3 j<4 = (save2 i<3 j<4 ∘ₚ (pprep (pprep abc))) ∘ₚ flip (save2 i<3 j<4 ) 
 
      abc : {i j : ℕ }  → (i ≤ 3 ) → ( j ≤ 4 ) → Permutation  5 5
      abc i<3 j<4 = ins2 3rot i<3 j<4
@@ -65,6 +66,33 @@
      aec : {i j : ℕ }  → (i ≤ 3 ) → ( j ≤ 4 ) → Permutation  5 5
      aec i<3 j<4 = ins2 (pinv 3rot) i<3 j<4
 
+     import Relation.Binary.Reasoning.Setoid as EqReasoning
+     abc→dba : {i j : ℕ }  → (i<3 : i ≤ 3 ) → (j<4 :  j ≤ 4 ) →  (abc i<3 j<4 ∘ₚ abc i<3 j<4 ) =p=  dba i<3 j<4 
+     abc→dba i<3 j<4 = lemma where
+       open EqReasoning (Algebra.Group.setoid (Symmetric 5))
+       lemma : (abc i<3 j<4 ∘ₚ abc i<3 j<4 ) =p=  dba i<3 j<4 
+       lemma = begin
+          abc i<3 j<4 ∘ₚ abc i<3 j<4 
+         ≈⟨ prefl ⟩
+          ((save2 i<3 j<4 ∘ₚ (pprep (pprep 3rot))) ∘ₚ flip (save2 i<3 j<4 )) ∘ₚ
+             ((save2 i<3 j<4 ∘ₚ (pprep (pprep 3rot))) ∘ₚ flip (save2 i<3 j<4 ))
+         ≈⟨ {!!} ⟩
+          (((save2 i<3 j<4 ∘ₚ (pprep (pprep 3rot))) ∘ₚ (flip (save2 i<3 j<4 ))) ∘ₚ
+             (save2 i<3 j<4 ∘ₚ (pprep (pprep 3rot)))) ∘ₚ flip (save2 i<3 j<4 )
+         ≈⟨ {!!} ⟩
+          (save2 i<3 j<4 ∘ₚ (pprep (pprep 3rot) ∘ₚ pprep (pprep 3rot))) ∘ₚ flip (save2 i<3 j<4 )
+         ≈⟨ {!!} ⟩
+          (save2 i<3 j<4 ∘ₚ (pprep (pprep (3rot ∘ₚ 3rot)))) ∘ₚ flip (save2 i<3 j<4 )
+         ≈⟨ prefl ⟩
+          dba i<3 j<4
+         ∎
+
+     dba→aec : {i j : ℕ }  → (i<3 : i ≤ 3 ) → (j<4 :  j ≤ 4 ) →  (dba i<3 j<4 ∘ₚ dba i<3 j<4 ) =p=  aec i<3 j<4 
+     dba→aec = {!!}
+
+     aec→abc : {i j : ℕ }  → (i<3 : i ≤ 3 ) → (j<4 :  j ≤ 4 ) →  (aec i<3 j<4 ∘ₚ aec i<3 j<4 ) =p=  abc i<3 j<4 
+     aec→abc = {!!}
+
      record Triple {i j : ℕ } (i<3 : i ≤ 3) (j<4 : j ≤ 4) : Set where
        field 
          dba0<3 : Fin 4
@@ -73,66 +101,30 @@
          aec1<4 : Fin 5
          abc= : abc i<3 j<4 =p= [ dba (fin≤n {3} dba0<3) (fin≤n {4} dba1<4)  , aec (fin≤n {3} aec0<3) (fin≤n {4} aec1<4) ]
 
-     open Triple
-     --                                                 a   b   c   d   e
-     t1 = (plist ( abc (n≤ 0) (n≤ 0) )  ++ ( 0 ∷ 0 ∷ [])) -- (  ∷   ∷ 3 ∷ 4 ∷ 2 ∷ []) ∷  cde  no 4 on top
-      -- ∷  (plist ( abc (n≤ 0) (n≤ 1) )  ++ ( 0 ∷ 1 ∷ [])) -- (  ∷   ∷ 3 ∷ 4 ∷ 2 ∷ []) ∷  
-      -- ∷  (plist ( abc (n≤ 0) (n≤ 2) )  ++ ( 0 ∷ 2 ∷ [])) -- (3 ∷   ∷   ∷ 4 ∷ 0 ∷ []) ∷     
-      -- ∷  (plist ( abc (n≤ 0) (n≤ 3) )  ++ ( 0 ∷ 3 ∷ [])) -- (2 ∷   ∷ 4 ∷   ∷ 0 ∷ []) ∷  120 : aec 
-      -- ∷  (plist ( abc (n≤ 0) (n≤ 4) )  ++ ( 0 ∷ 4 ∷ [])) -- (2 ∷   ∷ 3 ∷ 0 ∷   ∷ []) ∷  342 : dba,   (open c, put 1st) 
-       ∷  (plist ( abc (n≤ 1) (n≤ 0) )  ++ ( 1 ∷ 0 ∷ [])) -- (  ∷ 3 ∷   ∷ 4 ∷ 1 ∷ []) ∷ 
-       ∷  (plist ( abc (n≤ 1) (n≤ 1) )  ++ ( 1 ∷ 1 ∷ [])) -- (  ∷ 3 ∷   ∷ 4 ∷ 1 ∷ []) ∷
-      -- ∷  (plist ( abc (n≤ 1) (n≤ 2) )  ++ ( 1 ∷ 2 ∷ [])) -- (3 ∷   ∷   ∷ 4 ∷ 0 ∷ []) ∷   
-      -- ∷  (plist ( abc (n≤ 1) (n≤ 3) )  ++ ( 1 ∷ 3 ∷ [])) -- (1 ∷ 4 ∷   ∷   ∷ 0 ∷ []) ∷  
-      -- ∷  (plist ( abc (n≤ 1) (n≤ 4) )  ++ ( 1 ∷ 4 ∷ [])) -- (1 ∷ 3 ∷   ∷ 0 ∷   ∷ []) ∷  120 dba , 340 : dba
-      -- ∷  (plist ( abc (n≤ 2) (n≤ 0) )  ++ ( 2 ∷ 0 ∷ [])) -- (  ∷ 2 ∷ 4 ∷   ∷ 1 ∷ []) ∷  342 : aec    (open b, put 2nd) 
-      -- ∷  (plist ( abc (n≤ 2) (n≤ 1) )  ++ ( 2 ∷ 1 ∷ [])) -- (  ∷ 2 ∷ 4 ∷   ∷ 1 ∷ []) ∷   
-      -- ∷  (plist ( abc (n≤ 2) (n≤ 2) )  ++ ( 2 ∷ 2 ∷ [])) -- (2 ∷   ∷ 4 ∷   ∷ 0 ∷ []) ∷  340 : aec   -- 1 3 3 4
-      -- ∷  (plist ( abc (n≤ 2) (n≤ 3) )  ++ ( 2 ∷ 3 ∷ [])) -- (1 ∷ 4 ∷   ∷   ∷ 0 ∷ []) ∷ 
-      -- ∷  (plist ( abc (n≤ 2) (n≤ 4) )  ++ ( 2 ∷ 4 ∷ [])) -- (1 ∷ 2 ∷ 0 ∷   ∷   ∷ []) ∷
-      -- ∷  (plist ( abc (n≤ 3) (n≤ 0) )  ++ ( 3 ∷ 0 ∷ [])) -- (  ∷ 2 ∷ 3 ∷ 1 ∷   ∷ []) ∷   
-      -- ∷  (plist ( abc (n≤ 3) (n≤ 1) )  ++ ( 3 ∷ 1 ∷ [])) -- (  ∷ 2 ∷ 3 ∷ 1 ∷   ∷ []) ∷  
-      -- ∷  (plist ( abc (n≤ 3) (n≤ 2) )  ++ ( 3 ∷ 2 ∷ [])) -- (2 ∷   ∷ 3 ∷ 0 ∷   ∷ []) ∷ 
-      -- ∷  (plist ( abc (n≤ 3) (n≤ 3) )  ++ ( 3 ∷ 3 ∷ [])) -- (1 ∷ 3 ∷   ∷ 0 ∷   ∷ []) ∷
-      -- ∷  (plist ( abc (n≤ 3) (n≤ 4) )  ++ ( 3 ∷ 4 ∷ [])) -- (1 ∷ 2 ∷ 0 ∷   ∷   ∷ []) ∷ 
-       ∷ []
+     dba= :
+         {a a' : ℕ }  → (a<3 : a ≤ 3 ) → ( a<4 : a' ≤ 4 ) →
+         {b b' : ℕ }  → (b<3 : b ≤ 3 ) → ( b<4 : b' ≤ 4 ) →
+         {c c' : ℕ }  → (c<3 : c ≤ 3 ) → ( c<4 : c' ≤ 4 ) →
+         abc a<3 a<4 =p= [ dba b<3 b<4  , aec c<3 c<4 ] →
+         dba a<3 a<4 =p= [ aec b<3 b<4  , abc c<3 c<4 ]
+     dba= a<3 a<4 b<3 b<4 c<3 c<4 dq = {!!} where
+         open EqReasoning (Algebra.Group.setoid (Symmetric 5))
+         lemma1 : dba a<3 a<4 =p= [ aec b<3 b<4  , abc c<3 c<4 ]
+         lemma1 = begin
+               dba a<3 a<4
+             ≈⟨ ? ⟩
+               [ aec b<3 b<4  , abc c<3 c<4 ]
+             ∎
 
-     t8 : ( i : Fin 4 ) → (j : Fin 5)  → List ( List ℕ )
-     t8 i j = ((plist  [ dba  (n≤ 0) (n≤ 0)  , aec (fin≤n {3} i) (fin≤n {4} j)  ] ) ++ (8 ∷  0 ∷ 0 ∷ [] ))
-       ∷  ((plist ( [ dba  (n≤ 0) (n≤ 1)   , aec (fin≤n {3} i) (fin≤n {4} j)  ] )) ++ (8 ∷  0 ∷ 1 ∷ [] ))
-       ∷  ((plist ( [ dba  (n≤ 0) (n≤ 2)   , aec (fin≤n {3} i) (fin≤n {4} j)  ] )) ++ (8 ∷  0 ∷ 2 ∷ [] ))
-       ∷  ((plist ( [ dba  (n≤ 0) (n≤ 3)   , aec (fin≤n {3} i) (fin≤n {4} j)  ] )) ++ (8 ∷  0 ∷ 3 ∷ [] ))
-       ∷  ((plist ( [ dba  (n≤ 0) (n≤ 4)   , aec (fin≤n {3} i) (fin≤n {4} j)  ] )) ++ (8 ∷  0 ∷ 4 ∷ [] ))
-       ∷  ((plist ( [ dba  (n≤ 1) (n≤ 0)   , aec (fin≤n {3} i) (fin≤n {4} j)  ] )) ++ (8 ∷  1 ∷ 0 ∷ [] ))
-       ∷  ((plist ( [ dba  (n≤ 1) (n≤ 1)   , aec (fin≤n {3} i) (fin≤n {4} j)  ] )) ++ (8 ∷  1 ∷ 1 ∷ [] ))
-       ∷  ((plist ( [ dba  (n≤ 1) (n≤ 2)   , aec (fin≤n {3} i) (fin≤n {4} j)  ] )) ++ (8 ∷  1 ∷ 2 ∷ [] ))
-       ∷  ((plist ( [ dba  (n≤ 1) (n≤ 3)   , aec (fin≤n {3} i) (fin≤n {4} j)  ] )) ++ (8 ∷  1 ∷ 3 ∷ [] ))    --
-       ∷  ((plist ( [ dba  (n≤ 1) (n≤ 4)   , aec (fin≤n {3} i) (fin≤n {4} j)  ] )) ++ (8 ∷  1 ∷ 4 ∷ [] ))
-       ∷  ((plist ( [ dba  (n≤ 2) (n≤ 0)   , aec (fin≤n {3} i) (fin≤n {4} j)  ] )) ++ (8 ∷  2 ∷ 0 ∷ [] ))
-       ∷  ((plist ( [ dba  (n≤ 2) (n≤ 1)   , aec (fin≤n {3} i) (fin≤n {4} j)  ] )) ++ (8 ∷  2 ∷ 1 ∷ [] ))
-       ∷  ((plist ( [ dba  (n≤ 2) (n≤ 2)   , aec (fin≤n {3} i) (fin≤n {4} j)  ] )) ++ (8 ∷  2 ∷ 2 ∷ [] ))
-       ∷  ((plist ( [ dba  (n≤ 2) (n≤ 3)   , aec (fin≤n {3} i) (fin≤n {4} j)  ] )) ++ (8 ∷  2 ∷ 3 ∷ [] ))
-       ∷  ((plist ( [ dba  (n≤ 2) (n≤ 4)   , aec (fin≤n {3} i) (fin≤n {4} j)  ] )) ++ (8 ∷  2 ∷ 4 ∷ [] ))
-       ∷  ((plist ( [ dba  (n≤ 3) (n≤ 0)   , aec (fin≤n {3} i) (fin≤n {4} j)  ] )) ++ (8 ∷  3 ∷ 0 ∷ [] ))
-       ∷  ((plist ( [ dba  (n≤ 3) (n≤ 1)   , aec (fin≤n {3} i) (fin≤n {4} j)  ] )) ++ (8 ∷  3 ∷ 1 ∷ [] ))
-       ∷  ((plist ( [ dba  (n≤ 3) (n≤ 2)   , aec (fin≤n {3} i) (fin≤n {4} j)  ] )) ++ (8 ∷  3 ∷ 2 ∷ [] ))
-       ∷  ((plist ( [ dba  (n≤ 3) (n≤ 3)   , aec (fin≤n {3} i) (fin≤n {4} j)  ] )) ++ (8 ∷  3 ∷ 4 ∷ [] ))
-       ∷  ((plist ( [ dba  (n≤ 3) (n≤ 4)   , aec (fin≤n {3} i) (fin≤n {4} j)  ] )) ++ (8 ∷  3 ∷ 4 ∷ [] ))
-       ∷  []
+     aec= :
+         {a a' : ℕ }  → (a<3 : a ≤ 3 ) → ( a<4 : a' ≤ 4 ) →
+         {b b' : ℕ }  → (b<3 : b ≤ 3 ) → ( b<4 : b' ≤ 4 ) →
+         {c c' : ℕ }  → (c<3 : c ≤ 3 ) → ( c<4 : c' ≤ 4 ) →
+         dba a<3 a<4 =p= [ aec b<3 b<4  , abc c<3 c<4 ] →
+         aec a<3 a<4 =p= [ abc b<3 b<4  , dba c<3 c<4 ] 
+     aec= = {!!}
 
-     t88 = t1 ++ t8 (# 3) (# 1) 
-              ++ t8 (# 3) (# 2) 
-              ++ t8 (# 3) (# 3) 
-              ++ t8 (# 3) (# 4) 
-
-     --- 1 ∷ 2 ∷ 0 ∷   ∷   ∷ []      abc    --  abc (n≤ 3) (n≤ 4)
-     --- 3 ∷ 0 ∷   ∷ 1 ∷   ∷ []      dba
-     dba99 = ins2 (3rot ∘ₚ 3rot) (n≤ 1) (n≤ 4)
-     --- 4 ∷   ∷ 0 ∷   ∷ 2 ∷ []      aec
-     aec99 = ins2 (pinv 3rot) (n≤ 0) (n≤ 3)
-     tt1 = plist dba99 ∷ plist (pinv dba99) ∷ []
-     tt2 = plist aec99 ∷ plist (pinv aec99) ∷ []
-     tt5 = plist  [ dba99 , aec99  ]  -- =p=  abc  
+     open Triple
      triple : {i j : ℕ } → (i<3 : i ≤ 3) (j<4 : j ≤ 4) → Triple i<3 j<4
      triple z≤n z≤n =                               record { dba0<3 = # 0 ; dba1<4 = # 4 ; aec0<3 = # 2 ; aec1<4 = # 0 ; abc= = pleq _ _ refl }
      triple z≤n (s≤s z≤n) =                         record { dba0<3 = # 0 ; dba1<4 = # 4 ; aec0<3 = # 2 ; aec1<4 = # 0 ; abc= = pleq _ _ refl }
@@ -174,7 +166,7 @@
 
      open _=p=_
      counter-example :  ¬ (abc 0<3 0<4  =p= pid )
-     counter-example = {!!} -- p with peq p (# 1)
-     -- ...  | ()
+     counter-example eq with ←pleq _ _ eq
+     ...  | ()