# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1599270821 -32400
# Node ID dae027341d7376a628085757e81bf638132ccf8c
# Parent  206fc12e5c36b45890b20b03741c1ac3e754d322
...

diff -r 206fc12e5c36 -r dae027341d73 Putil.agda
--- a/Putil.agda	Sat Sep 05 10:34:53 2020 +0900
+++ b/Putil.agda	Sat Sep 05 10:53:41 2020 +0900
@@ -68,8 +68,6 @@
    piso→ (suc zero) = refl
    piso→ (suc (suc x)) = cong (λ k → suc (suc k) ) (inverseˡ perm) 
 
--- enumeration
-
 psawpn : {n : ℕ} → 1 < n → Permutation n n
 psawpn {suc zero}  (s≤s ())
 psawpn {suc n} (s≤s (s≤s x)) = pswap pid 
@@ -105,16 +103,16 @@
 plist {0} perm = []
 plist {suc n} perm = rev (plist1 perm n a<sa) 
 
--- 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
-
+--
 -- 0 ∷ 1 ∷ 2 ∷ 3 ∷ []                               -- 0 ∷ 1 ∷ 2 ∷ 3 ∷ [] 
 -- 1 ∷ 0 ∷ 2 ∷ 3 ∷ []    plist ( pins {3} (n≤ 1) )     1 ∷ 0 ∷ 2 ∷ 3 ∷ []
 -- 1 ∷ 2 ∷ 0 ∷ 3 ∷ []    plist ( pins {3} (n≤ 2) )     2 ∷ 0 ∷ 1 ∷ 3 ∷ []
 -- 1 ∷ 2 ∷ 3 ∷ 0 ∷ []    plist ( pins {3} (n≤ 3) )     3 ∷ 0 ∷ 1 ∷ 2 ∷ []
+--
+-- defined by pprep and pswap
+--
 -- pins  : {n m : ℕ} → m ≤ n → Permutation (suc n) (suc n)
 -- pins {_} {zero} _ = pid
 -- pins {suc _} {suc zero} _ = pswap pid
@@ -259,6 +257,9 @@
    perm00 zero zero | zero = refl
 
 
+----
+--  find insertion point of pins
+----
 p=0 : {n : ℕ }  → (perm : Permutation (suc n) (suc n) ) → ((perm ∘ₚ flip (pins (toℕ≤pred[n] (perm ⟨$⟩ʳ (# 0))))) ⟨$⟩ˡ (# 0)) ≡ # 0
 p=0 {zero} perm with ((perm ∘ₚ flip (pins (toℕ≤pred[n] (perm ⟨$⟩ʳ (# 0))))) ⟨$⟩ˡ (# 0)) 
 ... | zero = refl
@@ -285,6 +286,9 @@
                 (perm ⟨$⟩ʳ (# 0))
              ∎ )
 
+----
+--  other elements are preserved in pins
+----
 px=x : {n : ℕ }  → (x : Fin (suc n)) → pins ( toℕ≤pred[n] x ) ⟨$⟩ʳ (# 0) ≡ x
 px=x {n} zero = refl
 px=x {suc n} (suc x) = p001 where
@@ -325,7 +329,9 @@
 taileq refl = refl
 
 --
--- plist equalizer 
+-- plist injection / equalizer 
+--
+--    if plist0 of two perm looks the same, the permutations are the same
 --
 pleq  : {n  : ℕ} → (x y : Permutation n n ) → plist0 x ≡ plist0 y → x =p= y
 pleq  {0} x y refl = record { peq = λ q → pleq0 q } where
@@ -424,6 +430,11 @@
    f0 :  FL 0 
    _::_ :  { n : ℕ } → Fin (suc n ) → FL n → FL (suc n)
 
+--
+-- shrink operation ( reverse of pprep )
+--
+--     shrink (pprep perm)  refl =p=  perm
+
 shlem→ : {n  : ℕ} → (perm : Permutation (suc n) (suc n) ) → (p0=0 : perm ⟨$⟩ˡ (# 0) ≡ # 0 ) → (x : Fin (suc n) ) →  perm ⟨$⟩ˡ x ≡ zero → x ≡ zero
 shlem→ perm p0=0 x px=0 = begin
           x                                  ≡⟨ sym ( inverseʳ perm ) ⟩