Mercurial > hg > Members > kono > Proof > automaton

comparison agda/gcd.agda @ 149:d3a8572ced9c

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
non terminating GCD
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 01 Jan 2021 12:16:32 +0900
parents 8207b69c500b
children 36d3ecce01b2
comparison
equal deleted inserted replaced
148:8207b69c500b 149:d3a8572ced9c
6 open import Data.Empty 6 open import Data.Empty
7 open import Data.Unit using (⊤ ; tt) 7 open import Data.Unit using (⊤ ; tt)
8 open import Relation.Nullary 8 open import Relation.Nullary
9 open import Relation.Binary.PropositionalEquality 9 open import Relation.Binary.PropositionalEquality
10 open import Relation.Binary.Definitions 10 open import Relation.Binary.Definitions
11 open import nat
11 12
12 even : (n : ℕ ) → Set 13 even : (n : ℕ ) → Set
13 even zero = ⊤ 14 even zero = ⊤
14 even (suc zero) = ⊥ 15 even (suc zero) = ⊥
15 even (suc (suc n)) = even n 16 even (suc (suc n)) = even n
28 n*even {zero} {n} en = tt 29 n*even {zero} {n} en = tt
29 n*even {suc m} {n} en = n+even {n} {m * n} en (n*even {m} {n} en) 30 n*even {suc m} {n} en = n+even {n} {m * n} en (n*even {m} {n} en)
30 31
31 even*n : {n m : ℕ } → even n → even ( n * m ) 32 even*n : {n m : ℕ } → even n → even ( n * m )
32 even*n {n} {m} en = subst even (*-comm m n) (n*even {m} {n} en) 33 even*n {n} {m} en = subst even (*-comm m n) (n*even {m} {n} en)
34
35 gcd2 : ( i i0 j j0 : ℕ ) → i ≤ i0 → j ≤ j0 → i0 < j0 → ℕ
36 gcd2 zero i0 zero j0 i<i0 j<j0 i<j = j0
37 gcd2 zero i0 (suc zero) j0 i<i0 j<j0 i<j = 1
38 gcd2 zero zero (suc (suc j)) j0 i<i0 j<j0 i<j = j0
39 -- i<i0 : zero ≤ suc i0
40 -- j<j0 : suc (suc j) ≤ j0
41 -- i<j : suc i0 < j0
42 gcd2 zero (suc i0) (suc (suc j)) j0 i<i0 j<j0 i<j with <-cmp (suc (suc j)) (suc i0) -- non terminating
43 ... | tri< a ¬b ¬c = gcd2 i0 (suc i0) (suc j) (suc (suc j)) refl-≤s refl-≤s {!!}
44 ... | tri≈ ¬a refl ¬c = suc i0
45 ... | tri> ¬a ¬b c = gcd2 i0 (suc i0) (suc j) (suc (suc j)) refl-≤s refl-≤s {!!}
46 -- = gcd2 (suc j) (suc (suc j)) i0 (suc i0) refl-≤s refl-≤s {!!} -- suc (suc j) < suc i0
47 gcd2 (suc zero) i0 zero j0 i<i0 j<j0 i<j = 1
48 gcd2 (suc (suc i)) i0 zero zero i<i0 j<j0 i<j = i0
49 gcd2 (suc (suc i)) i0 zero (suc j0) i<i0 j<j0 i<j = gcd2 (suc i) (suc (suc i)) j0 (suc j0) refl-≤s refl-≤s {!!} -- suc (suc i) < suc j0
50 gcd2 (suc i) i0 (suc j) j0 i<i0 j<j0 i<j = gcd2 i i0 j j0 (≤-trans refl-≤s i<i0) (≤-trans refl-≤s j<j0) i<j
33 51
34 gcd1 : ( i i0 j j0 : ℕ ) → ℕ 52 gcd1 : ( i i0 j j0 : ℕ ) → ℕ
35 gcd1 zero i0 zero j0 with <-cmp i0 j0 53 gcd1 zero i0 zero j0 with <-cmp i0 j0
36 ... | tri< a ¬b ¬c = j0 54 ... | tri< a ¬b ¬c = j0
37 ... | tri≈ ¬a refl ¬c = i0 55 ... | tri≈ ¬a refl ¬c = i0
55 gcd (suc (suc n)) 2 73 gcd (suc (suc n)) 2
56 ≡⟨ even→gcd=2 {suc (suc n)} en (s≤s z≤n) ⟩ 74 ≡⟨ even→gcd=2 {suc (suc n)} en (s≤s z≤n) ⟩
57 2 75 2
58 ∎ where open ≡-Reasoning 76 ∎ where open ≡-Reasoning
59 77
60 open import nat
61
62 -- gcd26 : { n m : ℕ} → n > 1 → m > 1 → n - m > 0 → gcd n m ≡ gcd (n - m) m 78 -- gcd26 : { n m : ℕ} → n > 1 → m > 1 → n - m > 0 → gcd n m ≡ gcd (n - m) m
63 -- gcd27 : { n m : ℕ} → n > 1 → m > 1 → n - m > 0 → gcd n k ≡ k → k ≤ n 79 -- gcd27 : { n m : ℕ} → n > 1 → m > 1 → n - m > 0 → gcd n k ≡ k → k ≤ n
64 80
65 gcd22 : ( i i0 o o0 : ℕ ) → gcd1 (suc i) i0 (suc o) o0 ≡ gcd1 i i0 o o0 81 gcd22 : ( i i0 o o0 : ℕ ) → gcd1 (suc i) i0 (suc o) o0 ≡ gcd1 i i0 o o0
66 gcd22 zero i0 zero o0 = refl 82 gcd22 zero i0 zero o0 = refl
87 103
88 gcd26 : (n m i : ℕ) → 1 < n → 1 < m → gcd n i ≡ m → ¬ ( gcd n m ≡ 1 ) 104 gcd26 : (n m i : ℕ) → 1 < n → 1 < m → gcd n i ≡ m → ¬ ( gcd n m ≡ 1 )
89 gcd26 n m i 1<n 1<m gi g1 = gcd261 n n m m i i 1<n 1<m gi g1 where 105 gcd26 n m i 1<n 1<m gi g1 = gcd261 n n m m i i 1<n 1<m gi g1 where
90 gcd261 : (n n0 m m0 i i0 : ℕ) → 1 < n → 1 < m0 → gcd1 n n0 i i0 ≡ m0 → ¬ ( gcd1 n n0 m m0 ≡ 1 ) 106 gcd261 : (n n0 m m0 i i0 : ℕ) → 1 < n → 1 < m0 → gcd1 n n0 i i0 ≡ m0 → ¬ ( gcd1 n n0 m m0 ≡ 1 )
91 gcd261 zero n0 m m0 i i0 () 1<m gi g1 107 gcd261 zero n0 m m0 i i0 () 1<m gi g1
108 -- gi : gcd1 (suc n) n0 zero i0 ≡ m0
109 -- g1 : gcd1 (suc n) n0 m m0 ≡ 1
92 gcd261 (suc n) n0 m m0 zero i0 1<n 1<m gi g1 = {!!} 110 gcd261 (suc n) n0 m m0 zero i0 1<n 1<m gi g1 = {!!}
111 -- gi : gcd1 (suc n) n0 (suc i) i0 ≡ m0
112 -- g1 : gcd1 (suc n) n0 zero m0 ≡ 1
93 gcd261 (suc n) n0 zero m0 (suc i) i0 1<n 1<m gi g1 = {!!} 113 gcd261 (suc n) n0 zero m0 (suc i) i0 1<n 1<m gi g1 = {!!}
94 -- 1<n : 1 < suc n
95 -- 1<m : 1 < m0
96 -- gi : gcd1 (suc n) n0 (suc i) i0 ≡ m0 -- gi : gcd1 n n0 i i0 ≡ m0
97 -- g1 : gcd1 (suc n) n0 (suc m) m0 ≡ 1 -- g1 : gcd1 n n0 m m0 ≡ 1
98 gcd261 (suc zero) n0 (suc m) m0 (suc i) i0 1<n 1<m gi g1 = ⊥-elim ( nat-<≡ 1<n ) 114 gcd261 (suc zero) n0 (suc m) m0 (suc i) i0 1<n 1<m gi g1 = ⊥-elim ( nat-<≡ 1<n )
99 gcd261 (suc (suc zero)) n0 (suc m) m0 (suc i) i0 1<n 1<m gi g1 = {!!} 115 gcd261 (suc (suc zero)) n0 (suc m) m0 (suc zero) i0 1<n 1<m gi g1 = ⊥-elim ( nat-≡< gi 1<m )
116 -- gi : gcd1 0 n0 i i0 ≡ m0
117 gcd261 (suc (suc zero)) n0 (suc zero) m0 (suc (suc i)) i0 1<n 1<m gi g1 = {!!}
118 -- gi : gcd1 0 n0 i i0 ≡ m0
119 -- g1 : gcd1 0 n0 m m0 ≡ 1
120 gcd261 (suc (suc zero)) n0 (suc (suc m)) m0 (suc (suc i)) i0 1<n 1<m gi g1 = {!!}
100 gcd261 (suc (suc (suc n))) n0 (suc m) m0 (suc i) i0 1<n 1<m gi g1 = 121 gcd261 (suc (suc (suc n))) n0 (suc m) m0 (suc i) i0 1<n 1<m gi g1 =
101 gcd261 (suc (suc n)) n0 m m0 i i0 (s≤s (s≤s z≤n)) 1<m gi g1 122 gcd261 (suc (suc n)) n0 m m0 i i0 (s≤s (s≤s z≤n)) 1<m gi g1
102 123
103 gcdsym2 : (i j : ℕ) → gcd1 zero i zero j ≡ gcd1 zero j zero i 124 gcdsym2 : (i j : ℕ) → gcd1 zero i zero j ≡ gcd1 zero j zero i
104 gcdsym2 i j with <-cmp i j | <-cmp j i 125 gcdsym2 i j with <-cmp i j | <-cmp j i