Mercurial > hg > Members > kono > Proof > prob1

changeset 1:cdadc85bc754

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 18:48:31 +0900
parents 06002e20ce5c
children 0dcf08f3ff18
files prob1.agda
diffstat 1 files changed, 44 insertions(+), 41 deletions(-) [+]
line wrap: on
line diff
--- a/prob1.agda	Mon Nov 25 18:00:51 2019 +0900
+++ b/prob1.agda	Mon Nov 25 18:48:31 2019 +0900
@@ -49,60 +49,63 @@
 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)
 
-test1 : {A M : ℕ } → (c : Cond1 A M 1 ) → Cond1.n c ≡ 0 → A ≡ Cond1.i c
-test1 {A} {M} c refl = lemma2 where
-    lemma1 : Cond1.i c + 1 * M ≡ M * 1 + A
-    lemma1 = Cond1.rule1 c
-    lemma2 : A ≡  Cond1.i c
-    lemma2 = begin
-            A
-        ≡⟨  +m= ( begin
-            A + M * 1 
-        ≡⟨ +-comm A _ ⟩
-            M * 1 + A
-        ≡⟨ sym (Cond1.rule1 c)  ⟩
-            Cond1.i c + 1 * M
-        ≡⟨ cong ( λ k → Cond1.i c + k ) (*-comm 1 _ ) ⟩
-            Cond1.i c + M * 1
-        ∎ ) ⟩
-            Cond1.i c 
-        ∎  where open ≡-Reasoning
+problem : ( A M k : ℕ ) → Set 
+problem A M k =  (suc A <  k * M ) → Cond1 A M k
 
-problem0-k=1 : ( A M : ℕ ) → (suc A <  M ) → Cond1 A M 1
-problem0-k=1 A M A<km = record { n = 0 ; i = A ; range-n = s≤s z≤n ; range-i = less-1 A<km ; rule1 = lemma1 }
+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 = {!!}
+
+--       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 = {!!}
 
 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
+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 {!!}
+    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
+    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
+         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 = {!!}