Mercurial > hg > Members > kono > Proof > automaton

changeset 190:4524527b1fe6

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 Tue, 15 Jun 2021 13:44:31 +0900
parents 6945d2aeb86a
children a3a72db6aed3
files automaton-in-agda/src/gcd.agda
diffstat 1 files changed, 25 insertions(+), 22 deletions(-) [+]
line wrap: on
line diff
--- a/automaton-in-agda/src/gcd.agda	Tue Jun 15 08:11:57 2021 +0900
+++ b/automaton-in-agda/src/gcd.agda	Tue Jun 15 13:44:31 2021 +0900
@@ -26,21 +26,20 @@
 
 
 decf : { n k : ℕ } → ( x : Factor k (suc n) ) → Factor k n
-decf {n} {k} record { factor = f ; remain = r ; is-factor = fa } = 
- decf1 {n} {k} f r fa where
-  decf1 : { n k : ℕ } → (f r : ℕ) → (f * k + r ≡ suc n)  → Factor k n 
-  decf1 {n} {zero} (suc f) zero fa  = ⊥-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 ⟩
+decf {n} {zero} record { factor = f ; remain = zero ; is-factor = fa } = ⊥-elim ( nat-≡< fa (
+        begin suc (f * zero + zero) ≡⟨ {!!}  ⟩
+        f * 0 ≡⟨ {!!} ⟩
+        zero ≤⟨ z≤n ⟩
         suc n ∎ )) where open ≤-Reasoning
-  decf1 {n} {suc k} (suc f) zero fa  = 
+decf {n} {suc k} record { factor = (suc f) ; remain = zero ; is-factor = fa } = 
      record { factor = f ; remain = k ; is-factor = ( begin -- fa : suc (k + f * suc k + zero) ≡ suc n
         f * suc k + k ≡⟨ +-comm _ k ⟩
         k + f * suc k ≡⟨ +-comm zero _ ⟩
         (k + f * suc k) + zero  ≡⟨ cong pred fa ⟩
         n ∎ ) }  where open ≡-Reasoning
-  decf1 {n} {k} f (suc r) fa  = 
+decf {n} {k} record { factor = zero ; remain = zero ; is-factor = fa } = {!!}
+decf {n} {k} record { factor = zero ; remain = (suc r) ; is-factor = fa } = {!!}
+decf {n} {k} record { factor = suc f1 ; remain = (suc r) ; is-factor = fa } = 
      record { factor = f ; remain = r ; is-factor = ( begin -- fa : f * k + suc r ≡ suc n
         f * k + r ≡⟨ cong pred ( begin
           suc ( f * k + r ) ≡⟨ +-comm _ r ⟩
@@ -49,27 +48,31 @@
           (suc r ) + f * k ≡⟨ +-comm (suc r) _ ⟩
           f * k + suc r  ≡⟨ fa ⟩
           suc n ∎ ) ⟩ 
-        n ∎ ) }  where open ≡-Reasoning
+        n ∎ ) }  where
+          open ≡-Reasoning
+          f = suc f1
 
 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 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) →  (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} {zero} {i0} (suc f) zero fa i0f div = ⊥-elim (nat-≡< fa (
+decf-step {i} {zero} {i0} record { factor = (suc f) ; remain = zero ; is-factor = fa } 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 i0f div = 
-      record { factor = f ;  is-factor = (
+decf-step {i} {suc k} {i0} record { factor = suc f ;  remain = zero ; is-factor = fa } i0f div = 
+   record { factor = f ;  is-factor = (
         begin f * suc k + 0 ≡⟨ {!!} ⟩
-        i - k ∎ ) }  where open ≡-Reasoning
-   decf-step1 {i} {k} {i0}  f (suc r) fa i0f div = 
-      record { factor = f ;  is-factor = (
+        i - k  ≡⟨ refl  ⟩
+        (i - remain (decf (record { factor = suc f ; remain = zero ; is-factor = fa }))) ∎ ) }  where open ≡-Reasoning
+decf-step {i} {suc k} {i0} record { factor = zero ;  remain = zero ; is-factor = fa } i0f div = {!!}
+decf-step {i} {k} {i0} record { factor = zero ; remain = suc r ; is-factor = fa } i0f div = {!!}
+decf-step {i} {k} {i0} record { factor = suc f1 ; remain = suc r ; is-factor = fa } i0f div = 
+   record { factor = f ;  is-factor = (
         begin f * k + 0 ≡⟨ {!!} ⟩
-         i -r  ∎ ) }  where
-            open ≡-Reasoning
+         (i - remain (decf {i} {k} (record { factor = f ; remain = suc r ; is-factor = fa }))) ∎ ) }  where
+   open ≡-Reasoning
+   f = suc f1
+   df1 : remain (decf {i} {k} (record { factor = f ; remain = suc r ; is-factor = fa })) ≡ r
+   df1 = {!!}
 
 ifk0 : (  i0 k : ℕ ) → (i0f : Factor k i0 )  → ( i0=0 : remain i0f ≡ 0 )  → factor i0f * k + 0 ≡ i0
 ifk0 i0 k i0f i0=0 = begin