Mercurial > hg > Members > kono > Proof > automaton

changeset 187:1402c5b17160

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 Mon, 14 Jun 2021 09:06:20 +0900
parents 08f4ec41ea93
children ec896c9e0044
files automaton-in-agda/src/gcd.agda automaton-in-agda/src/root2.agda
diffstat 2 files changed, 30 insertions(+), 26 deletions(-) [+]
line wrap: on
line diff
--- a/automaton-in-agda/src/gcd.agda	Mon Jun 14 02:17:58 2021 +0900
+++ b/automaton-in-agda/src/gcd.agda	Mon Jun 14 09:06:20 2021 +0900
@@ -24,22 +24,36 @@
 
 open Factor
 
-open ≡-Reasoning
 
 decf : { n k : ℕ } → ( x : Factor k (suc n) ) → Factor k n
-decf {n} {k} x with remain x | inspect remain x
-... | zero | record { eq = e } = record { factor = factor x ; remain = k ; is-factor = {!!} } where
-   d0 : factor x * k + remain x ≡ suc n
-   d0 = is-factor x
-   d1 : factor x * k + k ≡ n
-   d1 = {!!}
-... | suc r | record { eq = e } = record { factor = factor x ; remain = r ; is-factor = {!!} }
+decf {n} {zero} record { factor = (suc f) ; remain = zero ; is-factor = 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 } = 
+     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} {k} record { factor = f ; 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 ⟩
+          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
 
 ifk0 : (  i0 k : ℕ ) → (i0f : Factor k i0 )  → ( i0=0 : remain i0f ≡ 0 )  → factor i0f * k + 0 ≡ i0
 ifk0 i0 k i0f i0=0 = begin
    factor i0f * k + 0  ≡⟨ cong (λ m → factor i0f * k + m) (sym i0=0)  ⟩
    factor i0f * k + remain i0f  ≡⟨ is-factor i0f ⟩
    i0 ∎ 
+         where open ≡-Reasoning
 
 ifzero : {k : ℕ } → (jf :  Factor k zero ) →  remain jf ≡ 0
 ifzero {k} record { factor = zero ; remain = zero ; is-factor = is-factor } = refl
@@ -76,12 +90,12 @@
 gcd-gt zero i0 (suc zero) j0 k if i0f jf j0f i0=0 j0=0 ir=i0 jr=j0 = {!!} -- can't happen
 gcd-gt zero zero (suc (suc j)) j0 k if i0f jf j0f i0=0 j0=0 ir=i0 jr=j0 = record { factor = factor j0f ; is-factor = ifk0 j0 k j0f j0=0 } 
 gcd-gt zero (suc i0) (suc (suc j)) j0 k if i0f jf j0f i0=0 j0=0 ir=i0 jr=j0 =  
-    gcd-gt i0 (suc i0) (suc j) (suc (suc j))  k (decf i0f) {!!} {!!} 
+    gcd-gt i0 (suc i0) (suc j) (suc (suc j))  k (decf i0f) i0f (decf jf)
        record { factor = factor jf ; remain = remain jf ; is-factor = {!!} } i0=0 {!!} {!!} {!!}  
 gcd-gt (suc zero) i0 zero j0 k if i0f jf j0f i0=0 j0=0 ir=i0 jr=j0 = {!!} -- can't happen
-gcd-gt (suc (suc i)) i0 zero zero k if i0f jf j0f i0=0 j0=0 ir=i0 jr=j0 = {!!}
+gcd-gt (suc (suc i)) i0 zero zero k if i0f jf j0f i0=0 j0=0 ir=i0 jr=j0 = record { factor = factor i0f ; is-factor = ifk0 i0 k i0f i0=0 } 
 gcd-gt (suc (suc i)) i0 zero (suc j0) k if i0f jf j0f i0=0 j0=0 ir=i0 jr=j0 =
-     gcd-gt (suc i) (suc (suc i)) j0 (suc j0) k (decf if) {!!} (decf {!!}) j0f j0=0 {!!} {!!} {!!} 
+     gcd-gt (suc i) (suc (suc i)) j0 (suc j0) k (decf if) if (decf j0f) j0f {!!} {!!} {!!} {!!} 
 gcd-gt (suc zero) i0 (suc j) j0 k if i0f jf j0f i0=0 j0=0 ir=i0 jr=j0 = 
      gcd-gt zero i0 j j0 k (decf if) i0f (decf jf) j0f i0=0 j0=0 {!!} {!!}
 gcd-gt (suc (suc i)) i0 (suc j) j0 k if i0f jf j0f i0=0 j0=0 ir=i0 jr=j0 = 
--- a/automaton-in-agda/src/root2.agda	Mon Jun 14 02:17:58 2021 +0900
+++ b/automaton-in-agda/src/root2.agda	Mon Jun 14 09:06:20 2021 +0900
@@ -17,24 +17,14 @@
     i j : ℕ
     coprime : gcd i j ≡ 1
 
-even→gcd=2 : {n : ℕ} → even n → n > 0 → gcd n 2 ≡ 2
-even→gcd=2 {suc (suc zero)} en (s≤s z≤n) = refl
-even→gcd=2 {suc (suc (suc (suc n)))} en (s≤s z≤n) = begin
+even→gcd=2 : {n : ℕ} → even n → gcd n 2 ≡ 2
+even→gcd=2 {zero} en  = refl
+even→gcd=2 {suc (suc zero)} en  = refl
+even→gcd=2 {suc (suc (suc (suc n)))} en  = begin
        gcd (suc (suc (suc (suc n)))) 2 ≡⟨⟩
-       gcd (suc (suc n)) 2 ≡⟨ even→gcd=2 {suc (suc n)} en (s≤s z≤n) ⟩
+       gcd (suc (suc n)) 2 ≡⟨ even→gcd=2 {suc (suc n)} en  ⟩
        2 ∎ where open ≡-Reasoning
 
-even→gcd : (n m : ℕ) → even n → even m → even (gcd n m)
-even→gcd zero zero en em = tt
-even→gcd zero (suc (suc m)) en em = em
-even→gcd (suc (suc n)) zero en em = en
-even→gcd (suc (suc n)) (suc (suc m)) en em = ee2 n n (suc (suc m)) (suc (suc m))  refl refl
-       (subst (λ k → even k) (gcdsym {suc (suc m)} {n})  (ee2 m m n n refl refl (subst (λ k → even k) (gcdsym {n} {m}) ee1))) where
-   ee1 : even (gcd n m)
-   ee1 = even→gcd n m en em
-   ee2 : (i i0 j j0 : ℕ) → i ≡ i0 → j ≡ j0 → even (gcd1 i i j0 j0)  → even (gcd1 (suc (suc i)) (suc (suc i)) j0 j0) 
-   ee2 i i0 j j0 i=i0 j=j0 e = {!!}
-
 even^2 : {n : ℕ} → even ( n * n ) → even n
 even^2 {n} en with even? n
 ... | yes y = y