Mercurial > hg > Members > kono > Proof > galois

view Putil.agda @ 57:518d364a58a3

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
shrink worked
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 23 Aug 2020 19:23:08 +0900
parents e26f784cd6b1
children 80d61b6776d3
line wrap: on
line source

module Putil where

open import Level hiding ( suc ; zero )
open import Algebra
open import Algebra.Structures
open import Data.Fin hiding ( _<_  ; _≤_ ; _-_ ; _+_ )
open import Data.Fin.Properties hiding ( <-trans ; ≤-trans ) renaming ( <-cmp to <-fcmp )
open import Data.Fin.Permutation
open import Function hiding (id ; flip)
open import Function.Inverse as Inverse using (_↔_; Inverse; _InverseOf_)
open import Function.LeftInverse  using ( _LeftInverseOf_ )
open import Function.Equality using (Π)
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 ; _++_ ; head ) renaming (reverse to rev )
open import nat

open import Symmetric


open import Relation.Nullary
open import Data.Empty
open import  Relation.Binary.Core
open import fin

-- An inductive construction of permutation

-- we already have refl and trans in the Symmetric Group

pprep  : {n : ℕ }  → Permutation n n → Permutation (suc n) (suc n)
pprep {n} perm =  permutation p→ p← record { left-inverse-of = piso→ ; right-inverse-of = piso← } where
   p→ : Fin (suc n) → Fin (suc n)
   p→ zero = zero
   p→ (suc x) = suc ( perm  ⟨$⟩ˡ x)

   p← : Fin (suc n) → Fin (suc n)
   p← zero = zero
   p← (suc x) = suc ( perm  ⟨$⟩ʳ x)

   piso← : (x : Fin (suc n)) → p→ ( p← x ) ≡ x
   piso← zero = refl
   piso← (suc x) = cong (λ k → suc k ) (inverseˡ perm) 

   piso→ : (x : Fin (suc n)) → p← ( p→ x ) ≡ x
   piso→ zero = refl
   piso→ (suc x) = cong (λ k → suc k ) (inverseʳ perm) 

pswap  : {n : ℕ }  → Permutation n n → Permutation (suc (suc n)) (suc (suc  n ))
pswap {n} perm = permutation p→ p← record { left-inverse-of = piso→ ; right-inverse-of = piso← } where
   p→ : Fin (suc (suc n)) → Fin (suc (suc n)) 
   p→ zero = suc zero 
   p→ (suc zero) = zero 
   p→ (suc (suc x)) = suc ( suc ( perm  ⟨$⟩ˡ x) )

   p← : Fin (suc (suc n)) → Fin (suc (suc n)) 
   p← zero = suc zero 
   p← (suc zero) = zero 
   p← (suc (suc x)) = suc ( suc ( perm  ⟨$⟩ʳ x) )
   
   piso← : (x : Fin (suc (suc n)) ) → p→ ( p← x ) ≡ x
   piso← zero = refl
   piso← (suc zero) = refl
   piso← (suc (suc x)) = cong (λ k → suc (suc k) ) (inverseˡ perm) 

   piso→ : (x : Fin (suc (suc n)) ) → p← ( p→ x ) ≡ x
   piso→ zero = refl
   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 

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
   pfill1 : (i : ℕ ) → i ≤ n  → Permutation (n - i) (n - i)  →  Permutation n n
   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 (inseert swap at position m )
--     not easy to write directory beacause left-inverse-of may contains Fin relations
--
psawpim : {n m : ℕ} → suc (suc m) ≤ n → Permutation n n
psawpim {n} {m} m≤n = pfill m≤n ( psawpn (s≤s (s≤s z≤n)) )

n≤ : (i : ℕ ) → {j : ℕ } → i ≤ i + j
n≤ (zero) {j} = z≤n
n≤ (suc i) {j} = s≤s ( n≤ i )

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  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 ∷ [] 
-- 1 ∷ 0 ∷ 2 ∷ 3 ∷ []    plist ( pins {3} (n≤ 1) )
-- 1 ∷ 2 ∷ 0 ∷ 3 ∷ []
-- 1 ∷ 2 ∷ 3 ∷ 0 ∷ []

pins  : {n m : ℕ} → m ≤ n → Permutation (suc n) (suc n)
pins {_} {zero} _ = pid
pins {suc _} {suc zero} _ = pswap pid
pins {suc (suc n)} {suc m} (s≤s m<n) =  pins1 (suc m) (suc (suc n)) lem0 where
    pins1 : (i j : ℕ ) → j ≤ suc (suc n)  → Permutation (suc (suc (suc n ))) (suc (suc (suc n)))
    pins1 _ zero _ = pid
    pins1 zero _ _ = pid
    pins1 (suc i) (suc j) (s≤s si≤n) = psawpim {suc (suc (suc n))} {j}  (s≤s (s≤s si≤n))  ∘ₚ  pins1 i j (≤-trans si≤n refl-≤s ) 

plist  : {n  : ℕ} → Permutation n n → List ℕ
plist {0} perm = []
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) 

data  FL : (n : ℕ )→ Set where
   f0 :  FL 0 
   _::_ :  { n : ℕ } → Fin (suc n ) → FL n → FL (suc n)

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

   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

   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)}))

   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 )

   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)

   p← : Fin n → Fin n 
   p← x  = fromℕ≤ (shlem← x)

   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ℕ _ _ ⟩ 
          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 )

   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ℕ _ _ ⟩ 
          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 )

FL→perm   : {n : ℕ }  → FL n → Permutation n n 
FL→perm f0 = pid
FL→perm (x :: fl) = pprep (FL→perm fl)  ∘ₚ pins ( toℕ≤pred[n] x )

t1 = plist (shrink (pid {3}  ∘ₚ (pins (n≤ 1))) refl)
t3 =  plist ( FL→perm ((# 1) :: ((# 0) :: ( (# 0) :: (( # 0 ) :: f0 )) )))  --  (0 ∷ 1 ∷ 2 ∷ []) ∷
    ∷ plist ( FL→perm ((# 1) :: ((# 0) :: ( (# 1) :: (( # 0 ) :: f0 )) )))  --  (0 ∷ 2 ∷ 1 ∷ []) ∷
    ∷ plist ( FL→perm ((# 1) :: ((# 1) :: ( (# 0) :: (( # 0 ) :: f0 )) )))  --  (1 ∷ 0 ∷ 2 ∷ []) ∷
    ∷ plist ( FL→perm ((# 1) :: ((# 1) :: ( (# 1) :: (( # 0 ) :: f0 )) )))  --  (2 ∷ 0 ∷ 1 ∷ []) ∷
    ∷ plist ( FL→perm ((# 1) :: ((# 2) :: ( (# 0) :: (( # 0 ) :: f0 )) )))  --  (1 ∷ 2 ∷ 0 ∷ []) ∷
    ∷ plist ( FL→perm ((# 1) :: ((# 2) :: ( (# 1) :: (( # 0 ) :: f0 )) )))  --  (2 ∷ 1 ∷ 0 ∷ []) ∷ 
    ∷ plist ( (flip (FL→perm ((# 1) :: ((# 1) :: ( (# 0) :: (( # 0 ) :: f0 )) )))))
    ∷ plist ( (flip (FL→perm ((# 1) :: ((# 1) :: ( (# 0) :: (( # 0 ) :: f0 )) ))) ∘ₚ (FL→perm ((# 1) :: (((# 1) :: ( (# 0) :: (( # 0 ) :: f0 )) )))) ))
    ∷ []

perm→FL   : {n : ℕ }  → Permutation n n → FL n
perm→FL {zero} perm = f0
perm→FL {suc n} perm = (perm ⟨$⟩ˡ fromℕ≤ a<sa ) :: perm→FL ( shrink fl1 {!!} ) where
    fl1 : Permutation (suc n) (suc n)
    fl1 = perm ∘ₚ pinv ( pins (fin<n {n} {{!!}}))
    fl1=pprep : perm =p= pprep ( shrink fl1 {!!} )
    fl1=pprep = {!!}

FL→iso : {n : ℕ }  → (fl : FL n )  → perm→FL ( FL→perm fl ) ≡ fl
FL→iso f0 = refl
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 = {!!} where
   fl0 :  {n : ℕ }  → (fl : FL n )  → {!!} 
   fl0 = {!!}

all-perm : (n : ℕ ) → List (Permutation (suc n) (suc n) )
all-perm n = pls6 n where
   lem1 : {i n : ℕ } → i ≤ n → i < suc n
   lem1 z≤n = s≤s z≤n
   lem1 (s≤s lt) = s≤s (lem1 lt)
   lem2 : {i n : ℕ } → i ≤ n → i ≤ suc n
   lem2 i≤n = ≤-trans i≤n ( refl-≤s )
   pls4 :  ( i n : ℕ ) → (i<n : i ≤ n ) → Permutation n n → List (Permutation (suc n) (suc n))  → List (Permutation (suc n) (suc n)) 
   pls4 zero n i≤n perm x = (pprep perm ∘ₚ pins i≤n ) ∷ x
   pls4 (suc i) n i≤n  perm x = pls4 i n (≤-trans refl-≤s i≤n ) perm (pprep perm ∘ₚ pins {n} {suc i} i≤n  ∷ x)
   pls5 :  ( n : ℕ ) → List (Permutation n n) → List (Permutation (suc n) (suc n))  → List (Permutation (suc n) (suc n)) 
   pls5 n [] x = x
   pls5 n (h ∷ x) y = pls5  n x (pls4 n n lem0 h y)
   pls6 :  ( n : ℕ ) → List (Permutation (suc n) (suc n)) 
   pls6 zero = pid ∷ []
   pls6 (suc n) =  pls5 (suc n) (rev (pls6 n) ) []   -- rev to put id first

pls : (n : ℕ ) → List (List ℕ )
pls n = Data.List.map plist (all-perm n) where