Mercurial > hg > Members > kono > Proof > prob1
changeset 14:8415d3f77fe0
minus clean up
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Wed, 27 Nov 2019 09:59:51 +0900 |
parents | 0e63ca7fd224 |
children | 559bada080d5 |
files | nat.agda prob1.agda |
diffstat | 2 files changed, 237 insertions(+), 230 deletions(-) [+] |
line wrap: on
line diff
--- a/nat.agda Wed Nov 27 09:35:08 2019 +0900 +++ b/nat.agda Wed Nov 27 09:59:51 2019 +0900 @@ -1,56 +1,225 @@ module nat where -open import Data.Nat renaming ( zero to Zero ; suc to Suc ; ℕ to Nat ; _⊔_ to _n⊔_ ) +open import Data.Nat +open import Data.Nat.Properties open import Data.Empty open import Relation.Nullary open import Relation.Binary.PropositionalEquality +open import Relation.Binary.Core open import logic -nat-<> : { x y : Nat } → x < y → y < x → ⊥ +nat-<> : { x y : ℕ } → x < y → y < x → ⊥ nat-<> (s≤s x<y) (s≤s y<x) = nat-<> x<y y<x -nat-≤> : { x y : Nat } → x ≤ y → y < x → ⊥ +nat-≤> : { x y : ℕ } → x ≤ y → y < x → ⊥ nat-≤> (s≤s x<y) (s≤s y<x) = nat-≤> x<y y<x -nat-<≡ : { x : Nat } → x < x → ⊥ +nat-<≡ : { x : ℕ } → x < x → ⊥ nat-<≡ (s≤s lt) = nat-<≡ lt -nat-≡< : { x y : Nat } → x ≡ y → x < y → ⊥ +nat-≡< : { x y : ℕ } → x ≡ y → x < y → ⊥ nat-≡< refl lt = nat-<≡ lt -¬a≤a : {la : Nat} → Suc la ≤ la → ⊥ +¬a≤a : {la : ℕ} → suc la ≤ la → ⊥ ¬a≤a (s≤s lt) = ¬a≤a lt -a<sa : {la : Nat} → la < Suc la -a<sa {Zero} = s≤s z≤n -a<sa {Suc la} = s≤s a<sa +a<sa : {la : ℕ} → la < suc la +a<sa {zero} = s≤s z≤n +a<sa {suc la} = s≤s a<sa -=→¬< : {x : Nat } → ¬ ( x < x ) -=→¬< {Zero} () -=→¬< {Suc x} (s≤s lt) = =→¬< lt +=→¬< : {x : ℕ } → ¬ ( x < x ) +=→¬< {zero} () +=→¬< {suc x} (s≤s lt) = =→¬< lt ->→¬< : {x y : Nat } → (x < y ) → ¬ ( y < x ) +>→¬< : {x y : ℕ } → (x < y ) → ¬ ( y < x ) >→¬< (s≤s x<y) (s≤s y<x) = >→¬< x<y y<x -<-∨ : { x y : Nat } → x < Suc y → ( (x ≡ y ) ∨ (x < y) ) -<-∨ {Zero} {Zero} (s≤s z≤n) = case1 refl -<-∨ {Zero} {Suc y} (s≤s lt) = case2 (s≤s z≤n) -<-∨ {Suc x} {Zero} (s≤s ()) -<-∨ {Suc x} {Suc y} (s≤s lt) with <-∨ {x} {y} lt -<-∨ {Suc x} {Suc y} (s≤s lt) | case1 eq = case1 (cong (λ k → Suc k ) eq) -<-∨ {Suc x} {Suc y} (s≤s lt) | case2 lt1 = case2 (s≤s lt1) +<-∨ : { x y : ℕ } → x < suc y → ( (x ≡ y ) ∨ (x < y) ) +<-∨ {zero} {zero} (s≤s z≤n) = case1 refl +<-∨ {zero} {suc y} (s≤s lt) = case2 (s≤s z≤n) +<-∨ {suc x} {zero} (s≤s ()) +<-∨ {suc x} {suc y} (s≤s lt) with <-∨ {x} {y} lt +<-∨ {suc x} {suc y} (s≤s lt) | case1 eq = case1 (cong (λ k → suc k ) eq) +<-∨ {suc x} {suc y} (s≤s lt) | case2 lt1 = case2 (s≤s lt1) -max : (x y : Nat) → Nat -max Zero Zero = Zero -max Zero (Suc x) = (Suc x) -max (Suc x) Zero = (Suc x) -max (Suc x) (Suc y) = Suc ( max x y ) +max : (x y : ℕ) → ℕ +max zero zero = zero +max zero (suc x) = (suc x) +max (suc x) zero = (suc x) +max (suc x) (suc y) = suc ( max x y ) --- _*_ : Nat → Nat → Nat +-- _*_ : ℕ → ℕ → ℕ -- _*_ zero _ = zero -- _*_ (suc n) m = m + ( n * m ) -exp : Nat → Nat → Nat -exp _ Zero = 1 -exp n (Suc m) = n * ( exp n m ) +exp : ℕ → ℕ → ℕ +exp _ zero = 1 +exp n (suc m) = n * ( exp n m ) + +minus : (a b : ℕ ) → ℕ +minus a zero = a +minus zero (suc b) = zero +minus (suc a) (suc b) = minus a b + +_-_ = minus + +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) + +sa=b→a<b : { n m : ℕ } → suc n ≡ m → n < m +sa=b→a<b {0} {suc zero} refl = s≤s z≤n +sa=b→a<b {suc n} {suc (suc n)} refl = s≤s (sa=b→a<b refl) + +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-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 + +<-minus : {x y z : ℕ } → x + z < y + z → x < y +<-minus {x} {y} {z} lt = <-minus-0 ( subst₂ ( λ j k → j < k ) (+-comm x _) (+-comm y _ ) lt ) + +x≤x+y : {z y : ℕ } → z ≤ z + y +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) + +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 ) + +*≤ : {x y z : ℕ } → x ≤ y → x * z ≤ y * z +*≤ lt = *-mono-≤ lt ≤-refl + +≤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) + +refl-≤s : {x : ℕ } → x ≤ suc x +refl-≤s {zero} = z≤n +refl-≤s {suc x} = s≤s (refl-≤s {x}) + +x<y→≤ : {x y : ℕ } → x < y → x ≤ suc y +x<y→≤ {zero} {.(suc _)} (s≤s z≤n) = z≤n +x<y→≤ {suc x} {suc y} (s≤s lt) = s≤s (x<y→≤ {x} {y} lt) + +open import Data.Product + +minus<=0 : {x y : ℕ } → x ≤ y → minus x y ≡ 0 +minus<=0 {0} {zero} z≤n = refl +minus<=0 {0} {suc y} z≤n = refl +minus<=0 {suc x} {suc y} (s≤s le) = minus<=0 {x} {y} le + +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 +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} (x<y→≤ a)) ⟩ + 0 * z + ≡⟨ sym (minus<=0 {x * z} {z + y * z} le ) ⟩ + minus (x * z) (z + y * z) + ∎ where + open ≡-Reasoning + le : x * z ≤ z + y * z + le = ≤-trans lemma (subst (λ k → y * z ≤ k ) (+-comm _ z ) (x≤x+y {y * z} {z} ) ) where + lemma : x * z ≤ y * z + lemma = *≤ {x} {y} {z} (≤to< a) +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} refl-≤s ) ⟩ + 0 * z + ≡⟨ sym (minus<=0 {x * z} {z + y * z} (lt {x} {z} )) ⟩ + minus (x * z) (z + y * z) + ∎ where + open ≡-Reasoning + lt : {x z : ℕ } → x * z ≤ z + x * z + lt {zero} {zero} = z≤n + lt {suc x} {zero} = lt {x} {zero} + lt {x} {suc z} = ≤-trans lemma refl-≤s where + lemma : x * suc z ≤ z + x * suc z + lemma = subst (λ k → x * suc z ≤ k ) (+-comm _ z) (x≤x+y {x * suc z} {z}) +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 : {x y z : ℕ } → suc y ≤ x → z + y * z ≤ x * z + lt {x} {y} {z} le = *≤ le + +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 + minus (minus x y) z + z + ≡⟨ minus+n {_} {z} lemma ⟩ + minus x y + ≡⟨ +m= {_} {_} {y} ( begin + minus x y + y + ≡⟨ minus+n {_} {y} lemma1 ⟩ + x + ≡⟨ sym ( minus+n {_} {z + y} gt ) ⟩ + minus x (z + y) + (z + y) + ≡⟨ sym ( +-assoc (minus x (z + y)) _ _ ) ⟩ + minus x (z + y) + z + y + ∎ ) ⟩ + minus x (z + y) + z + ≡⟨ cong (λ k → minus x k + z ) (+-comm _ y ) ⟩ + minus x (y + z) + z + ∎ ) where + open ≡-Reasoning + lemma1 : suc x > y + lemma1 = x+y<z→x<z (subst (λ k → k < suc x ) (+-comm z _ ) gt ) + 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 k (suc n) * M + ≡⟨ distr-minus-* {k} {suc n} {M} ⟩ + minus (k * M ) ((suc n) * M) + ≡⟨⟩ + 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 ) ⟩ + 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 +
--- a/prob1.agda Wed Nov 27 09:35:08 2019 +0900 +++ b/prob1.agda Wed Nov 27 09:59:51 2019 +0900 @@ -7,171 +7,9 @@ open import logic open import nat open import Data.Empty +open import Data.Product open import Relation.Nullary -minus : (a b : ℕ ) → ℕ -minus a zero = a -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) - -sa=b→a<b : { n m : ℕ } → suc n ≡ m → n < m -sa=b→a<b {0} {suc zero} refl = s≤s z≤n -sa=b→a<b {suc n} {suc (suc n)} refl = s≤s (sa=b→a<b refl) - -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-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 - -<-minus : {x y z : ℕ } → x + z < y + z → x < y -<-minus {x} {y} {z} lt = <-minus-0 ( subst₂ ( λ j k → j < k ) (+-comm x _) (+-comm y _ ) lt ) - -x≤x+y : {z y : ℕ } → z ≤ z + y -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) - -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 ) - -*< : {x y z : ℕ } → x ≤ y → x * z ≤ y * z -*< lt = *-mono-≤ lt ≤-refl - -≤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) - -refl-≤s : {x : ℕ } → x ≤ suc x -refl-≤s {zero} = z≤n -refl-≤s {suc x} = s≤s (refl-≤s {x}) - -x<y→≤ : {x y : ℕ } → x < y → x ≤ suc y -x<y→≤ {zero} {.(suc _)} (s≤s z≤n) = z≤n -x<y→≤ {suc x} {suc y} (s≤s lt) = s≤s (x<y→≤ {x} {y} lt) - -open import Data.Product - -minus<=0 : {x y : ℕ } → x ≤ y → minus x y ≡ 0 -minus<=0 {0} {zero} z≤n = refl -minus<=0 {0} {suc y} z≤n = refl -minus<=0 {suc x} {suc y} (s≤s le) = minus<=0 {x} {y} le - -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 -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} (x<y→≤ a)) ⟩ - 0 * z - ≡⟨ sym (minus<=0 {x * z} {z + y * z} le ) ⟩ - minus (x * z) (z + y * z) - ∎ where - open ≡-Reasoning - le : x * z ≤ z + y * z - le = ≤-trans lemma (subst (λ k → y * z ≤ k ) (+-comm _ z ) (x≤x+y {y * z} {z} ) ) where - lemma : x * z ≤ y * z - lemma = *< {x} {y} {z} (≤to< a) -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} refl-≤s ) ⟩ - 0 * z - ≡⟨ sym (minus<=0 {x * z} {z + y * z} (lt {x} {z} )) ⟩ - minus (x * z) (z + y * z) - ∎ where - open ≡-Reasoning - lt : {x z : ℕ } → x * z ≤ z + x * z - lt {zero} {zero} = z≤n - lt {suc x} {zero} = lt {x} {zero} - lt {x} {suc z} = ≤-trans lemma refl-≤s where - lemma : x * suc z ≤ z + x * suc z - lemma = subst (λ k → x * suc z ≤ k ) (+-comm _ z) (x≤x+y {x * suc z} {z}) -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 : {x y z : ℕ } → suc y ≤ x → z + y * z ≤ x * z - lt {x} {y} {z} le = *< le - -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 - minus (minus x y) z + z - ≡⟨ minus+n {_} {z} lemma ⟩ - minus x y - ≡⟨ +m= {_} {_} {y} ( begin - minus x y + y - ≡⟨ minus+n {_} {y} lemma1 ⟩ - x - ≡⟨ sym ( minus+n {_} {z + y} gt ) ⟩ - minus x (z + y) + (z + y) - ≡⟨ sym ( +-assoc (minus x (z + y)) _ _ ) ⟩ - minus x (z + y) + z + y - ∎ ) ⟩ - minus x (z + y) + z - ≡⟨ cong (λ k → minus x k + z ) (+-comm _ y ) ⟩ - minus x (y + z) + z - ∎ ) where - open ≡-Reasoning - lemma1 : suc x > y - lemma1 = x+y<z→x<z (subst (λ k → k < suc x ) (+-comm z _ ) gt ) - 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 k (suc n) * M - ≡⟨ distr-minus-* {k} {suc n} {M} ⟩ - minus (k * M ) ((suc n) * M) - ≡⟨⟩ - 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 ) ⟩ - 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 -- All variables are positive integer -- A = -M*n + i +k*M - M @@ -205,70 +43,70 @@ problem0-k=k (suc k) A zero A<kM = {!!} 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 > (minus k n ) * M ) → minus A (minus k n * M) < M → Cond1 A M (suc k) - cck n n<k gt lt = record { n = n ; i = minus A ((minus k n) * M ) ; range-n = n<k ; range-i = lt ; rule1 = lemma2 } where - lemma2 : minus A (minus k n * M) + suc k * M ≡ M * suc n + A + 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 + lemma2 : A - ((k - n) * M) + suc k * M ≡ M * suc n + A lemma2 = begin - minus A (minus k n * M) + suc k * M ≡⟨ cong ( λ x → minus A (minus k n * M) + suc x * M ) (sym (minus+n {k} {n} n<k )) ⟩ - minus A (minus k n * M) + (suc ((minus k n ) + n )) * M ≡⟨ cong ( λ x → minus A (minus k n * M) + suc x * M ) (+-comm _ n) ⟩ - minus A (minus k n * M) + (suc (n + (minus k n ) )) * M ≡⟨⟩ - minus A (minus k n * M) + (suc n + (minus k n ) ) * M ≡⟨ cong ( λ x → minus A (minus k n * M) + x * M ) (+-comm (suc n) _) ⟩ - minus A (minus k n * M) + ((minus k n ) + suc n ) * M ≡⟨ cong ( λ x → minus A (minus k n * M) + x ) (((proj₂ *-distrib-+)) M (minus k n) _ ) ⟩ - minus A (minus k n * M) + ((minus k n * M) + (suc n) * M) ≡⟨ sym (+-assoc (minus A (minus k n * M)) _ ((suc n) * M)) ⟩ - minus A (minus k n * M) + (minus k n * M) + (suc n) * M ≡⟨ cong ( λ x → x + (suc n) * M ) ( minus+n {A} {minus k n * M} gt ) ⟩ + A - ((k - n) * M) + suc k * M ≡⟨ cong ( λ x → A - ((k - n) * M) + suc x * M ) (sym (minus+n {k} {n} n<k )) ⟩ + A - ((k - n) * M) + (suc (((k - n) ) + n )) * M ≡⟨ cong ( λ x → A - ((k - n) * M) + suc x * M ) (+-comm _ n) ⟩ + A - ((k - n) * M) + (suc (n + ((k - n) ) )) * M ≡⟨⟩ + A - ((k - n) * M) + (suc n + ((k - n) ) ) * M ≡⟨ cong ( λ x → A - ((k - n) * M) + x * M ) (+-comm (suc n) _) ⟩ + A - ((k - n) * M) + (((k - n) ) + suc n ) * M ≡⟨ cong ( λ x → A - ((k - n) * M) + x ) (((proj₂ *-distrib-+)) M ((k - n)) _ ) ⟩ + A - ((k - n) * M) + (((k - n) * M) + (suc n) * M) ≡⟨ sym (+-assoc (A - ((k - n) * M)) _ ((suc n) * M)) ⟩ + A - ((k - n) * M) + ((k - n) * M) + (suc n) * M ≡⟨ cong ( λ x → x + (suc n) * M ) ( minus+n {A} {(k - n) * M} gt ) ⟩ A + (suc n) * M ≡⟨ cong ( λ k → A + k ) (*-comm (suc n) _ ) ⟩ A + M * (suc n) ≡⟨ +-comm A _ ⟩ M * (suc n) + A ∎ where open ≡-Reasoning - -- loop on range of A : (minus k n ) * M ≤ A < (minus k n ) * M + M - nextc : (n : ℕ ) → (suc n < suc k) → suc (minus k n * M) > M -- M + n * M < suc (minus k n * M) + n * M + -- 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 (minus (k * M) (n * M)) + n * M + 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} {!!})) {!!} - cc : (n : ℕ) → n < suc k → suc A > minus k n * M → Cond1 A M (suc k) + 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 : minus A (minus k 0 * M) < M + 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 (minus A (minus k (suc n) * M)) 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 : (minus A (minus k (suc n) * M)) ≡ M → A ≡ minus k n * M + a=mk0 : (A - ((k - (suc n)) * M)) ≡ M → A ≡ (k - n) * M a=mk0 a=mk = sym ( begin - minus k n * M - ≡⟨ sym ( minus+n {minus k n * M} {M} (nextc n n<k )) ⟩ - minus (minus k n * M ) M + M + (k - n) * M + ≡⟨ sym ( minus+n {(k - n) * M} {M} (nextc n n<k )) ⟩ + ((k - n) * M ) - M + M ≡⟨ +-comm _ M ⟩ - M + minus (minus k n * M ) M + M + (((k - n) * M ) - M) ≡⟨ cong (λ x → M + x ) (sym (minus-* {M} {k} {!!} )) ⟩ - M + (minus k (suc n) * M) - ≡⟨ cong (λ x → x + minus k (suc n) * M) (sym a=mk) ⟩ - minus A (minus k (suc n) * M) + (minus k (suc n) * M) - ≡⟨ minus+n {A} {minus k (suc n) * M} k<A ⟩ + 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 : (minus A (minus k (suc n) * M)) ≡ M → suc A > minus k n * M - lemma1 a=mk = subst (λ x → minus k n * M < suc x ) (sym (a=mk0 a=mk )) a<sa + 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 + minus k (suc n) * M → A > M + minus k n - M → A > minus k n - lemma3 : (minus A (minus k (suc n) * M)) > M → suc A > minus k n * M + -- 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 + minus k (suc n) * M ≡ minus k n * M + lemma6 : M + (k - (suc n)) * M ≡ (k - n) * M lemma6 = begin - M + minus k (suc n) * M + M + (k - (suc n)) * M ≡⟨ cong (λ x → M + x) (minus-* {M} {k} {!!} ) ⟩ - M + minus (minus k n * M ) M + M + (((k - n) * M ) - M ) ≡⟨ +-comm M _ ⟩ - minus (minus k n * M ) M + M + ((k - n) * M ) - M + M ≡⟨ minus+n {_} {M} (nextc n n<k) ⟩ - minus k n * M + (k - n) * M ∎ where open ≡-Reasoning - lemma4 : (M + minus k (suc n) * M) < A - lemma4 = subst (λ x → (M + minus k (suc n) * M) < x ) (minus+n {A}{minus k (suc n) * M} k<A ) ( <-plus mk<a ) - lemma5 : minus k n * M < A + 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 > minus k k * M + start-range : (k : ℕ ) → suc A > (k - k) * M start-range zero = s≤s z≤n start-range (suc k) = start-range k