Mercurial > hg > Members > kono > Proof > galois

changeset 50:ddec1ef4f5e4

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 23 Aug 2020 13:39:14 +0900
parents 8b3b95362ca9
children 3e677c24a6cc
files Putil.agda
diffstat 1 files changed, 70 insertions(+), 3 deletions(-) [+]
line wrap: on
line diff
--- a/Putil.agda	Sat Aug 22 19:55:41 2020 +0900
+++ b/Putil.agda	Sun Aug 23 13:39:14 2020 +0900
@@ -130,9 +130,76 @@
    f0 :  FL 0 
    _::_ :  { n : ℕ } → Fin (suc n ) → FL n → FL (suc n)
 
+open import logic 
+
+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
+
+   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
+
+   sh2 : {x : Fin n} → ¬ perm ⟨$⟩ˡ (suc x) ≡ zero
+   sh2 {x} eq with shlem→ (suc x) eq
+   sh2 {x} eq | ()
+
+   p→ : Fin n → Fin n 
+   p→ x = fin-1 ( perm ⟨$⟩ˡ (suc x) ) sh2
+
+   ssh4 : (x : Fin n  ) → suc (p→  x) ≡ perm ⟨$⟩ˡ (suc x)
+   ssh4 = {!!}
+
+   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 = fin-1 ( perm ⟨$⟩ʳ (suc x) ) sh1 
+
+-- fin-1-sx
+   piso← : (x : Fin n ) → p→ ( p← x ) ≡ x
+   piso← x = sh3 where
+      sh3 :  fin-1 ( perm ⟨$⟩ˡ (suc (  fin-1 ( perm ⟨$⟩ʳ (suc x)  ) sh1 ))) sh2 ≡ x
+      sh3 =  begin
+          fin-1 ( perm ⟨$⟩ˡ (suc (  fin-1 ( perm ⟨$⟩ʳ (suc x)  ) sh1 ))) sh2
+           ≡⟨ cong (λ k → fin-1 (perm ⟨$⟩ˡ k ) (sh4 k) ) (fin-1-xs _ sh5 ) ⟩
+          fin-1 ( perm ⟨$⟩ˡ ( perm ⟨$⟩ʳ (suc x)  )) sh6 ≡⟨ cong (λ k → fin-1 k {!!} ) (inverseˡ perm) ⟩
+          fin-1 (suc x) (λ ()) ≡⟨ fin-1-sx x ⟩
+          x
+       ∎ where
+           open ≡-Reasoning
+           sh4 : (k : Fin (suc n)) → ¬ Inverse.from perm Π.⟨$⟩ k ≡ zero
+           sh4 = {!!}
+           sh5  : ¬ Inverse.to perm Π.⟨$⟩ suc x ≡ zero
+           sh5 = {!!}
+           sh6  : ¬ Inverse.from perm Π.⟨$⟩ (Inverse.to perm Π.⟨$⟩ suc x) ≡ zero
+           sh6 = {!!}
+
+
+   piso→ : (x : Fin n ) → p← ( p→ x ) ≡ x
+   piso→ x = sh4 where
+      sh4 :  fin-1 ( perm ⟨$⟩ʳ (suc (  fin-1 ( perm ⟨$⟩ˡ (suc x)  ) sh2 ))) sh1 ≡ x
+      sh4 = {!!}
+
 perm→FL   : {n : ℕ }  → Permutation n n → FL n
 perm→FL {zero} perm = f0
-perm→FL {suc n} perm = (perm ⟨$⟩ˡ fromℕ≤ a<sa ) :: perm→FL {n} ( remove (fromℕ≤ a<sa) perm )
+perm→FL {suc n} perm = (perm ⟨$⟩ˡ fromℕ≤ a<sa ) :: perm→FL ( shrink fl1 {!!} ) where
+    fl1 : Permutation (suc n) (suc n)
+    fl1 = perm ∘ₚ pinv ( pins {!!})
+    fl1=pprep : perm =p= pprep ( shrink fl1 {!!} )
+    fl1=pprep = {!!}
 
 FL→perm   : {n : ℕ }  → FL n → Permutation n n 
 FL→perm f0 = pid
@@ -140,8 +207,8 @@
 
 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 = {!!}
+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