Mercurial > hg > Members > kono > Proof > automaton

changeset 218:689be82c08fa

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 Mon, 21 Jun 2021 19:22:06 +0900
parents 119ab3f823f1
children 4f9cc768640f
files automaton-in-agda/src/gcd.agda
diffstat 1 files changed, 10 insertions(+), 10 deletions(-) [+]
line wrap: on
line diff
--- a/automaton-in-agda/src/gcd.agda	Mon Jun 21 17:57:07 2021 +0900
+++ b/automaton-in-agda/src/gcd.agda	Mon Jun 21 19:22:06 2021 +0900
@@ -234,21 +234,21 @@
    k + 0 ≡⟨ +-comm _ 0 ⟩
    k  ∎ where open ≡-Reasoning
 
-decD : {k m : ℕ} → k > 1 → Dec (Dividable k m)
-decD {k} {m} k>1 = n-induction {_} {_} {ℕ} {λ m → Dec (Dividable k m)} F I m where
+decD : {k m : ℕ} → k > 1 → Dec (Dividable k m ∧ (0 < m))
+decD {k} {m} k>1 = n-induction {_} {_} {ℕ} {λ m → Dec (Dividable k m ∧ ( 0 < m)) } F I m where
         F : ℕ → ℕ
         F m = m
-        F0 : ( m : ℕ ) → F (m - k) ≡ 0 →  Dec  (Dividable k m )
-        F0 0 eq =  yes div0
+        F0 : ( m : ℕ ) → F (m - k) ≡ 0 →  Dec  (Dividable k m  ∧ (0 < m ))
+        F0 0 eq =   no (λ d → ⊥-elim ( nat-≡< refl (proj2 d)))
         F0 (suc m) eq with <-cmp k (suc m)
-        ... | tri< a ¬b ¬c = yes record { factor = 1 ; is-factor =
-            subst (λ g → 1 * k + 0 ≡ g ) (sym (i-j=0→i=j (<to≤ a) eq )) div1*k+0=k }  where -- (suc m - k) ≡ 0 → k ≡ suc m, k ≤ suc m
-        ... | tri≈ ¬a refl ¬c = yes record { factor = 1 ; is-factor = div1*k+0=k }
-        ... | tri> ¬a ¬b c = no (div<k k>1 (s≤s z≤n ) c )
+        ... | tri< a ¬b ¬c = yes ⟪ record { factor = 1 ; is-factor =
+            subst (λ g → 1 * k + 0 ≡ g ) (sym (i-j=0→i=j (<to≤ a) eq )) div1*k+0=k }  , {!!} ⟫ where -- (suc m - k) ≡ 0 → k ≡ suc m, k ≤ suc m
+        ... | tri≈ ¬a refl ¬c =  yes  ⟪ record { factor = 1 ; is-factor = div1*k+0=k } , {!!} ⟫
+        ... | tri> ¬a ¬b c = no ( λ d →  ⊥-elim (div<k k>1 (s≤s z≤n ) c (proj1 d)) )
         decl : {m  : ℕ } → 0 < m → m - k < m
         decl {m} 0<m = y-x<y (<-trans a<sa k>1 ) 0<m 
-        ind : (p : ℕ ) → Dec (Dividable k (p - k)) → Dec (Dividable k p)
-        ind p (yes y) = yes (subst (λ g → Dividable k g) (minus+n k≤p ) (proj1 ( div+div y div= ))) where
+        ind : (p : ℕ ) → Dec (Dividable k (p - k) ∧ ( 0 < p - k)) → Dec (Dividable k p ∧ ( 0 < p))
+        ind p (yes y) = yes ⟪ (subst (λ g → Dividable k g) (minus+n k≤p ) (proj1 ( div+div (proj1 y) div= ))) , {!!} ⟫ where
            k≤p :  k < suc p -- k * factor y + 0 ≡ p - k 
            k≤p  = {!!}
         ind p (no n) = no (λ d → n {!!} )