Mercurial > hg > Members > kono > Proof > prob1
view prob1.agda @ 18:e35d729efd58
fix
author | kono |
---|---|
date | Fri, 27 Mar 2020 14:37:08 +0900 |
parents | 61a889d975e1 |
children | 9f5bf86fe6dd |
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) 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)) problem1-0 : (A M k : ℕ ) → (x : suc A < k * M ) → (c1 : Cond1 A M k ) → Cond1.i c1 ≡ Cond1.i (problem0-k=k k A M x) problem1-0 A (suc m) (suc k) x c1 = {!!} where -- 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 → ( Cond1.i c1 ≡ Cond1.i (problem0-k=k k A M {!!}) ) cck n n<k k<A i<M = {!!} where c0 = record { n = n ; i = A - (((k - n)) * M ) ; range-n = n<k ; range-i = {!!} ; rule1 = {!!} } lemma-i : (i : ℕ ) → i < M → i + suc k * M ≡ M * suc n + A → i ≡ A - (k - n) * M lemma-i = {!!} lemma-n : (n1 : ℕ ) → ¬ ( n1 ≡ n ) → ¬ ( ( i : ℕ ) → i < M → i + suc k * M ≡ M * suc n1 + A → i ≡ A - (k - n1) * M ) lemma-n = {!!} cc : (n : ℕ) → n < suc k → suc A > (k - n) * M → ( Cond1.i c1 ≡ Cond1.i (problem0-k=k k A M {!!}) ) cc zero n<k k<A = cck 0 n<k k<A {!!} 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 {!!} cc (suc n) n<k k<A | tri≈ ¬a b ¬c = {!!} cc (suc n) n<k k<A | tri> ¬a ¬b c = {!!} start-range : (k : ℕ ) → suc A > (k - k) * M start-range zero = s≤s z≤n start-range (suc k) = start-range k