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

diff -r 42eeb9f299eb -r ba190266d4ee src/Putil.agda
--- a/src/Putil.agda	Sat Sep 23 09:38:52 2023 +0900
+++ b/src/Putil.agda	Sat Sep 23 12:16:07 2023 +0900
@@ -16,10 +16,7 @@
 open import Relation.Binary.PropositionalEquality hiding ( [_] )
 open import Data.List using (List; []; _∷_ ; length ; _++_ ; head ; tail ) renaming (reverse to rev )
 open import nat
-
 open import Symmetric
-
-
 open import Relation.Nullary
 open import Data.Empty
 open import  Relation.Binary.Core
@@ -263,28 +260,28 @@
 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 with perm ⟨$⟩ʳ (# 0) | inspect (_⟨$⟩ʳ_ perm ) (# 0)| toℕ≤pred[n] (perm ⟨$⟩ʳ (# 0)) | inspect toℕ≤pred[n] (perm ⟨$⟩ʳ (# 0))
-... | zero |  record { eq = e} |  m<n | _ = p001 where
-   p001 : perm ⟨$⟩ˡ ( pins m<n ⟨$⟩ʳ zero) ≡ zero
-   p001 = subst (λ k → perm ⟨$⟩ˡ k ≡ zero ) e (inverseˡ perm)
-... | suc t |  record { eq = e } | m<n | record { eq = e1 }  = 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 = ?
+-- ... | 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 
 
 ----
 --  other elements are preserved in pins
@@ -487,34 +484,43 @@
 sh1 perm p0=0 {x} eq with shlem← perm p0=0 (suc x) eq
 sh1 perm p0=0 {x} eq | ()
 
+0<x→px<n : {n  : ℕ} → (x : Fin n) → (c :  0 < toℕ x ) 
+     → Data.Nat.pred (toℕ x) < n
+0<x→px<n {n} x c = sx≤py→x≤y ( begin
+     suc (suc (Data.Nat.pred (toℕ x))) ≡⟨ cong suc (sucprd c) ⟩
+     suc (toℕ x) <⟨ fin<n ⟩
+     suc n ∎ ) where
+        open Data.Nat.Properties.≤-Reasoning
 
--- 0 ∷ 1 ∷ 2 ∷ 3 ∷ [] → 0 ∷ 1 ∷ 2 ∷ [] 
-shrink : {n  : ℕ} → (perm : Permutation (suc n) (suc n) ) → perm ⟨$⟩ˡ (# 0) ≡ # 0 → Permutation n n
-shrink {n} perm p0=0  = permutation p→ p← piso← piso→  where
-
-   p00 : (x : Fin n) → (c :  0 < toℕ (perm ⟨$⟩ʳ (suc x) ) ) → Data.Nat.pred (toℕ (Inverse.to perm (suc x))) < n
-   p00 x c = sx≤py→x≤y ( begin
+sh1p<n : {n : ℕ } → (perm : Permutation (suc n) (suc n) ) → (x : Fin n) → (c :  0 < toℕ (perm ⟨$⟩ʳ (suc x) ) ) 
+       → Data.Nat.pred (toℕ (Inverse.to perm (suc x))) < n
+sh1p<n {n} perm x c = sx≤py→x≤y ( begin
      suc (suc (Data.Nat.pred (toℕ (Inverse.to perm (suc x))))) ≡⟨ cong suc (sucprd c) ⟩
      suc (toℕ (Inverse.to perm (suc x))) ≤⟨ fin<n ⟩
      suc n ∎ ) where
         open Data.Nat.Properties.≤-Reasoning
 
-   p01 : (x : Fin n) → (c :  0 < toℕ (perm ⟨$⟩ˡ (suc x) ) ) → Data.Nat.pred (toℕ (Inverse.from perm (suc x))) < n
-   p01 x c = sx≤py→x≤y ( begin
+sh2p<n : {n : ℕ } → (perm : Permutation (suc n) (suc n) ) → (x : Fin n) → (c :  0 < toℕ (perm ⟨$⟩ˡ (suc x) ) ) 
+       → Data.Nat.pred (toℕ (Inverse.from perm (suc x))) < n
+sh2p<n {n} perm x c = sx≤py→x≤y ( begin
      suc (suc (Data.Nat.pred (toℕ (Inverse.from perm (suc x))))) ≡⟨ cong suc (sucprd c) ⟩
      suc (toℕ (Inverse.from perm (suc x))) ≤⟨ fin<n ⟩
      suc n ∎ ) where
         open Data.Nat.Properties.≤-Reasoning
 
+-- 0 ∷ 1 ∷ 2 ∷ 3 ∷ [] → 0 ∷ 1 ∷ 2 ∷ [] 
+shrink : {n  : ℕ} → (perm : Permutation (suc n) (suc n) ) → perm ⟨$⟩ˡ (# 0) ≡ # 0 → Permutation n n
+shrink {n} perm p0=0  = permutation p→ p← piso← piso→  where
+
    p→ : Fin n → Fin n 
    p→ x with <-fcmp (perm ⟨$⟩ʳ (suc x) ) (# 0)
    p→ x | tri≈ ¬a b ¬c = ⊥-elim (sh1 perm p0=0 b)
-   p→ x | tri> ¬a ¬b c = fromℕ< {Data.Nat.pred (toℕ (Inverse.to perm (suc x)))} (p00 x c) 
+   p→ x | tri> ¬a ¬b c = fromℕ< {Data.Nat.pred (toℕ (Inverse.to perm (suc x)))} (sh1p<n perm  x c) 
 
    p← : Fin n → Fin n 
    p← x with <-fcmp (perm ⟨$⟩ˡ (suc x)) (# 0)
    p← x | tri≈ ¬a b ¬c = ⊥-elim (sh2 perm p0=0 b)
-   p← x | tri> ¬a ¬b c = fromℕ< {Data.Nat.pred (toℕ (Inverse.from perm (suc x)))} (p01 x c)
+   p← x | tri> ¬a ¬b c = fromℕ< {Data.Nat.pred (toℕ (Inverse.from perm (suc x)))} (sh2p<n perm x c)
 
    --  using "with" something binded in ≡ is prohibited
    --  with perm ⟨$⟩ʳ (suc q) in e generates w != Inverse.to perm (suc q) of type Fin (suc n)  error
@@ -530,14 +536,14 @@
            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ℕ< (p01 x c)))) ∸ 1  ≡⟨ cong (λ k → toℕ (Inverse.to perm k)  ∸ 1) (p11 _ c (p01 x c) ) ⟩
+              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 (Inverse.from perm (suc x))) ∸ 1  ≡⟨ cong (λ k → toℕ k  ∸ 1) (inverseʳ perm) ⟩
               toℕ (suc x) ∸ 1  ≡⟨ refl ⟩
               toℕ x ∎
            p08 : z ≡ x
            p08 = begin
              z ≡⟨ sym (py=z) ⟩
-             fromℕ< {Data.Nat.pred (toℕ (Inverse.to perm (suc y)))} (p00 y c₁)  ≡⟨ lemma10 p15 ⟩
+             fromℕ< {Data.Nat.pred (toℕ (Inverse.to perm (suc y)))} (sh1p<n perm  y c₁)  ≡⟨ lemma10 p15 ⟩
              fromℕ< {toℕ x} fin<n  ≡⟨ fromℕ<-toℕ _ _  ⟩
              x ∎  
 
@@ -553,14 +559,14 @@
            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ℕ< (p00 x c)))) ∸ 1  ≡⟨ cong (λ k → toℕ (Inverse.from perm k)  ∸ 1) (p11 _ c (p00 x c) ) ⟩
+              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 (Inverse.to perm (suc x))) ∸ 1  ≡⟨ cong (λ k → toℕ k  ∸ 1) (inverseˡ perm) ⟩
               toℕ (suc x) ∸ 1  ≡⟨ refl ⟩
               toℕ x ∎
            p08 : z ≡ x
            p08 = begin
              z ≡⟨ sym (py=z) ⟩
-             fromℕ< {Data.Nat.pred (toℕ (Inverse.from perm (suc y)))} (p01 y c₁)  ≡⟨ lemma10 p15 ⟩
+             fromℕ< {Data.Nat.pred (toℕ (Inverse.from perm (suc y)))} (sh2p<n perm y c₁)  ≡⟨ lemma10 p15 ⟩
              fromℕ< {toℕ x} fin<n  ≡⟨ fromℕ<-toℕ _ _  ⟩
              x ∎  
 
@@ -573,30 +579,28 @@
         s002 = begin
             fromℕ< (≤-trans fin<n (s≤s (Data.Nat.Properties.≤-reflexive refl))) ≡⟨ lemma10 refl ⟩ 
             fromℕ< fin<n  ≡⟨ fromℕ<-toℕ (perm ⟨$⟩ʳ zero) fin<n ⟩ 
-            perm ⟨$⟩ʳ zero ∎ where
-               open ≡-Reasoning
+            perm ⟨$⟩ʳ zero ∎ where open ≡-Reasoning
     s001 (suc x) with <-fcmp (suc (perm ⟨$⟩ʳ (suc x))) (# 0) 
     ... | tri> ¬a ¬b c = s002 where
         s002 :  fromℕ< (≤-trans fin<n (s≤s (Data.Nat.Properties.≤-reflexive refl))) ≡ perm ⟨$⟩ʳ (suc x)
         s002 = begin
             fromℕ< (≤-trans fin<n (s≤s (Data.Nat.Properties.≤-reflexive refl))) ≡⟨ lemma10 refl ⟩ 
             fromℕ< fin<n  ≡⟨ fromℕ<-toℕ (perm ⟨$⟩ʳ (suc x)) fin<n ⟩ 
-            perm ⟨$⟩ʳ (suc x) ∎ where
-               open ≡-Reasoning
+            perm ⟨$⟩ʳ (suc x) ∎ where open ≡-Reasoning
 
 shrink-iso2 : { n : ℕ } → {perm : Permutation (suc n) (suc n)} 
    → (p=0 : perm ⟨$⟩ˡ (# 0) ≡ # 0)  → pprep (shrink perm p=0) =p= perm
 shrink-iso2 {n} {perm} p=0 = record { peq =  s001 } where
     s001 : (q : Fin (suc n)) → (pprep (shrink perm p=0) ⟨$⟩ʳ q) ≡ perm ⟨$⟩ʳ q
     s001 zero = begin
-         zero
-       ≡⟨ sym ( inverseʳ perm ) ⟩
-         perm ⟨$⟩ʳ ( perm ⟨$⟩ˡ zero )
-       ≡⟨ cong (λ k → perm ⟨$⟩ʳ k ) p=0 ⟩
-         perm ⟨$⟩ʳ zero
-       ∎ where
-          open ≡-Reasoning 
-    s001 (suc q) = ?
+         zero ≡⟨ sym ( inverseʳ perm ) ⟩
+         perm ⟨$⟩ʳ ( perm ⟨$⟩ˡ zero ) ≡⟨ cong (λ k → perm ⟨$⟩ʳ k ) p=0 ⟩
+         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)  ⟩
+         perm ⟨$⟩ʳ (suc q) ∎ where open ≡-Reasoning 
+    ... | tri≈ ¬a b ¬c = ⊥-elim (sh1 perm p=0 b)
 
 
 shrink-cong : { n : ℕ } → {x y : Permutation (suc n) (suc n)}
@@ -604,23 +608,11 @@
     → (x=0 :  x ⟨$⟩ˡ (# 0) ≡ # 0 ) → (y=0 : y ⟨$⟩ˡ (# 0) ≡ # 0 )  → shrink x x=0 =p=  shrink y y=0 
 shrink-cong {n} {x} {y} x=y x=0 y=0  = record  { peq = p002 } where
     p002 : (q : Fin n) → (shrink x x=0 ⟨$⟩ʳ q) ≡ (shrink y y=0 ⟨$⟩ʳ q)
-    p002 q = ?
---    p002 q with x ⟨$⟩ʳ (suc q) | inspect (_⟨$⟩ʳ_ x ) (suc q) | y ⟨$⟩ʳ (suc q) | inspect (_⟨$⟩ʳ_ y ) (suc q)
---    p002 q | zero   | record { eq = ex } | zero   | ey                  = ⊥-elim ( sh1 x x=0 ex )
---    p002 q | zero   | record { eq = ex } | suc py | ey                  = ⊥-elim ( sh1 x x=0 ex )
---    p002 q | suc px | ex                 | zero   | record { eq = ey }  = ⊥-elim ( sh1 y y=0 ey )
---    p002 q | suc px | record { eq = ex } | suc py | record { eq = ey }  = p003 ( begin
---           suc px
---         ≡⟨ sym ex ⟩
---           x ⟨$⟩ʳ (suc q)
---         ≡⟨ peq x=y (suc q) ⟩
---           y ⟨$⟩ʳ (suc q)
---         ≡⟨ ey ⟩
---           suc py
---         ∎ ) where
---        p003 : suc px ≡ suc py → px ≡ py
---        p003 refl = refl
--- 
+    p002 q with  <-fcmp (x ⟨$⟩ʳ (suc q) ) (# 0) | <-fcmp (y ⟨$⟩ʳ (suc q) ) (# 0)
+    ... | tri≈ ¬a b ¬c | _ = ⊥-elim ( sh1 x x=0 b )
+    ... | _ | tri≈ ¬a₁ b ¬c = ⊥-elim ( sh1 y y=0 b )
+    ... | tri> ¬a ¬b c | tri> ¬a' ¬b' c' = lemma10 (cong (λ k → toℕ k ∸ 1) (peq x=y _))
+
 open import FLutil
 
 FL→perm   : {n : ℕ }  → FL n → Permutation n n 
@@ -774,4 +766,9 @@
 
 pFL0 : {n : ℕ } → FL0 {n} ≡ perm→FL pid
 pFL0 {zero} = refl
-pFL0 {suc n} = cong (λ k → zero :: k ) ? -- pFL0
+pFL0 {suc n} = cong (λ k → zero :: k ) pf3 where
+   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 = ?
+