Mercurial > hg > Members > kono > Proof > galois

changeset 81:59aaf2000591

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
plist0
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 26 Aug 2020 19:09:32 +0900
parents b0c344ece453
children fcb9e29d1894
files Putil.agda sym5.agda
diffstat 2 files changed, 17 insertions(+), 4 deletions(-) [+]
line wrap: on
line diff
--- a/Putil.agda	Wed Aug 26 18:19:40 2020 +0900
+++ b/Putil.agda	Wed Aug 26 19:09:32 2020 +0900
@@ -157,9 +157,22 @@
   pleq0 ()
 pleq  {suc n} x y eq = record { peq = λ q → pleq1 n a<sa eq q fin<n } where
   pleq1 : (i : ℕ ) → (i<sn : i < suc n ) →  plist2 x i i<sn ≡ plist2 y i i<sn → (q : Fin (suc n)) → toℕ q < suc i → x ⟨$⟩ʳ q ≡ y ⟨$⟩ʳ q
-  pleq1 zero i<sn eq q (s≤s q<i) = {!!}
+  pleq1 zero i<sn eq q q<i with  <-cmp (toℕ q) zero
+  ... | tri< () ¬b ¬c
+  ... | tri> ¬a ¬b c = ⊥-elim (nat-≤> c q<i )
+  ... | tri≈ ¬a b ¬c = begin
+          x ⟨$⟩ʳ q
+       ≡⟨ cong ( λ k → x ⟨$⟩ʳ k ) (toℕ-injective b )⟩
+          x ⟨$⟩ʳ zero
+       ≡⟨ toℕ-injective (headeq eq) ⟩
+          y ⟨$⟩ʳ zero
+       ≡⟨ cong ( λ k → y ⟨$⟩ʳ k ) (sym (toℕ-injective b )) ⟩
+          y ⟨$⟩ʳ q
+       ∎ where
+          open ≡-Reasoning
   pleq1 (suc i) (s≤s i<sn) eq q q<i with <-cmp (toℕ q) (suc i)
   ... | tri< a ¬b ¬c = pleq1 i (<-trans i<sn a<sa ) (taileq eq) q a
+  ... | tri> ¬a ¬b c = ⊥-elim (nat-≤> c q<i )
   ... | tri≈ ¬a b ¬c = begin
             x ⟨$⟩ʳ q
        ≡⟨ cong (λ k → x ⟨$⟩ʳ k) (pleq3 b) ⟩
@@ -182,7 +195,6 @@
                ∎ ) where open ≡-Reasoning
           pleq2 : toℕ ( x ⟨$⟩ʳ (suc (fromℕ< i<sn)) ) ≡ toℕ ( y ⟨$⟩ʳ (suc (fromℕ< i<sn)) )
           pleq2 = headeq eq
-  ... | tri> ¬a ¬b c = ⊥-elim (nat-≤> c q<i )
 
 data  FL : (n : ℕ )→ Set where
    f0 :  FL 0 
--- a/sym5.agda	Wed Aug 26 18:19:40 2020 +0900
+++ b/sym5.agda	Wed Aug 26 19:09:32 2020 +0900
@@ -142,9 +142,9 @@
      triple (s≤s (s≤s (s≤s z≤n))) (s≤s (s≤s z≤n)) = {!!}
      triple (s≤s (s≤s (s≤s z≤n))) (s≤s (s≤s (s≤s z≤n))) = {!!}
      triple (s≤s (s≤s (s≤s z≤n))) (s≤s (s≤s (s≤s (s≤s z≤n)))) = 
-        record { dba0<3 = # 1 ; dba1<4 = # 4 ; aec0<3 = # 0 ; aec1<4 = # 3 ; abc= = tt7 }  where
+        record { dba0<3 = # 1 ; dba1<4 = fromℕ< a<sa ; aec0<3 = # 0 ; aec1<4 = # 3 ; abc= = tt7 }  where
              tt7 : abc (s≤s (s≤s (s≤s z≤n))) (s≤s (s≤s (s≤s (s≤s z≤n)))) =p=
-                   [ dba (fin≤n  {3} (# 1))(fin≤n  {4} (# 4)) , aec (fin≤n  {3} (# 0)) (fin≤n {4} (# 3))  ]  
+                   [ dba (fin≤n  {3} (# 1))(fin≤n  {4} (fromℕ< a<sa)) , aec (fin≤n  {3} (# 0)) (fin≤n {4} (# 3))  ]  
              tt7 = record { peq = λ q → lll q } where
                 lll : (q : Fin 5) → _
                 lll zero = refl
@@ -152,6 +152,7 @@
                 lll (suc (suc zero)) = refl
                 lll (suc (suc (suc zero))) = refl
                 lll (suc (suc (suc (suc zero)))) = refl
+             tt19 = {!!}
 
 
      dervie-any-3rot : (n : ℕ ) → {i j : ℕ }  → (i<3 : i ≤ 3 ) → (j<4 : j ≤ 4 ) → deriving n (abc i<3 j<4 )