Mercurial > hg > Members > kono > Proof > automaton

changeset 148:8207b69c500b

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 Thu, 31 Dec 2020 15:20:14 +0900
parents 0d8a834c9c50
children d3a8572ced9c
files agda/gcd.agda agda/root2.agda
diffstat 2 files changed, 236 insertions(+), 192 deletions(-) [+]
line wrap: on
line diff
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/agda/gcd.agda	Thu Dec 31 15:20:14 2020 +0900
@@ -0,0 +1,235 @@
+{-# OPTIONS --allow-unsolved-metas #-}
+module gcd where
+
+open import Data.Nat 
+open import Data.Nat.Properties
+open import Data.Empty
+open import Data.Unit using (⊤ ; tt)
+open import Relation.Nullary
+open import Relation.Binary.PropositionalEquality
+open import Relation.Binary.Definitions
+
+even : (n : ℕ ) → Set
+even zero = ⊤
+even (suc zero) = ⊥
+even (suc (suc n)) = even n
+
+even? : (n : ℕ ) → Dec ( even n )
+even? zero = yes tt
+even? (suc zero) = no (λ ())
+even? (suc (suc n)) = even? n
+
+n+even : {n m : ℕ } → even n → even m  → even ( n + m )
+n+even {zero} {zero} tt tt = tt
+n+even {zero} {suc m} tt em = em
+n+even {suc (suc n)} {m} en em = n+even {n} {m} en em
+
+n*even : {m n : ℕ } → even n → even ( m * n )
+n*even {zero} {n} en = tt
+n*even {suc m} {n} en = n+even {n} {m * n} en (n*even {m} {n} en) 
+
+even*n : {n m : ℕ } → even n → even ( n * m )
+even*n {n} {m} en = subst even (*-comm m n) (n*even {m} {n} en)
+
+gcd1 : ( i i0 j j0 : ℕ ) → ℕ
+gcd1 zero i0 zero j0 with <-cmp i0 j0
+... | tri< a ¬b ¬c = j0
+... | tri≈ ¬a refl ¬c = i0
+... | tri> ¬a ¬b c = i0
+gcd1 zero i0 (suc zero) j0 = 1
+gcd1 zero zero (suc (suc j)) j0 = j0
+gcd1 zero (suc i0) (suc (suc j)) j0 = gcd1 i0 (suc i0) (suc j) (suc (suc j))
+gcd1 (suc zero) i0 zero j0 = 1
+gcd1 (suc (suc i)) i0 zero zero = i0
+gcd1 (suc (suc i)) i0 zero (suc j0) = gcd1 (suc i) (suc (suc i))  j0 (suc j0)
+gcd1 (suc i) i0 (suc j) j0 = gcd1 i i0 j j0  
+
+gcd : ( i j : ℕ ) → ℕ
+gcd i j = gcd1 i i j j 
+
+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
+       gcd (suc (suc (suc (suc n)))) 2
+    ≡⟨⟩
+       gcd (suc (suc n)) 2
+    ≡⟨ even→gcd=2 {suc (suc n)} en (s≤s z≤n) ⟩
+       2
+    ∎ where open ≡-Reasoning
+
+open import nat
+
+-- gcd26 : { n m : ℕ} → n > 1 → m > 1 → n - m > 0 → gcd n m ≡ gcd (n - m) m
+-- gcd27 : { n m : ℕ} → n > 1 → m > 1 → n - m > 0 → gcd n k ≡ k → k ≤ n
+
+gcd22 : ( i i0 o o0 : ℕ ) → gcd1 (suc i) i0 (suc o) o0 ≡ gcd1 i i0 o o0
+gcd22 zero i0 zero o0 = refl
+gcd22 zero i0 (suc o) o0 = refl
+gcd22 (suc i) i0 zero o0 = refl
+gcd22 (suc i) i0 (suc o) o0 = refl 
+
+-- gcd27 : ( i i0 : ℕ ) → gcd1 i i0 0 1 ≤ 1
+-- gcd27 zero zero = ≤-refl
+-- gcd27 zero (suc i0) = {!!}
+-- gcd27 (suc i) zero = {!!}
+-- gcd27 (suc i) (suc i0) = {!!}
+
+gcd-kk : ( i : ℕ ) → gcd1 i i i i ≡ i
+gcd-kk zero = refl
+gcd-kk (suc i) = gcd-kk1 i i i i refl refl where
+   gcd-kk1 : (i i0 j j0 : ℕ) → i ≡ j → i0 ≡ j0 →  gcd1 (suc i) (suc i0) (suc j) (suc j0) ≡ suc i0
+   gcd-kk1 zero i0 zero j0 i=j i0=j0 with <-cmp (suc i0) (suc j0)
+   ... | tri< a ¬b ¬c = ⊥-elim (¬b (cong suc i0=j0))
+   ... | tri≈ ¬a refl ¬c = refl
+   ... | tri> ¬a ¬b c = ⊥-elim (¬b (cong suc i0=j0))
+   gcd-kk1 (suc i) i0 (suc j) j0 refl i0=j0 = 
+        gcd-kk1 i i0 j j0 refl i0=j0 
+
+gcd26 : (n m i : ℕ) → 1 < n → 1 < m  → gcd n i ≡ m → ¬ ( gcd n m ≡ 1 )
+gcd26 n m i 1<n 1<m gi g1 = gcd261 n n m m i i 1<n 1<m gi g1 where
+    gcd261 : (n n0 m m0 i i0 : ℕ) → 1 < n → 1 < m0  → gcd1 n n0 i i0 ≡ m0 → ¬ ( gcd1 n n0 m m0 ≡ 1 )
+    gcd261 zero n0 m m0 i i0 () 1<m gi g1
+    gcd261 (suc n) n0 m m0 zero i0 1<n 1<m gi g1 = {!!}
+    gcd261 (suc n) n0 zero m0 (suc i) i0 1<n 1<m gi g1 = {!!}
+    -- 1<n      : 1 < suc n
+    -- 1<m      : 1 < m0
+    -- gi       : gcd1 (suc n) n0 (suc i) i0 ≡ m0 -- gi       : gcd1 n n0 i i0 ≡ m0
+    -- g1       : gcd1 (suc n) n0 (suc m) m0 ≡ 1  -- g1       : gcd1 n n0 m m0 ≡ 1
+    gcd261 (suc zero) n0 (suc m) m0 (suc i) i0 1<n 1<m gi g1 = ⊥-elim ( nat-<≡ 1<n  )
+    gcd261 (suc (suc zero)) n0 (suc m) m0 (suc i) i0 1<n 1<m gi g1 = {!!}
+    gcd261 (suc (suc (suc n))) n0 (suc m) m0 (suc i) i0 1<n 1<m gi g1 = 
+        gcd261 (suc (suc n)) n0 m m0 i i0 (s≤s (s≤s z≤n)) 1<m gi g1
+
+gcdsym2 : (i j : ℕ) → gcd1 zero i zero j ≡ gcd1 zero j zero i
+gcdsym2 i j with <-cmp i j | <-cmp j i
+... | tri< a ¬b ¬c | tri< a₁ ¬b₁ ¬c₁ = ⊥-elim (nat-<> a a₁) 
+... | tri< a ¬b ¬c | tri≈ ¬a b ¬c₁ = ⊥-elim (nat-≡< (sym b) a) 
+... | tri< a ¬b ¬c | tri> ¬a ¬b₁ c = refl
+... | tri≈ ¬a b ¬c | tri< a ¬b ¬c₁ = ⊥-elim (nat-≡< (sym b) a) 
+... | tri≈ ¬a refl ¬c | tri≈ ¬a₁ refl ¬c₁ = refl
+... | tri≈ ¬a b ¬c | tri> ¬a₁ ¬b c = ⊥-elim (nat-≡< b c) 
+... | tri> ¬a ¬b c | tri< a ¬b₁ ¬c = refl
+... | tri> ¬a ¬b c | tri≈ ¬a₁ b ¬c = ⊥-elim (nat-≡< b c) 
+... | tri> ¬a ¬b c | tri> ¬a₁ ¬b₁ c₁ = ⊥-elim (nat-<> c c₁) 
+gcdsym1 : ( i i0 j j0 : ℕ ) → gcd1 i i0 j j0 ≡ gcd1 j j0 i i0
+gcdsym1 zero zero zero zero = refl
+gcdsym1 zero zero zero (suc j0) = refl
+gcdsym1 zero (suc i0) zero zero = refl
+gcdsym1 zero (suc i0) zero (suc j0) = gcdsym2 (suc i0) (suc j0)
+gcdsym1 zero zero (suc zero) j0 = refl
+gcdsym1 zero zero (suc (suc j)) j0 = refl
+gcdsym1 zero (suc i0) (suc zero) j0 = refl
+gcdsym1 zero (suc i0) (suc (suc j)) j0 = gcdsym1 i0 (suc i0) (suc j) (suc (suc j))
+gcdsym1 (suc zero) i0 zero j0 = refl
+gcdsym1 (suc (suc i)) i0 zero zero = refl
+gcdsym1 (suc (suc i)) i0 zero (suc j0) = gcdsym1 (suc i) (suc (suc i))j0 (suc j0) 
+gcdsym1 (suc i) i0 (suc j) j0 = subst₂ (λ j k → j ≡ k ) (sym (gcd22 i _ _ _)) (sym (gcd22 j _ _ _)) (gcdsym1 i i0 j j0 )
+
+gcdsym : { n m : ℕ} → gcd n m ≡ gcd m n
+gcdsym {n} {m} = gcdsym1 n n m m 
+
+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
+   gcd23 : {i0 j0 : ℕ } → 1 < i0  → 1 < j0 → 1 < gcd1 zero i0 zero j0
+   gcd23 {i0} {j0} 1<i 1<j with <-cmp i0 j0
+   ... | tri< a ¬b ¬c = 1<j
+   ... | tri≈ ¬a refl ¬c = 1<i
+   ... | tri> ¬a ¬b c = 1<i
+   1<ss : {j : ℕ} → 1 < suc (suc j)
+   1<ss = s≤s (s≤s z≤n)
+   gcd21 : ( i i0 j j0 o o0 : ℕ ) → 1 < i0 → 1 < j0 → 1 < o0 →  gcd1 i i0 o o0 ≡ k → gcd1 j j0 o o0 ≡ k → gcd1 i i0 j j0 ≡ 1 → ⊥
+   gcd21 zero i0 zero j0 o o0 1<i 1<j 1<o refl gm gnm = nat-≡< (sym gnm) (gcd23 1<i 1<j)
+   gcd21 zero i0 (suc j) j0 zero o0 1<i 1<j 1<o refl gm gnm = gcd25 i0 o0 j j0 1<o 1<i 1<k gm (subst (λ k → k ≡ 1) (gcdsym1 zero _ (suc j) _) gnm)  where
+      -- gcd1 (suc j) (suc (suc j)) (suc o0) (suc (suc o0)) ≡ suc (suc i0) , gcd1 (suc j) (suc (suc j)) (suc i0) (suc (suc i0)) ≡ 1
+      gcd25 : (i0 o0 j j0 : ℕ) → 1 < o0 → 1 < i0
+            → 1 < gcd1 zero i0 zero o0 
+            → ( gm : gcd1 (suc j) j0 zero o0 ≡ gcd1 zero i0 zero o0 ) → (gnm : gcd1 (suc j) j0 zero i0 ≡ 1) → ⊥
+      gcd25 i0 o0 zero j0 1<o 1<i 1<k gm refl with <-cmp i0 o0
+      ... | tri< a ¬b ¬c    = ⊥-elim ( nat-≡< gm 1<o )
+      ... | tri≈ ¬a refl ¬c = ⊥-elim ( nat-≡< gm 1<o )
+      ... | tri> ¬a ¬b c    = ⊥-elim ( nat-≡< gm 1<i )
+      -- gm       : gcd1 (suc j) (suc (suc j)) (suc o0) (suc (suc o0)) ≡ (gcd1 zero (suc i0) zero (suc (suc o0))
+      --            gcd1 j       (suc (suc j))       o0 (suc (suc o0)) 
+      -- gnm      : gcd1 (suc j) (suc (suc j)) i0 (suc i0) ≡ 1
+      gcd25 i0       (suc zero)     (suc j) j0 1<o 1<i 1<k gm gnm = {!!} -- ⊥-elim ( nat-≤> (subst (λ k → k ≤ 1 ) gm (gcd27 (suc j) (suc (suc j)))) 1<k )
+      gcd25 (suc zero) (suc (suc o0)) (suc j) j0 1<o 1<i 1<k gm gnm = {!!}
+      --     (suc (suc i0)) > (suc (suc o0)) → gm = gnm → (suc (suc i0)) ≡ 1
+      --     (suc (suc i0)) < (suc (suc o0)) → ? gcd1 (suc j) (suc (suc j)) (suc o0) (suc (suc o0)) ≡  (suc (suc o0)) 
+      --                                         gcd1 (suc j) (suc (suc j)) (suc i0) (suc (suc i0)) ≡  1
+      gcd25 (suc (suc i0)) (suc (suc o0)) (suc j) j0 1<o 1<i 1<k gm gnm with <-cmp  (suc (suc i0))   (suc (suc o0))
+      ... | tri< a ¬b ¬c = {!!}
+      ... | tri≈ ¬a b ¬c = {!!}
+      ... | tri> ¬a ¬b c = gcd26 {!!} {!!} {!!} {!!} {!!} {!!} {!!}
+   gcd21 zero i0 (suc j) j0 (suc zero) o0 1<i 1<j 1<o refl gm gnm = nat-<≡ 1<k
+   gcd21 zero (suc i0) (suc j) j0 (suc (suc o)) o0 1<i 1<j 1<o gn gm gnm = 
+       gcd21 i0 {!!} (suc j) j0 (suc o) (suc (suc o)) 1<i 1<j {!!} gn {!!} {!!}
+   gcd21 (suc i) i0 zero j0 o o0 1<i 1<j 1<o gn gm gnm = {!!}
+   gcd21 (suc i) i0 (suc j) j0 zero o0 1<i 1<j 1<o gn gm gnm = {!!}
+   gcd21 (suc i) i0 (suc j) j0 (suc o) o0 1<i 1<j 1<o gn gm gnm = 
+       gcd21 i i0 j j0 o o0 1<i 1<j 1<o (subst (λ m → m ≡ k) (gcd22 i i0 _ _ ) gn)
+                                        (subst (λ m → m ≡ k) (gcd22 j j0 _ _ ) gm) (subst (λ k → k ≡ 1) (gcd22 i i0 _ _ ) gnm)
+
+record Even (i : ℕ) : Set where
+  field
+     j : ℕ
+     is-twice : i ≡ 2 * j
+
+e2 : (i : ℕ) → even i → Even i
+e2 zero en = record { j = 0 ; is-twice = refl }
+e2 (suc (suc i)) en = record { j = suc (Even.j (e2 i en )) ; is-twice = e21 } where
+   e21 : suc (suc i) ≡ 2 * suc (Even.j (e2 i en))
+   e21 = begin
+    suc (suc i)  ≡⟨ cong (λ k → suc (suc k)) (Even.is-twice (e2 i en))  ⟩
+    suc (suc (2 * Even.j (e2 i en)))  ≡⟨ sym (*-distribˡ-+ 2 1 _) ⟩
+    2 * suc (Even.j (e2 i en))      ∎ where open ≡-Reasoning
+
+record Odd (i : ℕ) : Set where
+  field
+     j : ℕ
+     is-twice : i ≡ suc (2 * j )
+
+odd2 : (i : ℕ) → ¬ even i → even (suc i) 
+odd2 zero ne = ⊥-elim ( ne tt )
+odd2 (suc zero) ne = tt
+odd2 (suc (suc i)) ne = odd2 i ne 
+
+odd3 : (i : ℕ) → ¬ even i →  Odd i
+odd3 zero ne = ⊥-elim ( ne tt )
+odd3 (suc zero) ne = record { j = 0 ; is-twice = refl }
+odd3 (suc (suc i))  ne = record { j = Even.j (e2 (suc i) (odd2 i ne)) ; is-twice = odd31 } where
+  odd31 : suc (suc i) ≡ suc (2 * Even.j (e2 (suc i) (odd2 i ne)))
+  odd31 = begin
+    suc (suc i) ≡⟨  cong suc (Even.is-twice (e2 (suc i) (odd2 i ne)))  ⟩
+    suc (2 * (Even.j (e2 (suc i) (odd2 i ne))))      ∎ where open ≡-Reasoning
+
+odd4 : (i : ℕ) → even i → ¬ even ( suc i )
+odd4 (suc (suc i)) en en1 = odd4 i en en1 
+
+even^2 : {n : ℕ} → even ( n * n ) → even n
+even^2 {n} en with even? n
+... | yes y = y
+... | no ne = ⊥-elim ( odd4 ((2 * m) + 2 * m * suc (2 * m)) (n+even {2 * m} {2 * m * suc (2 * m)} ee3 ee4) (subst (λ k → even k) ee2 en )) where
+    m : ℕ
+    m = Odd.j ( odd3 n ne )
+    ee3 : even (2 * m)
+    ee3 = subst (λ k → even k ) (*-comm m 2) (n*even {m} {2} tt )
+    ee4 : even ((2 * m) * suc (2 * m))
+    ee4 = even*n {(2 * m)} {suc (2 * m)} (even*n {2} {m} tt )
+    ee2 : n * n ≡ suc (2 * m) + ((2 * m) * (suc (2 * m) ))
+    ee2 = begin n * n ≡⟨ cong ( λ k → k * k) (Odd.is-twice (odd3 n ne)) ⟩
+       suc (2 * m) * suc (2 * m) ≡⟨ *-distribʳ-+ (suc (2 * m)) 1 ((2 * m) ) ⟩
+        (1 * suc (2 * m)) + 2 * m * suc (2 * m) ≡⟨ cong (λ k → k + 2 * m * suc (2 * m)) (begin
+        suc m + 1 * m + 0 * (suc m + 1 * m ) ≡⟨ +-comm (suc m + 1 * m) 0 ⟩
+        suc m + 1 * m  ≡⟨⟩
+        suc (2 * m)  
+        ∎) ⟩ suc (2 * m)  + 2 * m * suc (2 * m) ∎ where open ≡-Reasoning
+
+open import nat
+
+e3 : {i j : ℕ } → 2 * i ≡ 2 * j →  i ≡ j
+e3 {zero} {zero} refl = refl
+e3 {suc x} {suc y} eq with <-cmp x y
+... | tri< a ¬b ¬c = ⊥-elim ( nat-≡< eq (s≤s (<-trans (<-plus a) (<-plus-0 (s≤s (<-plus a ))))))
+... | tri≈ ¬a b ¬c = cong suc b
+... | tri> ¬a ¬b c = ⊥-elim ( nat-≡< (sym eq) (s≤s (<-trans (<-plus c) (<-plus-0 (s≤s (<-plus c ))))))
+
--- a/agda/root2.agda	Thu Dec 31 03:21:05 2020 +0900
+++ b/agda/root2.agda	Thu Dec 31 15:20:14 2020 +0900
@@ -8,200 +8,9 @@
 open import Relation.Binary.PropositionalEquality
 open import Relation.Binary.Definitions
 
-even : (n : ℕ ) → Set
-even zero = ⊤
-even (suc zero) = ⊥
-even (suc (suc n)) = even n
-
-even? : (n : ℕ ) → Dec ( even n )
-even? zero = yes tt
-even? (suc zero) = no (λ ())
-even? (suc (suc n)) = even? n
-
-n+even : {n m : ℕ } → even n → even m  → even ( n + m )
-n+even {zero} {zero} tt tt = tt
-n+even {zero} {suc m} tt em = em
-n+even {suc (suc n)} {m} en em = n+even {n} {m} en em
-
-n*even : {m n : ℕ } → even n → even ( m * n )
-n*even {zero} {n} en = tt
-n*even {suc m} {n} en = n+even {n} {m * n} en (n*even {m} {n} en) 
-
-even*n : {n m : ℕ } → even n → even ( n * m )
-even*n {n} {m} en = subst even (*-comm m n) (n*even {m} {n} en)
-
-gcd1 : ( i i0 j j0 : ℕ ) → ℕ
-gcd1 zero i0 zero j0 with <-cmp i0 j0
-... | tri< a ¬b ¬c = j0
-... | tri≈ ¬a refl ¬c = i0
-... | tri> ¬a ¬b c = i0
-gcd1 zero i0 (suc zero) j0 = 1
-gcd1 zero zero (suc (suc j)) j0 = j0
-gcd1 zero (suc i0) (suc (suc j)) j0 = gcd1 i0 (suc i0) (suc j) (suc (suc j))
-gcd1 (suc zero) i0 zero j0 = 1
-gcd1 (suc (suc i)) i0 zero zero = i0
-gcd1 (suc (suc i)) i0 zero (suc j0) = gcd1 (suc i) (suc (suc i))  j0 (suc j0)
-gcd1 (suc i) i0 (suc j) j0 = gcd1 i i0 j j0  
-
-gcd : ( i j : ℕ ) → ℕ
-gcd i j = gcd1 i i j j 
-
-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
-       gcd (suc (suc (suc (suc n)))) 2
-    ≡⟨⟩
-       gcd (suc (suc n)) 2
-    ≡⟨ even→gcd=2 {suc (suc n)} en (s≤s z≤n) ⟩
-       2
-    ∎ where open ≡-Reasoning
-
+open import gcd
 open import nat
 
--- gcd26 : { n m : ℕ} → n > 1 → m > 1 → n - m > 0 → gcd n m ≡ gcd (n - m) m
--- gcd25 : { n m : ℕ} → n > 1 → m > 1 → n - m > 0 → gcd n m ≡ gcd m n
--- gcd27 : { n m : ℕ} → n > 1 → m > 1 → n - m > 0 → gcd n k ≡ k → k ≤ n
-
-gcd22 : ( i i0 o o0 : ℕ ) → gcd1 (suc i) i0 (suc o) o0 ≡ gcd1 i i0 o o0
-gcd22 zero i0 zero o0 = refl
-gcd22 zero i0 (suc o) o0 = refl
-gcd22 (suc i) i0 zero o0 = refl
-gcd22 (suc i) i0 (suc o) o0 = refl 
-
-gcd27 : ( i i0 : ℕ ) → gcd1 i i0 0 1 ≤ 1
-gcd27 zero zero = ≤-refl
-gcd27 zero (suc i0) = {!!}
-gcd27 (suc i) zero = {!!}
-gcd27 (suc i) (suc i0) = {!!}
-
-gcdsym0 : (i : ℕ) → gcd1 zero i zero i ≡ gcd1 zero i zero i
-gcdsym0 i = refl
-gcdsym2 : (i j : ℕ) → gcd1 zero i zero j ≡ gcd1 zero j zero i
-gcdsym2 i j with <-cmp i j | <-cmp j i
-... | tri< a ¬b ¬c | tri< a₁ ¬b₁ ¬c₁ = ⊥-elim (nat-<> a a₁) 
-... | tri< a ¬b ¬c | tri≈ ¬a b ¬c₁ = ⊥-elim (nat-≡< (sym b) a) 
-... | tri< a ¬b ¬c | tri> ¬a ¬b₁ c = refl
-... | tri≈ ¬a b ¬c | tri< a ¬b ¬c₁ = ⊥-elim (nat-≡< (sym b) a) 
-... | tri≈ ¬a refl ¬c | tri≈ ¬a₁ refl ¬c₁ = refl
-... | tri≈ ¬a b ¬c | tri> ¬a₁ ¬b c = ⊥-elim (nat-≡< b c) 
-... | tri> ¬a ¬b c | tri< a ¬b₁ ¬c = refl
-... | tri> ¬a ¬b c | tri≈ ¬a₁ b ¬c = ⊥-elim (nat-≡< b c) 
-... | tri> ¬a ¬b c | tri> ¬a₁ ¬b₁ c₁ = ⊥-elim (nat-<> c c₁) 
-gcdsym1 : ( i i0 j j0 : ℕ ) → gcd1 i i0 j j0 ≡ gcd1 j j0 i i0
-gcdsym1 zero zero zero zero = refl
-gcdsym1 zero zero zero (suc j0) = refl
-gcdsym1 zero (suc i0) zero zero = refl
-gcdsym1 zero (suc i0) zero (suc j0) = gcdsym2 (suc i0) (suc j0)
-gcdsym1 zero zero (suc zero) j0 = refl
-gcdsym1 zero zero (suc (suc j)) j0 = refl
-gcdsym1 zero (suc i0) (suc zero) j0 = refl
-gcdsym1 zero (suc i0) (suc (suc j)) j0 = gcdsym1 i0 (suc i0) (suc j) (suc (suc j))
-gcdsym1 (suc zero) i0 zero j0 = refl
-gcdsym1 (suc (suc i)) i0 zero zero = refl
-gcdsym1 (suc (suc i)) i0 zero (suc j0) = gcdsym1 (suc i) (suc (suc i))j0 (suc j0) 
-gcdsym1 (suc i) i0 (suc j) j0 = subst₂ (λ j k → j ≡ k ) (sym (gcd22 i _ _ _)) (sym (gcd22 j _ _ _)) (gcdsym1 i i0 j j0 )
-
-gcdsym : { n m : ℕ} → gcd n m ≡ gcd m n
-gcdsym {n} {m} = gcdsym1 n n m m 
-
-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
-   gcd23 : {i0 j0 : ℕ } → 1 < i0  → 1 < j0 → 1 < gcd1 zero i0 zero j0
-   gcd23 {i0} {j0} 1<i 1<j with <-cmp i0 j0
-   ... | tri< a ¬b ¬c = 1<j
-   ... | tri≈ ¬a refl ¬c = 1<i
-   ... | tri> ¬a ¬b c = 1<i
-   1<ss : {j : ℕ} → 1 < suc (suc j)
-   1<ss = s≤s (s≤s z≤n)
-   gcd21 : ( i i0 j j0 o o0 : ℕ ) → 1 < i0 → 1 < j0 → 1 < o0 →  gcd1 i i0 o o0 ≡ k → gcd1 j j0 o o0 ≡ k → gcd1 i i0 j j0 ≡ 1 → ⊥
-   gcd21 zero i0 zero j0 o o0 1<i 1<j 1<o refl gm gnm = nat-≡< (sym gnm) (gcd23 1<i 1<j)
-   gcd21 zero i0 (suc j) j0 zero o0 1<i 1<j 1<o refl gm gnm = gcd25 i0 o0 j j0 1<o 1<i 1<k gm (subst (λ k → k ≡ 1) (gcdsym1 zero _ (suc j) _) gnm)  where
-      gcd25 : (i0 o0 j j0 : ℕ) → 1 < o0 → 1 < i0
-            → 1 < gcd1 zero i0 zero o0 
-            → ( gm : gcd1 (suc j) j0 zero o0 ≡ gcd1 zero i0 zero o0 ) → (gnm : gcd1 (suc j) j0 zero i0 ≡ 1) → ⊥
-      gcd25 i0 o0 zero j0 1<o 1<i 1<k gm refl with <-cmp i0 o0
-      ... | tri< a ¬b ¬c    = ⊥-elim ( nat-≡< gm 1<o )
-      ... | tri≈ ¬a refl ¬c = ⊥-elim ( nat-≡< gm 1<o )
-      ... | tri> ¬a ¬b c    = ⊥-elim ( nat-≡< gm 1<i )
-      -- gm       : gcd1 (suc j) (suc (suc j)) (suc o0) (suc (suc o0)) ≡ (gcd1 zero (suc i0) zero (suc (suc o0))
-      --            gcd1 j       (suc (suc j))       o0 (suc (suc o0)) 
-      -- gnm      : gcd1 (suc j) (suc (suc j)) i0 (suc i0) ≡ 1
-      gcd25 i0       (suc zero)     (suc j) j0 1<o 1<i 1<k gm gnm = ⊥-elim ( nat-≤> (subst (λ k → k ≤ 1 ) gm (gcd27 (suc j) (suc (suc j)))) 1<k )
-      gcd25 (suc zero) (suc (suc o0)) (suc j) j0 1<o 1<i 1<k gm gnm = {!!}
-      gcd25 (suc (suc i0)) (suc (suc o0)) (suc j) j0 1<o 1<i 1<k gm gnm = {!!}
-   gcd21 zero i0 (suc j) j0 (suc zero) o0 1<i 1<j 1<o refl gm gnm = nat-<≡ 1<k
-   gcd21 zero (suc i0) (suc j) j0 (suc (suc o)) o0 1<i 1<j 1<o gn gm gnm = 
-       gcd21 i0 {!!} (suc j) j0 (suc o) (suc (suc o)) 1<i 1<j {!!} gn {!!} {!!}
-   gcd21 (suc i) i0 zero j0 o o0 1<i 1<j 1<o gn gm gnm = {!!}
-   gcd21 (suc i) i0 (suc j) j0 zero o0 1<i 1<j 1<o gn gm gnm = {!!}
-   gcd21 (suc i) i0 (suc j) j0 (suc o) o0 1<i 1<j 1<o gn gm gnm = 
-       gcd21 i i0 j j0 o o0 1<i 1<j 1<o (subst (λ m → m ≡ k) (gcd22 i i0 _ _ ) gn)
-                                        (subst (λ m → m ≡ k) (gcd22 j j0 _ _ ) gm) (subst (λ k → k ≡ 1) (gcd22 i i0 _ _ ) gnm)
-
-record Even (i : ℕ) : Set where
-  field
-     j : ℕ
-     is-twice : i ≡ 2 * j
-
-e2 : (i : ℕ) → even i → Even i
-e2 zero en = record { j = 0 ; is-twice = refl }
-e2 (suc (suc i)) en = record { j = suc (Even.j (e2 i en )) ; is-twice = e21 } where
-   e21 : suc (suc i) ≡ 2 * suc (Even.j (e2 i en))
-   e21 = begin
-    suc (suc i)  ≡⟨ cong (λ k → suc (suc k)) (Even.is-twice (e2 i en))  ⟩
-    suc (suc (2 * Even.j (e2 i en)))  ≡⟨ sym (*-distribˡ-+ 2 1 _) ⟩
-    2 * suc (Even.j (e2 i en))      ∎ where open ≡-Reasoning
-
-record Odd (i : ℕ) : Set where
-  field
-     j : ℕ
-     is-twice : i ≡ suc (2 * j )
-
-odd2 : (i : ℕ) → ¬ even i → even (suc i) 
-odd2 zero ne = ⊥-elim ( ne tt )
-odd2 (suc zero) ne = tt
-odd2 (suc (suc i)) ne = odd2 i ne 
-
-odd3 : (i : ℕ) → ¬ even i →  Odd i
-odd3 zero ne = ⊥-elim ( ne tt )
-odd3 (suc zero) ne = record { j = 0 ; is-twice = refl }
-odd3 (suc (suc i))  ne = record { j = Even.j (e2 (suc i) (odd2 i ne)) ; is-twice = odd31 } where
-  odd31 : suc (suc i) ≡ suc (2 * Even.j (e2 (suc i) (odd2 i ne)))
-  odd31 = begin
-    suc (suc i) ≡⟨  cong suc (Even.is-twice (e2 (suc i) (odd2 i ne)))  ⟩
-    suc (2 * (Even.j (e2 (suc i) (odd2 i ne))))      ∎ where open ≡-Reasoning
-
-odd4 : (i : ℕ) → even i → ¬ even ( suc i )
-odd4 (suc (suc i)) en en1 = odd4 i en en1 
-
-even^2 : {n : ℕ} → even ( n * n ) → even n
-even^2 {n} en with even? n
-... | yes y = y
-... | no ne = ⊥-elim ( odd4 ((2 * m) + 2 * m * suc (2 * m)) (n+even {2 * m} {2 * m * suc (2 * m)} ee3 ee4) (subst (λ k → even k) ee2 en )) where
-    m : ℕ
-    m = Odd.j ( odd3 n ne )
-    ee3 : even (2 * m)
-    ee3 = subst (λ k → even k ) (*-comm m 2) (n*even {m} {2} tt )
-    ee4 : even ((2 * m) * suc (2 * m))
-    ee4 = even*n {(2 * m)} {suc (2 * m)} (even*n {2} {m} tt )
-    ee2 : n * n ≡ suc (2 * m) + ((2 * m) * (suc (2 * m) ))
-    ee2 = begin n * n ≡⟨ cong ( λ k → k * k) (Odd.is-twice (odd3 n ne)) ⟩
-       suc (2 * m) * suc (2 * m) ≡⟨ *-distribʳ-+ (suc (2 * m)) 1 ((2 * m) ) ⟩
-        (1 * suc (2 * m)) + 2 * m * suc (2 * m) ≡⟨ cong (λ k → k + 2 * m * suc (2 * m)) (begin
-        suc m + 1 * m + 0 * (suc m + 1 * m ) ≡⟨ +-comm (suc m + 1 * m) 0 ⟩
-        suc m + 1 * m  ≡⟨⟩
-        suc (2 * m)  
-        ∎) ⟩ suc (2 * m)  + 2 * m * suc (2 * m) ∎ where open ≡-Reasoning
-
-open import nat
-
-e3 : {i j : ℕ } → 2 * i ≡ 2 * j →  i ≡ j
-e3 {zero} {zero} refl = refl
-e3 {suc x} {suc y} eq with <-cmp x y
-... | tri< a ¬b ¬c = ⊥-elim ( nat-≡< eq (s≤s (<-trans (<-plus a) (<-plus-0 (s≤s (<-plus a ))))))
-... | tri≈ ¬a b ¬c = cong suc b
-... | tri> ¬a ¬b c = ⊥-elim ( nat-≡< (sym eq) (s≤s (<-trans (<-plus c) (<-plus-0 (s≤s (<-plus c ))))))
-
 record Rational : Set where
   field
     i j : ℕ