Mercurial > hg > Members > kono > Proof > galois

changeset 53:2283d6f8a2fb

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
connected
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 23 Aug 2020 16:34:19 +0900
parents 0377ac873d39
children 8224694a4dda
files Putil.agda
diffstat 1 files changed, 31 insertions(+), 4 deletions(-) [+]
line wrap: on
line diff
--- a/Putil.agda	Sun Aug 23 15:23:41 2020 +0900
+++ b/Putil.agda	Sun Aug 23 16:34:19 2020 +0900
@@ -171,11 +171,13 @@
          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₁ = {!!}
@@ -184,7 +186,32 @@
    piso← x | tri> ¬a ¬b c = {!!}
 
    piso→ : (x : Fin n ) → p← ( p→ x ) ≡ x
-   piso→ 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₁ = {!!}
+   piso→ x | tri< a ¬b ¬c | tri> ¬a ¬b₁ c = {!!}
+   piso→ x | tri≈ ¬a b ¬c = {!!}
+   piso→ x | tri> ¬a ¬b c = {!!}
 
 perm→FL   : {n : ℕ }  → Permutation n n → FL n
 perm→FL {zero} perm = f0