Mercurial > hg > Members > kono > Proof > automaton

changeset 212:cb36711e8b06

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, 21 Jun 2021 00:43:09 +0900
parents 28d4fb7b576f
children 9aec75fa796c
files automaton-in-agda/src/gcd.agda
diffstat 1 files changed, 60 insertions(+), 47 deletions(-) [+]
line wrap: on
line diff
--- a/automaton-in-agda/src/gcd.agda	Sun Jun 20 23:51:35 2021 +0900
+++ b/automaton-in-agda/src/gcd.agda	Mon Jun 21 00:43:09 2021 +0900
@@ -138,6 +138,47 @@
 gcd11 : ( i  : ℕ ) → gcd i i ≡ i
 gcd11 i = gcdmm i i 
 
+
+gcd203 : (i : ℕ) → gcd1 (suc i) (suc i) i i ≡ 1
+gcd203 zero = refl
+gcd203 (suc i) = gcd205 (suc i) where
+   gcd205 : (j : ℕ) → gcd1 (suc j) (suc (suc i)) j (suc i) ≡ 1
+   gcd205 zero = refl
+   gcd205 (suc j) = subst (λ k → k ≡ 1) (gcd22 (suc j)  (suc (suc i)) j (suc i)) (gcd205 j)
+
+gcd204 : (i : ℕ) → gcd1 1 1 i i ≡ 1
+gcd204 zero = refl
+gcd204 (suc zero) = refl
+gcd204 (suc (suc zero)) = refl
+gcd204 (suc (suc (suc i))) = gcd204 (suc (suc i)) 
+
+gcd+j : ( i j : ℕ ) → gcd (i + j) j ≡ gcd i j
+gcd+j i j = gcd200 i i j j refl refl where
+       gcd202 : (i j1 : ℕ) → (i + suc j1) ≡ suc (i + j1)
+       gcd202 zero j1 = refl
+       gcd202 (suc i) j1 = cong suc (gcd202 i j1)
+       gcd201 : (i i0 j j0 j1 : ℕ) → gcd1 (i + j1) (i0 + suc j) j1 j0 ≡ gcd1 i (i0 + suc j) zero j0
+       gcd201 i i0 j j0 zero = subst (λ k → gcd1 k (i0 + suc j) zero j0 ≡ gcd1 i (i0 + suc j) zero j0 ) (+-comm zero i) refl
+       gcd201 i i0 j j0 (suc j1) = begin
+          gcd1 (i + suc j1)   (i0 + suc j) (suc j1) j0 ≡⟨ cong (λ k → gcd1 k (i0 + suc j) (suc j1) j0 ) (gcd202 i j1) ⟩
+          gcd1 (suc (i + j1)) (i0 + suc j) (suc j1) j0 ≡⟨ gcd22 (i + j1) (i0 + suc j) j1 j0 ⟩
+          gcd1 (i + j1) (i0 + suc j) j1 j0 ≡⟨ gcd201 i i0 j j0 j1 ⟩
+          gcd1 i (i0 + suc j) zero j0 ∎ where open ≡-Reasoning
+       gcd200 : (i i0 j j0 : ℕ) → i ≡ i0 → j ≡ j0 → gcd1 (i + j) (i0 + j) j j0 ≡ gcd1 i i j0 j0
+       gcd200 i .i zero .0 refl refl = subst (λ k → gcd1 k k zero zero ≡ gcd1 i i zero zero ) (+-comm zero i) refl 
+       gcd200 (suc (suc i)) i0 (suc j) (suc j0) i=i0 j=j0 = gcd201 (suc (suc i)) i0 j (suc j0) (suc j)
+       gcd200 zero zero (suc zero) .1 i=i0 refl = refl
+       gcd200 zero zero (suc (suc j)) .(suc (suc j)) i=i0 refl = begin
+          gcd1 (zero + suc (suc j)) (zero + suc (suc j)) (suc (suc j)) (suc (suc j)) ≡⟨ gcdmm (suc (suc j)) (suc (suc j)) ⟩
+          suc (suc j) ≡⟨ sym (gcd20 (suc (suc j))) ⟩
+          gcd1 zero zero (suc (suc j)) (suc (suc j)) ∎ where open ≡-Reasoning
+       gcd200 zero (suc i0) (suc j) .(suc j) () refl
+       gcd200 (suc zero) .1 (suc j) .(suc j) refl refl = begin
+          gcd1 (1 + suc j) (1 + suc j) (suc j) (suc j) ≡⟨ gcd203 (suc j) ⟩
+          1 ≡⟨ sym ( gcd204 (suc j)) ⟩
+          gcd1 1 1 (suc j) (suc j) ∎ where open ≡-Reasoning
+       gcd200 (suc (suc i)) i0 (suc j) zero i=i0 ()
+
 div1 : { k : ℕ } → k > 1 →  ¬  Dividable k 1
 div1 {k} k>1 record { factor = (suc f) ; is-factor = fa } = ⊥-elim ( nat-≡< (sym fa) ( begin
     2 ≤⟨ k>1 ⟩
@@ -228,7 +269,7 @@
 gcd-div i j k k>1 if jf = gcd-gt i i j j k k>1 (DtoF if) if (DtoF jf) jf (div-div k>1 if jf)
 
 gcd-divable : ( i j  : ℕ )
-      → Dividable ( gcd i j ) i ∧ Dividable ( gcd i  j ) j
+      → Dividable ( gcd i j ) i ∧ Dividable ( gcd i j ) j
 gcd-divable i j  = f-induction {_} {_} {ℕ ∧ ℕ}
    {λ p  → Dividable ( gcd (proj1 p) (proj2 p) ) (proj1 p) ∧ Dividable ( gcd (proj1 p)  (proj2 p) ) (proj2 p)} F I ⟪ i , j ⟫ where
         F : ℕ ∧ ℕ → ℕ
@@ -311,15 +352,28 @@
              → Dividable (gcd i j) i ∧ Dividable (gcd i j) j
         ind zero zero prev = ind0 where
            ind0 : Dividable (gcd zero zero) zero ∧ Dividable (gcd zero zero) zero
-           ind0 = {!!}
+           ind0 = ⟪ div0 , div0 ⟫
         ind zero (suc j) prev = ind1 where
            ind1 : Dividable (gcd zero (suc j)) zero ∧ Dividable (gcd zero (suc j)) (suc j)
-           ind1 = {!!}
+           ind1 = ⟪ div0 , subst (λ k → Dividable k (suc j)) (sym (trans (gcdsym {zero} {suc j}) (gcd20 (suc j)))) div=  ⟫
         ind (suc i) zero prev = ind2 where
            ind2 : Dividable (gcd (suc i) zero) (suc i) ∧ Dividable (gcd (suc i) zero) zero
-           ind2 = {!!}
+           ind2 = ⟪  subst (λ k → Dividable k (suc i)) (sym (trans refl (gcd20 (suc i)))) div= , div0 ⟫
         ind (suc i) (suc j) prev with <-cmp i j
-        ... | tri< a ¬b ¬c = {!!}
+        ... | tri< a ¬b ¬c = ⟪ ind3 (suc i) (proj1 prev)   , ind4 (proj2 prev) ⟫ where
+            ind3 : (s : ℕ ) → Dividable (gcd1 (suc i) (suc i) (j - i) (j - i)) s
+                 → Dividable (gcd1 (suc i) (suc i) (suc j) (suc j)) s 
+            ind3 s prev = 
+               subst (λ k → Dividable k s) ( begin
+                 gcd (suc i) (j - i)  ≡⟨ gcdsym {suc i} {j - i} ⟩
+                 gcd (j - i ) (suc i)   ≡⟨ sym (gcd+j (j - i) (suc i)) ⟩
+                 gcd ((j - i) + suc i) (suc i)  ≡⟨ cong (λ k → gcd k (suc i)) ( begin
+                  (suc j - suc i) + suc i ≡⟨ minus+n {suc j} {suc i} (<-trans ( s≤s a) a<sa ) ⟩ -- i ≤ n →  suc (suc i) ≤ suc (suc (suc n)) 
+                  suc j ∎ ) ⟩
+                 gcd (suc j) (suc i)  ≡⟨ gcdsym {suc j} {suc i} ⟩
+                 gcd (suc i) (suc j)  ∎ ) prev where open ≡-Reasoning 
+            ind4 : Dividable (gcd (suc i) (j - i)) (j - i) → Dividable (gcd (suc i) (suc j)) (suc j)
+            ind4 = {!!}
         ... | tri≈ ¬a b ¬c = {!!}
         ... | tri> ¬a ¬b c = {!!}
         --ind3 where
@@ -335,47 +389,6 @@
           } 
 
 
-gcd203 : (i : ℕ) → gcd1 (suc i) (suc i) i i ≡ 1
-gcd203 zero = refl
-gcd203 (suc i) = gcd205 (suc i) where
-   gcd205 : (j : ℕ) → gcd1 (suc j) (suc (suc i)) j (suc i) ≡ 1
-   gcd205 zero = refl
-   gcd205 (suc j) = subst (λ k → k ≡ 1) (gcd22 (suc j)  (suc (suc i)) j (suc i)) (gcd205 j)
-
-gcd204 : (i : ℕ) → gcd1 1 1 i i ≡ 1
-gcd204 zero = refl
-gcd204 (suc zero) = refl
-gcd204 (suc (suc zero)) = refl
-gcd204 (suc (suc (suc i))) = gcd204 (suc (suc i)) 
-
-gcd2 : ( i j : ℕ ) → gcd (i + j) j ≡ gcd i j
-gcd2 i j = gcd200 i i j j refl refl where
-       gcd202 : (i j1 : ℕ) → (i + suc j1) ≡ suc (i + j1)
-       gcd202 zero j1 = refl
-       gcd202 (suc i) j1 = cong suc (gcd202 i j1)
-       gcd201 : (i i0 j j0 j1 : ℕ) → gcd1 (i + j1) (i0 + suc j) j1 j0 ≡ gcd1 i (i0 + suc j) zero j0
-       gcd201 i i0 j j0 zero = subst (λ k → gcd1 k (i0 + suc j) zero j0 ≡ gcd1 i (i0 + suc j) zero j0 ) (+-comm zero i) refl
-       gcd201 i i0 j j0 (suc j1) = begin
-          gcd1 (i + suc j1)   (i0 + suc j) (suc j1) j0 ≡⟨ cong (λ k → gcd1 k (i0 + suc j) (suc j1) j0 ) (gcd202 i j1) ⟩
-          gcd1 (suc (i + j1)) (i0 + suc j) (suc j1) j0 ≡⟨ gcd22 (i + j1) (i0 + suc j) j1 j0 ⟩
-          gcd1 (i + j1) (i0 + suc j) j1 j0 ≡⟨ gcd201 i i0 j j0 j1 ⟩
-          gcd1 i (i0 + suc j) zero j0 ∎ where open ≡-Reasoning
-       gcd200 : (i i0 j j0 : ℕ) → i ≡ i0 → j ≡ j0 → gcd1 (i + j) (i0 + j) j j0 ≡ gcd1 i i j0 j0
-       gcd200 i .i zero .0 refl refl = subst (λ k → gcd1 k k zero zero ≡ gcd1 i i zero zero ) (+-comm zero i) refl 
-       gcd200 (suc (suc i)) i0 (suc j) (suc j0) i=i0 j=j0 = gcd201 (suc (suc i)) i0 j (suc j0) (suc j)
-       gcd200 zero zero (suc zero) .1 i=i0 refl = refl
-       gcd200 zero zero (suc (suc j)) .(suc (suc j)) i=i0 refl = begin
-          gcd1 (zero + suc (suc j)) (zero + suc (suc j)) (suc (suc j)) (suc (suc j)) ≡⟨ gcdmm (suc (suc j)) (suc (suc j)) ⟩
-          suc (suc j) ≡⟨ sym (gcd20 (suc (suc j))) ⟩
-          gcd1 zero zero (suc (suc j)) (suc (suc j)) ∎ where open ≡-Reasoning
-       gcd200 zero (suc i0) (suc j) .(suc j) () refl
-       gcd200 (suc zero) .1 (suc j) .(suc j) refl refl = begin
-          gcd1 (1 + suc j) (1 + suc j) (suc j) (suc j) ≡⟨ gcd203 (suc j) ⟩
-          1 ≡⟨ sym ( gcd204 (suc j)) ⟩
-          gcd1 1 1 (suc j) (suc j) ∎ where open ≡-Reasoning
-       gcd200 (suc (suc i)) i0 (suc j) zero i=i0 ()
-
-
 gcdmul+1 : ( m n : ℕ ) → gcd (m * n + 1) n ≡ 1
 gcdmul+1 zero n = gcd204 n
 gcdmul+1 (suc m) n = begin
@@ -387,7 +400,7 @@
          m * n + (1 + n)  ≡⟨ sym ( +-assoc (m * n) _ _ ) ⟩
          m * n + 1 + n ∎ 
        ) ⟩
-      gcd (m * n + 1 + n) n ≡⟨ gcd2 (m * n + 1) n ⟩
+      gcd (m * n + 1 + n) n ≡⟨ gcd+j (m * n + 1) n ⟩
       gcd (m * n + 1) n ≡⟨ gcdmul+1 m n ⟩
       1 ∎ where open ≡-Reasoning