Mercurial > hg > Members > kono > Proof > galois

changeset 19:5091302d990d

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 Tue, 18 Aug 2020 23:21:03 +0900
parents 71ba20fff6f6
children 65e6c97a03cd ce6a1a08653a
files Symmetric.agda
diffstat 1 files changed, 23 insertions(+), 13 deletions(-) [+]
line wrap: on
line diff
--- a/Symmetric.agda	Tue Aug 18 22:50:41 2020 +0900
+++ b/Symmetric.agda	Tue Aug 18 23:21:03 2020 +0900
@@ -121,38 +121,48 @@
    p→ x | tri> ¬a ¬b c =  fin+1 (perm ⟨$⟩ʳ (fromℕ≤ (pred<n {_} {x} 0<s  )))
 
    p← : Fin (suc (suc n)) → Fin (suc (suc n))
-   p← x with <-cmp (toℕ x) (suc n)
-   p← x | tri< a ¬b ¬c = fin+1 (perm ⟨$⟩ˡ (fromℕ≤ x<sn))  where
+   p← x = lemma (suc n) refl x where
+     lemma : (i : ℕ ) → i ≡ suc n → (x : Fin (suc (suc n))) → Fin (suc (suc n))
+     lemma i refl x with <-cmp (toℕ x) i
+     lemma i refl x | tri< a ¬b ¬c = fin+1 (perm ⟨$⟩ˡ (fromℕ≤ x<sn))  where
        x<sn : toℕ x < suc n
        x<sn = a
-   p← x | tri≈ ¬a b ¬c = fromℕ≤ (s≤s (s≤s m<n))
-   p← x | tri> ¬a ¬b c = ⊥-elim ( nat-≤> c  fin<n )
-
+     lemma i refl x | tri≈ ¬a b ¬c = fromℕ≤ (s≤s (s≤s m<n))
+     lemma i refl x | tri> ¬a ¬b c = ⊥-elim ( nat-≤> c  fin<n )
    piso← : (x : Fin (suc (suc n))) → p← ( p→ x ) ≡ x
    piso← x with <-cmp (toℕ x) m
    piso← x | tri< a ¬b ¬c = {!!}
    piso← x | tri≈ ¬a refl ¬c = begin
           p← ( fromℕ≤ a<sa )
-       ≡⟨ {!!}  ⟩
+       ≡⟨ lem4 refl ⟩
           fromℕ≤ (s≤s (s≤s m<n))
-       ≡⟨ {!!}  ⟩
+       ≡⟨ {!!} ⟩
           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} refl with <-cmp (toℕ x) (suc n)
             lem4  refl | tri< a ¬b ¬c = {!!}
-            lem4  refl | tri≈ ¬a b ¬c = {!!}
+            lem4  refl | tri≈ ¬a b ¬c = refl
             lem4  refl | tri> ¬a ¬b c = {!!}
    piso← x | tri> ¬a ¬b c = {!!}
    piso→ : (x : Fin (suc (suc n))) → p→ ( p← x ) ≡ x
-   piso→ x with <-cmp (toℕ x) (suc n)
-   piso→ x | tri< a ¬b ¬c = {!!}
-   piso→ x | tri≈ ¬a b ¬c = begin
-          {!!} -- fromℕ≤ (s≤s (s≤s m<n))
+   piso→ x = lemma2 (suc n) refl x where
+     lemma2 : (i : ℕ ) → i ≡ suc n → (x : Fin (suc (suc n))) → p→ ( p← x ) ≡ x
+     lemma2 i refl x with <-cmp (toℕ x)  i
+     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 ⟩
+          fromℕ≤ a<sa
        ≡⟨ {!!}  ⟩
           x
        ∎  where
             open ≡-Reasoning
-   piso→ x | tri> ¬a ¬b c = {!!}
+            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 = refl
+            lem5 refl | tri> ¬a ¬b c = {!!}
+     lemma2 i refl x | tri> ¬a ¬b c = {!!}