Mercurial > hg > Members > kono > Proof > automaton

changeset 195:373b6e0ec595

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
... remove f>1
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 17 Jun 2021 10:01:26 +0900
parents ee25ec7a27f6
children 6764fe96994f
files automaton-in-agda/src/gcd.agda
diffstat 1 files changed, 31 insertions(+), 36 deletions(-) [+]
line wrap: on
line diff
--- a/automaton-in-agda/src/gcd.agda	Thu Jun 17 00:00:12 2021 +0900
+++ b/automaton-in-agda/src/gcd.agda	Thu Jun 17 10:01:26 2021 +0900
@@ -20,16 +20,15 @@
 record Dividable (n m : ℕ ) : Set where
    field 
       factor : ℕ
-      f>0 : factor > 0
       is-factor : factor * n + 0 ≡ m 
 
 open Factor
 
 DtoF : {n m : ℕ} → Dividable n m → Factor n m
-DtoF {n} {m} record { factor = f ; f>0 = f>0 ; is-factor = fa } = record { factor = f ; remain = 0 ; is-factor = fa }
+DtoF {n} {m} record { factor = f ; is-factor = fa } = record { factor = f ; remain = 0 ; is-factor = fa }
 
-FtoD : {n m : ℕ} → (fc : Factor n m) → factor fc > 0 → remain fc ≡ 0 → Dividable n m 
-FtoD {n} {m} record { factor = f ; remain = r ; is-factor = fa } f>0 refl = record { factor = f ; f>0 = f>0  ; is-factor = fa }
+FtoD : {n m : ℕ} → (fc : Factor n m) → remain fc ≡ 0 → Dividable n m 
+FtoD {n} {m} record { factor = f ; remain = r ; is-factor = fa } refl = record { factor = f ; is-factor = fa }
 
 decf : { n k : ℕ } → ( x : Factor k (suc n) ) → Factor k n
 decf {n} {k} record { factor = f ; remain = r ; is-factor = fa } = 
@@ -63,9 +62,9 @@
         (k + f * suc k) + zero  ≡⟨ cong pred fa ⟩
         n ∎ ) }  where open ≡-Reasoning
 
-decf-step : {i k i0 : ℕ } → k > 1 → (if : Factor k (suc i)) → (i0f : Factor k i0)
-     → Dividable k (suc i - remain if)  → Dividable k (i - remain (decf {i} {k} if))
-decf-step {i} {suc k} {i0} k>1 if i0f div = decf-step1 {i} {suc k} {i0} (factor if) (remain if) (is-factor if) {!!} i0f div where
+decf-eq : {i k : ℕ } → k > 1 → (if : Factor k (suc i)) 
+     → (div : Dividable k (suc i - remain if))  → factor if ≡ Dividable.factor div
+decf-eq {i} {suc k} k>1 if div = if1 where
    if0 : suc (suc i) > remain if
    if0 = begin
         suc (remain if) ≤⟨ s≤s (m≤n+m _ (factor if * suc k)) ⟩
@@ -79,23 +78,27 @@
         (suc i - remain if) + remain if ≡⟨ cong (λ g → g + remain if) (sym (Dividable.is-factor div )) ⟩
         (Dividable.factor div * suc k + 0) + remain if  ≡⟨ cong (λ g → g + remain if) (+-comm _ 0) ⟩
         Dividable.factor div * suc k + remain if ∎  )) ⟩ Dividable.factor div ∎   where open ≡-Reasoning
-   decf-step1 : {i k i0 : ℕ } →  (f r : ℕ) → (fa : f * k + r ≡ suc i) → f > 0  →  (i0f : Factor k i0)
+
+decf-step : {i k : ℕ } → k > 1 → (if : Factor k (suc i)) 
+     → Dividable k (suc i - remain if)  → Dividable k (i - remain (decf {i} {k} if))
+decf-step {i} {suc k}  k>1 if div = decf-step1 {i} {suc k}  (factor if) (remain if) (is-factor if) div where
+   decf-step1 : {i k : ℕ } →  (f r : ℕ) → (fa : f * k + r ≡ suc i) 
         → Dividable k (suc i - r)  → Dividable k (i - remain (decf record {factor = f ; remain = r ; is-factor = fa}))
-   decf-step1 {i} {k} {i0}  f (suc r) fa f>0 i0f div = 
-      record { factor = f ;  f>0 = f>0 ; is-factor = ( --  f * k + suc r ≡ suc i → f * k + suc r ≡ suc i
+   decf-step1 {i} {k}   f (suc r) fa div = 
+      record { factor = f ;  is-factor = ( --  f * k + suc r ≡ suc i → f * k + suc r ≡ suc i
         begin f * k + 0 ≡⟨ +-comm _ 0 ⟩
         f * k ≡⟨ sym ( x=y+z→x-z=y {suc i} {_} {suc r} (sym fa) ) ⟩
         suc i - suc r ≡⟨ refl ⟩
         i - r ≡⟨ refl ⟩
          (i - remain (decf (record { factor = f ; remain = suc r ; is-factor = fa }))) ∎ ) }  where
             open ≡-Reasoning
-   decf-step1 {i} {zero} {i0} (suc f) zero fa f>0 i0f div = ⊥-elim (nat-≡< fa (
+   decf-step1 {i} {zero}  (suc f) zero fa div = ⊥-elim (nat-≡< fa (
         begin suc (suc f * zero + zero) ≡⟨ cong suc (+-comm _ zero)  ⟩
         suc (f * 0) ≡⟨ cong suc (*-comm f zero)  ⟩
         suc zero ≤⟨ s≤s z≤n ⟩
         suc i ∎ )) where open ≤-Reasoning  -- suc (0 + i) ≡ i0
-   decf-step1 {i} {suc k} {i0} (suc f)  zero fa f>0 i0f div = 
-      record { factor = f ;  f>0 = {!!} ; is-factor = ( --  suc (k + f * suc k + zero) ≡ suc i →  f * suc k + 0 ≡ i - k 
+   decf-step1 {i} {suc k}  (suc f)  zero fa div = 
+      record { factor = f ;  is-factor = ( --  suc (k + f * suc k + zero) ≡ suc i →  f * suc k + 0 ≡ i - k 
         begin f * suc k + 0 ≡⟨ sym ( x=y+z→x-z=y {i} {_} {k} (begin
           i ≡⟨ sym (cong pred fa) ⟩
           pred (suc f * suc k + zero) ≡⟨ refl ⟩
@@ -136,36 +139,28 @@
 gcd : ( i j : ℕ ) → ℕ
 gcd i j = gcd1 i i j j 
 
-nfk : {k : ℕ } → k > 1 → ¬ (Dividable k 0)
-nfk {k} k>1 fk1 = ⊥-elim ( nat-≡< (sym (Dividable.is-factor fk1)) ( begin 
-        1 <⟨ k>1 ⟩
-        k ≡⟨ +-comm 0 _ ⟩
-        k + 0 * k ≡⟨ refl ⟩
-        1 * k ≤⟨ *≤ (Dividable.f>0 fk1 ) ⟩
-        Dividable.factor fk1 * k ≡⟨ sym (+-comm _ 0) ⟩
-        Dividable.factor fk1 * k + 0 ∎  )) where open ≤-Reasoning
+¬div : { i k : ℕ } → k > 1 →  Dividable k i → ¬ Dividable k (suc i)
+¬div = {!!}
 
 gcd-gt : ( i i0 j j0 k : ℕ ) → k > 1 → (if : Factor k i) (i0f : Dividable k i0 ) (jf : Factor k j ) (j0f : Dividable k j0)
    → Dividable k (i - remain if) → Dividable k (j - remain jf) 
    → Dividable k ( gcd1 i i0 j j0 ) 
-gcd-gt zero i0 zero j0 k k>1 if i0f jf j0f ir=i0 jr=j0 with <-cmp i0 j0
+gcd-gt zero i0 zero j0 k k>1 if i0f jf j0f i-r j-r with <-cmp i0 j0
 ... | tri< a ¬b ¬c = i0f 
 ... | tri≈ ¬a refl ¬c = i0f
 ... | tri> ¬a ¬b c = j0f
-gcd-gt zero i0 (suc zero) j0 k k>1 if i0f jf j0f ir=i0 jr=j0 =
-     ⊥-elim ( nfk k>1 (subst (λ g → Dividable k g ) (minus<=0 {zero} {remain if} z≤n) ir=i0)) -- can't happen
-gcd-gt zero zero (suc (suc j)) j0 k k>1 if i0f jf j0f ir=i0 jr=j0 = j0f
-gcd-gt zero (suc i0) (suc (suc j)) j0 k k>1 if i0f jf j0f ir=i0 jr=j0 =   
-    gcd-gt i0 (suc i0) (suc j) (suc (suc j))  k k>1 (decf (DtoF i0f)) i0f (decf jf) (FtoD jf {!!} {!!}) {!!} (decf-step k>1 jf {!!} jr=j0 )
-gcd-gt (suc zero) i0 zero j0 k k>1 if i0f jf j0f ir=i0 jr=j0 = 
-     ⊥-elim ( nfk k>1 (subst (λ g → Dividable k g ) (minus<=0 {zero} {remain jf} z≤n) jr=j0)) -- can't happen
-gcd-gt (suc (suc i)) i0 zero zero k k>1 if i0f jf j0f ir=i0 jr=j0 = i0f
-gcd-gt (suc (suc i)) i0 zero (suc j0) k k>1 if i0f jf j0f ir=i0 jr=j0 =
-     gcd-gt (suc i) (suc (suc i)) j0 (suc j0) k k>1 (decf if) {!!} (decf (DtoF j0f)) j0f (decf-step k>1 if jf ir=i0 ) {!!}
-gcd-gt (suc zero) i0 (suc j) j0 k k>1 if i0f jf j0f ir=i0 jr=j0 =  
-     gcd-gt zero i0 j j0 k k>1 (decf if) i0f (decf jf) j0f (decf-step k>1 if jf ir=i0 ) (decf-step k>1 jf if jr=j0 )
-gcd-gt (suc (suc i)) i0 (suc j) j0 k k>1 if i0f jf j0f ir=i0 jr=j0 = 
-     gcd-gt (suc i) i0 j j0 k k>1 (decf if) i0f (decf jf) j0f (decf-step k>1 if jf ir=i0 ) (decf-step k>1 jf if jr=j0 )
+gcd-gt zero i0 (suc zero) j0 k k>1 if i0f jf j0f i-r j-r = {!!} -- can't happen
+gcd-gt zero zero (suc (suc j)) j0 k k>1 if i0f jf j0f i-r j-r = j0f
+gcd-gt zero (suc i0) (suc (suc j)) j0 k k>1 if i0f jf j0f i-r j-r =   
+    gcd-gt i0 (suc i0) (suc j) (suc (suc j))  k k>1 (decf (DtoF i0f)) i0f (decf jf) {!!} {!!} (decf-step k>1 jf j-r )
+gcd-gt (suc zero) i0 zero j0 k k>1 if i0f jf j0f i-r j-r = {!!} -- can't happen
+gcd-gt (suc (suc i)) i0 zero zero k k>1 if i0f jf j0f i-r j-r = i0f
+gcd-gt (suc (suc i)) i0 zero (suc j0) k k>1 if i0f jf j0f i-r j-r = --   
+     gcd-gt (suc i) (suc (suc i)) j0 (suc j0) k k>1 (decf if) {!!} (decf (DtoF j0f)) j0f (decf-step k>1 if i-r ) {!!}
+gcd-gt (suc zero) i0 (suc j) j0 k k>1 if i0f jf j0f i-r j-r =  
+     gcd-gt zero i0 j j0 k k>1 (decf if) i0f (decf jf) j0f (decf-step k>1 if i-r ) (decf-step k>1 jf j-r )
+gcd-gt (suc (suc i)) i0 (suc j) j0 k k>1 if i0f jf j0f i-r j-r = 
+     gcd-gt (suc i) i0 j j0 k k>1 (decf if) i0f (decf jf) j0f (decf-step k>1 if i-r ) (decf-step k>1 jf j-r )
 
 gcd-div : ( i j k : ℕ ) → k > 1 → (if : Dividable k i) (jf : Dividable k j ) 
    → Dividable k ( gcd i  j )