Mercurial > hg > Members > kono > Proof > automaton

changeset 149:d3a8572ced9c

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
non terminating GCD
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 01 Jan 2021 12:16:32 +0900
parents 8207b69c500b
children 36d3ecce01b2
files agda/gcd.agda
diffstat 1 files changed, 28 insertions(+), 7 deletions(-) [+]
line wrap: on
line diff
--- a/agda/gcd.agda	Thu Dec 31 15:20:14 2020 +0900
+++ b/agda/gcd.agda	Fri Jan 01 12:16:32 2021 +0900
@@ -8,6 +8,7 @@
 open import Relation.Nullary
 open import Relation.Binary.PropositionalEquality
 open import Relation.Binary.Definitions
+open import nat
 
 even : (n : ℕ ) → Set
 even zero = ⊤
@@ -31,6 +32,23 @@
 even*n : {n m : ℕ } → even n → even ( n * m )
 even*n {n} {m} en = subst even (*-comm m n) (n*even {m} {n} en)
 
+gcd2 : ( i i0 j j0 : ℕ ) → i ≤ i0 → j ≤ j0 → i0 < j0  → ℕ
+gcd2 zero i0 zero j0 i<i0 j<j0 i<j = j0
+gcd2 zero i0 (suc zero) j0 i<i0 j<j0 i<j = 1
+gcd2 zero zero (suc (suc j)) j0 i<i0 j<j0 i<j = j0
+-- i<i0 : zero ≤ suc i0
+-- j<j0 : suc (suc j) ≤ j0
+-- i<j  : suc i0 < j0
+gcd2 zero (suc i0) (suc (suc j)) j0 i<i0 j<j0 i<j with <-cmp (suc (suc j)) (suc i0)  -- non terminating
+... | tri< a ¬b ¬c = gcd2 i0 (suc i0) (suc j) (suc (suc j)) refl-≤s refl-≤s {!!}
+... | tri≈ ¬a refl ¬c = suc i0
+... | tri> ¬a ¬b c = gcd2 i0 (suc i0) (suc j) (suc (suc j)) refl-≤s refl-≤s {!!}
+-- = gcd2  (suc j) (suc (suc j))  i0 (suc i0) refl-≤s refl-≤s {!!} -- suc (suc j) < suc i0
+gcd2 (suc zero) i0 zero j0 i<i0 j<j0 i<j = 1
+gcd2 (suc (suc i)) i0 zero zero i<i0 j<j0 i<j = i0
+gcd2 (suc (suc i)) i0 zero (suc j0) i<i0 j<j0 i<j  = gcd2 (suc i) (suc (suc i))  j0 (suc j0)   refl-≤s refl-≤s {!!} --  suc (suc i) < suc j0
+gcd2 (suc i) i0 (suc j) j0 i<i0 j<j0 i<j = gcd2 i i0 j j0 (≤-trans refl-≤s i<i0) (≤-trans refl-≤s j<j0) i<j  
+
 gcd1 : ( i i0 j j0 : ℕ ) → ℕ
 gcd1 zero i0 zero j0 with <-cmp i0 j0
 ... | tri< a ¬b ¬c = j0
@@ -57,8 +75,6 @@
        2
     ∎ where open ≡-Reasoning
 
-open import nat
-
 -- gcd26 : { n m : ℕ} → n > 1 → m > 1 → n - m > 0 → gcd n m ≡ gcd (n - m) m
 -- gcd27 : { n m : ℕ} → n > 1 → m > 1 → n - m > 0 → gcd n k ≡ k → k ≤ n
 
@@ -89,14 +105,19 @@
 gcd26 n m i 1<n 1<m gi g1 = gcd261 n n m m i i 1<n 1<m gi g1 where
     gcd261 : (n n0 m m0 i i0 : ℕ) → 1 < n → 1 < m0  → gcd1 n n0 i i0 ≡ m0 → ¬ ( gcd1 n n0 m m0 ≡ 1 )
     gcd261 zero n0 m m0 i i0 () 1<m gi g1
+    -- gi       : gcd1 (suc n) n0 zero i0 ≡ m0
+    -- g1       : gcd1 (suc n) n0 m m0 ≡ 1
     gcd261 (suc n) n0 m m0 zero i0 1<n 1<m gi g1 = {!!}
+    -- gi       : gcd1 (suc n) n0 (suc i) i0 ≡ m0
+    -- g1       : gcd1 (suc n) n0 zero m0 ≡ 1
     gcd261 (suc n) n0 zero m0 (suc i) i0 1<n 1<m gi g1 = {!!}
-    -- 1<n      : 1 < suc n
-    -- 1<m      : 1 < m0
-    -- gi       : gcd1 (suc n) n0 (suc i) i0 ≡ m0 -- gi       : gcd1 n n0 i i0 ≡ m0
-    -- g1       : gcd1 (suc n) n0 (suc m) m0 ≡ 1  -- g1       : gcd1 n n0 m m0 ≡ 1
     gcd261 (suc zero) n0 (suc m) m0 (suc i) i0 1<n 1<m gi g1 = ⊥-elim ( nat-<≡ 1<n  )
-    gcd261 (suc (suc zero)) n0 (suc m) m0 (suc i) i0 1<n 1<m gi g1 = {!!}
+    gcd261 (suc (suc zero)) n0 (suc m) m0 (suc zero) i0 1<n 1<m gi g1 = ⊥-elim (  nat-≡< gi 1<m )
+    -- gi       : gcd1 0 n0 i i0 ≡ m0
+    gcd261 (suc (suc zero)) n0 (suc zero) m0 (suc (suc i)) i0 1<n 1<m gi g1 = {!!}
+    -- gi       : gcd1 0 n0 i i0 ≡ m0
+    -- g1       : gcd1 0 n0 m m0 ≡ 1
+    gcd261 (suc (suc zero)) n0 (suc (suc m)) m0 (suc (suc i)) i0 1<n 1<m gi g1 = {!!}
     gcd261 (suc (suc (suc n))) n0 (suc m) m0 (suc i) i0 1<n 1<m gi g1 = 
         gcd261 (suc (suc n)) n0 m m0 i i0 (s≤s (s≤s z≤n)) 1<m gi g1