Mercurial > hg > Members > kono > Proof > automaton

changeset 157:0b74851665ee

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
( n k : ℕ ) → 1 < n → gcd n k ≤ n
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 02 Jan 2021 16:51:34 +0900
parents 91265c971200
children c332bb9dbf98
files agda/gcd.agda
diffstat 1 files changed, 17 insertions(+), 10 deletions(-) [+]
line wrap: on
line diff
--- a/agda/gcd.agda	Sat Jan 02 11:49:44 2021 +0900
+++ b/agda/gcd.agda	Sat Jan 02 16:51:34 2021 +0900
@@ -35,9 +35,9 @@
 
 gcd1 : ( i i0 j j0 : ℕ ) → ℕ
 gcd1 zero i0 zero j0 with <-cmp i0 j0
-... | tri< a ¬b ¬c = j0
+... | tri< a ¬b ¬c = i0
 ... | tri≈ ¬a refl ¬c = i0
-... | tri> ¬a ¬b c = i0
+... | tri> ¬a ¬b c = j0
 gcd1 zero i0 (suc zero) j0 = 1
 gcd1 zero zero (suc (suc j)) j0 = j0
 gcd1 zero (suc i0) (suc (suc j)) j0 = gcd1 i0 (suc i0) (suc j) (suc (suc j))
@@ -156,18 +156,25 @@
           gcd1 1 1 (suc j) (suc j) ∎ where open ≡-Reasoning
        gcd200 (suc (suc i)) i0 (suc j) zero i=i0 ()
 
-gcd6 : ( i i0 j j0 n n0 : ℕ) → gcd1 i i0 j j0 ≡  gcd1 0 n 0 n0 → n ≡ n0
-gcd6 i i0 j j0 n n0 = {!!} 
-
 gcd5 : ( n k : ℕ ) → 1 < n → gcd n k ≤ n
 gcd5 n k 0<n = gcd50 n n k k 0<n ≤-refl ≤-refl where
+    gcd52 : {i : ℕ } → 1 < suc (suc i)
+    gcd52 {zero} = a<sa
+    gcd52 {suc i} = <-trans (gcd52 {i}) a<sa
     gcd50 : (i i0 j j0 : ℕ) → 1 < i0 → i ≤ i0 → j ≤ j0 →  gcd1 i i0 j j0 ≤ i0 
     gcd50 zero i0 zero j0 0<i i<i0 j<j0 with <-cmp i0 j0
-    ... | tri< a ¬b ¬c = {!!} -- ≤-refl    -- j0 ≤ i0
-    ... | tri≈ ¬a refl ¬c =  ≤-refl
-    ... | tri> ¬a ¬b c = ≤-refl
-    gcd50 zero i0 (suc j) j0 0<i  i<i0 j<j0 = {!!}
-    gcd50 (suc i) i0 j j0 0<i  i<i0 j<j0 = {!!}
+    ... | tri< a ¬b ¬c = ≤-refl    
+    ... | tri≈ ¬a refl ¬c =  ≤-refl 
+    ... | tri> ¬a ¬b c = ≤-trans refl-≤s c  
+    gcd50 zero (suc i0) (suc zero) j0 0<i i<i0 j<j0 = gcd51 0<i where 
+       gcd51 : 1 < suc i0 → gcd1 zero (suc i0) 1 j0 ≤ suc i0
+       gcd51 1<i = ≤to< 1<i
+    gcd50 zero (suc i0) (suc (suc j)) j0 0<i i<i0 j<j0 = gcd50 i0 (suc i0) (suc j) (suc (suc j)) 0<i refl-≤s refl-≤s
+    gcd50 (suc zero) i0 zero j0 0<i i<i0 j<j0 = ≤to< 0<i
+    gcd50 (suc (suc i)) i0 zero zero 0<i i<i0 j<j0 = ≤-refl
+    gcd50 (suc (suc i)) i0 zero (suc j0) 0<i i<i0 j<j0 = ≤-trans (gcd50 (suc i) (suc (suc i))  j0 (suc j0) gcd52  refl-≤s refl-≤s) i<i0
+    gcd50 (suc i) i0 (suc j) j0 0<i i<i0 j<j0 = subst (λ k → k ≤ i0 ) (sym (gcd22 i i0 j j0))
+        (gcd50 i i0 j j0 0<i (≤-trans refl-≤s i<i0) (≤-trans refl-≤s j<j0)) 
 
 gcd4 : ( n k : ℕ ) → 1 < n  → gcd n k ≡ k → k ≤ n
 gcd4 = {!!}