Mercurial > hg > Members > kono > Proof > prob1

annotate prob1.agda @ 3:e909c828cefe

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
which way?
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 25 Nov 2019 21:07:46 +0900
parents 0dcf08f3ff18
children 2a36d771d388
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
0
06002e20ce5c incudtion selection on diophantos equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
1 module prob1 where
06002e20ce5c incudtion selection on diophantos equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
2
06002e20ce5c incudtion selection on diophantos equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
3 open import Relation.Binary.PropositionalEquality
06002e20ce5c incudtion selection on diophantos equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
4 open import Relation.Binary.Core
06002e20ce5c incudtion selection on diophantos equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
5 open import Data.Nat
06002e20ce5c incudtion selection on diophantos equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
6 open import Data.Nat.Properties
06002e20ce5c incudtion selection on diophantos equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
7 open import logic
06002e20ce5c incudtion selection on diophantos equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
8 open import nat
06002e20ce5c incudtion selection on diophantos equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
9 open import Data.Empty
06002e20ce5c incudtion selection on diophantos equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
10 open import Relation.Nullary
06002e20ce5c incudtion selection on diophantos equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
11
06002e20ce5c incudtion selection on diophantos equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
12 minus : (a b : ℕ ) → ℕ
06002e20ce5c incudtion selection on diophantos equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
13 minus a zero = a
06002e20ce5c incudtion selection on diophantos equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
14 minus zero (suc b) = zero
06002e20ce5c incudtion selection on diophantos equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
15 minus (suc a) (suc b) = minus a b
06002e20ce5c incudtion selection on diophantos equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
16
2
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1
diff changeset
17 m+= : {i j m : ℕ } → m + i ≡ m + j → i ≡ j
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1
diff changeset
18 m+= {i} {j} {zero} refl = refl
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1
diff changeset
19 m+= {i} {j} {suc m} eq = m+= {i} {j} {m} ( cong (λ k → pred k ) eq )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1
diff changeset
20
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1
diff changeset
21 +m= : {i j m : ℕ } → i + m ≡ j + m → i ≡ j
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1
diff changeset
22 +m= {i} {j} {m} eq = m+= ( subst₂ (λ j k → j ≡ k ) (+-comm i _ ) (+-comm j _ ) eq )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1
diff changeset
23
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1
diff changeset
24 less-1 : { n m : ℕ } → suc n < m → n < m
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1
diff changeset
25 less-1 {zero} {suc (suc _)} (s≤s (s≤s z≤n)) = s≤s z≤n
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1
diff changeset
26 less-1 {suc n} {suc m} (s≤s lt) = s≤s (less-1 {n} {m} lt)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1
diff changeset
27
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1
diff changeset
28 minus+n : {x y : ℕ } → suc x > y → minus x y + y ≡ x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1
diff changeset
29 minus+n {x} {zero} _ = trans (sym (+-comm zero _ )) refl
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1
diff changeset
30 minus+n {zero} {suc y} (s≤s ())
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1
diff changeset
31 minus+n {suc x} {suc y} (s≤s lt) = begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1
diff changeset
32 minus (suc x) (suc y) + suc y
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1
diff changeset
33 ≡⟨ +-comm _ (suc y) ⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1
diff changeset
34 suc y + minus x y
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1
diff changeset
35 ≡⟨ cong ( λ k → suc k ) (
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1
diff changeset
36 begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1
diff changeset
37 y + minus x y
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1
diff changeset
38 ≡⟨ +-comm y _ ⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1
diff changeset
39 minus x y + y
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1
diff changeset
40 ≡⟨ minus+n {x} {y} lt ⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1
diff changeset
41 x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1
diff changeset
42 ∎
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1
diff changeset
43 ) ⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1
diff changeset
44 suc x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1
diff changeset
45 ∎ where open ≡-Reasoning
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1
diff changeset
46
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1
diff changeset
47 <-minus : {x y z : ℕ } → x + z < y + z → x < y
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1
diff changeset
48 <-minus = {!!}
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1
diff changeset
49
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1
diff changeset
50
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1
diff changeset
51 -- trans (sym (+-comm (suc y) _ )) (cong ( λ k → suc k ) {!!} ) -- (trans ? (+-comm _ _ ) )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1
diff changeset
52
0
06002e20ce5c incudtion selection on diophantos equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
53 -- All variables are positive integer
06002e20ce5c incudtion selection on diophantos equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
54 -- A = -M*n + i +k*M - M
06002e20ce5c incudtion selection on diophantos equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
55 -- where n is in range (0,…,k-1) and i is in range(0,…,M-1)
06002e20ce5c incudtion selection on diophantos equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
56 -- Goal: Prove that A can take all values of (0,…,k*M-1)
06002e20ce5c incudtion selection on diophantos equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
57 -- A1 = -M*n1 + i1 +k*M M, A2 = -M*n2 + i2 +k*M - M
06002e20ce5c incudtion selection on diophantos equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
58 -- (1) If n1!=n2 or i1!=i2 then A1!=A2
06002e20ce5c incudtion selection on diophantos equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
59 -- Or its contraposition: (2) if A1=A2 then n1=n2 and i1=i2
06002e20ce5c incudtion selection on diophantos equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
60 -- Proof by contradiction: Suppose A1=A2 and (n1!=n2 or i1!=i2) becomes
06002e20ce5c incudtion selection on diophantos equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
61 -- contradiction
06002e20ce5c incudtion selection on diophantos equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
62 -- Induction on n and i
06002e20ce5c incudtion selection on diophantos equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
63
06002e20ce5c incudtion selection on diophantos equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
64 record Cond1 (A M k : ℕ ) : Set where
06002e20ce5c incudtion selection on diophantos equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
65 field
06002e20ce5c incudtion selection on diophantos equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
66 n : ℕ
06002e20ce5c incudtion selection on diophantos equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
67 i : ℕ
06002e20ce5c incudtion selection on diophantos equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
68 range-n : n < k
06002e20ce5c incudtion selection on diophantos equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
69 range-i : i < M
06002e20ce5c incudtion selection on diophantos equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
70 rule1 : i + k * M ≡ M * (suc n) + A -- A ≡ (i + k * M ) - (M * (suc n))
06002e20ce5c incudtion selection on diophantos equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
71
06002e20ce5c incudtion selection on diophantos equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
72 -- k = 1 → n = 0 → ∀ M → A = i
06002e20ce5c incudtion selection on diophantos equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
73 -- k = 2 → n = 1 →
06002e20ce5c incudtion selection on diophantos equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
74
06002e20ce5c incudtion selection on diophantos equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
75 -- i + 2 * M = M * (suc n) + A i = suc n → A = 0
06002e20ce5c incudtion selection on diophantos equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
76
1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
77 problem : ( A M k : ℕ ) → Set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
78 problem A M k = (suc A < k * M ) → Cond1 A M k
0
06002e20ce5c incudtion selection on diophantos equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
79
2
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1
diff changeset
80 problem0-k=k : ( k A M : ℕ ) → problem A M k
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1
diff changeset
81 problem0-k=k zero A M ()
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1
diff changeset
82 problem0-k=k (suc k) A M A<kM = cc where
3
e909c828cefe which way?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 2
diff changeset
83 ccn : (suc A > k * M ) → Cond1 A M (suc k)
e909c828cefe which way?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 2
diff changeset
84 ccn gt = record { n = 0 ; i = minus A (k * M ) ; range-n = s≤s z≤n ; range-i = A-Mk<M {k} gt A<kM ; rule1 = lemma1 } where
2
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1
diff changeset
85 A-Mk<M : {k A M : ℕ } → (suc A > k * M ) → ( suc A < (suc k ) * M ) → minus A (k * M ) < M
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1
diff changeset
86 A-Mk<M {k} {A} {M} lt1 lt2 = <-minus ( subst₂ (λ j k → j < k ) (sym (minus+n {A} {k * M} lt1 )) refl (<-trans a<sa lt2) )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1
diff changeset
87 lemma1 : minus A (k * M) + suc k * M ≡ M * 1 + A
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1
diff changeset
88 lemma1 = begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1
diff changeset
89 minus A (k * M) + suc k * M
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1
diff changeset
90 ≡⟨⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1
diff changeset
91 minus A (k * M) + (M + k * M )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1
diff changeset
92 ≡⟨ cong ( λ x → minus A (k * M) + x ) (+-comm M _ ) ⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1
diff changeset
93 minus A (k * M) + (k * M + M )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1
diff changeset
94 ≡⟨ sym ( +-assoc _ (k * M ) M ) ⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1
diff changeset
95 (minus A (k * M) + k * M ) + M
3
e909c828cefe which way?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 2
diff changeset
96 ≡⟨ cong ( λ k → k + M ) (minus+n {A} {k * M} gt ) ⟩
2
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1
diff changeset
97 A + M
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1
diff changeset
98 ≡⟨⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1
diff changeset
99 A + ( 0 + M )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1
diff changeset
100 ≡⟨ cong ( λ k → A + k ) (+-comm 0 _ ) ⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1
diff changeset
101 A + ( M + 0 )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1
diff changeset
102 ≡⟨⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1
diff changeset
103 A + 1 * M
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1
diff changeset
104 ≡⟨ cong ( λ k → A + k ) (*-comm 1 _ ) ⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1
diff changeset
105 A + M * 1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1
diff changeset
106 ≡⟨ +-comm A _ ⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1
diff changeset
107 M * 1 + A
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1
diff changeset
108 ∎ where open ≡-Reasoning
1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
109
2
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1
diff changeset
110 next-cc : (A M k : ℕ ) → ((suc A < k * M ) → Cond1 A M k) → (suc A < k * M ) → Cond1 A M (suc k)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1
diff changeset
111 next-cc A M k cc A<kM = record { n = k ; i = Cond1.i (cc A<kM ) ; range-n = {!!} ; range-i = Cond1.range-i (cc A<kM ) ; rule1 = {!!} }
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1
diff changeset
112 cc : Cond1 A M (suc k)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1
diff changeset
113 cc with <-cmp (suc A) (k * M)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1
diff changeset
114 cc | tri< a ¬b ¬c = next-cc A M k ( problem0-k=k k A M ) a
3
e909c828cefe which way?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 2
diff changeset
115 cc | tri≈ ¬a b ¬c = next-cc A M k ( problem0-k=k k A M ) ?
e909c828cefe which way?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 2
diff changeset
116 cc | tri> ¬a ¬b c = ccn c
0
06002e20ce5c incudtion selection on diophantos equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
117
06002e20ce5c incudtion selection on diophantos equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
118 problem0 : ( A M k : ℕ ) → M > 0 → k > 0 → (suc A < k * M ) → Cond1 A M k
1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
119 problem0 A (suc M) (suc k) 0<M 0<k A<kM = lemma1 k M A<kM a<sa a<sa where
0
06002e20ce5c incudtion selection on diophantos equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
120 --- i loop in n loop
06002e20ce5c incudtion selection on diophantos equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
121 lemma1-i : ( n i : ℕ ) → (suc A < suc k * suc M ) → n < suc k → i < suc M → Dec ( Cond1 A (suc M) (suc k) )
1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
122 lemma1-i n zero A<kM _ _ with <-cmp (1 + suc k * suc M ) ( suc M * suc n + A)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
123 lemma1-i n zero A<kM _ _ | tri< a ¬b ¬c = no {!!}
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
124 lemma1-i n zero A<kM n<k i<M | tri≈ ¬a b ¬c = yes record { n = n ; i = suc zero ; range-n = n<k ; range-i = {!!} ; rule1 = b }
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
125 lemma1-i n zero A<kM _ _ | tri> ¬a ¬b c = no {!!}
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
126 lemma1-i n (suc i) A<kM _ _ with <-cmp (suc i + suc k * suc M ) ( suc M * suc n + A)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
127 lemma1-i n (suc i) A<kM n<k i<M | tri≈ ¬a b ¬c = yes record { n = n ; i = suc i ; range-n = n<k ; range-i = i<M ; rule1 = b }
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
128 lemma1-i n (suc i) A<kM n<k i<M | tri< a ¬b ¬c = lemma1-i n i A<kM n<k (less-1 i<M)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
129 lemma1-i n (suc i) A<kM n<k i<M | tri> ¬a ¬b c = no {!!}
0
06002e20ce5c incudtion selection on diophantos equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
130 --- n loop
06002e20ce5c incudtion selection on diophantos equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
131 lemma1 : ( n i : ℕ ) → (suc A < suc k * suc M ) → n < suc k → i < suc M → Cond1 A (suc M) (suc k)
1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
132 lemma1 n i A<kM _ _ with <-cmp (i + suc k * suc M ) ( suc M * suc n + A)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
133 lemma1 n i A<kM n<k i<M | tri≈ ¬a b ¬c = record { n = n ; i = i ; range-n = n<k ; range-i = i<M ; rule1 = b }
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
134 lemma1 zero i A<kM n<k i<M | tri< a ¬b ¬c = lemma2 i A<kM i<M where
0
06002e20ce5c incudtion selection on diophantos equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
135 --- i + k * M ≡ M + A case
06002e20ce5c incudtion selection on diophantos equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
136 lemma2 : ( i : ℕ ) → (suc A < suc k * suc M ) → i < suc M → Cond1 A (suc M) (suc k)
1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
137 lemma2 zero A<kM i<M = {!!} -- A = A = k * M
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
138 lemma2 (suc i) A<kM i<M with <-cmp ( suc i + suc k * suc M ) ( suc M * 1 + A)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
139 lemma2 (suc i) A<kM i<M | tri≈ ¬a b ¬c = record { n = zero ; i = suc i ; range-n = n<k ; range-i = i<M ; rule1 = b }
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
140 lemma2 (suc i) A<kM i<M | tri< a ¬b ¬c = lemma2 i A<kM (less-1 i<M)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
141 lemma2 (suc i) A<kM i<M | tri> ¬a ¬b c = {!!} -- can't happen
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
142 lemma1 (suc n) i A<kM n<k i<M | tri< a ¬b ¬c with lemma1-i (suc n) i A<kM n<k i<M
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
143 lemma1 (suc n) i A<kM n<k i<M | tri< a ¬b ¬c | yes p = p
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
144 lemma1 (suc n) i A<kM n<k i<M | tri< a ¬b ¬c | no ¬p = lemma1 n i A<kM (less-1 n<k) i<M
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
145 lemma1 n i A<kM n<k i<M | tri> ¬a ¬b c = {!!} where -- can't happen
0
06002e20ce5c incudtion selection on diophantos equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
146 cannot1 : { n k M i A : ℕ } → n < suc k → i < suc M → (i + suc k * suc M ) > ( suc M * suc n + A) → ¬ ( suc A < suc k * suc M )
06002e20ce5c incudtion selection on diophantos equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
147 cannot1 = {!!}
06002e20ce5c incudtion selection on diophantos equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
148
06002e20ce5c incudtion selection on diophantos equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
149 problem1 : (A1 A2 M k : ℕ )
06002e20ce5c incudtion selection on diophantos equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
150 → (c1 : Cond1 A1 M k ) → (c2 : Cond1 A2 M k )
06002e20ce5c incudtion selection on diophantos equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
151 → ( A1 ≡ A2 ) → ( Cond1.n c1 ≡ Cond1.n c2 ) ∧ ( Cond1.i c1 ≡ Cond1.i c2 )
06002e20ce5c incudtion selection on diophantos equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
152 problem1 = {!!}
06002e20ce5c incudtion selection on diophantos equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
153