Mercurial > hg > Members > kono > Proof > prob1
view prob1.agda @ 24:0b53b08e7ae4
...
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Mon, 30 Mar 2020 02:10:49 +0900 |
parents | f2db03a8af2c |
children | 805986409de4 |
line wrap: on
line source
module prob1 where open import Relation.Binary.PropositionalEquality open import Relation.Binary.Core open import Data.Nat open import Data.Nat.Properties open import logic open import nat open import Data.Empty open import Data.Product open import Relation.Nullary -- open import Relation.Binary.Definitions -- All variables are positive integer -- A = -M*n + i +k*M - M -- where n is in range (0,…,k-1) and i is in range(0,…,M-1) -- Goal: Prove that A can take all values of (0,…,k*M-1) -- A1 = -M*n1 + i1 +k*M M, A2 = -M*n2 + i2 +k*M - M -- (1) If n1!=n2 or i1!=i2 then A1!=A2 -- Or its contraposition: (2) if A1=A2 then n1=n2 and i1=i2 -- Proof by contradiction: Suppose A1=A2 and (n1!=n2 or i1!=i2) becomes -- contradiction -- Induction on n and i record Cond1 (A M k : ℕ ) : Set where field n : ℕ i : ℕ range-n : n < k range-i : i < M rule1 : i + k * M ≡ M * (suc n) + A -- A ≡ (i + k * M ) - (M * (suc n)) -- k = 1 → n = 0 → ∀ M → A = i -- k = 2 → n = 1 → -- i + 2 * M = M * (suc n) + A i = suc n → A = 0 problem : ( A M k : ℕ ) → Set problem A M k = (suc A < k * M ) → Cond1 A M k problem0-k=k : ( k A M : ℕ ) → problem A M k problem0-k=k zero A M () problem0-k=k (suc k) A zero A<kM = ⊥-elim ( nat-<> A<kM (subst (λ x → x < suc A) (*-comm _ k ) 0<s )) problem0-k=k (suc k) A (suc m) A<kM = cc k a<sa (start-range k) module kk where M = suc m cck : ( n : ℕ ) → n < suc k → (suc A > ((k - n) ) * M ) → A - ((k - n) * M) < M → Cond1 A M (suc k) cck n n<k gt lt = record { n = n ; i = A - (((k - n)) * M ) ; range-n = n<k ; range-i = lt ; rule1 = lemma2 } where lemma2 : A - ((k - n) * M) + suc k * M ≡ M * suc n + A lemma2 = begin A - ((k - n) * M) + suc k * M ≡⟨ cong ( λ x → A - ((k - n) * M) + suc x * M ) (sym (minus+n {k} {n} n<k )) ⟩ A - ((k - n) * M) + (suc (((k - n) ) + n )) * M ≡⟨ cong ( λ x → A - ((k - n) * M) + suc x * M ) (+-comm _ n) ⟩ A - ((k - n) * M) + (suc (n + ((k - n) ) )) * M ≡⟨⟩ A - ((k - n) * M) + (suc n + ((k - n) ) ) * M ≡⟨ cong ( λ x → A - ((k - n) * M) + x * M ) (+-comm (suc n) _) ⟩ A - ((k - n) * M) + (((k - n) ) + suc n ) * M ≡⟨ cong ( λ x → A - ((k - n) * M) + x ) (((proj₂ *-distrib-+)) M ((k - n)) _ ) ⟩ A - ((k - n) * M) + (((k - n) * M) + (suc n) * M) ≡⟨ sym (+-assoc (A - ((k - n) * M)) _ ((suc n) * M)) ⟩ A - ((k - n) * M) + ((k - n) * M) + (suc n) * M ≡⟨ cong ( λ x → x + (suc n) * M ) ( minus+n {A} {(k - n) * M} gt ) ⟩ A + (suc n) * M ≡⟨ cong ( λ k → A + k ) (*-comm (suc n) _ ) ⟩ A + M * (suc n) ≡⟨ +-comm A _ ⟩ M * (suc n) + A ∎ where open ≡-Reasoning nM<kM : {n : ℕ } → suc n < suc k → n * M < k * M nM<kM {n} n<k = *< {n} {k} {m} ( <-minus-0 n<k ) -- loop on range of A : ((k - n) ) * M ≤ A < ((k - n) ) * M + M nextc : (n : ℕ ) → (suc n < suc k) → M < suc ((k - n) * M) nextc n n<k with k - n | inspect (_-_ k) n nextc n n<k | 0 | record { eq = e } = ⊥-elim ( nat-≡< (sym e) (minus>0 n<k) ) nextc n n<k | suc n0 | _ = s≤s (s≤s lemma) where lemma : m ≤ m + n0 * suc m lemma = x≤x+y cc : (n : ℕ) → n < suc k → suc A > (k - n) * M → Cond1 A M (suc k) cc zero n<k k<A = cck 0 n<k k<A lemma where a<m : suc A < M + k * M a<m = A<kM lemma : A - ((k - 0) * M) < M lemma = <-minus {_} {_} {k * M} (subst (λ x → x < M + k * M) (sym (minus+n {A} {k * M} k<A )) (less-1 a<m) ) cc (suc n) n<k k<A with <-cmp (A - ((k - (suc n)) * M)) M cc (suc n) n<k k<A | tri< a ¬b ¬c = cck (suc n) n<k k<A a cc (suc n) n<k k<A | tri≈ ¬a b ¬c = cc n (less-1 n<k) (lemma1 b) where a=mk0 : (A - ((k - (suc n)) * M)) ≡ M → A ≡ (k - n) * M a=mk0 a=mk = sym ( begin (k - n) * M ≡⟨ sym ( minus+n {(k - n) * M} {M} (nextc n n<k )) ⟩ ((k - n) * M ) - M + M ≡⟨ +-comm _ M ⟩ M + (((k - n) * M ) - M) ≡⟨ cong (λ x → M + x ) (sym (minus-* {M} {k} (<-minus-0 n<k ))) ⟩ M + (k - (suc n) * M) ≡⟨ cong (λ x → x + (k - (suc n)) * M) (sym a=mk) ⟩ A - ((k - (suc n)) * M) + ((k - (suc n)) * M) ≡⟨ minus+n {A} {(k - (suc n)) * M} k<A ⟩ A ∎ ) where open ≡-Reasoning lemma1 : (A - ((k - (suc n)) * M)) ≡ M → suc A > (k - n) * M lemma1 a=mk = subst (λ x → (k - n) * M < suc x ) (sym (a=mk0 a=mk )) a<sa cc (suc n) n<k k<A | tri> ¬a ¬b c = cc n (less-1 n<k) (lemma3 c) where -- A > M + (k - (suc n)) * M → A > M + (k - n) - M → A > (k - n) lemma3 : (A - ((k - (suc n)) * M)) > M → suc A > (k - n) * M lemma3 mk<a = <-trans lemma5 a<sa where lemma6 : M + (k - (suc n)) * M ≡ (k - n) * M lemma6 = begin M + (k - (suc n)) * M ≡⟨ cong (λ x → M + x) (minus-* {M} {k} (<-minus-0 n<k)) ⟩ M + (((k - n) * M ) - M ) ≡⟨ +-comm M _ ⟩ ((k - n) * M ) - M + M ≡⟨ minus+n {_} {M} (nextc n n<k) ⟩ (k - n) * M ∎ where open ≡-Reasoning lemma4 : (M + (k - (suc n)) * M) < A lemma4 = subst (λ x → (M + (k - (suc n)) * M) < x ) (minus+n {A}{(k - (suc n)) * M} k<A ) ( <-plus mk<a ) lemma5 : (k - n) * M < A lemma5 = subst (λ x → x < A ) lemma6 lemma4 start-range : (k : ℕ ) → suc A > (k - k) * M start-range zero = s≤s z≤n start-range (suc k) = start-range k -- problem0 : ( A M k : ℕ ) → M > 0 → k > 0 → (suc A < k * M ) → Cond1 A M k -- problem0 A (suc M) (suc k) 0<M 0<k A<kM = lemma1 k M A<kM a<sa a<sa where -- --- i loop in n loop -- lemma1-i : ( n i : ℕ ) → (suc A < suc k * suc M ) → n < suc k → i < suc M → Dec ( Cond1 A (suc M) (suc k) ) -- lemma1-i n zero A<kM _ _ with <-cmp (1 + suc k * suc M ) ( suc M * suc n + A) -- lemma1-i n zero A<kM _ _ | tri< a ¬b ¬c = no {!!} -- 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 } -- lemma1-i n zero A<kM _ _ | tri> ¬a ¬b c = no {!!} -- lemma1-i n (suc i) A<kM _ _ with <-cmp (suc i + suc k * suc M ) ( suc M * suc n + A) -- 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 } -- 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) -- lemma1-i n (suc i) A<kM n<k i<M | tri> ¬a ¬b c = no {!!} -- --- n loop -- lemma1 : ( n i : ℕ ) → (suc A < suc k * suc M ) → n < suc k → i < suc M → Cond1 A (suc M) (suc k) -- lemma1 n i A<kM _ _ with <-cmp (i + suc k * suc M ) ( suc M * suc n + A) -- 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 } -- lemma1 zero i A<kM n<k i<M | tri< a ¬b ¬c = lemma2 i A<kM i<M where -- --- i + k * M ≡ M + A case -- lemma2 : ( i : ℕ ) → (suc A < suc k * suc M ) → i < suc M → Cond1 A (suc M) (suc k) -- lemma2 zero A<kM i<M = {!!} -- A = A = k * M -- lemma2 (suc i) A<kM i<M with <-cmp ( suc i + suc k * suc M ) ( suc M * 1 + A) -- 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 } -- lemma2 (suc i) A<kM i<M | tri< a ¬b ¬c = lemma2 i A<kM (less-1 i<M) -- lemma2 (suc i) A<kM i<M | tri> ¬a ¬b c = {!!} -- can't happen -- 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 -- lemma1 (suc n) i A<kM n<k i<M | tri< a ¬b ¬c | yes p = p -- 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 -- lemma1 n i A<kM n<k i<M | tri> ¬a ¬b c = {!!} where -- can't happen -- 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 ) -- cannot1 = {!!} -- range-n : n < k -- range-i : i < M -- rule1 : i + k * M ≡ M * (suc n) + A -- A ≡ (i + k * M ) - (M * (suc n)) record UCond1 (A M k : ℕ ) : Set where field c1 : Cond1 A M k u1 : {j m : ℕ} → j < Cond1.i c1 → m < k → ¬ ( j + k * M ≡ M * (suc m) + A ) -- u2 : {j m : ℕ} → Cond1.i c1 < j → j < M → m < k → ¬ ( j + k * M ≡ M * (suc m) + A ) -- u3 : {j m : ℕ} → j < M → m < Cond1.n c1 → ¬ ( j + k * M ≡ M * (suc m) + A ) -- u4 : {j m : ℕ} → j < M → Cond1.n c1 < m → m < k → ¬ ( j + k * M ≡ M * (suc m) + A ) problem1-0 : (k A M : ℕ ) → (A<kM : suc A < k * M ) → UCond1 A M k problem1-0 zero A M () problem1-0 (suc k) A zero A<kM = ⊥-elim ( nat-<> A<kM (subst (λ x → x < suc A) (*-comm _ k ) 0<s )) problem1-0 (suc k) A (suc m) A<kM = cc k a<sa (start-range k) where M = suc m cck : ( n : ℕ ) → n < suc k → (suc A > ((k - n) ) * M ) → A - ((k - n) * M) < M → UCond1 A M (suc k) cck n n<k k<A i<M = c0 where c1 : Cond1 A M (suc k) c1 = kk.cck k A m A<kM n n<k k<A i<M lemma4 : {i j x y z : ℕ} → j + x ≡ y → i + x ≡ z → j < i → y < z lemma4 {i} {j} {x} refl refl (s≤s z≤n) = s≤s (subst (λ k → x ≤ k ) (+-comm x _) x≤x+y) lemma4 refl refl (s≤s (s≤s lt)) = s≤s (lemma4 refl refl (s≤s lt) ) lemma5 : {m1 : ℕ} → M * suc m1 + A < M * suc n + A → M + (M * suc m1 + A) ≤ M * suc n + A lemma5 = {!!} lemma6 : {i j x : ℕ} → M + (j + x ) ≤ i + x → M ≤ i lemma6 {i} {j} {x} lt = ≤-minus {M} {i} {x} (x+y≤z→x≤z ( begin M + x + j ≡⟨ +-assoc M _ _ ⟩ M + (x + j ) ≡⟨ cong (λ k → M + k ) (+-comm x _ ) ⟩ M + (j + x) ≤⟨ lt ⟩ i + x ∎ )) where open ≤-Reasoning lemma-u1 : {j : ℕ} {m1 : ℕ} → j < (A - ((k - n) * M)) → m1 < suc k → ¬ j + suc k * M ≡ M * suc m1 + A lemma-u1 {j} {m1} j<akM m1<k eq with <-cmp j M lemma-u1 {j} {m1} j<akM m1<k eq | tri< a ¬b ¬c = ⊥-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 lemma3 : M + (M * suc m1 + A) ≤ M * suc n + A lemma3 = lemma5 (lemma4 eq (Cond1.rule1 c1) j<akM) lemma-u1 {j} {m1} j<akM m1<k eq | tri≈ ¬a b ¬c = ⊥-elim (nat-≡< b ( (≤-trans j<akM (≤-trans refl-≤s i<M )))) lemma-u1 {j} {m1} j<akM m1<k eq | tri> ¬a ¬b c = ⊥-elim (nat-<> (≤-trans i<M (less-1 c)) j<akM ) 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 } cc : (n : ℕ) → n < suc k → suc A > (k - n) * M → UCond1 A M (suc k) cc zero n<k k<A = cck 0 n<k k<A lemma where a<m : suc A < M + k * M a<m = A<kM lemma : A - ((k - 0) * M) < M lemma = <-minus {_} {_} {k * M} (subst (λ x → x < M + k * M) (sym (minus+n {A} {k * M} k<A )) (less-1 a<m) ) cc (suc n) n<k k<A with <-cmp (A - ((k - (suc n)) * M)) M cc (suc n) n<k k<A | tri< a ¬b ¬c = cck (suc n) n<k k<A a cc (suc n) n<k k<A | tri≈ ¬a b ¬c = cc n (less-1 n<k) (lemma1 b) where a=mk0 : (A - ((k - (suc n)) * M)) ≡ M → A ≡ (k - n) * M a=mk0 a=mk = sym ( begin (k - n) * M ≡⟨ sym ( minus+n {(k - n) * M} {M} (kk.nextc k A m A<kM n n<k )) ⟩ ((k - n) * M ) - M + M ≡⟨ +-comm _ M ⟩ M + (((k - n) * M ) - M) ≡⟨ cong (λ x → M + x ) (sym (minus-* {M} {k} (<-minus-0 n<k ))) ⟩ M + (k - (suc n) * M) ≡⟨ cong (λ x → x + (k - (suc n)) * M) (sym a=mk) ⟩ A - ((k - (suc n)) * M) + ((k - (suc n)) * M) ≡⟨ minus+n {A} {(k - (suc n)) * M} k<A ⟩ A ∎ ) where open ≡-Reasoning lemma1 : (A - ((k - (suc n)) * M)) ≡ M → suc A > (k - n) * M lemma1 a=mk = subst (λ x → (k - n) * M < suc x ) (sym (a=mk0 a=mk )) a<sa cc (suc n) n<k k<A | tri> ¬a ¬b c = cc n (less-1 n<k) (lemma3 c) where lemma3 : (A - ((k - (suc n)) * M)) > M → suc A > (k - n) * M lemma3 mk<a = <-trans lemma5 a<sa where lemma6 : M + (k - (suc n)) * M ≡ (k - n) * M lemma6 = begin M + (k - (suc n)) * M ≡⟨ cong (λ x → M + x) (minus-* {M} {k} (<-minus-0 n<k)) ⟩ M + (((k - n) * M ) - M ) ≡⟨ +-comm M _ ⟩ ((k - n) * M ) - M + M ≡⟨ minus+n {_} {M} (kk.nextc k A m A<kM n n<k ) ⟩ (k - n) * M ∎ where open ≡-Reasoning lemma4 : (M + (k - (suc n)) * M) < A lemma4 = subst (λ x → (M + (k - (suc n)) * M) < x ) (minus+n {A}{(k - (suc n)) * M} k<A ) ( <-plus mk<a ) lemma5 : (k - n) * M < A lemma5 = subst (λ x → x < A ) lemma6 lemma4 start-range : (k : ℕ ) → suc A > (k - k) * M start-range zero = s≤s z≤n start-range (suc k) = start-range k