Mercurial > hg > Members > kono > Proof > galois

changeset 52:0377ac873d39

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 15:23:41 +0900
parents 3e677c24a6cc
children 2283d6f8a2fb
files Putil.agda
diffstat 1 files changed, 24 insertions(+), 2 deletions(-) [+]
line wrap: on
line diff
--- a/Putil.agda	Sun Aug 23 14:43:35 2020 +0900
+++ b/Putil.agda	Sun Aug 23 15:23:41 2020 +0900
@@ -152,10 +152,32 @@
    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 x)))  n
-   piso← x | tri< a ¬b ¬c | tri< a₁ ¬b₁ ¬c₁ = {!!}
+   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))
+          ≡⟨ {!!} ⟩ 
+             toℕ (Inverse.from perm Π.⟨$⟩ ( Inverse.to perm Π.⟨$⟩ (fin+1 x) ))
+          ≡⟨ {!!} ⟩ 
+             toℕ (fin+1 x)
+          ≡⟨ {!!} ⟩ 
+             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 = {!!}