Mercurial > hg > Members > kono > Proof > galois

changeset 92:2e5d0b142eca

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 Sat, 29 Aug 2020 09:36:52 +0900
parents 482ef04890f8
children 4cae99fadd61
files Putil.agda
diffstat 1 files changed, 29 insertions(+), 4 deletions(-) [+]
line wrap: on
line diff
--- a/Putil.agda	Sat Aug 29 07:48:45 2020 +0900
+++ b/Putil.agda	Sat Aug 29 09:36:52 2020 +0900
@@ -169,6 +169,35 @@
           ≡⟨ toℕ-fromℕ< ( s≤s ( ≤-trans fin<n  a≤sa ) ) ⟩
             suc (toℕ x)
           ∎ 
+
+   piso→ : (x : Fin (suc (suc n)) ) → p← ( p→ x ) ≡ x
+   piso→ zero with <-cmp (toℕ (fromℕ< (≤-trans (s≤s z≤n) (s≤s (s≤s  m≤n) )))) (suc m)
+   ... | tri< a ¬b ¬c = refl
+   piso→ (suc x) with <-cmp (toℕ (suc x)) (suc m)
+   ... | tri≈ ¬a b ¬c = {!!}
+   ... | tri> ¬a ¬b c = {!!} 
+   ... | tri< a ¬b ¬c = p10 (fromℕ< (≤-trans (s≤s  a) (s≤s (s≤s  m≤n) ))) refl  where
+       p10 : (y : Fin (suc (suc n)) ) → y ≡ fromℕ< (≤-trans (s≤s  a) (s≤s (s≤s  m≤n) ))  → p← y ≡ suc x
+       p10 zero ()
+       p10 (suc y) eq with <-cmp (toℕ y) (suc m) -- eq : suc y ≡ suc (suc (fromℕ< (≤-pred (≤-trans a (s≤s m≤n))))) ,  a : suc x < suc m
+       ... | tri< a₁ ¬b ¬c = p11 where
+           p12 : (toℕ (fromℕ< (≤-pred (≤-trans a (s≤s m≤n))))) ≡ (toℕ x)
+           p12 = {!!}
+           p11 : fromℕ< (≤-trans (fin<n {_} {y}) a≤sa ) ≡ suc x
+           p11 = begin
+              fromℕ< (≤-trans (fin<n {_} {y}) a≤sa )
+             ≡⟨ {!!} ⟩
+              fromℕ< (≤-trans (fin<n {_} {suc (fromℕ< (≤-pred (≤-trans a (s≤s m≤n))))}) a≤sa )
+             ≡⟨ {!!} ⟩
+              fromℕ< (≤-trans (fin<n {_} {fromℕ< (≤-trans a (s≤s m≤n))}) a≤sa )
+             ≡⟨ fromℕ<-irrelevant _ _ (cong suc p12 ) (≤-trans (fin<n {_} {fromℕ< (≤-trans a (s≤s m≤n))}) a≤sa) (s≤s (fin<n {suc n}))  ⟩
+              suc (fromℕ< (fin<n {suc n} {x} )) 
+             ≡⟨ cong suc (fromℕ<-toℕ x _ ) ⟩
+              suc x
+             ∎
+       ... | tri≈ ¬a b ¬c = {!!}
+       ... | tri> ¬a ¬b c = {!!}
+
    piso← : (x : Fin (suc (suc n)) ) → p→ ( p← x ) ≡ x
    piso← zero with <-cmp (toℕ (fromℕ< (s≤s (s≤s m≤n)))) (suc m) | mm
    ... | tri< a ¬b ¬c | t = ⊥-elim ( ¬b t )
@@ -204,10 +233,6 @@
              suc x
           ∎ 
 
-
-   piso→ : (x : Fin (suc (suc n)) ) → p← ( p→ x ) ≡ x
-   piso→ = {!!}
-
 t7 =  plist (pins' {3} (n≤ 3)) ∷ plist (flip ( pins' {3} (n≤ 3) )) ∷  plist ( pins' {3} (n≤ 3)  ∘ₚ  flip ( pins' {3} (n≤ 3))) ∷ []
 t8 =  {!!}