Mercurial > hg > Members > kono > Proof > prob1

changeset 8:cca92e69b629

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
almost done
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 26 Nov 2019 11:04:15 +0900
parents f5828d8af20c
children e0811846b265
files prob1.agda
diffstat 1 files changed, 63 insertions(+), 13 deletions(-) [+]
line wrap: on
line diff
--- a/prob1.agda	Tue Nov 26 08:36:56 2019 +0900
+++ b/prob1.agda	Tue Nov 26 11:04:15 2019 +0900
@@ -55,6 +55,29 @@
 <-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 )
 
+<-plus : {x y z : ℕ } → x < y → x + z < y + z 
+<-plus = {!!}
+
+distr-minus-* : {x y z : ℕ } → (minus x y) * z ≡ minus (x * z) (y * z) 
+distr-minus-* = {!!}
+
+minus- : {x y z : ℕ } → minus (minus x y) z ≡ minus x (y + z)
+minus- = {!!}
+
+minus-* : {M k n : ℕ } → minus k (suc n) * M ≡ minus (minus k n * M ) M
+minus-* {M} {k} {n} = begin
+           minus k (suc n) * M
+        ≡⟨ distr-minus-* {k} {suc n} {M}  ⟩
+           minus (k * M ) ((suc n) * M)
+        ≡⟨⟩
+           minus (k * M ) (M + n * M  )
+        ≡⟨ cong (λ x → minus (k * M) x) (+-comm M _ ) ⟩
+           minus (k * M ) ((n * M) + M )
+        ≡⟨ sym ( minus- {k * M} {n * M} ) ⟩
+           minus (minus (k * M ) (n * M)) M
+        ≡⟨ cong (λ x → minus x M ) ( sym ( distr-minus-* {k} {n} )) ⟩
+           minus (minus k n * M ) M
+        ∎  where open ≡-Reasoning
 
 -- All variables are positive integer
 -- A = -M*n + i +k*M  - M
@@ -87,7 +110,7 @@
 
 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
+problem0-k=k (suc k) A M A<kM = cc k a<sa (start-range k) 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
@@ -103,18 +126,45 @@
            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 )
+     --  loop on  range  of A : (minus k n ) * M ≤ A < (minus k n ) * M + M
+     cc : (n : ℕ) → n < suc k → suc A > minus 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 : minus A (minus 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 (minus A (minus 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
+        lemma2 : suc (minus k n * M) > M
+        lemma2 = {!!}
+        a=mk0 :  (minus A (minus k (suc n) * M)) ≡  M → A ≡ minus k n * M
+        a=mk0 a=mk = sym ( begin
+           minus k n * M 
+         ≡⟨ sym ( minus+n {minus k n * M} {M} lemma2 ) ⟩
+           minus (minus k n * M ) M + M
+         ≡⟨ +-comm _ M ⟩
+           M + minus (minus k n * M ) M
+         ≡⟨ cong (λ x → M + x ) (sym (minus-* {M} {k}  )) ⟩
+           M + (minus k (suc n) * M) 
+         ≡⟨ cong (λ x → x + minus k (suc n) * M) (sym a=mk) ⟩
+           minus A (minus k (suc n) * M) + (minus k (suc n) * M) 
+         ≡⟨ minus+n {A} {minus k (suc n) * M} k<A ⟩
+           A
+         ∎ ) where open ≡-Reasoning
+        lemma1 : (minus A (minus k (suc n) * M)) ≡  M → suc A > minus k n * M
+        lemma1 a=mk = subst (λ x → minus 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 + minus k (suc n) * M → A > M + minus k n - M → A >  minus k n
+        lemma3 : (minus A (minus k (suc n) * M)) > M  → suc A > minus k n * M
+        lemma3 mk<a = <-trans lemma5 a<sa where
+            lemma4 : (M + minus k (suc n) * M) < A
+            lemma4 = subst (λ x → (M + minus k (suc n) * M)  < x ) (minus+n {A}{minus k (suc n) * M} {!!} ) ( <-plus mk<a )
+            lemma5 : minus k n * M < A
+            lemma5 = subst (λ x → x < A ) {!!} lemma4
+     start-range : (k : ℕ ) → suc A > minus 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