# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1695463946 -32400
# Node ID e9ac545595970d19bbadde5aa1b8295b2ba05fb3
# Parent  ba190266d4ee4bc415fb9b8d133f30e613f0ab4c
...

diff -r ba190266d4ee -r e9ac54559597 src/Putil.agda
--- a/src/Putil.agda	Sat Sep 23 12:16:07 2023 +0900
+++ b/src/Putil.agda	Sat Sep 23 19:12:26 2023 +0900
@@ -253,35 +253,66 @@
    perm00 x y with p ⟨$⟩ˡ x
    perm00 zero zero | zero = refl
 
+pred-fin : {n : ℕ } → (y : Fin (suc n)) → 0 < toℕ y → (y<n : Data.Nat.pred (toℕ y) < n) → suc (fromℕ< y<n) ≡ y 
+pred-fin {.(suc _)} zero () (s≤s z≤n)
+pred-fin {suc n} (suc zero) 0<y (s≤s z≤n) = refl
+pred-fin {suc n} (suc (suc y)) 0<y y<n = p13 where
+  p14 : toℕ (suc y) < suc n
+  p14 = y<n
+  sy<n : Data.Nat.pred (toℕ (suc y)) < n
+  sy<n = px≤py ( begin 
+     suc (suc (toℕ y))  ≡⟨ refl ⟩
+     suc (toℕ (suc y))  ≤⟨ p14 ⟩
+     suc n  ∎ ) where open ≤-Reasoning 
+  p12 : suc (fromℕ< sy<n ) ≡ suc y 
+  p12 = pred-fin (suc y) (s≤s z≤n) sy<n
+  p16 : fromℕ< y<n ≡ suc (fromℕ< sy<n)
+  p16 = lemma10 refl 
+  p13 : suc (fromℕ< y<n) ≡ suc (suc y)
+  p13 = cong suc (trans p16 p12  )
 
 ----
 --  find insertion point of pins
 ----
+
+p011 : (n m : ℕ) → (perm : Permutation (suc n) (suc n) ) → (m≤n : m ≤ n) → 0 < m → (perm ∘ₚ flip (pins m≤n )) ⟨$⟩ˡ (# 0) ≡ perm ⟨$⟩ˡ (fromℕ< (s≤s m≤n))
+p011 zero zero perm z≤n _ = refl
+p011 zero (suc t) perm () _
+p011 (suc n) (suc m) perm (s≤s m≤n) _ with <-cmp (toℕ {suc (suc n)} (# 0)) (suc m)
+... | tri< a ¬b ¬c = refl
+... | tri≈ ¬a () ¬c
+... | tri> ¬a ¬b ()
+p011 (suc n) zero perm m≤n ()
+
 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
-p=0 {suc n} perm = ?
--- ... | zero | m<n = p001 where
---    p001 : perm ⟨$⟩ˡ ( pins m<n ⟨$⟩ʳ zero) ≡ zero
---    p001 = subst (λ k → perm ⟨$⟩ˡ k ≡ zero ) e (inverseˡ perm)
--- ... | suc t  | m<n   = p002 where   -- m<n  : suc (toℕ t) ≤ suc n
---    p002 : perm ⟨$⟩ˡ ( pins m<n ⟨$⟩ʳ zero) ≡ zero
---    p002 = p005 zero (toℕ t)  refl m<n refl where   -- suc (toℕ t) ≤ suc n
---       p003 : (s : Fin (suc (suc n))) → s ≡ (perm ⟨$⟩ʳ (# 0)) → perm ⟨$⟩ˡ s  ≡ # 0
---       p003 s eq = subst (λ k → perm ⟨$⟩ˡ k ≡ zero ) (sym eq) (inverseˡ perm)
---       p005 : (x :  Fin (suc (suc n))) → (m : ℕ ) → x ≡ zero → (m≤n : suc m ≤ suc n ) → m ≡ toℕ t → perm ⟨$⟩ˡ ( pins m≤n ⟨$⟩ʳ zero) ≡ zero
---       p005 zero m eq (s≤s m≤n) meq = p004 where
---           p004 :  perm ⟨$⟩ˡ (fromℕ< (s≤s (s≤s m≤n))) ≡ zero
---           p004 = p003  (fromℕ< (s≤s (s≤s m≤n))) (
---              begin
---                 fromℕ< (s≤s (s≤s m≤n))
---              ≡⟨ lemma10 {suc (suc n)}  (cong suc meq) {s≤s (s≤s m≤n)} {subst (λ k →  suc k < suc (suc n)) meq (s≤s (s≤s m≤n)) } ⟩
---                 fromℕ< (subst (λ k →  suc k < suc (suc n)) meq (s≤s (s≤s m≤n)) )
---              ≡⟨ fromℕ<-toℕ {suc (suc n)} (suc t) (subst (λ k →  suc k < suc (suc n)) meq (s≤s (s≤s m≤n)) ) ⟩
---                 suc t
---              ≡⟨ sym e ⟩
---                 (perm ⟨$⟩ʳ (# 0))
---              ∎ )   where open ≡-Reasoning 
+p=0 {suc n} perm with Inverse.to perm zero in eq
+... | zero = p002 where
+    p002 : Inverse.from perm (Inverse.to (pins (toℕ≤pred[n] zero)) zero) ≡ zero
+    p002 = subst (λ k → perm ⟨$⟩ˡ k ≡ zero ) eq (inverseˡ perm)
+... | suc t = p012 where
+    p003 : 0 < toℕ (Inverse.to perm zero)
+    p003 = subst ( λ k → 0 < k ) (cong toℕ (sym eq)) (s≤s z≤n)
+    p002 : toℕ (Inverse.to perm zero) ≤ suc n
+    p002 = toℕ≤pred[n] (Inverse.to perm zero)
+    p001 : suc (toℕ (Data.Fin.pred (Inverse.to perm zero))) ≤ suc n
+    p001 = begin
+        suc (toℕ (Data.Fin.pred (Inverse.to perm zero)))  ≡⟨  {!!} ⟩
+        suc (Data.Nat.pred (toℕ (Inverse.to perm zero)))  ≡⟨ sucprd p003 ⟩
+        toℕ (Inverse.to perm zero)  ≤⟨ p002 ⟩
+        suc n  ∎ where open ≤-Reasoning
+    p007 : Data.Nat.pred (suc (toℕ (Inverse.to perm zero))) < suc n
+    p007 = ?
+    p012 : Inverse.from perm (Inverse.to (pins (toℕ≤pred[n] (suc t))) zero) ≡ # 0 
+    p012 = begin
+        Inverse.from perm (Inverse.to (pins (toℕ≤pred[n] (suc t))) zero) ≡⟨ ? ⟩ 
+        perm ∘ₚ flip (pins (toℕ≤pred[n] (perm ⟨$⟩ʳ # 0))) ⟨$⟩ˡ # 0 ≡⟨ p011 _ _ perm p001 (s≤s z≤n) ⟩
+        perm ⟨$⟩ˡ suc (fromℕ< p001) ≡⟨ cong (λ k → perm ⟨$⟩ˡ k ) (lemma10 ?) ⟩
+        perm ⟨$⟩ˡ suc (fromℕ< ?) ≡⟨ cong (λ k → perm ⟨$⟩ˡ k ) (pred-fin (Inverse.to perm zero) p003 ? ) ⟩
+        perm ⟨$⟩ˡ (Inverse.to perm zero) ≡⟨ inverseˡ perm  ⟩
+        # 0 ∎ where 
+            open ≡-Reasoning
 
 ----
 --  other elements are preserved in pins
@@ -439,24 +470,6 @@
    pswap-dist1 (suc zero) = refl
    pswap-dist1 (suc (suc q)) =  cong ( λ k → suc (suc k) ) refl
 
-p11 : {n : ℕ } → (y : Fin (suc n)) → 0 < toℕ y → (y<n : Data.Nat.pred (toℕ y) < n) → suc (fromℕ< y<n) ≡ y 
-p11 {.(suc _)} zero () (s≤s z≤n)
-p11 {suc n} (suc zero) 0<y (s≤s z≤n) = refl
-p11 {suc n} (suc (suc y)) 0<y y<n = p13 where
-  p14 : toℕ (suc y) < suc n
-  p14 = y<n
-  sy<n : Data.Nat.pred (toℕ (suc y)) < n
-  sy<n = px≤py ( begin 
-     suc (suc (toℕ y))  ≡⟨ refl ⟩
-     suc (toℕ (suc y))  ≤⟨ p14 ⟩
-     suc n  ∎ ) where open ≤-Reasoning 
-  p12 : suc (fromℕ< sy<n ) ≡ suc y 
-  p12 = p11 (suc y) (s≤s z≤n) sy<n
-  p16 : fromℕ< y<n ≡ suc (fromℕ< sy<n)
-  p16 = lemma10 refl 
-  p13 : suc (fromℕ< y<n) ≡ suc (suc y)
-  p13 = cong suc (trans p16 p12  )
-
 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 ) ⟩
@@ -536,7 +549,7 @@
            p15 : toℕ (Inverse.to perm (suc y)) ∸ 1 ≡ toℕ x
            p15 = begin
               toℕ (Inverse.to perm (suc y)) ∸ 1  ≡⟨ cong (λ k → toℕ (Inverse.to perm (suc k))  ∸ 1   ) (sym px=y) ⟩
-              toℕ (Inverse.to perm (suc (fromℕ< (sh2p<n perm x c)))) ∸ 1  ≡⟨ cong (λ k → toℕ (Inverse.to perm k)  ∸ 1) (p11 _ c (sh2p<n perm x c) ) ⟩
+              toℕ (Inverse.to perm (suc (fromℕ< (sh2p<n perm x c)))) ∸ 1  ≡⟨ cong (λ k → toℕ (Inverse.to perm k)  ∸ 1) (pred-fin _ c (sh2p<n perm x c) ) ⟩
               toℕ (Inverse.to perm (Inverse.from perm (suc x))) ∸ 1  ≡⟨ cong (λ k → toℕ k  ∸ 1) (inverseʳ perm) ⟩
               toℕ (suc x) ∸ 1  ≡⟨ refl ⟩
               toℕ x ∎
@@ -559,7 +572,7 @@
            p15 : toℕ (Inverse.from perm (suc y)) ∸ 1 ≡ toℕ x
            p15 = begin
               toℕ (Inverse.from perm (suc y)) ∸ 1  ≡⟨ cong (λ k → toℕ (Inverse.from perm (suc k))  ∸ 1   ) (sym px=y) ⟩
-              toℕ (Inverse.from perm (suc (fromℕ< (sh1p<n perm  x c)))) ∸ 1  ≡⟨ cong (λ k → toℕ (Inverse.from perm k)  ∸ 1) (p11 _ c (sh1p<n perm  x c) ) ⟩
+              toℕ (Inverse.from perm (suc (fromℕ< (sh1p<n perm  x c)))) ∸ 1  ≡⟨ cong (λ k → toℕ (Inverse.from perm k)  ∸ 1) (pred-fin _ c (sh1p<n perm  x c) ) ⟩
               toℕ (Inverse.from perm (Inverse.to perm (suc x))) ∸ 1  ≡⟨ cong (λ k → toℕ k  ∸ 1) (inverseˡ perm) ⟩
               toℕ (suc x) ∸ 1  ≡⟨ refl ⟩
               toℕ x ∎
@@ -598,7 +611,7 @@
          perm ⟨$⟩ʳ zero ∎ where open ≡-Reasoning 
     s001 (suc q) with <-fcmp ((perm ⟨$⟩ʳ (suc q))) (# 0) 
     ... | tri> ¬a ¬b c = begin
-         suc (fromℕ< (sh1p<n perm q c)) ≡⟨ p11 (perm ⟨$⟩ʳ suc q) c (sh1p<n perm q c)  ⟩
+         suc (fromℕ< (sh1p<n perm q c)) ≡⟨ pred-fin (perm ⟨$⟩ʳ suc q) c (sh1p<n perm q c)  ⟩
          perm ⟨$⟩ʳ (suc q) ∎ where open ≡-Reasoning 
     ... | tri≈ ¬a b ¬c = ⊥-elim (sh1 perm p=0 b)
 
@@ -770,5 +783,5 @@
    pf4 : FL0 {n} ≡ perm→FL pid
    pf4 = pFL0
    pf3 : FL0 {n} ≡ perm→FL (shrink (pid ∘ₚ flip (pins (toℕ≤pred[n] {suc n} (pid ⟨$⟩ʳ # 0)))) (p=0 pid))
-   pf3 = ?
+   pf3 = {!!}