# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1597928362 -32400
# Node ID 9ce6141ef479ddae091052aad757ea0ddedd00f9
# Parent  84c84695de9458017dcd8d2cbcba8b80fc8f8b41
start again

diff -r 84c84695de94 -r 9ce6141ef479 Symmetric.agda
--- a/Symmetric.agda	Thu Aug 20 14:13:08 2020 +0900
+++ b/Symmetric.agda	Thu Aug 20 21:59:22 2020 +0900
@@ -14,7 +14,7 @@
 open import Data.Nat -- using (ℕ; suc; zero; s≤s ; z≤n )
 open import Data.Nat.Properties -- using (<-trans)
 open import Relation.Binary.PropositionalEquality 
-open import Data.List using (List; []; _∷_ ; length ; _++_ )
+open import Data.List using (List; []; _∷_ ; length ; _++_ ) renaming (reverse to rev )
 open import nat
 
 fid : {p : ℕ } → Fin p → Fin p
@@ -122,61 +122,11 @@
    piso→ (suc zero) = refl
    piso→ (suc (suc x)) = cong (λ k → suc (suc k) ) (inverseʳ perm) 
 
-Finnm : {n m : ℕ } → Fin (n + m) ≡ Fin (m + n)
-Finnm {n} {m} =  cong (λ k → Fin k ) (+-comm n _ )
-
-Finnmconv : {n m : ℕ } → Fin (m + n) →  Fin (n + m)
-Finnmconv {n} {m} x = subst (λ k → Fin k ) (+-comm m _) x
-
-m+n→n : {n m : ℕ } → (x : Fin (n + m)) → toℕ x < n  →  Fin n
-m+n→n x x<n = fromℕ≤ x<n
-
-n→m+n : {n m : ℕ } → (x : Fin n) →  Fin (n + m)
-n→m+n {n} {m} x = Finnmconv {n} {m} (raise m x ) 
-
-m+n→m : {n m : ℕ } → (x : Fin (n + m)) → n ≤ toℕ x  →  Fin m
-m+n→m x n<x = reduce≥ x n<x
-
-m→m+n : {n m : ℕ } → (x : Fin m) →  Fin (n + m)
-m→m+n {zero} {m} x = x
-m→m+n {suc n} {m} x = suc (m→m+n x)
-
-lem0 : {n : ℕ } → n ≤ n
-lem0 {zero} = z≤n
-lem0 {suc n} = s≤s lem0
-
-lem00 : {n m : ℕ } → n ≡ m → n ≤ m
-lem00 refl = lem0
-
-pconcat  : {n m : ℕ }  → Permutation n n → Permutation m m → Permutation (n + m) (n + m)
-pconcat {n} {m} p q = permutation p→ p← record { left-inverse-of = piso→ ; right-inverse-of = piso← } where
-   p→ : Fin (n + m) → Fin (n + m) 
-   p→ x with <-cmp (toℕ x ) n
-   p→ x | tri< a ¬b ¬c = n→m+n (p  ⟨$⟩ˡ (m+n→n  x a ))
-   p→ x | tri≈ ¬a b ¬c = m→m+n (q  ⟨$⟩ˡ (m+n→m x (lem00 (sym b)) ) )
-   p→ x | tri> ¬a ¬b c = m→m+n (q  ⟨$⟩ˡ (m+n→m x (≤to< c)  ))
-
-   p← : Fin (n + m) → Fin (n + m) 
-   p← x with <-cmp (toℕ x ) n
-   p← x | tri< a ¬b ¬c = n→m+n (p  ⟨$⟩ʳ (m+n→n  x a ))
-   p← x | tri≈ ¬a b ¬c = m→m+n (q  ⟨$⟩ʳ (m+n→m x (lem00 (sym b)))) 
-   p← x | tri> ¬a ¬b c = m→m+n (q  ⟨$⟩ʳ (m+n→m x (≤to< c)) )
-   
-   piso← : (x : Fin (n + m) ) → p→ ( p← x ) ≡ x
-   piso← x with <-cmp (toℕ x ) n
-   piso← x | tri< a ¬b ¬c = ?
-   piso← x | tri≈ ¬a b ¬c = ?
-   piso← x | tri> ¬a ¬b c = ?
-
-   piso→ : (x : Fin (n + m) ) → p← ( p→ x ) ≡ x
-   piso→ = {!!}
-
-
 -- enumeration
 
-psawpn : {n m : ℕ} → suc m < n → Permutation n n
-psawpn {suc zero} {m} (s≤s ())
-psawpn {suc n} {m} (s≤s (s≤s x)) = pswap pid 
+psawpn : {n : ℕ} → 1 < n → Permutation n n
+psawpn {suc zero}  (s≤s ())
+psawpn {suc n} (s≤s (s≤s x)) = pswap pid 
 
 pfill : { n m : ℕ } → m ≤ n → Permutation  m m → Permutation n n
 pfill {n} {m} m≤n perm = pfill1 (n - m) (n-m<n n m ) (subst (λ k → Permutation k k ) (n-n-m=m m≤n ) perm) where
@@ -184,15 +134,25 @@
    pfill1 0 _ perm = perm
    pfill1 (suc i) i<n perm = pfill1 i (≤to< i<n) (subst (λ k → Permutation k k ) (si-sn=i-n i<n ) ( pprep perm ) )
 
+psawpim : {n m : ℕ} → 1 < m → m ≤ n → Permutation n n
+psawpim {n} {m} 1<m m≤n = pfill m≤n ( psawpn 1<m )
+
+-- pconcat :  {n m : ℕ } → Permutation  m m → Permutation n n → Permutation (m + n)  (m + n) 
+-- pconcat {n} {m} p q = pfill {n + m} {m} ? p ∘ₚ ?
+
+-- inductivley enmumerate permutations
+--    from n-1 length create n length inserting new element at position m
+
 eperm  : {n m : ℕ} → m ≤ n → Permutation n n → Permutation (suc n) (suc n)
 eperm {0} {0} z≤n perm = pid
 eperm {suc n} {0} z≤n perm = pprep perm
-eperm {n} {suc m} (s≤s m<n) perm = eperm1 m 2 lemm3 (pswap {0} pid ) (pprep perm) where
+eperm {n} {suc m} (s≤s m<n) perm = eperm1 m 2 lemm3  (pprep perm) where
     lemm3 : 2 + m ≤ suc n
     lemm3 = s≤s (s≤s m<n)
-    eperm1 : (m i : ℕ ) → i + m ≤ suc n  → Permutation i i → Permutation (suc n)(suc n) → Permutation (suc n)(suc n)
-    eperm1 zero i i<ssm sw perm = perm ∘ₚ ( pfill (subst (λ k → k ≤ suc n) (+-comm i _) i<ssm) sw )  -- i + zero ≤ suc (suc n) → i ≤ suc (suc n)
-    eperm1 (suc m) i i<ssm sw perm = eperm1 m (suc i) (lemm4 i<ssm ) (pprep sw) perm where
+    eperm1 : (m i : ℕ ) → i + m ≤ suc n  → Permutation (suc n)(suc n) → Permutation (suc n)(suc n)
+    eperm1 zero i i<ssm perm = perm ∘ₚ (psawpim {suc n} {i + m} {!!}  {!!} ) --- 1 < i + m , i + m ≤ suc (suc n)
+                                                                             -- m<n   : m ≤ n , i<ssm : i + zero ≤ suc (suc n)
+    eperm1 (suc m) i i<ssm perm = eperm1 m (suc i) (lemm4 i<ssm )  perm where
        lemm4 : i + suc m ≤ suc n → suc i + m ≤ suc n
        lemm4 lt = begin
           suc i + m  ≡⟨ cong (λ k → suc k ) ( +-comm i _ ) ⟩
@@ -203,12 +163,17 @@
 
 plist  : {n  : ℕ} → Permutation n n → List ℕ
 plist {0} perm = []
-plist {suc j} perm = plist1 j a<sa where
+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) 
 
+testp = plist (psawpim {6} {4} (s≤s (s≤s z≤n)) (s≤s (s≤s (s≤s (s≤s z≤n)))))
+testi00 = plist(pid {3}  )                                                           -- 0 ∷ 1 ∷ 2 ∷ []
+testi = plist (pid {3}  ∘ₚ psawpim {3} {2} (s≤s (s≤s z≤n))  (s≤s (s≤s z≤n)))         -- 0 ∷ 2 ∷ 1 ∷ []  -- 1 ∷ 0 ∷ 2 ∷ []
+testi0 = plist (pid {3}  ∘ₚ psawpim {3} {3} (s≤s (s≤s z≤n))  (s≤s ( s≤s (s≤s z≤n)))) -- 1 ∷ 0 ∷ 2 ∷ []  -- 1 ∷ 2 ∷ 0 ∷ []
+
 test0 = plist (eperm {1} {0} z≤n pid)
 test1 = plist (eperm {1} {1} (s≤s z≤n) pid)
 test = eperm {3} ( s≤s ( s≤s z≤n )) ( eperm (s≤s z≤n) pid )
@@ -220,9 +185,12 @@
 test24 = plist (eperm {2} {2} (s≤s (s≤s z≤n)) (eperm {1} {1}  (s≤s z≤n)  pid))
 test3 =  test11  ∷ test12 ∷ test21 ∷ test22 ∷ test23 ∷ test24 ∷ []
 
-NL : (n : ℕ ) → Set
-NL 0 = ℕ
-NL (suc n) = List ( NL n )
+lem0 : {n : ℕ } → n ≤ n
+lem0 {zero} = z≤n
+lem0 {suc n} = s≤s lem0
+
+lem00 : {n m : ℕ } → n ≡ m → n ≤ m
+lem00 refl = lem0
 
 pls : (n : ℕ ) → List (List ℕ )
 pls n = Data.List.map plist (pls6 n) where