Mercurial > hg > Members > kono > Proof > automaton

changeset 194:ee25ec7a27f6

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 Thu, 17 Jun 2021 00:00:12 +0900
parents 875eb1fa9694
children 373b6e0ec595
files automaton-in-agda/src/gcd.agda
diffstat 1 files changed, 50 insertions(+), 35 deletions(-) [+]
line wrap: on
line diff
--- a/automaton-in-agda/src/gcd.agda	Wed Jun 16 08:36:40 2021 +0900
+++ b/automaton-in-agda/src/gcd.agda	Thu Jun 17 00:00:12 2021 +0900
@@ -20,16 +20,16 @@
 record Dividable (n m : ℕ ) : Set where
    field 
       factor : ℕ
-      f>1 : factor > 1
+      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>1 = f>1 ; is-factor = fa } = record { factor = f ; remain = 0 ; is-factor = fa }
+DtoF {n} {m} record { factor = f ; f>0 = f>0 ; is-factor = fa } = record { factor = f ; remain = 0 ; is-factor = fa }
 
-FtoD : {n m : ℕ} → (fc : Factor n m) → factor fc > 1 → remain fc ≡ 0 → Dividable n m 
-FtoD {n} {m} record { factor = f ; remain = r ; is-factor = fa } f>1 refl = record { factor = f ; f>1 = f>1  ; 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 }
 
 decf : { n k : ℕ } → ( x : Factor k (suc n) ) → Factor k n
 decf {n} {k} record { factor = f ; remain = r ; is-factor = fa } = 
@@ -63,26 +63,39 @@
         (k + f * suc k) + zero  ≡⟨ cong pred fa ⟩
         n ∎ ) }  where open ≡-Reasoning
 
-decf-step : {i k i0 : ℕ } → (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} {k} {i0} if i0f div = 
-  decf-step1 {i} {k} {i0} (factor if) (remain if) (is-factor if) {!!} i0f div where
-   decf-step1 : {i k i0 : ℕ } →  (f r : ℕ) → (fa : f * k + r ≡ suc i) → f > 1  →  (i0f : Factor k i0)
+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
+   if0 : suc (suc i) > remain if
+   if0 = begin
+        suc (remain if) ≤⟨ s≤s (m≤n+m _ (factor if * suc k)) ⟩
+        suc (factor if * suc k + remain if) ≡⟨ cong suc ( is-factor if) ⟩
+        suc (suc i) ∎  where open ≤-Reasoning
+   if1 : factor if ≡ Dividable.factor div
+   if1 = begin
+        factor if  ≡⟨ *-cancelʳ-≡ _ _ {k} ( +-cancelʳ-≡ _ _ ( begin
+        factor if * suc k + remain if ≡⟨ is-factor if ⟩
+        suc i ≡⟨ sym (minus+n {suc i} {remain if} if0) ⟩
+        (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)
         → 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>1 i0f div = 
-      record { factor = f ;  f>1 = {!!} ; is-factor = ( --  f * k + suc r ≡ suc i → f * k + suc r ≡ suc i
+   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
         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>1 i0f div = ⊥-elim (nat-≡< fa (
+   decf-step1 {i} {zero} {i0} (suc f) zero fa f>0 i0f 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>1 i0f div = 
-      record { factor = f ;  f>1 = {!!} ; is-factor = ( --  suc (k + f * suc k + zero) ≡ suc i →  f * suc k + 0 ≡ i - k 
+   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 
         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 ⟩
@@ -123,38 +136,40 @@
 gcd : ( i j : ℕ ) → ℕ
 gcd i j = gcd1 i i j j 
 
-nfk : (k : ℕ ) → k > 1 → ¬ (Dividable k 1)
-nfk k k>1 fk1 = ⊥-elim ( nat-≡< (sym (Dividable.is-factor fk1))  {!!} )
+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
 
 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
-... | tri< a ¬b ¬c = record { factor = Dividable.factor i0f ; f>1 = {!!} ; is-factor = ifk0 i0 k {!!} {!!} } 
-... | tri≈ ¬a refl ¬c = record { factor = Dividable.factor i0f ; f>1 = {!!} ;  is-factor = ifk0 i0 k {!!} {!!} } 
-... | tri> ¬a ¬b c = record { factor = Dividable.factor j0f ; f>1 = {!!} ;  is-factor = ifk0 j0 k {!!} {!!} } 
-gcd-gt zero i0 (suc zero) j0 k k>1 if i0f jf j0f ir=i0 jr=j0 = {!!} -- can't happen
-gcd-gt zero zero (suc (suc j)) j0 k k>1 if i0f jf j0f ir=i0 jr=j0 = record { factor = Dividable.factor j0f ; f>1 = {!!} ; is-factor = ifk0 j0 k {!!} {!!} } 
-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 {!!}) i0f (decf {!!}) {!!} {!!} (decf-step jf {!!} jr=j0 )
-gcd-gt (suc zero) i0 zero j0 k k>1 if i0f jf j0f ir=i0 jr=j0 = {!!} -- can't happen
-gcd-gt (suc (suc i)) i0 zero zero k k>1 if i0f jf j0f ir=i0 jr=j0 = record { factor = Dividable.factor i0f ; f>1 = {!!} ; is-factor = ifk0 i0 k {!!} {!!} } 
+... | 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 {!!}) j0f (decf-step if {!!} ir=i0 ) {!!}
+     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 if {!!} ir=i0 ) (decf-step jf {!!} 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 if {!!} ir=i0 ) (decf-step jf {!!} 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-div : ( i j k : ℕ ) → k > 1 → (if : Factor k i) (jf : Factor k j ) 
-   → remain if ≡ 0 → remain jf ≡  0
+gcd-div : ( i j k : ℕ ) → k > 1 → (if : Dividable k i) (jf : Dividable k j ) 
    → Dividable k ( gcd i  j ) 
-gcd-div i j k k>1 if jf i0=0 j0=0 = gcd-gt i i j j k k>1 if {!!} jf {!!} {!!} {!!} where
-    gf4 : {m n : ℕ} → n ≡ 0  →  n + m ≡ m
-    gf4 {m} {n} eq = begin
-        n + m ≡⟨ cong (λ k → k + m) eq  ⟩
-        0 + m ≡⟨  refl  ⟩
-        m ∎  where open ≡-Reasoning
+gcd-div i j k k>1 if jf = gcd-gt i i j j k k>1 (DtoF if) if (DtoF jf) jf {!!} {!!} 
 
 
 -- gcd26 : { n m : ℕ} → n > 1 → m > 1 → n - m > 0 → gcd n m ≡ gcd (n - m) m