Mercurial > hg > Members > kono > Proof > prob1

changeset 13:0e63ca7fd224

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 27 Nov 2019 09:35:08 +0900
parents a30f516a3fdf
children 8415d3f77fe0
files prob1.agda
diffstat 1 files changed, 48 insertions(+), 24 deletions(-) [+]
line wrap: on
line diff
--- a/prob1.agda	Tue Nov 26 18:06:53 2019 +0900
+++ b/prob1.agda	Wed Nov 27 09:35:08 2019 +0900
@@ -70,37 +70,57 @@
 x+y<z→x<z {zero} {y} {suc z} (s≤s lt1) = s≤s z≤n
 x+y<z→x<z {suc x} {y} {suc z} (s≤s lt1) = s≤s ( x+y<z→x<z {x} {y} {z} lt1 )
 
--- <-plus-0 (subst₂ ( λ j k → j < k ) (+-comm _  _ ) (+-comm _ _) (<-plus-0 {x} {y} {z} lt ) )
+*< : {x y z : ℕ } → x ≤ y → x * z ≤ y * z 
+*< lt = *-mono-≤ lt ≤-refl
+
+≤to< : {x y  : ℕ } → x < y → x ≤ y 
+≤to< {zero} {suc y} (s≤s z≤n) = z≤n
+≤to< {suc x} {suc y} (s≤s lt) = s≤s (≤to< {x} {y}  lt)
+
+refl-≤s : {x : ℕ } → x ≤ suc x
+refl-≤s {zero} = z≤n
+refl-≤s {suc x} = s≤s (refl-≤s {x})
+
+x<y→≤ : {x y : ℕ } → x < y →  x ≤ suc y
+x<y→≤ {zero} {.(suc _)} (s≤s z≤n) = z≤n
+x<y→≤ {suc x} {suc y} (s≤s lt) = s≤s (x<y→≤ {x} {y} lt)
 
 open import Data.Product
 
-minus<=0 : {x y : ℕ } → x < y → minus x y ≡ 0
-minus<=0 {zero} {.(suc _)} (s≤s lt) = refl
-minus<=0 {suc x} {suc y} (s≤s lt) = minus<=0 {x} {y} lt
+minus<=0 : {x y : ℕ } → x ≤ y → minus x y ≡ 0
+minus<=0 {0} {zero} z≤n = refl
+minus<=0 {0} {suc y} z≤n = refl
+minus<=0 {suc x} {suc y} (s≤s le) = minus<=0 {x} {y} le
 
 distr-minus-* : {x y z : ℕ } → (minus x y) * z ≡ minus (x * z) (y * z) 
 distr-minus-* {x} {zero} {z} = refl
 distr-minus-* {x} {suc y} {z} with <-cmp x y
 distr-minus-* {x} {suc y} {z} | tri< a ¬b ¬c = begin
           minus x (suc y) * z
-        ≡⟨ cong (λ k → k * z ) (minus<=0 {x} {suc y} (<-trans a a<sa )) ⟩
+        ≡⟨ cong (λ k → k * z ) (minus<=0 {x} {suc y} (x<y→≤ a)) ⟩
            0 * z 
-        ≡⟨ sym (minus<=0 {x * z} {z + y * z} lt ) ⟩
+        ≡⟨ sym (minus<=0 {x * z} {z + y * z} le ) ⟩
           minus (x * z) (z + y * z) 
         ∎  where
             open ≡-Reasoning
-            lt : x * z < z + y * z
-            lt = {!!}
+            le : x * z ≤ z + y * z
+            le  = ≤-trans lemma (subst (λ k → y * z ≤ k ) (+-comm _ z ) (x≤x+y {y * z} {z} ) ) where
+               lemma : x * z ≤ y * z
+               lemma = *< {x} {y} {z} (≤to< a)
 distr-minus-* {x} {suc y} {z} | tri≈ ¬a refl ¬c = begin
           minus x (suc y) * z
-        ≡⟨ cong (λ k → k * z ) (minus<=0 {x} {suc y} a<sa) ⟩
+        ≡⟨ cong (λ k → k * z ) (minus<=0 {x} {suc y} refl-≤s ) ⟩
            0 * z 
-        ≡⟨ sym (minus<=0 {x * z} {z + y * z} lt ) ⟩
+        ≡⟨ sym (minus<=0 {x * z} {z + y * z} (lt {x} {z} )) ⟩
           minus (x * z) (z + y * z) 
         ∎  where
             open ≡-Reasoning
-            lt : x * z < z + y * z
-            lt = {!!}
+            lt : {x z : ℕ } →  x * z ≤ z + x * z
+            lt {zero} {zero} = z≤n
+            lt {suc x} {zero} = lt {x} {zero}
+            lt {x} {suc z} = ≤-trans lemma refl-≤s where
+               lemma : x * suc z ≤   z + x * suc z
+               lemma = subst (λ k → x * suc z ≤ k ) (+-comm _ z) (x≤x+y {x * suc z} {z}) 
 distr-minus-* {x} {suc y} {z} | tri> ¬a ¬b c = +m= {_} {_} {suc y * z} ( begin
            minus x (suc y) * z + suc y * z
         ≡⟨ sym (proj₂ *-distrib-+ z  (minus x (suc y) )  _) ⟩
@@ -111,8 +131,8 @@
            minus (x * z) (suc y * z) + suc y * z
         ∎ ) where
             open ≡-Reasoning
-            lt : y < x → z + y * z ≤ x * z
-            lt = {!!}
+            lt : {x y z : ℕ } → suc y ≤ x → z + y * z ≤ x * z
+            lt {x} {y} {z} le = *< le 
 
 minus- : {x y z : ℕ } → suc x > z + y → minus (minus x y) z ≡ minus x (y + z)
 minus- {x} {y} {z} gt = +m= {_} {_} {z} ( begin
@@ -138,8 +158,8 @@
              lemma : suc (minus x y) > z
              lemma = <-minus {_} {_} {y} ( subst ( λ x → z + y < suc x ) (sym (minus+n {x} {y}  lemma1 ))  gt )
 
-minus-* : {M k n : ℕ } → minus k (suc n) * M ≡ minus (minus k n * M ) M
-minus-* {M} {k} {n} = begin
+minus-* : {M k n : ℕ } → suc (k * M) > M + n * M → minus k (suc n) * M ≡ minus (minus k n * M ) M
+minus-* {M} {k} {n} lt = begin
            minus k (suc n) * M
         ≡⟨ distr-minus-* {k} {suc n} {M}  ⟩
            minus (k * M ) ((suc n) * M)
@@ -147,7 +167,7 @@
            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} {!!} ) ⟩
+        ≡⟨ sym ( minus- {k * M} {n * M} lt ) ⟩
            minus (minus (k * M ) (n * M)) M
         ≡⟨ cong (λ x → minus x M ) ( sym ( distr-minus-* {k} {n} )) ⟩
            minus (minus k n * M ) M
@@ -182,7 +202,9 @@
 
 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 (start-range k) where
+problem0-k=k (suc k) A zero A<kM = {!!} 
+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 >  (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
@@ -199,8 +221,10 @@
            M * (suc n) + A
           ∎  where open ≡-Reasoning
      --  loop on  range  of A : (minus k n ) * M ≤ A < (minus k n ) * M + M
-     lemma2 : (n : ℕ ) → suc (minus k n * M) > M
-     lemma2 = {!!}
+     nextc : (n : ℕ ) → (suc n < suc k) → suc (minus k n * M) > M --  M + n * M < suc (minus k n * M) + n * M
+     nextc n n<k = <-minus {_} {_} {n * M} ( subst ( λ x → M + n * M < suc x + n * M ) (sym ( distr-minus-* {k} {n} {M} )) lemma ) where
+          lemma : M + n * M < suc (minus (k * M) (n * M)) + n * M
+          lemma = subst ( λ x → suc n * M < suc x ) (sym (minus+n {k * M} {n * 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 
@@ -213,11 +237,11 @@
         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 n)) ⟩
+         ≡⟨ sym ( minus+n {minus k n * M} {M} (nextc n n<k )) ⟩
            minus (minus k n * M ) M + M
          ≡⟨ +-comm _ M ⟩
            M + minus (minus k n * M ) M
-         ≡⟨ cong (λ x → M + x ) (sym (minus-* {M} {k}  )) ⟩
+         ≡⟨ 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) 
@@ -233,11 +257,11 @@
             lemma6 :  M + minus k (suc n) * M ≡ minus k n * M
             lemma6 = begin
                   M + minus k (suc n) * M 
-               ≡⟨ cong (λ x → M + x) (minus-* {M} {k}  )  ⟩
+               ≡⟨ cong (λ x → M + x) (minus-* {M} {k} {!!} )  ⟩
                   M + minus (minus k n * M ) M
                ≡⟨ +-comm M _ ⟩
                   minus (minus k n * M ) M + M
-               ≡⟨ minus+n {_} {M} (lemma2 n) ⟩
+               ≡⟨ minus+n {_} {M} (nextc n n<k) ⟩
                   minus k n * M
                ∎  where open ≡-Reasoning
             lemma4 : (M + minus k (suc n) * M) < A