Mercurial > hg > Members > kono > Proof > prob1

changeset 15:559bada080d5

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
reasoning on < ?
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 27 Nov 2019 13:47:04 +0900
parents 8415d3f77fe0
children 3557795c7bb3
files logic.agda nat.agda prob1.agda
diffstat 3 files changed, 74 insertions(+), 14 deletions(-) [+]
line wrap: on
line diff
--- a/logic.agda	Wed Nov 27 09:59:51 2019 +0900
+++ b/logic.agda	Wed Nov 27 13:47:04 2019 +0900
@@ -44,6 +44,7 @@
 dont-orb {A} {B} (case1 a) ¬B = a
 
 
+
 infixr  130 _∧_
 infixr  140 _∨_
 infixr  150 _⇔_
@@ -70,6 +71,7 @@
 
 open import Relation.Binary.PropositionalEquality
 
+
 ≡-Bool-func : {A B : Bool } → ( A ≡ true → B ≡ true ) → ( B ≡ true → A ≡ true ) → A ≡ B
 ≡-Bool-func {true} {true} a→b b→a = refl
 ≡-Bool-func {false} {true} a→b b→a with b→a refl
--- a/nat.agda	Wed Nov 27 09:59:51 2019 +0900
+++ b/nat.agda	Wed Nov 27 13:47:04 2019 +0900
@@ -1,3 +1,4 @@
+{-# OPTIONS --allow-unsolved-metas #-}
 module nat where
 
 open import Data.Nat 
@@ -98,6 +99,18 @@
            suc x
         ∎  where open ≡-Reasoning
 
+
+-- open import Relation.Binary.PropositionalEquality
+
+-- postulate extensionality : { n : Level}  → Relation.Binary.PropositionalEquality.Extensionality n n -- (Level.suc n)
+
+-- <-≡-iff : {A B : (a b : ℕ ) → Set } → {a b : ℕ }  → (A a b → B a b ) → (B a b → A a b ) → A ≡ B
+-- <-≡-iff {A} {B} ab ba = {!!}
+
+
+0<s : {x : ℕ } → zero < suc x
+0<s {_} = s≤s z≤n 
+
 <-minus-0 : {x y z : ℕ } → z + x < z + y → x < y
 <-minus-0 {x} {suc _} {zero} lt = lt
 <-minus-0 {x} {y} {suc z} (s≤s lt) = <-minus-0 {x} {y} {z} lt
@@ -109,13 +122,20 @@
 x≤x+y {zero} {y} = z≤n
 x≤x+y {suc z} {y} = s≤s  (x≤x+y {z} {y})
 
--- <-plus-0 : {x y z : ℕ } → x < y → z + x < z + y 
--- <-plus-0 {x} {y} {z} lt = {!!}
-
 <-plus : {x y z : ℕ } → x < y → x + z < y + z 
 <-plus {zero} {suc y} {z} (s≤s z≤n) = s≤s (subst (λ k → z ≤ k ) (+-comm z _ ) x≤x+y  )
 <-plus {suc x} {suc y} {z} (s≤s lt) = s≤s (<-plus {x} {y} {z} lt)
 
+<-plus-0 : {x y z : ℕ } → x < y → z + x < z + y 
+<-plus-0 {x} {y} {z} lt = subst₂ (λ j k → j < k ) (+-comm _ z) (+-comm _ z) ( <-plus {x} {y} {z} lt )
+
+≤-plus-≡ : {x y z : ℕ } → (x ≤ y ) ≡ (z + x ≤ z + y )
+≤-plus-≡ {zero} {zero} {zero} = refl
+≤-plus-≡ {zero} {zero} {suc z} with ≤-plus-≡ {zero} {zero} {z}
+... | eq = {!!}
+≤-plus-≡ {zero} {suc y} {z} = {!!}
+≤-plus-≡ {suc x} {y} {z} = {!!}
+
 x+y<z→x<z : {x y z : ℕ } → x + y < z → x < z 
 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 )
@@ -123,6 +143,18 @@
 *≤ : {x y z : ℕ } → x ≤ y → x * z ≤ y * z 
 *≤ lt = *-mono-≤ lt ≤-refl
 
+*< : {x y z : ℕ } → x < y → x * suc z < y * suc z 
+*< {zero} {suc y} lt = s≤s z≤n
+*< {suc x} {suc y} (s≤s lt) = <-plus-0 (*< lt)
+
+<to<s : {x y  : ℕ } → x < y → x < suc y
+<to<s {zero} {suc y} (s≤s lt) = s≤s z≤n
+<to<s {suc x} {suc y} (s≤s lt) = s≤s (<to<s {x} {y} lt)
+
+<tos<s : {x y  : ℕ } → x < y → suc x < suc y
+<tos<s {zero} {suc y} (s≤s z≤n) = s≤s (s≤s z≤n)
+<tos<s {suc x} {suc y} (s≤s lt) = s≤s (<tos<s {x} {y} lt)
+
 ≤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)
@@ -142,6 +174,10 @@
 minus<=0 {0} {suc y} z≤n = refl
 minus<=0 {suc x} {suc y} (s≤s le) = minus<=0 {x} {y} le
 
+minus>0 : {x y : ℕ } → x < y → 0 < minus y x 
+minus>0 {zero} {suc _} (s≤s z≤n) = s≤s z≤n
+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-* {x} {zero} {z} = refl
 distr-minus-* {x} {suc y} {z} with <-cmp x y
@@ -208,8 +244,12 @@
              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 : ℕ } → suc (k * M) > M + n * M → minus k (suc n) * M ≡ minus (minus k n * M ) M
-minus-* {M} {k} {n} lt = begin
+minus-* : {M k n : ℕ } → n < k  → minus k (suc n) * M ≡ minus (minus k n * M ) M
+minus-* {zero} {k} {n} lt = {!!}
+minus-* {suc m} {k} {n} lt with <-cmp k 1
+minus-* {suc m} {k} {n} lt | tri< a ¬b ¬c = {!!}
+minus-* {suc m} {k} {n} lt | tri≈ ¬a b ¬c = {!!}
+minus-* {suc m} {k} {n} lt | tri> ¬a ¬b c = begin
            minus k (suc n) * M
         ≡⟨ distr-minus-* {k} {suc n} {M}  ⟩
            minus (k * M ) ((suc n) * M)
@@ -217,9 +257,23 @@
            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} lt ) ⟩
+        ≡⟨ sym ( minus- {k * M} {n * M} (lemma lt) ) ⟩
            minus (minus (k * M ) (n * M)) M
         ≡⟨ cong (λ x → minus x M ) ( sym ( distr-minus-* {k} {n} )) ⟩
            minus (minus k n * M ) M
-        ∎  where open ≡-Reasoning
+        ∎  where
+             open ≡-Reasoning
+             M = suc m
+             lemma : {n k m : ℕ } → n < k  → suc (k * suc m) > suc m + n * suc m
+             lemma {zero} {suc k} {m} (s≤s lt) = s≤s (s≤s (subst (λ x → x ≤ m + k * suc m) (+-comm 0 _ ) x≤x+y ))
+             lemma {suc n} {suc k} {m} (s≤s lt) = lemma1 (lemma {n} {k} {m} lt ) where
+                 lemma1 : suc (suc m + n * suc m) ≤ suc (k * suc m) → suc (suc m + suc n * suc m ) ≤ suc (suc k * suc m) 
+                 lemma1 (s≤s lt) = s≤s ( s≤s (subst (λ x → x ) (
+                   begin
+                     suc m + n * suc m ≤ k * suc m
+                   ≡⟨⟩
+                     suc n * suc m     ≤ k * suc m
+                   ≡⟨ ≤-plus-≡ ⟩
+                     m + suc n * suc m ≤ m + k * suc m
+                   ∎ ) lt ))  where open ≡-Reasoning
 
--- a/prob1.agda	Wed Nov 27 09:59:51 2019 +0900
+++ b/prob1.agda	Wed Nov 27 13:47:04 2019 +0900
@@ -40,7 +40,7 @@
 
 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 = {!!} 
+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) where
      M = suc m
      cck :  ( n : ℕ ) →  n < suc k  → (suc A >  ((k - n) ) * M )  → A - ((k - n) * M) < M →  Cond1 A M (suc k)
@@ -58,11 +58,15 @@
            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) → suc ((k - n) * M) > M --  M + n * M < suc ((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 ((k * M) - (n * M)) + n * M
-          lemma = subst ( λ x → suc n * M < suc x ) (sym (minus+n {k * M} {n * 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 
@@ -79,7 +83,7 @@
            ((k - n) * M ) - M + M
          ≡⟨ +-comm _ M ⟩
            M + (((k - n) * M ) - M)
-         ≡⟨ cong (λ x → M + x ) (sym (minus-* {M} {k} {!!}  )) ⟩
+         ≡⟨ 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) 
@@ -95,7 +99,7 @@
             lemma6 :  M + (k - (suc n)) * M ≡ (k - n) * M
             lemma6 = begin
                   M + (k - (suc n)) * M 
-               ≡⟨ cong (λ x → M + x) (minus-* {M} {k} {!!} )  ⟩
+               ≡⟨ cong (λ x → M + x) (minus-* {M} {k} (<-minus-0 n<k))  ⟩
                   M + (((k - n) * M ) - M )
                ≡⟨ +-comm M _ ⟩
                   ((k - n) * M ) - M + M