Mercurial > hg > Members > kono > Proof > galois

changeset 93:4cae99fadd61

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 12:06:57 +0900
parents 2e5d0b142eca
children 4efab088abd0
files Putil.agda
diffstat 1 files changed, 24 insertions(+), 18 deletions(-) [+]
line wrap: on
line diff
--- a/Putil.agda	Sat Aug 29 09:36:52 2020 +0900
+++ b/Putil.agda	Sat Aug 29 12:06:57 2020 +0900
@@ -174,29 +174,35 @@
    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 = p13 {!!} refl where
+       p13 : (y : Fin (suc (suc n)) ) → y ≡ {!!} → p← y ≡ suc x
+       p13 = {!!}
    ... | 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
+       p10 (suc y) eq = p15 where
+          p12 : toℕ y ≡ suc (toℕ x)
+          p12 = begin
+               toℕ y
+             ≡⟨ cong (λ k → Data.Nat.pred (toℕ k)) eq ⟩
+               toℕ (fromℕ< (≤-trans a (s≤s m≤n)))
+             ≡⟨ toℕ-fromℕ< {suc (toℕ x)} {suc n} (≤-trans a (s≤s m≤n)) ⟩
+               suc (toℕ x)
              ∎
-       ... | tri≈ ¬a b ¬c = {!!}
-       ... | tri> ¬a ¬b c = {!!}
+          p15 : p← (suc y) ≡ suc x
+          p15 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
+            p11 : fromℕ< (≤-trans (fin<n {_} {y}) a≤sa ) ≡ suc x
+            p11 = begin
+               fromℕ< (≤-trans (fin<n {_} {y}) a≤sa )
+              ≡⟨ fromℕ<-irrelevant _ _ p12 _ (s≤s (fin<n {suc n}))  ⟩
+               suc (fromℕ< (fin<n {suc n} {x} )) 
+              ≡⟨ cong suc (fromℕ<-toℕ x _ ) ⟩
+               suc x
+              ∎
+          ... | tri≈ ¬a b ¬c = ⊥-elim ( nat-≡< b (subst (λ k → k < suc m) (sym p12) a ))  --  suc x < suc m -> y = suc x  → toℕ y < suc m 
+          ... | tri> ¬a ¬b c = ⊥-elim ( nat-<> c (subst (λ k → k < suc m) (sym p12) a ))  
 
    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