Mercurial > hg > Members > kono > Proof > galois

changeset 31:039e8511da2a

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fperm connected
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 19 Aug 2020 16:18:32 +0900
parents a9fa68dfbd26
children 5b299203acf0
files Symmetric.agda
diffstat 1 files changed, 23 insertions(+), 4 deletions(-) [+]
line wrap: on
line diff
--- a/Symmetric.agda	Wed Aug 19 16:08:32 2020 +0900
+++ b/Symmetric.agda	Wed Aug 19 16:18:32 2020 +0900
@@ -105,8 +105,20 @@
    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 = {!!}
-   piso← x | tri> ¬a ¬b c = {!!}
+   piso← x | tri< a ¬b ¬c = begin
+          p← ( fin+1 (perm ⟨$⟩ʳ (fromℕ≤ x<sn)) ) 
+       ≡⟨ {!!} ⟩
+          x
+       ∎  where
+            open ≡-Reasoning
+            x<sn : toℕ x < suc n
+            x<sn = <-trans a (s≤s m<n)
+   piso← x | tri> ¬a ¬b c = begin
+          p← ( fin+1 (perm ⟨$⟩ʳ (fromℕ≤ (pred<n {_} {x} 0<s  ))))
+       ≡⟨ {!!} ⟩
+          x
+       ∎  where
+            open ≡-Reasoning
    piso← x | tri≈ ¬a refl ¬c = begin
           p← ( fromℕ≤ a<sa )
        ≡⟨ lem4 refl ⟩
@@ -124,8 +136,15 @@
    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 = {!!}
+     lemma2 i refl x | tri< a ¬b ¬c = begin
+           p→ ( fin+1 (perm ⟨$⟩ˡ (fromℕ≤ x<sn)))
+       ≡⟨ {!!} ⟩
+          x
+       ∎  where
+            open ≡-Reasoning
+            x<sn : toℕ x < suc n
+            x<sn = a
+     lemma2 i refl x | tri> ¬a ¬b c = ⊥-elim ( nat-≤> c  fin<n )
      lemma2 i refl x | tri≈ ¬a b ¬c = begin
           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 ))  {!!} ⟩