Mercurial > hg > Members > kono > Proof > prob1

changeset 26:fd8633b6d551

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
clean up
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 30 Mar 2020 10:31:16 +0900
parents 805986409de4
children 73511e7ddf5c
files prob1.agda
diffstat 1 files changed, 26 insertions(+), 121 deletions(-) [+]
line wrap: on
line diff
--- a/prob1.agda	Mon Mar 30 03:50:30 2020 +0900
+++ b/prob1.agda	Mon Mar 30 10:31:16 2020 +0900
@@ -34,16 +34,19 @@
 --   k = 2 → n = 1 →
 --   i + 2 * M = M * (suc n) + A    i = suc n → A = 0 
 
-problem : ( A M k : ℕ ) → Set 
-problem A M k =  (suc A <  k * M ) → Cond1 A M k
-
-
+record UCond1 (A M k : ℕ )  : Set where
+   field
+      c1 : Cond1 A M k
+      u1 : {j m : ℕ} → j < Cond1.i c1  → m < k   → ¬ ( j + k * M  ≡ M * (suc m) + A    )
+      -- u2 : {j m : ℕ} → Cond1.i c1  < j → j < M  → m < k   → ¬ ( j + k * M  ≡ M * (suc m) + A    )
+      -- u3 : {j m : ℕ} → j < M → m < Cond1.n c1  → ¬ ( j + k * M  ≡ M * (suc m) + A    )
+      -- u4 : {j m : ℕ} → j < M → Cond1.n c1 < m  → m < k   → ¬ ( j + k * M  ≡ M * (suc m) + A    )
 
-problem0-k=k : ( k A M : ℕ ) → problem A M k
-problem0-k=k zero A M ()
-problem0-k=k (suc k) A zero A<kM = ⊥-elim ( nat-<> A<kM (subst (λ x → x < suc A) (*-comm _ k ) 0<s ))
-problem0-k=k (suc k) A (suc m) A<kM = cc k a<sa (start-range k)
-  module kk where
+problem1-0 : (k A M : ℕ )  → (A<kM : suc A <  k * M )
+    → UCond1 A M k 
+problem1-0 zero A M () 
+problem1-0 (suc k) A zero A<kM = ⊥-elim ( nat-<> A<kM (subst (λ x → x < suc A) (*-comm _ k ) 0<s ))
+problem1-0 (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 >  ((k - n) ) * M )  → A - ((k - n) * M) < M →  Cond1 A M (suc k)
      cck n n<k gt lt =  record { n = n ; i = A - (((k - n)) * M ) ; range-n = n<k   ; range-i = lt ; rule1 = lemma2 }  where
@@ -60,115 +63,10 @@
            A + M * (suc n)                                         ≡⟨ +-comm A _ ⟩
            M * (suc n) + A
           ∎  where open ≡-Reasoning
-     nM<kM : {n : ℕ } → suc n < suc k → n * M < k * M
-     nM<kM {n} n<k = *< {n} {k} {m} ( <-minus-0 n<k )
-     --  loop on  range  of A : ((k - n) ) * M ≤ A < ((k - n) ) * M + M
-     nextc : (n : ℕ ) → (suc n < suc k) → M < suc ((k - n) * M) 
-     nextc n n<k with k - n | inspect (_-_ k) n
-     nextc n n<k | 0 | record { eq = e } = ⊥-elim ( nat-≡< (sym e) (minus>0 n<k) )
-     nextc n n<k | suc n0 | _ = s≤s (s≤s lemma) where
-        lemma : m ≤ m + n0 * suc m
-        lemma = x≤x+y
-     cc : (n : ℕ) → n < suc k → suc A > (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 : A - ((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 (A - ((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
-        a=mk0 :  (A - ((k - (suc n)) * M)) ≡  M → A ≡ (k - n) * M
-        a=mk0 a=mk = sym ( begin
-           (k - n) * M 
-         ≡⟨ sym ( minus+n {(k - n) * M} {M} (nextc n n<k )) ⟩
-           ((k - n) * M ) - M + M
-         ≡⟨ +-comm _ M ⟩
-           M + (((k - n) * M ) - M)
-         ≡⟨ cong (λ x → M + x ) (sym (minus-* {M} {k} (<-minus-0 n<k ))) ⟩
-           M + (k - (suc n) * M) 
-         ≡⟨ cong (λ x → x + (k - (suc n)) * M) (sym a=mk) ⟩
-           A - ((k - (suc n)) * M) + ((k - (suc n)) * M) 
-         ≡⟨ minus+n {A} {(k - (suc n)) * M} k<A ⟩
-           A
-         ∎ ) where open ≡-Reasoning
-        lemma1 : (A - ((k - (suc n)) * M)) ≡  M → suc A > (k - n) * M
-        lemma1 a=mk = subst (λ x → (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 + (k - (suc n)) * M → A > M + (k - n) - M → A >  (k - n)
-        lemma3 : (A - ((k - (suc n)) * M)) > M  → suc A > (k - n) * M
-        lemma3 mk<a = <-trans lemma5 a<sa where
-            lemma6 :  M + (k - (suc n)) * M ≡ (k - n) * M
-            lemma6 = begin
-                  M + (k - (suc n)) * M 
-               ≡⟨ cong (λ x → M + x) (minus-* {M} {k} (<-minus-0 n<k))  ⟩
-                  M + (((k - n) * M ) - M )
-               ≡⟨ +-comm M _ ⟩
-                  ((k - n) * M ) - M + M
-               ≡⟨ minus+n {_} {M} (nextc n n<k) ⟩
-                  (k - n) * M
-               ∎  where open ≡-Reasoning
-            lemma4 : (M + (k - (suc n)) * M) < A
-            lemma4 = subst (λ x → (M + (k - (suc n)) * M)  < x ) (minus+n {A}{(k - (suc n)) * M} k<A ) ( <-plus mk<a )
-            lemma5 : (k - n) * M < A
-            lemma5 = subst (λ x → x < A ) lemma6 lemma4
-     start-range : (k : ℕ ) → suc A > (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
---     --- 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 = {!!}
-
---      range-n : n < k
---      range-i : i < M
---      rule1 : i + k * M  ≡ M * (suc n) + A    -- A ≡ (i + k * M ) - (M * (suc n)) 
-
-record UCond1 (A M k : ℕ )  : Set where
-   field
-      c1 : Cond1 A M k
-      u1 : {j m : ℕ} → j < Cond1.i c1  → m < k   → ¬ ( j + k * M  ≡ M * (suc m) + A    )
-      -- u2 : {j m : ℕ} → Cond1.i c1  < j → j < M  → m < k   → ¬ ( j + k * M  ≡ M * (suc m) + A    )
-      -- u3 : {j m : ℕ} → j < M → m < Cond1.n c1  → ¬ ( j + k * M  ≡ M * (suc m) + A    )
-      -- u4 : {j m : ℕ} → j < M → Cond1.n c1 < m  → m < k   → ¬ ( j + k * M  ≡ M * (suc m) + A    )
-
-problem1-0 : (k A M : ℕ )  → (A<kM : suc A <  k * M )
-    → UCond1 A M k 
-problem1-0 zero A M () 
-problem1-0 (suc k) A zero A<kM = ⊥-elim ( nat-<> A<kM (subst (λ x → x < suc A) (*-comm _ k ) 0<s ))
-problem1-0 (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 >  ((k - n) ) * M )  → A - ((k - n) * M) < M → UCond1 A M (suc k)
-     cck n n<k k<A i<M = c0 where
+     cck-u :  ( n : ℕ ) →  n < suc k  → (suc A >  ((k - n) ) * M )  → A - ((k - n) * M) < M → UCond1 A M (suc k)
+     cck-u n n<k k<A i<M = c0 where
         c1 : Cond1 A M (suc k) 
-        c1 = kk.cck k A m A<kM n n<k k<A i<M 
+        c1 = cck n n<k k<A i<M 
         lemma4 : {i j x y z : ℕ} → j + x ≡ y → i + x ≡ z → j < i → y < z
         lemma4 {i} {j} {x} refl refl (s≤s z≤n) = s≤s (subst (λ k → x ≤ k ) (+-comm x _) x≤x+y)
         lemma4 refl refl (s≤s (s≤s lt)) = s≤s (lemma4 refl refl (s≤s lt) )
@@ -208,20 +106,27 @@
         lemma-u1 {j} {m1} j<akM m1<k eq | tri≈ ¬a b ¬c = ⊥-elim (nat-≡< b ( (≤-trans j<akM (≤-trans refl-≤s i<M )))) 
         lemma-u1 {j} {m1} j<akM m1<k eq | tri> ¬a ¬b c = ⊥-elim (nat-<> (≤-trans i<M (less-1 c)) j<akM ) 
         c0  =  record { c1 = record { n = n ; i = A - (((k - n)) * M ) ; range-n = n<k   ; range-i = i<M; rule1 = Cond1.rule1 c1 } ; u1 = lemma-u1 }
+     --  loop on  range  of A : ((k - n) ) * M ≤ A < ((k - n) ) * M + M
+     nextc : (n : ℕ ) → (suc n < suc k) → M < suc ((k - n) * M) 
+     nextc n n<k with k - n | inspect (_-_ k) n
+     nextc n n<k | 0 | record { eq = e } = ⊥-elim ( nat-≡< (sym e) (minus>0 n<k) )
+     nextc n n<k | suc n0 | _ = s≤s (s≤s lemma) where
+        lemma : m ≤ m + n0 * suc m
+        lemma = x≤x+y
      cc : (n : ℕ) → n < suc k → suc A > (k - n) * M → UCond1 A M (suc k)
-     cc zero n<k k<A = cck 0 n<k k<A lemma where
+     cc zero n<k k<A = cck-u 0 n<k k<A lemma where
         a<m : suc A < M + k * M 
         a<m = A<kM
         lemma : A - ((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 (A - ((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 = cck-u (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
         a=mk0 :  (A - ((k - (suc n)) * M)) ≡  M → A ≡ (k - n) * M
         a=mk0 a=mk = sym ( begin
            (k - n) * M 
-         ≡⟨ sym ( minus+n {(k - n) * M} {M} (kk.nextc k A m A<kM n n<k )) ⟩
+         ≡⟨ sym ( minus+n {(k - n) * M} {M} (nextc n n<k )) ⟩
            ((k - n) * M ) - M + M
          ≡⟨ +-comm _ M ⟩
            M + (((k - n) * M ) - M)
@@ -245,7 +150,7 @@
                   M + (((k - n) * M ) - M )
                ≡⟨ +-comm M _ ⟩
                   ((k - n) * M ) - M + M
-               ≡⟨ minus+n {_} {M} (kk.nextc k A m A<kM n n<k ) ⟩
+               ≡⟨ minus+n {_} {M} (nextc n n<k ) ⟩
                   (k - n) * M
                ∎  where open ≡-Reasoning
             lemma4 : (M + (k - (suc n)) * M) < A