Mercurial > hg > Members > kono > Proof > automaton

changeset 153:d78fc1951c26

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 Sat, 02 Jan 2021 03:43:24 +0900
parents f42008080919
children ba7d4cc92e60
files agda/gcd.agda
diffstat 1 files changed, 20 insertions(+), 13 deletions(-) [+]
line wrap: on
line diff
--- a/agda/gcd.agda	Sat Jan 02 01:59:47 2021 +0900
+++ b/agda/gcd.agda	Sat Jan 02 03:43:24 2021 +0900
@@ -163,19 +163,26 @@
 gcd11 i = gcdmm i i 
 
 gcd2 : ( i j : ℕ ) → gcd (i + j) j ≡ gcd i j
-gcd2 zero zero = refl
-gcd2 zero (suc j) = begin
-       gcd (zero + suc j) (suc j) ≡⟨⟩
-       gcd (suc j) (suc j) ≡⟨ gcd11 (suc j) ⟩
-       suc j ≡⟨ sym (gcd20 (suc j)) ⟩
-       gcd (suc j) zero  ≡⟨ gcdsym {suc j} ⟩
-       gcd zero (suc j) ∎ where open ≡-Reasoning
-gcd2 (suc i) zero = begin
-       gcd (suc i + zero) zero ≡⟨ cong (λ k → gcd k zero) (+-comm (suc i) _ ) ⟩
-       gcd (suc i) zero ∎ where open ≡-Reasoning
-gcd2 (suc i) (suc j) = gcd200 (suc i) (suc i) (suc j) (suc j) where
-       gcd200 : (i i0 j j0 : ℕ) → gcd1 (i + j0) (i0 + j0) j j0 ≡ gcd1 i i0 j j0
-       gcd200 i i0 j j0 = {!!}
+gcd2 i j = gcd200 i i j j 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 : ℕ) → gcd1 (i + j) (i0 + j) j j0 ≡ gcd1 i i j0 j0
+       -- gcd200 i i0 zero j0 = subst₂ (λ m k → gcd1 m k zero j0 ≡ gcd1 i i0 zero j0 ) (+-comm zero i) (+-comm zero i0) refl
+       gcd200 i i0 zero j0 = {!!}
+       gcd200 (suc (suc i)) i0 (suc j) (suc j0) = gcd201 (suc (suc i)) i0 j (suc j0) (suc j)
+       gcd200 zero zero (suc zero) j0 = {!!}
+       gcd200 zero zero (suc (suc j)) j0 = {!!}
+       gcd200 zero (suc i0) (suc j) j0 = {!!}
+       gcd200 (suc zero) i0 (suc j) j0 = {!!}
+       gcd200 (suc (suc i)) i0 (suc j) zero = ?
 
 gcd24 : { n m k : ℕ} → n > 1 → m > 1 → k > 1 → gcd n k ≡ k → gcd m k ≡ k → ¬ ( gcd n m ≡ 1 )
 gcd24 {n} {m} {k} 1<n 1<m 1<k gn gm gnm = gcd21 n n m m k k 1<n 1<m 1<k gn gm gnm where