Mercurial > hg > Members > kono > Proof > galois

changeset 61:c16749815259

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
another shrink
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 24 Aug 2020 12:04:25 +0900
parents 48926e810f5f
children a66f773330b4
files Putil.agda
diffstat 1 files changed, 80 insertions(+), 118 deletions(-) [+]
line wrap: on
line diff
--- a/Putil.agda	Mon Aug 24 10:40:26 2020 +0900
+++ b/Putil.agda	Mon Aug 24 12:04:25 2020 +0900
@@ -143,131 +143,90 @@
 open import logic 
 
 -- 0 ∷ 1 ∷ 2 ∷ 3 ∷ [] → 0 ∷ 1 ∷ 2 ∷ [] 
-shrink : {n  : ℕ} → (perm : Permutation (suc n) (suc n) ) → perm ⟨$⟩ˡ (fromℕ n) ≡ fromℕ n → Permutation n n
-shrink {n} perm pn=n  = permutation p→ p← record { left-inverse-of = piso→ ; right-inverse-of = piso← } where
-
-   sh3 : (x : Fin n) → ¬ ( toℕ (perm ⟨$⟩ˡ (fin+1 x)) ≡  n )
-   sh3 x eq = ⊥-elim ( nat-≡< sh31 fin<n ) where
-       sh31 : toℕ x ≡ n
-       sh31 = begin
-           toℕ x 
-        ≡⟨ sym fin+1-toℕ ⟩
-            toℕ (fin+1 x)
-        ≡⟨ cong (λ k → toℕ k ) (sym ( inverseʳ perm))  ⟩
-            toℕ (perm ⟨$⟩ʳ (perm ⟨$⟩ˡ (fin+1 x)))
-        ≡⟨ cong (λ k →  toℕ (perm ⟨$⟩ʳ k )) (sym (toℕ→from eq)) ⟩
-            toℕ (perm ⟨$⟩ʳ fromℕ n)
-        ≡⟨ cong ( λ k → toℕ (perm ⟨$⟩ʳ k )) (sym pn=n) ⟩
-            toℕ (perm ⟨$⟩ʳ (perm ⟨$⟩ˡ (fromℕ n) ))
-        ≡⟨ cong (λ k → toℕ k ) ( inverseʳ perm ) ⟩
-            toℕ (fromℕ n)
-        ≡⟨ toℕ-fromℕ _ ⟩
-            n 
-        ∎ where 
-        open ≡-Reasoning
+shrink : {n  : ℕ} → (perm : Permutation (suc n) (suc n) ) → perm ⟨$⟩ˡ (# 0) ≡ # 0 → Permutation n n
+shrink {n} perm p0=0  = permutation p→ p← record { left-inverse-of = piso→ ; right-inverse-of = piso← } where
+   shlem→ : (x : Fin (suc n) ) →  perm ⟨$⟩ˡ x ≡ zero → x ≡ zero
+   shlem→ x px=0 = begin
+          x                                  ≡⟨ sym ( inverseʳ perm ) ⟩
+          perm ⟨$⟩ʳ ( perm ⟨$⟩ˡ x)           ≡⟨ cong (λ k →  perm ⟨$⟩ʳ k ) px=0 ⟩
+          perm ⟨$⟩ʳ zero                     ≡⟨ cong (λ k →  perm ⟨$⟩ʳ k ) (sym p0=0) ⟩
+          perm ⟨$⟩ʳ ( perm ⟨$⟩ˡ zero)        ≡⟨ inverseʳ perm  ⟩
+          zero
+       ∎ where open ≡-Reasoning
 
-   sh4 : (x : Fin n) → ¬ ( toℕ (perm ⟨$⟩ʳ (fin+1 x)) ≡  n )
-   sh4 x eq = ⊥-elim ( nat-≡< sh41 fin<n ) where
-       sh41 : toℕ x ≡ n
-       sh41 = begin
-            toℕ x
-        ≡⟨ sym fin+1-toℕ ⟩
-            toℕ (fin+1 x)
-        ≡⟨ cong (λ k → toℕ k ) (sym ( inverseˡ perm))  ⟩
-            toℕ (perm ⟨$⟩ˡ (perm ⟨$⟩ʳ (fin+1 x)))
-        ≡⟨ cong (λ k →  toℕ (perm ⟨$⟩ˡ k )) (sym (toℕ→from eq)) ⟩
-            toℕ ((perm ⟨$⟩ˡ fromℕ n))
-        ≡⟨ cong (λ k → toℕ k) pn=n ⟩
-            toℕ (fromℕ n)
-        ≡⟨ toℕ-fromℕ _ ⟩
-            n 
-        ∎ where 
-        open ≡-Reasoning
+   shlem← : (x : Fin (suc n)) → perm ⟨$⟩ʳ x ≡ zero → x ≡ zero
+   shlem← x px=0 =  begin
+          x                                  ≡⟨ sym (inverseˡ perm ) ⟩
+          perm ⟨$⟩ˡ ( perm ⟨$⟩ʳ x )          ≡⟨ cong (λ k →  perm ⟨$⟩ˡ k ) px=0 ⟩
+          perm ⟨$⟩ˡ zero                     ≡⟨ p0=0  ⟩
+          zero
+       ∎ where open ≡-Reasoning
 
-   sh5 : (x : Fin n) → ¬ ( toℕ (perm ⟨$⟩ˡ (fin+1 x)) >  n )
-   sh5 x lt = ⊥-elim ( nat-≤> lt (fin<n {suc n} {perm ⟨$⟩ˡ (fin+1 x)}))
-
-   sh6 : (x : Fin n) → ¬ ( toℕ (perm ⟨$⟩ʳ (fin+1 x)) >  n )
-   sh6 x lt = ⊥-elim ( nat-≤> lt (fin<n {suc n} {perm ⟨$⟩ʳ (fin+1 x)}))
+   sh2 : {x : Fin n} → ¬ perm ⟨$⟩ˡ (suc x) ≡ zero
+   sh2 {x} eq with shlem→ (suc x) eq
+   sh2 {x} eq | ()
 
-   shlem→ : (x : Fin n ) → toℕ (perm ⟨$⟩ˡ (fin+1 x))  < n 
-   shlem→ x with <-cmp (toℕ (perm ⟨$⟩ˡ (fin+1 x)))  n
-   shlem→ x | tri< a ¬b ¬c = a
-   shlem→ x | tri≈ ¬a b ¬c = ⊥-elim ( sh3 x b )
-   shlem→ x | tri> ¬a ¬b c = ⊥-elim ( sh5 x c )
+   p→ : Fin n → Fin n 
+   p→ x with perm ⟨$⟩ˡ (suc x) | inspect (_⟨$⟩ˡ_ perm ) (suc x) 
+   p→ x | zero  | record { eq = e } = ⊥-elim ( sh2 {x} e )
+   p→ x | suc t | _ = t
 
-   shlem← : (x : Fin n) → toℕ (perm ⟨$⟩ʳ (fin+1 x))  < n 
-   shlem← x with <-cmp (toℕ (perm ⟨$⟩ʳ (fin+1 x)))  n
-   shlem← x | tri< a ¬b ¬c = a
-   shlem← x | tri≈ ¬a b ¬c = ⊥-elim ( sh4 x b )
-   shlem← x | tri> ¬a ¬b c = ⊥-elim ( sh6 x c )
-
-   p→ : (x : Fin n ) →  Fin n 
-   p→ x  = fromℕ≤ (shlem→ x)
+   sh1 : {x : Fin n} → ¬ perm ⟨$⟩ʳ (suc x) ≡ zero
+   sh1 {x} eq with shlem← (suc x) eq
+   sh1 {x} eq | ()
 
    p← : Fin n → Fin n 
-   p← x  = fromℕ≤ (shlem← x)
+   p← x with perm ⟨$⟩ʳ (suc x) | inspect (_⟨$⟩ʳ_ perm ) (suc x) 
+   p← x | zero  | record { eq = e } = ⊥-elim ( sh1 {x} e )
+   p← x | suc t | _ = t
 
-   ff : { x y n : ℕ } → (x ≡ y ) → (x<n : x < n) → (y<n : y < n) → fromℕ≤ x<n ≡ fromℕ≤ y<n
-   ff refl _ _ = lemma10 refl
-
-   -- a    : (toℕ (Inverse.to perm Π.⟨$⟩ fin+1 x)) < n
-   -- a₁   : (toℕ (Inverse.from perm Π.⟨$⟩ fin+1 (fromℕ≤ a))) < n
    piso← : (x : Fin n ) → p→ ( p← x ) ≡ x
-   piso← x with <-cmp (toℕ (perm ⟨$⟩ʳ (fin+1 x)))  n
-   piso← x | tri< a ¬b ¬c with <-cmp (toℕ (perm ⟨$⟩ˡ (fin+1 (fromℕ≤ a))))  n
-   piso← x | tri< a ¬b ¬c | tri< a₁ ¬b₁ ¬c₁ = begin
-          fromℕ≤ a₁
-      ≡⟨ ff sh1 a₁ (toℕ<n x) ⟩ 
-          fromℕ≤ (toℕ<n x)
-      ≡⟨ fromℕ≤-toℕ _ _ ⟩ 
+   piso← x with perm ⟨$⟩ʳ (suc x) | inspect (_⟨$⟩ʳ_ perm ) (suc x) 
+   piso← x | zero  | record { eq = e } = ⊥-elim ( sh1 {x} e )
+   piso← x | suc t | _ with perm ⟨$⟩ˡ (suc t) | inspect (_⟨$⟩ˡ_ perm ) (suc t)
+   piso← x | suc t | _ | zero |  record { eq = e } =  ⊥-elim ( sh2 e )
+   piso← x | suc t |  record { eq = e0 } | suc t1 |  record { eq = e1 } = begin
+          t1
+       ≡⟨ plem0 plem1 ⟩
           x
-      ∎ where
-         open ≡-Reasoning 
-         sh1 : toℕ (Inverse.from perm Π.⟨$⟩ fin+1 (fromℕ≤ a)) ≡ toℕ x
-         sh1 = begin
-             toℕ (Inverse.from perm Π.⟨$⟩ fin+1 (fromℕ≤ a))
-          ≡⟨ cong (λ k →  toℕ (Inverse.from perm Π.⟨$⟩ k)) (fin+1≤ a ) ⟩ 
-             toℕ (Inverse.from perm Π.⟨$⟩ (fromℕ≤ (<-trans a a<sa ) ))
-          ≡⟨ cong (λ k →  toℕ (Inverse.from perm Π.⟨$⟩ k)) (fromℕ≤-toℕ (Inverse.to perm Π.⟨$⟩ (fin+1 x)) (<-trans a a<sa)  ) ⟩ 
-             toℕ (Inverse.from perm Π.⟨$⟩ ( Inverse.to perm Π.⟨$⟩ (fin+1 x) ))
-          ≡⟨ cong (λ k → toℕ k) (inverseˡ perm) ⟩ 
-             toℕ (fin+1 x)
-          ≡⟨ fin+1-toℕ ⟩ 
-             toℕ  x
-          ∎ 
-   piso← x | tri< a ¬b ¬c | tri≈ ¬a b ¬c₁ = ⊥-elim ( sh3 (fromℕ≤ a) b )
-   piso← x | tri< a ¬b ¬c | tri> ¬a ¬b₁ c =  ⊥-elim ( sh5 _ c )
-   piso← x | tri≈ ¬a b ¬c = ⊥-elim ( sh4 x b )
-   piso← x | tri> ¬a ¬b c = ⊥-elim ( sh6 x c )
+       ∎ where
+          open ≡-Reasoning
+          plem0 :  suc t1 ≡ suc x → t1 ≡ x
+          plem0 refl = refl
+          plem1 :  suc t1 ≡ suc x
+          plem1 = begin
+               suc t1
+            ≡⟨ sym e1 ⟩
+               Inverse.from perm Π.⟨$⟩ suc t
+            ≡⟨ cong (λ k →  Inverse.from perm Π.⟨$⟩ k ) (sym e0 ) ⟩
+               Inverse.from perm Π.⟨$⟩ ( Inverse.to perm Π.⟨$⟩ suc x )
+            ≡⟨ inverseˡ perm   ⟩
+               suc x
+            ∎ 
 
    piso→ : (x : Fin n ) → p← ( p→ x ) ≡ x
-   piso→ x with <-cmp (toℕ (perm ⟨$⟩ˡ (fin+1 x)))  n
-   piso→ x | tri< a ¬b ¬c with <-cmp (toℕ (perm ⟨$⟩ʳ (fin+1 (fromℕ≤ a))))  n
-   piso→ x | tri< a ¬b ¬c | tri< a₁ ¬b₁ ¬c₁ = begin
-          fromℕ≤ a₁
-      ≡⟨ ff sh2 a₁ (toℕ<n x) ⟩ 
-          fromℕ≤ (toℕ<n x)
-      ≡⟨ fromℕ≤-toℕ _ _ ⟩ 
+   piso→ x with perm ⟨$⟩ˡ (suc x) | inspect (_⟨$⟩ˡ_ perm ) (suc x)
+   piso→ x | zero  | record { eq = e } = ⊥-elim ( sh2 {x} e )
+   piso→ x | suc t | _ with perm ⟨$⟩ʳ (suc t) | inspect (_⟨$⟩ʳ_ perm ) (suc t)
+   piso→ x | suc t | _ | zero |  record { eq = e } =  ⊥-elim ( sh1 e )
+   piso→ x | suc t |  record { eq = e0 } | suc t1 |  record { eq = e1 } = begin
+          t1
+       ≡⟨ plem2 plem3 ⟩
           x
-      ∎ where
-         open ≡-Reasoning 
-         sh2 : toℕ (Inverse.to perm Π.⟨$⟩ fin+1 (fromℕ≤ a)) ≡ toℕ x
-         sh2 = begin
-             toℕ (Inverse.to perm Π.⟨$⟩ fin+1 (fromℕ≤ a))
-          ≡⟨ cong (λ k →  toℕ (Inverse.to perm Π.⟨$⟩ k)) (fin+1≤ a ) ⟩ 
-             toℕ (Inverse.to perm Π.⟨$⟩ (fromℕ≤ (<-trans a a<sa ) ))
-          ≡⟨ cong (λ k →  toℕ (Inverse.to perm Π.⟨$⟩ k)) (fromℕ≤-toℕ (Inverse.from perm Π.⟨$⟩ (fin+1 x)) (<-trans a a<sa)  ) ⟩ 
-             toℕ (Inverse.to perm Π.⟨$⟩ ( Inverse.from perm Π.⟨$⟩ (fin+1 x) ))
-          ≡⟨ cong (λ k → toℕ k) (inverseʳ perm) ⟩ 
-             toℕ (fin+1 x)
-          ≡⟨ fin+1-toℕ ⟩ 
-             toℕ  x
-          ∎ 
-   piso→ x | tri< a ¬b ¬c | tri≈ ¬a b ¬c₁ = ⊥-elim ( sh4 (fromℕ≤ a) b )
-   piso→ x | tri< a ¬b ¬c | tri> ¬a ¬b₁ c =  ⊥-elim ( sh6 _ c )
-   piso→ x | tri≈ ¬a b ¬c = ⊥-elim ( sh3 x b )
-   piso→ x | tri> ¬a ¬b c = ⊥-elim ( sh5 x c )
+       ∎ where
+          open ≡-Reasoning
+          plem2 :  suc t1 ≡ suc x → t1 ≡ x
+          plem2 refl = refl
+          plem3 :  suc t1 ≡ suc x
+          plem3 = begin
+               suc t1
+            ≡⟨ sym e1 ⟩
+               Inverse.to perm Π.⟨$⟩ suc t
+            ≡⟨ cong (λ k →  Inverse.to perm Π.⟨$⟩ k ) (sym e0 ) ⟩
+               Inverse.to perm Π.⟨$⟩ ( Inverse.from perm Π.⟨$⟩ suc x )
+            ≡⟨ inverseʳ perm   ⟩
+               suc x
+            ∎
 
 FL→perm   : {n : ℕ }  → FL n → Permutation n n 
 FL→perm f0 = pid
@@ -276,7 +235,7 @@
 t40 =                (# 2) :: ( (# 1) :: (( # 0 ) :: f0 )) 
 t4 =  FL→perm ((# 2) :: t40 )
 
-t1 = plist (shrink (pid {3}  ∘ₚ (pins (n≤ 1))) refl)
+-- t1 = plist (shrink (pid {3}  ∘ₚ (pins (n≤ 1))) refl)
 t2 = plist ((pid {5} ) ∘ₚ transpose (# 2) (# 4)) ∷ plist (pid {5} ∘ₚ reverse )   ∷  []
 t3 = plist (FL→perm t40) -- ∷ plist (pprep (FL→perm t40))
     -- ∷ plist ( pprep (FL→perm t40) ∘ₚ  pins ( n≤ 0 {3}  ))
@@ -293,15 +252,17 @@
     -- ∷ plist ( (flip (FL→perm ((# 3) :: ((# 1) :: ( (# 0) :: (( # 0 ) :: f0 )) ))) ∘ₚ (FL→perm ((# 3) :: (((# 1) :: ( (# 0) :: (( # 0 ) :: f0 )) )))) ))
     ∷ []
 
+p=0 : {n : ℕ }  → (perm : Permutation (suc n) (suc n) ) → ((perm ∘ₚ flip (pins (toℕ≤pred[n] (perm ⟨$⟩ʳ (# 0))))) ⟨$⟩ˡ (# 0)) ≡ # 0
+p=0 perm  = {!!}
 
 perm→FL   : {n : ℕ }  → Permutation n n → FL n
 perm→FL {zero} perm = f0
-perm→FL {suc n} perm = (perm ⟨$⟩ʳ (# 0)) :: perm→FL (remove (# 0) perm)  
+perm→FL {suc n} perm = (perm ⟨$⟩ʳ (# 0)) :: perm→FL (shrink (perm ∘ₚ flip (pins (toℕ≤pred[n] (perm ⟨$⟩ʳ (# 0))))) (p=0 perm) ) 
 
 -- t5 = plist t4 ∷ plist ( t4  ∘ₚ flip (pins ( n≤  3 ) ))
 t5 = plist (t4) ∷ plist (flip t4)
     ∷ ( toℕ (t4 ⟨$⟩ˡ fromℕ≤ a<sa) ∷ [] )
-    ∷ ( toℕ (t4 ⟨$⟩ˡ (# 0)) ∷ [] )
+    ∷ ( toℕ (t4 ⟨$⟩ʳ (# 0)) ∷ [] )
     -- ∷  plist ( t4  ∘ₚ flip (pins ( n≤  1 ) ))
     ∷  plist (remove (# 0) t4  )
     ∷  plist ( FL→perm t40 )
@@ -311,12 +272,13 @@
 
 FL→iso : {n : ℕ }  → (fl : FL n )  → perm→FL ( FL→perm fl ) ≡ fl
 FL→iso f0 = refl
-FL→iso (x :: fl) = {!!} 
+FL→iso (x :: fl) = {!!} -- with FL→iso fl
+-- ... | t = {!!}
 
 open _=p=_
 FL←iso : {n : ℕ }  → (perm : Permutation n n )  → FL→perm ( perm→FL perm  ) =p= perm
 FL←iso {0} perm = record { peq = λ () }
-FL←iso {suc n} perm = {!!} 
+FL←iso {suc n} perm = {!!}
 
 all-perm : (n : ℕ ) → List (Permutation (suc n) (suc n) )
 all-perm n = pls6 n where