Mercurial > hg > Members > kono > Proof > galois

changeset 34:c9dbbe12a03b

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
inductive hg: Enter commit message. Lines beginning with 'HG:' are removed.
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 19 Aug 2020 19:55:32 +0900
parents a986f22cde84
children 0364ad4f2a47
files Symmetric.agda
diffstat 1 files changed, 72 insertions(+), 138 deletions(-) [+]
line wrap: on
line diff
--- a/Symmetric.agda	Wed Aug 19 18:23:20 2020 +0900
+++ b/Symmetric.agda	Wed Aug 19 19:55:32 2020 +0900
@@ -73,153 +73,87 @@
            j ⟨$⟩ˡ q
            ∎ where open ≡-Reasoning
 
-perm0 : {n : ℕ } → Permutation n n 
-perm0 = permutation fid fid record { left-inverse-of = λ x → refl ; right-inverse-of = λ x → refl }
-
 open import Relation.Nullary
 open import Data.Empty
 open import  Relation.Binary.Core
 open import fin
 
-fperm0  : {n : ℕ }  → Permutation n n → Permutation (suc n) (suc n)
-fperm0 {n} perm =  permutation p→ p← record { left-inverse-of = piso← ; right-inverse-of = {!!} } where
+-- An inductive definition of permutation
+
+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→ x with <-cmp (toℕ x) n
-   p→ x | tri< a ¬b ¬c = fin+1 ( perm  ⟨$⟩ˡ ( fromℕ≤ a ))
-   p→ x | tri≈ ¬a b ¬c = fromℕ≤ a<sa
-   p→ x | tri> ¬a ¬b c = ⊥-elim ( nat-≤> c fin<n )
-   
-   p← : Fin (suc n) → Fin (suc n)     
-   p← x with <-cmp (toℕ x) n
-   p← x | tri< a ¬b ¬c = fin+1 ( perm  ⟨$⟩ʳ ( fromℕ≤ a ))
-   p← x | tri≈ ¬a b ¬c = fromℕ≤ a<sa
-   p← x | tri> ¬a ¬b c = ⊥-elim ( nat-≤> c fin<n )
+   p→ zero = zero
+   p→ (suc x) = suc ( perm  ⟨$⟩ˡ x)
 
-   piso← : (x : Fin (suc n)) → p← ( p→ x ) ≡ x
-   piso← x with <-cmp (toℕ x) n
-   piso← x | tri< a ¬b ¬c = begin  
-          p← ( fin+1 (perm ⟨$⟩ˡ (fromℕ≤ a)) ) 
-       ≡⟨ {!!}  ⟩
-          fin+1 ( perm  ⟨$⟩ʳ ( perm  ⟨$⟩ˡ  ( fromℕ≤ a )) )
-       ≡⟨ cong (λ k → fin+1 k ) ( inverseʳ perm )  ⟩
-          fin+1 (fromℕ≤ a) 
-       ≡⟨ {!!}  ⟩
-           x
-       ∎ where
-         open ≡-Reasoning
-   piso← x | tri≈ ¬a b ¬c = begin
-          p← ( fromℕ≤ a<sa )
-       ≡⟨ {!!}  ⟩
-           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) = begin
+          p→ (p← (suc x)) 
+       ≡⟨⟩
+         suc (perm ⟨$⟩ˡ (perm ⟨$⟩ʳ x))
+       ≡⟨ cong (λ k → suc k ) (inverseˡ perm) ⟩
+          suc x
        ∎ where open ≡-Reasoning
-   piso← x | tri> ¬a ¬b c = ⊥-elim ( nat-≤> c fin<n )
 
-fswap  : {n m : ℕ } → suc m < n → Permutation n n 
-fswap {n} {m} n<m   = permutation p→ p→ record { left-inverse-of = piso← ; right-inverse-of =  piso←} where
-   p→ : Fin n → Fin (n)
-   p→ x with <-cmp (toℕ x) m
-   p→ x | tri< a ¬b ¬c = x
-   p→ x | tri≈ ¬a b ¬c = fromℕ≤ {suc m} {n} n<m
-   p→ x | tri> ¬a ¬b c with <-cmp (toℕ x) (suc m)
-   p→ x | tri> ¬a ¬b c | tri< a ¬b₁ ¬c = x
-   p→ x | tri> ¬a ¬b c | tri≈ ¬a₁ b ¬c = fromℕ≤ {m} {n} (<-trans a<sa n<m)
-   p→ x | tri> ¬a ¬b c | tri> ¬a₁ ¬b₁ c₁ = x
-   
-   piso← : (x : Fin (n)) → p→ ( p→ x ) ≡ x
-   piso← x with <-cmp (toℕ x) m
-   piso← x | tri< a ¬b ¬c = {!!}
-   piso← x | tri≈ ¬a b ¬c = {!!}
-   piso← x | tri> ¬a ¬b c with <-cmp (toℕ x) (suc m)
-   piso← x | tri> ¬a ¬b c | tri< a ¬b₁ ¬c = {!!}
-   piso← x | tri> ¬a ¬b c | tri≈ ¬a₁ b ¬c = {!!}
-   piso← x | tri> ¬a ¬b c | tri> ¬a₁ ¬b₁ c₁ = {!!}
+   piso→ : (x : Fin (suc n)) → p← ( p→ x ) ≡ x
+   piso→ zero = refl
+   piso→ (suc x) = begin
+          p← (p→ (suc x)) 
+       ≡⟨⟩
+         suc (perm ⟨$⟩ʳ (perm ⟨$⟩ˡ x))
+       ≡⟨ cong (λ k → suc k ) (inverseʳ perm) ⟩
+          suc x
+       ∎ where open ≡-Reasoning
 
-
-fperm  : {n m : ℕ} → m < n → Permutation n n → Permutation (suc n) (suc n)
-fperm {zero} ()
-fperm {suc n} {m} (s≤s m<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→ x with <-cmp (toℕ x) m
-   p→ x | tri< a ¬b ¬c = fin+1 (perm ⟨$⟩ʳ (fromℕ≤ x<sn))  where
-       x<sn : toℕ x < suc n
-       x<sn = <-trans a (s≤s m<n)
-   p→ x | tri≈ ¬a b ¬c = fromℕ≤ a<sa
-   p→ x | tri> ¬a ¬b c =  fin+1 (perm ⟨$⟩ʳ (fromℕ≤ (pred<n {_} {x} 0<s  )))
+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← x = lemma (suc n) refl x where
-     lemma : (i : ℕ ) → i ≡ suc n → (x : Fin (suc (suc n))) → Fin (suc (suc n))
-     lemma i refl x with <-cmp (toℕ x) i
-     lemma i refl x | tri< a ¬b ¬c = fin+1 (perm ⟨$⟩ˡ (fromℕ≤ x<sn))  where
-       x<sn : toℕ x < suc n
-       x<sn = a
-     lemma i refl x | tri≈ ¬a b ¬c = fromℕ≤ {m} {suc (suc n)} (<-trans (s≤s m<n ) a<sa ) 
-     lemma i refl x | tri> ¬a ¬b c = ⊥-elim ( nat-≤> c  fin<n )
-   lem8 : {x : Fin (suc (suc n)) } → toℕ ( fromℕ≤ {m} {suc (suc n)} (<-trans (s≤s m<n ) a<sa )) ≡ m
-   lem8 {x} = toℕ-fromℕ≤ (<-trans (s≤s m<n ) a<sa )
-   piso← : (x : Fin (suc (suc n))) → p← ( p→ x ) ≡ x
-   piso← x with <-cmp (toℕ x) m
-   piso← x | tri< a ¬b ¬c = begin
-          p← ( fin+1 (perm ⟨$⟩ʳ (fromℕ≤ x<sn)) ) 
-       ≡⟨ {!!} ⟩
-          fin+1 (perm ⟨$⟩ˡ (perm ⟨$⟩ʳ fromℕ≤ (<-trans a (s≤s m<n))))
-       ≡⟨ cong (λ k → fin+1 k ) (inverseˡ perm) ⟩
-          fin+1 (fromℕ≤ x<sn)
-       ≡⟨ {!!} ⟩
-          x
-       ∎  where
-            open ≡-Reasoning
-            k = inverseˡ perm 
-            x<sn : toℕ x < suc n
-            x<sn = <-trans a (s≤s m<n)
-   piso← x | tri> ¬a ¬b c = begin
-          p← ( fin+1 (perm ⟨$⟩ʳ (fromℕ≤ (pred<n {_} {x} 0<s  ))))
-       ≡⟨ {!!} ⟩
-          x
-       ∎  where
-            open ≡-Reasoning
-   piso← x | tri≈ ¬a refl ¬c = begin
-          p← ( fromℕ≤ a<sa )
-       ≡⟨ lem4 refl ⟩
-          fromℕ≤ {m} {suc (suc n)} (<-trans (s≤s m<n ) a<sa )
-       ≡⟨ {!!} ⟩
-          x
-       ∎  where
-            open ≡-Reasoning
-            lem4 : {x : Fin (suc (suc n)) } → x ≡ fromℕ≤ {suc n} a<sa  → p← x ≡ fromℕ≤ {m} {suc (suc n)} (<-trans (s≤s m<n ) a<sa )
-            lem4 {x} refl with <-cmp (toℕ x) (suc n)
-            lem4  refl | tri< a ¬b ¬c = ⊥-elim ( ¬b {!!} )
-            lem4  refl | tri≈ ¬a b ¬c = refl
-            lem4  refl | tri> ¬a ¬b c = ⊥-elim ( ¬b {!!} )
-   piso→ : (x : Fin (suc (suc n))) → p→ ( p← x ) ≡ x
-   piso→ x = lemma2 (suc n) refl x where
-     lemma2 : (i : ℕ ) → i ≡ suc n → (x : Fin (suc (suc n))) → p→ ( p← x ) ≡ x
-     lemma2 i refl x with <-cmp (toℕ x)  i
-     lemma2 i refl x | tri< a ¬b ¬c = begin
-           p→ ( fin+1 (perm ⟨$⟩ˡ (fromℕ≤ x<sn)))
-       ≡⟨ {!!} ⟩
-          x
-       ∎  where
-            open ≡-Reasoning
-            x<sn : toℕ x < suc n
-            x<sn = a
-     lemma2 i refl x | tri> ¬a ¬b c = ⊥-elim ( nat-≤> c  fin<n )
-     lemma2 i refl x | tri≈ ¬a b ¬c = begin
-          p→ (fromℕ≤ {m} {suc (suc n)} (<-trans (s≤s m<n ) a<sa ))
-       ≡⟨ lem5 (fromℕ≤ {m} {suc (suc n)} (<-trans (s≤s m<n ) a<sa ))  {!!} ⟩
-          fromℕ≤ a<sa
-       ≡⟨ {!!} ⟩
-          x
-       ∎  where
-            open ≡-Reasoning
-            lem7 : {x : Fin (suc (suc n)) } → x ≡ fromℕ≤ (s≤s (s≤s m<n)) → toℕ x ≡ m
-            lem7 refl = trans (toℕ-fromℕ≤ _) {!!}
-            lem6 : {x : Fin (suc (suc n)) } → x ≡ fromℕ≤ (s≤s (s≤s m<n)) → toℕ x ≡ (suc m)
-            lem6 refl = toℕ-fromℕ≤ _
-            -- lem5 : {x : Fin (suc (suc n)) } → x ≡ fromℕ≤ {m} {suc (suc n)} (<-trans (s≤s m<n ) a<sa ) → p→ x ≡ fromℕ≤ a<sa
-            lem5 : (x : Fin (suc (suc n)) ) → x ≡ fromℕ≤ {m} {suc (suc n)} (<-trans (s≤s m<n ) a<sa ) → p→ x ≡ fromℕ≤ a<sa
-            lem5 x eq with <-cmp (toℕ x) m
-            lem5 x eq | tri< a ¬b ¬c = {!!}
-            lem5 x eq | tri≈ ¬a refl ¬c = refl
-            lem5 x eq | tri> ¬a ¬b c = {!!}
+   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)) = begin
+          p→ (p← (suc (suc x)))
+       ≡⟨⟩
+         suc ( suc (perm ⟨$⟩ˡ (perm ⟨$⟩ʳ x)))
+       ≡⟨ cong (λ k → suc (suc k) ) (inverseˡ perm) ⟩
+          suc (suc x)
+       ∎ where open ≡-Reasoning
 
+   piso→ : (x : Fin (suc (suc n)) ) → p← ( p→ x ) ≡ x
+   piso→ zero = refl
+   piso→ (suc zero) = refl
+   piso→ (suc (suc x)) = begin
+          p← (p→ (suc (suc x)) )
+       ≡⟨⟩
+         suc (suc (perm ⟨$⟩ʳ (perm ⟨$⟩ˡ x)))
+       ≡⟨ cong (λ k → suc (suc k) ) (inverseʳ perm) ⟩
+          suc (suc x)
+       ∎ where open ≡-Reasoning
+
+-- enumeration
+
+psawpn : {n m : ℕ} → suc m < n → Permutation n n
+psawpn {suc zero} {m} (s≤s ())
+psawpn {suc n} {m} (s≤s (s≤s x)) = pswap pid 
+
+pfill : {n m : ℕ} → m < n → Permutation m m → Permutation n n
+pfill = {!!}
+
+eperm  : {n m : ℕ} → m < n → Permutation n n → Permutation (suc n) (suc n)
+eperm {zero} ()
+eperm {suc n} {0} (s≤s z≤n) perm = pprep perm
+eperm {suc (suc n)} {suc m} (s≤s (s≤s m<n)) perm = {!!}