Mercurial > hg > Members > kono > Proof > galois

changeset 30:a9fa68dfbd26

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 Wed, 19 Aug 2020 16:08:32 +0900
parents a65f3b17eade
children 039e8511da2a
files Symmetric.agda
diffstat 1 files changed, 18 insertions(+), 13 deletions(-) [+]
line wrap: on
line diff
--- a/Symmetric.agda	Wed Aug 19 11:54:19 2020 +0900
+++ b/Symmetric.agda	Wed Aug 19 16:08:32 2020 +0900
@@ -99,8 +99,10 @@
      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ℕ≤ (s≤s (s≤s m<n))
+     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 = {!!}
@@ -108,16 +110,16 @@
    piso← x | tri≈ ¬a refl ¬c = begin
           p← ( fromℕ≤ a<sa )
        ≡⟨ lem4 refl ⟩
-          fromℕ≤ (s≤s (s≤s m<n))
+          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ℕ≤ (s≤s (s≤s m<n))
+            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 = {!!}
+            lem4  refl | tri< a ¬b ¬c = ⊥-elim ( ¬b {!!} )
             lem4  refl | tri≈ ¬a b ¬c = refl
-            lem4  refl | tri> ¬a ¬b c = {!!}
+            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
@@ -125,18 +127,21 @@
      lemma2 i refl x | tri< a ¬b ¬c = {!!}
      lemma2 i refl x | tri> ¬a ¬b c = {!!}
      lemma2 i refl x | tri≈ ¬a b ¬c = begin
-          p→ (fromℕ≤ (s≤s (s≤s m<n)))
-       ≡⟨ lem5 refl ⟩
+          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ℕ≤ (s≤s (s≤s m<n)) → p→ x ≡ fromℕ≤ a<sa
-            lem5 refl with <-cmp (toℕ x) m
-            lem5 refl | tri< a ¬b ¬c = {!!}
-            lem5 refl | tri≈ ¬a refl ¬c = {!!}
-            lem5 refl | tri> ¬a ¬b c = {!!}
+            -- 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 = {!!}