Mercurial > hg > Members > kono > Proof > prob1
view prob1.agda @ 7:f5828d8af20c
...
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Tue, 26 Nov 2019 08:36:56 +0900 |
parents | fce6cadae300 |
children | cca92e69b629 |
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 Relation.Nullary minus : (a b : ℕ ) → ℕ minus a zero = a minus zero (suc b) = zero minus (suc a) (suc b) = minus a b m+= : {i j m : ℕ } → m + i ≡ m + j → i ≡ j m+= {i} {j} {zero} refl = refl m+= {i} {j} {suc m} eq = m+= {i} {j} {m} ( cong (λ k → pred k ) eq ) +m= : {i j m : ℕ } → i + m ≡ j + m → i ≡ j +m= {i} {j} {m} eq = m+= ( subst₂ (λ j k → j ≡ k ) (+-comm i _ ) (+-comm j _ ) eq ) less-1 : { n m : ℕ } → suc n < m → n < m less-1 {zero} {suc (suc _)} (s≤s (s≤s z≤n)) = s≤s z≤n less-1 {suc n} {suc m} (s≤s lt) = s≤s (less-1 {n} {m} lt) sa=b→a<b : { n m : ℕ } → suc n ≡ m → n < m sa=b→a<b {0} {suc zero} refl = s≤s z≤n sa=b→a<b {suc n} {suc (suc n)} refl = s≤s (sa=b→a<b refl) minus+n : {x y : ℕ } → suc x > y → minus x y + y ≡ x minus+n {x} {zero} _ = trans (sym (+-comm zero _ )) refl minus+n {zero} {suc y} (s≤s ()) minus+n {suc x} {suc y} (s≤s lt) = begin minus (suc x) (suc y) + suc y ≡⟨ +-comm _ (suc y) ⟩ suc y + minus x y ≡⟨ cong ( λ k → suc k ) ( begin y + minus x y ≡⟨ +-comm y _ ⟩ minus x y + y ≡⟨ minus+n {x} {y} lt ⟩ x ∎ ) ⟩ suc x ∎ where open ≡-Reasoning <-minus-0 : {x y z : ℕ } → z + x < z + y → x < y <-minus-0 {x} {suc _} {zero} lt = lt <-minus-0 {x} {y} {suc z} (s≤s lt) = <-minus-0 {x} {y} {z} lt <-minus : {x y z : ℕ } → x + z < y + z → x < y <-minus {x} {y} {z} lt = <-minus-0 ( subst₂ ( λ j k → j < k ) (+-comm x _) (+-comm y _ ) lt ) -- 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 open import Data.Product 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 M A<kM = cc k a<sa A<kM where cck : ( n : ℕ ) → n < suc k → (suc A > (minus k n ) * M ) → minus A (minus k n * M) < M → Cond1 A M (suc k) cck n n<k gt lt = record { n = n ; i = minus A ((minus k n) * M ) ; range-n = n<k ; range-i = lt ; rule1 = lemma2 } where lemma2 : minus A (minus k n * M) + suc k * M ≡ M * suc n + A lemma2 = begin minus A (minus k n * M) + suc k * M ≡⟨ cong ( λ x → minus A (minus k n * M) + suc x * M ) (sym (minus+n {k} {n} n<k )) ⟩ minus A (minus k n * M) + (suc ((minus k n ) + n )) * M ≡⟨ cong ( λ x → minus A (minus k n * M) + suc x * M ) (+-comm _ n) ⟩ minus A (minus k n * M) + (suc (n + (minus k n ) )) * M ≡⟨⟩ minus A (minus k n * M) + (suc n + (minus k n ) ) * M ≡⟨ cong ( λ x → minus A (minus k n * M) + x * M ) (+-comm (suc n) _) ⟩ minus A (minus k n * M) + ((minus k n ) + suc n ) * M ≡⟨ cong ( λ x → minus A (minus k n * M) + x ) (((proj₂ *-distrib-+)) M (minus k n) _ ) ⟩ minus A (minus k n * M) + ((minus k n * M) + (suc n) * M) ≡⟨ sym (+-assoc (minus A (minus k n * M)) _ ((suc n) * M)) ⟩ minus A (minus k n * M) + (minus k n * M) + (suc n) * M ≡⟨ cong ( λ x → x + (suc n) * M ) ( minus+n {A} {minus 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 i<range : {n : ℕ } → suc A < suc ((suc n) * M) → minus A (minus k n * M) < M i<range = {!!} gt : {n : ℕ } → suc A < suc ((suc n) * M) → (minus k n ) * M < suc A gt = {!!} next-lt : (n : ℕ ) → suc A < (suc n) * M → (A > (pred n * M)) → suc A < n * M next-lt n lt = {!!} cc : ( n : ℕ ) → n < suc k → suc A < (suc n) * M → Cond1 A M (suc k) cc 0 n<k lt = cck 0 n<k (gt {!!} ) (i<range {!!}) cc (suc n) n<k lt with <-cmp A (n * M) cc (suc n ) n<k lt | tri< a ¬b ¬c = cck (suc n) n<k (gt {!!} ) (i<range {!!}) cc (suc n ) n<k lt | tri≈ ¬a b ¬c = cck (suc n) n<k (gt {!!} ) (i<range {!!}) cc (suc n ) n<k lt | tri> ¬a ¬b c = cc n (less-1 n<k ) (next-lt (suc n) lt c ) 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 = {!!} problem1 : (A1 A2 M k : ℕ ) → (c1 : Cond1 A1 M k ) → (c2 : Cond1 A2 M k ) → ( A1 ≡ A2 ) → ( Cond1.n c1 ≡ Cond1.n c2 ) ∧ ( Cond1.i c1 ≡ Cond1.i c2 ) problem1 = {!!}