Mercurial > hg > Members > kono > Proof > automaton
changeset 190:4524527b1fe6
...
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Tue, 15 Jun 2021 13:44:31 +0900 (2021-06-15) |
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