Mercurial > hg > Members > kono > Proof > prob1

changeset 2:0dcf08f3ff18

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 Mon, 25 Nov 2019 21:05:25 +0900
parents cdadc85bc754
children e909c828cefe
files prob1.agda
diffstat 1 files changed, 72 insertions(+), 35 deletions(-) [+]
line wrap: on
line diff
--- a/prob1.agda	Mon Nov 25 18:48:31 2019 +0900
+++ b/prob1.agda	Mon Nov 25 21:05:25 2019 +0900
@@ -14,6 +14,42 @@
 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)
+
+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 : {x y z : ℕ } → x + z < y + z → x < y
+<-minus = {!!}
+
+
+-- trans (sym (+-comm (suc y) _ )) (cong ( λ k → suc k ) {!!} ) -- (trans ? (+-comm _  _ ) )
+
 -- 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)
@@ -38,45 +74,46 @@
 
 --   i + 2 * M = M * (suc n) + A    i = suc n → A = 0 
 
-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)
-
 problem : ( A M k : ℕ ) → Set 
 problem A M k =  (suc A <  k * M ) → Cond1 A M k
 
-problem0-k=1 : ( A M : ℕ ) → problem A M 1 
-problem0-k=1 A M A<kM = record { n = 0 ; i = A ; range-n = s≤s z≤n ; range-i = {!!} ; rule1 = lemma1 }
-  where
-    lemma1 : A + 1 * M ≡ M * 1 + A
-    lemma1 = trans (+-comm A _) ( cong ( λ k → k + A ) ( *-comm _ M ) )
-
-cc : (A M k : ℕ ) → (suc A <  k * M ) → Cond1 A M k
-cc A M k A<kM = {!!}
-
-next-cc : (A M k : ℕ ) → ((suc A <  k * M ) → Cond1 A M k) → (suc A <  (suc k ) * M )  → Cond1 A M (suc k)
-next-cc A M k A<kM cc = {!!}
+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 where
+     ccn :  (suc (suc A) >  k * M )  →  Cond1 A M (suc k)
+     ccn gt =  record { n = 0 ; i = minus A (k * M ) ; range-n = s≤s z≤n ; range-i = A-Mk<M {!!} A<kM ; rule1 = lemma1 } where
+        A-Mk<M : {k A M : ℕ } → (suc A >  k * M ) → ( suc A <  (suc k ) * M ) → minus A (k * M ) < M
+        A-Mk<M {k} {A} {M} lt1 lt2 = <-minus ( subst₂ (λ j k → j <  k ) (sym (minus+n {A} {k * M} lt1 )) refl (<-trans a<sa lt2) )
+        lemma1 : minus A (k * M) + suc k * M ≡ M * 1 + A
+        lemma1 = begin
+              minus A (k * M) + suc k * M 
+           ≡⟨⟩
+              minus A (k * M) + (M + k * M )
+           ≡⟨ cong ( λ x → minus A (k * M) + x ) (+-comm M _ ) ⟩
+              minus A (k * M) + (k * M + M )
+           ≡⟨ sym ( +-assoc _ (k * M ) M ) ⟩
+              (minus A (k * M) + k * M ) + M 
+           ≡⟨ cong ( λ k → k + M ) (minus+n {A} {k * M} ? ) ⟩
+              A + M 
+           ≡⟨⟩
+              A + ( 0 + M )
+           ≡⟨ cong ( λ k → A + k ) (+-comm 0 _ )  ⟩
+              A + ( M + 0 )
+           ≡⟨⟩
+              A + 1 * M 
+           ≡⟨ cong ( λ k → A + k ) (*-comm 1 _ )  ⟩
+              A + M * 1
+           ≡⟨ +-comm A _ ⟩
+              M * 1 + A
+           ∎  where open ≡-Reasoning
 
---       rule1 : i + k * M  ≡ M * (suc n) + A    -- A ≡ (i + k * M ) - (M * (suc n)) 
-problem0-k=2 : ( A M : ℕ ) → problem A M 2 
-problem0-k=2 A M A<kM = lemma where
-     cc1 : M < suc A → Cond1 A M 2
-     cc1 M<A = record { n = 0 ; i = minus A M ; range-n = s≤s z≤n ; range-i = {!!} ; rule1 = {!!} }
-     lemma : Cond1 A M 2
-     lemma with <-cmp A M
-     ... |  tri< a ¬b ¬c = record { n = 1 ; i = A ; range-n = s≤s (s≤s z≤n) ; range-i = a ; rule1 = {!!} }
-     ... |  tri≈ ¬a b ¬c = {!!}
-     ... |  tri> ¬a ¬b c = {!!}
-
-problem0-k=k : ( k A M : ℕ ) → problem A M k
-problem0-k=k k A M = {!!}
+     next-cc : (A M k : ℕ ) → ((suc A <  k * M ) → Cond1 A M k) → (suc A <  k * M )  → Cond1 A M (suc k)
+     next-cc A M k cc A<kM = record { n = k ; i = Cond1.i (cc A<kM )  ; range-n = {!!} ; range-i = Cond1.range-i (cc A<kM ) ; rule1 = {!!} }
+     cc :  Cond1 A M (suc k)
+     cc with <-cmp (suc A) (k * M)
+     cc | tri< a ¬b ¬c = next-cc A M k ( problem0-k=k k A M ) a 
+     cc | tri≈ ¬a b ¬c = ccn (subst (λ x → x > k * M ) (cong (λ k → suc k) (sym b )) a<sa  )
+     cc | tri> ¬a ¬b c = ccn (<-trans c a<sa)
 
 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