Mercurial > hg > Members > kono > Proof > automaton

changeset 189:6945d2aeb86a

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
expanding record does not work
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 15 Jun 2021 08:11:57 +0900
parents ec896c9e0044
children 4524527b1fe6
files automaton-in-agda/src/gcd.agda
diffstat 1 files changed, 29 insertions(+), 23 deletions(-) [+]
line wrap: on
line diff
--- a/automaton-in-agda/src/gcd.agda	Mon Jun 14 11:12:36 2021 +0900
+++ b/automaton-in-agda/src/gcd.agda	Tue Jun 15 08:11:57 2021 +0900
@@ -26,44 +26,50 @@
 
 
 decf : { n k : ℕ } → ( x : Factor k (suc n) ) → Factor k n
-decf {n} {zero} record { factor = (suc f) ; remain = zero ; is-factor = fa } = ⊥-elim ( nat-≡< fa (
+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 ⟩
         suc n ∎ )) where open ≤-Reasoning
-decf {n} {suc k} record { factor = (suc f) ; remain = zero ; is-factor = fa } = 
+  decf1 {n} {suc k} (suc f) zero 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
-decf {n} {zero} record { factor = f ; remain = (suc r) ; is-factor = fa } = {!!}
-decf {n} {suc k} record { factor = f ; remain = (suc r) ; is-factor = fa } = 
+  decf1 {n} {k} f (suc r) fa  = 
      record { factor = f ; remain = r ; is-factor = ( begin -- fa : f * k + suc r ≡ suc n
-        f * (suc k) + r ≡⟨ cong pred ( begin
-          suc ( f * (suc k) + r ) ≡⟨ +-comm _ r ⟩
-          r + suc (f * (suc k))  ≡⟨ sym (+-assoc r 1 _) ⟩
-          (r + 1) + f * (suc k) ≡⟨ cong (λ t → t + f * (suc k) ) (+-comm r 1) ⟩
-          (suc r ) + f * (suc k) ≡⟨ +-comm (suc r) _ ⟩
-          f * (suc k) + suc r  ≡⟨ fa ⟩
+        f * k + r ≡⟨ cong pred ( begin
+          suc ( f * k + r ) ≡⟨ +-comm _ r ⟩
+          r + suc (f * k)  ≡⟨ sym (+-assoc r 1 _) ⟩
+          (r + 1) + f * k ≡⟨ cong (λ t → t + f * k ) (+-comm r 1) ⟩
+          (suc r ) + f * k ≡⟨ +-comm (suc r) _ ⟩
+          f * k + suc r  ≡⟨ fa ⟩
           suc n ∎ ) ⟩ 
         n ∎ ) }  where open ≡-Reasoning
 
-decf-step : {i k i0 : ℕ } → (if : Factor k (suc i)) → (i0f : Factor k i0) → remain if + suc i ≡ i0 → remain (decf if) + i ≡ i0
-decf-step {i} {zero} {i0} record { factor = (suc f) ; remain = zero ; is-factor = fa } i0f eq = ⊥-elim (nat-≡< fa (
+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 (
         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-step {i} {suc k} {i0} record { factor = suc f ;  remain = zero ; is-factor = fa } i0f eq = begin
-        remain (decf (record { factor = suc f ; remain = zero ; is-factor = fa })) + i ≡⟨ refl ⟩
-        k + i  ≡⟨ {!!} ⟩
-        i0 ∎    where open ≡-Reasoning
-decf-step {i} {zero} {i0} record { factor = f ; remain = suc r ; is-factor = fa } i0f eq = {!!}
-decf-step {i} {suc k} {i0} record { factor = f ; remain = suc r ; is-factor = fa } i0f eq = begin
-        (remain (decf (record { factor = f ; remain = suc r ; is-factor = fa })) + i) ≡⟨ {!!} ⟩
-        suc (r + i) ≡⟨ {!!} ⟩
-        i0 ∎    where open ≡-Reasoning
+   decf-step1 {i} {suc k} {i0} (suc f)  zero 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 = (
+        begin f * k + 0 ≡⟨ {!!} ⟩
+         i -r  ∎ ) }  where
+            open ≡-Reasoning
 
 ifk0 : (  i0 k : ℕ ) → (i0f : Factor k i0 )  → ( i0=0 : remain i0f ≡ 0 )  → factor i0f * k + 0 ≡ i0
 ifk0 i0 k i0f i0=0 = begin
@@ -98,7 +104,7 @@
 
 gcd-gt : ( i i0 j j0 k : ℕ ) → (if : Factor k i) (i0f : Factor k i0 ) (jf : Factor k j ) (j0f : Factor k j0)
    → remain i0f ≡ 0 → remain j0f ≡  0
-   → (remain if + i ) ≡ i0  → (remain jf + j ) ≡ 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 if i0f jf j0f i0=0 j0=0 ir=i0 jr=j0 with <-cmp i0 j0
 ... | tri< a ¬b ¬c = record { factor = factor i0f ; is-factor = ifk0 i0 k i0f i0=0 } 
@@ -120,7 +126,7 @@
 gcd-div : ( i j k : ℕ ) → (if : Factor k i) (jf : Factor k j ) 
    → remain if ≡ 0 → remain jf ≡  0
    → Dividable k ( gcd i  j ) 
-gcd-div i j k if jf i0=0 j0=0 = gcd-gt i i j j k if if jf jf i0=0 j0=0 (gf4 i0=0) (gf4 j0=0) where
+gcd-div i j k if jf i0=0 j0=0 = gcd-gt i i j j k if if jf jf i0=0 j0=0 {!!} {!!} where
     gf4 : {m n : ℕ} → n ≡ 0  →  n + m ≡ m
     gf4 {m} {n} eq = begin
         n + m ≡⟨ cong (λ k → k + m) eq  ⟩