Mercurial > hg > Members > kono > Proof > prob1

changeset 12:a30f516a3fdf

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 Tue, 26 Nov 2019 18:06:53 +0900
parents ee2309eb1f5d
children 0e63ca7fd224
files prob1.agda
diffstat 1 files changed, 70 insertions(+), 33 deletions(-) [+]
line wrap: on
line diff
--- a/prob1.agda	Tue Nov 26 16:23:35 2019 +0900
+++ b/prob1.agda	Tue Nov 26 18:06:53 2019 +0900
@@ -72,8 +72,47 @@
 
 -- <-plus-0 (subst₂ ( λ j k → j < k ) (+-comm _  _ ) (+-comm _ _) (<-plus-0 {x} {y} {z} 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
+
 distr-minus-* : {x y z : ℕ } → (minus x y) * z ≡ minus (x * z) (y * z) 
-distr-minus-* = {!!}
+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 )) ⟩
+           0 * z 
+        ≡⟨ sym (minus<=0 {x * z} {z + y * z} lt ) ⟩
+          minus (x * z) (z + y * z) 
+        ∎  where
+            open ≡-Reasoning
+            lt : x * z < z + y * z
+            lt = {!!}
+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) ⟩
+           0 * z 
+        ≡⟨ sym (minus<=0 {x * z} {z + y * z} lt ) ⟩
+          minus (x * z) (z + y * z) 
+        ∎  where
+            open ≡-Reasoning
+            lt : x * z < z + y * z
+            lt = {!!}
+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) )  _) ⟩
+           ( minus x (suc y) + suc y ) * z
+        ≡⟨ cong (λ k → k * z) (minus+n {x} {suc y} (s≤s c))  ⟩
+           x * z 
+        ≡⟨ sym (minus+n {x * z} {suc y * z} (s≤s (lt c))) ⟩
+           minus (x * z) (suc y * z) + suc y * z
+        ∎ ) where
+            open ≡-Reasoning
+            lt : y < x → z + y * z ≤ x * z
+            lt = {!!}
 
 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 +177,6 @@
 
 --   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
 
@@ -211,36 +248,36 @@
      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 = {!!}
+-- 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 )