Mercurial > hg > Members > kono > Proof > prob1

comparison prob1.agda @ 27:73511e7ddf5c

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
u2 done
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 30 Mar 2020 14:28:14 +0900
parents fd8633b6d551
children 8ef3eecd159f
comparison
equal deleted inserted replaced
26:fd8633b6d551 27:73511e7ddf5c
36 36
37 record UCond1 (A M k : ℕ ) : Set where 37 record UCond1 (A M k : ℕ ) : Set where
38 field 38 field
39 c1 : Cond1 A M k 39 c1 : Cond1 A M k
40 u1 : {j m : ℕ} → j < Cond1.i c1 → m < k → ¬ ( j + k * M ≡ M * (suc m) + A ) 40 u1 : {j m : ℕ} → j < Cond1.i c1 → m < k → ¬ ( j + k * M ≡ M * (suc m) + A )
41 -- u2 : {j m : ℕ} → Cond1.i c1 < j → j < M → m < k → ¬ ( j + k * M ≡ M * (suc m) + A ) 41 u2 : {j m : ℕ} → Cond1.i c1 < j → j < M → m < k → ¬ ( j + k * M ≡ M * (suc m) + A )
42 -- u3 : {j m : ℕ} → j < M → m < Cond1.n c1 → ¬ ( j + k * M ≡ M * (suc m) + A ) 42 -- u3 : {j m : ℕ} → j < M → m < Cond1.n c1 → ¬ ( j + k * M ≡ M * (suc m) + A )
43 -- u4 : {j m : ℕ} → j < M → Cond1.n c1 < m → m < k → ¬ ( j + k * M ≡ M * (suc m) + A ) 43 -- u4 : {j m : ℕ} → j < M → Cond1.n c1 < m → m < k → ¬ ( j + k * M ≡ M * (suc m) + A )
44 44
45 problem1-0 : (k A M : ℕ ) → (A<kM : suc A < k * M ) 45 problem1-0 : (k A M : ℕ ) → (A<kM : suc A < k * M )
46 → UCond1 A M k 46 → UCond1 A M k
68 c1 : Cond1 A M (suc k) 68 c1 : Cond1 A M (suc k)
69 c1 = cck n n<k k<A i<M 69 c1 = cck n n<k k<A i<M
70 lemma4 : {i j x y z : ℕ} → j + x ≡ y → i + x ≡ z → j < i → y < z 70 lemma4 : {i j x y z : ℕ} → j + x ≡ y → i + x ≡ z → j < i → y < z
71 lemma4 {i} {j} {x} refl refl (s≤s z≤n) = s≤s (subst (λ k → x ≤ k ) (+-comm x _) x≤x+y) 71 lemma4 {i} {j} {x} refl refl (s≤s z≤n) = s≤s (subst (λ k → x ≤ k ) (+-comm x _) x≤x+y)
72 lemma4 refl refl (s≤s (s≤s lt)) = s≤s (lemma4 refl refl (s≤s lt) ) 72 lemma4 refl refl (s≤s (s≤s lt)) = s≤s (lemma4 refl refl (s≤s lt) )
73 lemma5 : {m1 : ℕ} → M * suc m1 + A < M * suc n + A 73 lemma5 : {m1 n : ℕ} → M * suc m1 + A < M * suc n + A
74 → M + (M * suc m1 + A) ≤ M * suc n + A 74 → M + (M * suc m1 + A) ≤ M * suc n + A
75 lemma5 {m1} lt with <-cmp m1 n 75 lemma5 {m1} {n} lt with <-cmp m1 n
76 lemma5 {m1} lt | tri< a ¬b ¬c = begin 76 lemma5 {m1} {n} lt | tri< a ¬b ¬c = begin
77 M + (M * suc m1 + A) 77 M + (M * suc m1 + A)
78 ≡⟨ sym (+-assoc M _ _ ) ⟩ 78 ≡⟨ sym (+-assoc M _ _ ) ⟩
79 (M + M * suc m1) + A 79 (M + M * suc m1) + A
80 ≡⟨ sym ( cong (λ k → (k + M * suc m1) + A) ((proj₂ *-identity) M )) ⟩ 80 ≡⟨ sym ( cong (λ k → (k + M * suc m1) + A) ((proj₂ *-identity) M )) ⟩
81 (M * suc zero + M * suc m1) + A 81 (M * suc zero + M * suc m1) + A
82 ≡⟨ sym ( cong (λ k → k + A) (( proj₁ *-distrib-+ ) M (suc zero) _ )) ⟩ 82 ≡⟨ sym ( cong (λ k → k + A) (( proj₁ *-distrib-+ ) M (suc zero) _ )) ⟩
83 M * suc (suc m1) + A 83 M * suc (suc m1) + A
84 ≤⟨ ≤-plus {_} {_} {A} (subst₂ (λ x y → x ≤ y ) (*-comm _ M ) (*-comm _ M ) (*≤ (s≤s a))) ⟩ 84 ≤⟨ ≤-plus {_} {_} {A} (subst₂ (λ x y → x ≤ y ) (*-comm _ M ) (*-comm _ M ) (*≤ (s≤s a))) ⟩
85 M * suc n + A 85 M * suc n + A
86 ∎ where open ≤-Reasoning 86 ∎ where open ≤-Reasoning
87 lemma5 {m1} lt | tri≈ ¬a refl ¬c = ⊥-elim ( nat-<≡ lt ) 87 lemma5 {m1} {n} lt | tri≈ ¬a refl ¬c = ⊥-elim ( nat-<≡ lt )
88 lemma5 {m1} lt | tri> ¬a ¬b c = ⊥-elim ( nat-<> lt (<-plus {_} {_} {A} (<≤+ (s≤s c) 88 lemma5 {m1} {n} lt | tri> ¬a ¬b c = ⊥-elim ( nat-<> lt (<-plus {_} {_} {A} (<≤+ (s≤s c)
89 (subst₂ (λ x y → x ≤ y ) (*-comm _ m ) (*-comm _ m ) (*≤ (s≤s (≤to< c))))))) 89 (subst₂ (λ x y → x ≤ y ) (*-comm _ m ) (*-comm _ m ) (*≤ (s≤s (≤to< c)))))))
90 lemma6 : {i j x : ℕ} → M + (j + x ) ≤ i + x → M ≤ i 90 lemma6 : {i j x : ℕ} → M + (j + x ) ≤ i + x → M ≤ i
91 lemma6 {i} {j} {x} lt = ≤-minus {M} {i} {x} (x+y≤z→x≤z ( begin 91 lemma6 {i} {j} {x} lt = ≤-minus {M} {i} {x} (x+y≤z→x≤z ( begin
92 M + x + j 92 M + x + j
93 ≡⟨ +-assoc M _ _ ⟩ 93 ≡⟨ +-assoc M _ _ ⟩
95 ≡⟨ cong (λ k → M + k ) (+-comm x _ ) ⟩ 95 ≡⟨ cong (λ k → M + k ) (+-comm x _ ) ⟩
96 M + (j + x) 96 M + (j + x)
97 ≤⟨ lt ⟩ 97 ≤⟨ lt ⟩
98 i + x 98 i + x
99 ∎ )) where open ≤-Reasoning 99 ∎ )) where open ≤-Reasoning
100 lemma-u1 : {j : ℕ} {m1 : ℕ} → j < (A - ((k - n) * M)) → m1 < suc k → ¬ j + suc k * M ≡ M * suc m1 + A 100 i : ℕ
101 i = A - ((k - n) * M)
102 lemma-u1 : {j : ℕ} {m1 : ℕ} → j < i → m1 < suc k → ¬ j + suc k * M ≡ M * suc m1 + A
101 lemma-u1 {j} {m1} j<akM m1<k eq with <-cmp j M 103 lemma-u1 {j} {m1} j<akM m1<k eq with <-cmp j M
102 lemma-u1 {j} {m1} j<akM m1<k eq | tri< a ¬b ¬c = 104 lemma-u1 {j} {m1} j<akM m1<k eq | tri< a ¬b ¬c =
103 ⊥-elim (nat-≤> (lemma6 (subst₂ (λ x y → M + x ≤ y) (sym eq) (sym (Cond1.rule1 c1 )) (lemma5 (lemma4 eq (Cond1.rule1 c1) j<akM ))) ) i<M ) where 105 ⊥-elim (nat-≤> (lemma6 (subst₂ (λ x y → M + x ≤ y) (sym eq) (sym (Cond1.rule1 c1 )) (lemma5 (lemma4 eq (Cond1.rule1 c1) j<akM ))) ) i<M ) where
104 lemma3 : M + (M * suc m1 + A) ≤ M * suc n + A 106 lemma3 : M + (M * suc m1 + A) ≤ M * suc n + A -- M + j ≤ i
105 lemma3 = lemma5 (lemma4 eq (Cond1.rule1 c1) j<akM) 107 lemma3 = lemma5 (lemma4 eq (Cond1.rule1 c1) j<akM)
106 lemma-u1 {j} {m1} j<akM m1<k eq | tri≈ ¬a b ¬c = ⊥-elim (nat-≡< b ( (≤-trans j<akM (≤-trans refl-≤s i<M )))) 108 lemma-u1 {j} {m1} j<akM m1<k eq | tri≈ ¬a b ¬c = ⊥-elim (nat-≡< b ( (≤-trans j<akM (≤-trans refl-≤s i<M ))))
107 lemma-u1 {j} {m1} j<akM m1<k eq | tri> ¬a ¬b c = ⊥-elim (nat-<> (≤-trans i<M (less-1 c)) j<akM ) 109 lemma-u1 {j} {m1} j<akM m1<k eq | tri> ¬a ¬b c = ⊥-elim (nat-<> (≤-trans i<M (less-1 c)) j<akM )
108 c0 = record { c1 = record { n = n ; i = A - (((k - n)) * M ) ; range-n = n<k ; range-i = i<M; rule1 = Cond1.rule1 c1 } ; u1 = lemma-u1 } 110 lemma-u2 : {j : ℕ} {m1 : ℕ} → (A - ((k - n) * M)) < j →
111 j < M → m1 < suc k → ¬ j + suc k * M ≡ M * suc m1 + A
112 lemma-u2 {j} {m1} i<j j<M m1<k eq = ⊥-elim ( nat-≤> (lemma6 (subst₂ (λ x y → M + x ≤ y) (sym (Cond1.rule1 c1)) (sym eq) lemma3-2)) j<M ) where
113 lemma3-2 : M + (M * suc n + A) ≤ M * suc m1 + A -- M + i ≤ j
114 lemma3-2 = lemma5 (lemma4 (Cond1.rule1 c1) eq i<j)
115 c0 = record { c1 = record { n = n ; i = A - (((k - n)) * M ) ; range-n = n<k ; range-i = i<M; rule1 = Cond1.rule1 c1 }
116 ; u1 = lemma-u1
117 ; u2 = lemma-u2
118 }
109 -- loop on range of A : ((k - n) ) * M ≤ A < ((k - n) ) * M + M 119 -- loop on range of A : ((k - n) ) * M ≤ A < ((k - n) ) * M + M
110 nextc : (n : ℕ ) → (suc n < suc k) → M < suc ((k - n) * M) 120 nextc : (n : ℕ ) → (suc n < suc k) → M < suc ((k - n) * M)
111 nextc n n<k with k - n | inspect (_-_ k) n 121 nextc n n<k with k - n | inspect (_-_ k) n
112 nextc n n<k | 0 | record { eq = e } = ⊥-elim ( nat-≡< (sym e) (minus>0 n<k) ) 122 nextc n n<k | 0 | record { eq = e } = ⊥-elim ( nat-≡< (sym e) (minus>0 n<k) )
113 nextc n n<k | suc n0 | _ = s≤s (s≤s lemma) where 123 nextc n n<k | suc n0 | _ = s≤s (s≤s lemma) where