Pi.Common.Arithmetic

{-# OPTIONS --without-K --rewriting #-}

module Pi.Common.Arithmetic where

open import lib.Base
open import lib.types.Nat using (_+_ ; ℕ-S-is-inj)
open import lib.PathGroupoid
open import lib.NType
open import Pi.Common.Misc

infix 4 _≤_ _<_

data _≤_ : ℕ -> ℕ -> Type₀ where
  z≤n : ∀ {n}                 → 0  ≤ n
  s≤s : ∀ {m n} (m≤n : m ≤ n) → S m ≤ S n

≤-has-all-paths : {m n : ℕ} -> (p : m ≤ n) -> (q : m ≤ n) -> p == q
≤-has-all-paths {O} {O} z≤n z≤n = idp
≤-has-all-paths {O} {S n} z≤n z≤n = idp
≤-has-all-paths {S m} {S n} (s≤s p) (s≤s q) = 
  let rec = ≤-has-all-paths p q 
  in  ap s≤s rec

instance
  ≤-level : {m n : ℕ} → is-prop (m ≤ n)
  ≤-level = all-paths-is-prop ≤-has-all-paths

_<_ : ℕ -> ℕ -> Type₀
m < n = S m ≤ n

≤-trans : {m n r : ℕ} -> m ≤ n -> n ≤ r -> m ≤ r
≤-trans z≤n       _         = z≤n
≤-trans (s≤s m≤n) (s≤s n≤o) = s≤s (≤-trans m≤n n≤o)

≤-reflexive : {p q : ℕ} -> p == q -> p ≤ q
≤-reflexive {0}  idp = z≤n
≤-reflexive {S m} idp = s≤s (≤-reflexive idp)

≤-up : {n m : ℕ} -> m ≤ n -> m ≤ S n
≤-up {n} {.0} z≤n = z≤n
≤-up {.(S _)} {.(S _)} (s≤s q) = s≤s (≤-up q)

≤-up2 : {n m : ℕ} -> m ≤ n -> S m ≤ S n
≤-up2 p = s≤s p

≤-down : {n m : ℕ} -> S m ≤ n -> m ≤ n
≤-down {.(S _)} {0} (s≤s p) = z≤n
≤-down {.(S _)} {S n} (s≤s p) = s≤s (≤-down p)

≤-down2 : {n m : ℕ} -> S m ≤ S n -> m ≤ n
≤-down2 {m} {n} (s≤s p) = p

≤-abs : {A : Type₀} -> {n : ℕ} -> (S n ≤ 0) -> A
≤-abs ()

1+n≰n : ∀ {n} → ¬ (1 + n ≤ n)
1+n≰n (s≤s le) = 1+n≰n le

abs-refl : {A : Type₀} -> {n : ℕ} -> n < n -> A
abs-refl p = ⊥-elim (1+n≰n p)

abs-suc : {A : Type₀} -> {n : ℕ} -> S n < n -> A
abs-suc {n} p = ⊥-elim (1+n≰n (≤-down p))

+-unit : {n : ℕ} -> n + 0 == n
+-unit {O} = idp
+-unit {S n} = ap S +-unit

+-S : ∀ m n → m + S n == S (m + n)
+-S 0    n = idp
+-S (S m) n = cong S (+-S m n)

+-comm : (m n : ℕ) -> (m + n) == (n + m)
+-comm O n = ! +-unit
+-comm (S m) n =
  begin
  S m + n   =⟨ idp ⟩
  S (m + n) =⟨ cong S (+-comm m n) ⟩
  S (n + m) =⟨ ≡-sym (+-S n m) ⟩
  n + S m   =∎

+-assoc : (m n r : ℕ) -> (m + n) + r == m + (n + r)
+-assoc 0    _ _ = idp
+-assoc (S m) n o = cong S (+-assoc m n o)

infixl 81 _∸_
_∸_ : ℕ → ℕ → ℕ
m ∸ 0   =  m
0 ∸ S n  =  0
S m ∸ S n  =  m ∸ n

≡-down2 : {p q : ℕ} -> (S p == S q) -> p == q   
≡-down2 {p} {q} r = ℕ-S-is-inj p q r


_≤?_ : (n m : ℕ) -> BoolDec (n ≤ m)
O ≤? m = yes z≤n
S n ≤? O = no (λ ())
S n ≤? S m with n ≤? m
... | yes p = yes (s≤s p)
... | no  q = no (λ x → q (≤-down2 x))

_<?_ : (n m : ℕ) -> BoolDec ((S n) ≤ m)
n <? m = (S n) ≤? m

_≟_ : (n m : ℕ) -> BoolDec (n == m)
O ≟ O = yes idp
O ≟ S m = no (λ ())
S n ≟ O = no (λ ())
S n ≟ S m with n ≟ m
... | yes p = yes (ap S p)
... | no  p = no (λ x → p (≡-down2 x))


module ≤-Reasoning where
    infix  1 ≤begin_
    infixr 2 _≤⟨⟩_ _≤⟨_⟩_ _≡⟨⟩_ _≡⟨_⟩_
    infix  3 _≤∎

    ≤begin_ : ∀ {x y : ℕ}
             → x ≤ y
               -----
             → x ≤ y
    ≤begin x≤y  =  x≤y

    _≤⟨⟩_ : ∀ (x : ℕ) {y : ℕ}
            → x ≤ y
              -----
            → x ≤ y
    x ≤⟨⟩ x≤y  =  x≤y

    _≡⟨⟩_ : ∀ (x : ℕ) {y : ℕ}
            → x == y
              -----
            → x ≤ y
    x ≡⟨⟩ x≡y  = ≤-reflexive x≡y

    _≤⟨_⟩_ : ∀ (x : ℕ) {y z : ℕ}
             → x ≤ y
             → y ≤ z
               -----
             → x ≤ z
    x ≤⟨ x≤y ⟩ y≤z  = ≤-trans x≤y y≤z

    _≡⟨_⟩_ : ∀ (x : ℕ) {y z : ℕ}
             → x == y
             → y ≤ z
               -----
             → x ≤ z
    x ≡⟨ x≡y ⟩ y≤z  = ≤-trans (≤-reflexive x≡y) y≤z

    _≤∎ : ∀ (x : ℕ)
           -----
          → x ≤ x
    x ≤∎  = ≤-reflexive idp

open ≤-Reasoning

≤-remove-+ : {p q r : ℕ} -> (p + q ≤ r) -> (q ≤ r)
≤-remove-+ {p = O} pqr = pqr
≤-remove-+ {p = S p} {r = S r} (s≤s pqr) = ≤-up (≤-remove-+ pqr)

+-three-assoc : {k i r : ℕ} -> k + (i + r) == (i + k) + r
+-three-assoc {k} {i} {r} = ! (+-assoc k i r) ∙ ap (λ e -> e + r) (+-comm k i)

introduce-≤-from-+ : {p q r : ℕ} -> (p + q == r) -> (p ≤ r)
introduce-≤-from-+ {O} {q} {r} pqr = z≤n
introduce-≤-from-+ {S p} {q} {S r} pqr = s≤s (introduce-≤-from-+ (≡-down2 pqr))

≤-up2-+ : {p q r : ℕ} -> (p ≤ q) -> (r + p ≤ r + q)
≤-up2-+ {p} {q} {O} pq = pq
≤-up2-+ {p} {q} {S r} pq = s≤s (≤-up2-+ pq)

+-left : (p r : ℕ) -> S (p + r) == p + S r
+-left p r = +-three-assoc {1} {p} {r} ∙ +-assoc p 1 r

≤-up2-r-+ : {p q r : ℕ} -> (p ≤ q) -> (p + r ≤ q + r)
≤-up2-r-+ {p} {q} {r} pq =
  ≤begin
    _
  ≡⟨ +-comm p r ⟩
    r + p
  ≤⟨ ≤-up2-+ pq ⟩
    r + q
  ≡⟨ ! (+-comm q r) ⟩
    q + r
  ≤∎

≤-up-+ : {p q r : ℕ} -> (p ≤ q) -> (p ≤ r + q)
≤-up-+ {p} {q} {O} pq = pq
≤-up-+ {p} {q} {S r} pq = ≤-up (≤-up-+ pq)

≤-up-r-+ : {p q r : ℕ} -> (p ≤ q) -> (p ≤ q + r)
≤-up-r-+ {p} {q} {r} pq =
  ≤begin
    p
  ≤⟨ ≤-up-+ pq ⟩
    r + q
  ≡⟨ ! (+-comm q r) ⟩
    q + r
  ≤∎


≤-down-+ : {p q r : ℕ} -> (p + r ≤ q) -> (p ≤ q)
≤-down-+ {p} {q} {O} pqr = 
  ≤begin
    p
  ≡⟨ +-comm O p ⟩
    p + O
  ≤⟨ pqr ⟩
    q
  ≤∎
≤-down-+ {p} {q} {S r} pqr =
  let lemma =
        ≤begin
          S (p + r)
        ≡⟨ +-left p r  ⟩
          p + S r
        ≤⟨ pqr ⟩
          q
        ≤∎
  in ≤-down-+ (≤-down lemma)

≡-down-+ : {p q r : ℕ} -> (r + p == r + q) -> (p == q)
≡-down-+ {p} {q} {O} pqr = pqr
≡-down-+ {p} {q} {S r} pqr = ≡-down-+ (≡-down2 pqr)


≡-up-+ : {p q p2 q2 : ℕ} -> (p == p2) -> (q == q2) -> (p + q == p2 + q2)
≡-up-+ {p} {q} {p2} {q2} pp qq = ap (λ e -> e + q) pp ∙ ap (λ e -> p2 + e) qq


≡-down-r-+ : {p q r : ℕ} -> (p + r == q + r) -> (p == q)
≡-down-r-+ {p} {q} {r} pqr = ≡-down-+ (+-comm r p ∙ pqr ∙ (+-comm q r))


∸-implies-≤ : {p q r : ℕ} -> (p == q ∸ r) -> (p ≤ q)
∸-implies-≤ {p} {q} {O} pqr = ≤-reflexive pqr
∸-implies-≤ {.0} {O} {S r} idp = z≤n
∸-implies-≤ {p} {S q} {S r} pqr = ≤-up (∸-implies-≤ {p} {q} {r} pqr)


introduce-∸ : {p q r : ℕ} -> (r ≤ q) -> (p + r == q) -> (p == q ∸ r)
introduce-∸ {p} {q} {O} qr pqr = ! (+-comm p O) ∙ pqr
introduce-∸ {p} {S q} {S r} (s≤s qr) pqr = introduce-∸ {p} {q} {r} qr (≡-down2 ((+-left p r) ∙  pqr))


eliminate-∸ : {p q r : ℕ} -> (r ≤ q) -> (p == q ∸ r) -> (p + r == q)
eliminate-∸ {p} {q} {O} rq pqr = +-comm p O ∙ pqr
eliminate-∸ {p} {S q} {S r} (s≤s qr) pqr = 
  let rec = eliminate-∸ {p} {q} {r} qr pqr
  in  ! (+-left p r) ∙ ap S rec


introduce-∸-≤ : {p q r : ℕ} -> (r ≤ q) -> (p + r ≤ q) -> (p ≤ q ∸ r)
introduce-∸-≤ {p} {q} {O} qr pqr = ≤-trans (≤-reflexive (! (+-comm p O))) pqr
introduce-∸-≤ {p} {S q} {S r} (s≤s qr) pqr = introduce-∸-≤ {p} {q} {r} qr (≤-down2 (≤-trans (≤-reflexive (+-left p r)) pqr))


eliminate-∸-≤ : {p q r : ℕ} -> (r ≤ q) -> (p ≤ q ∸ r) -> (p + r ≤ q)
eliminate-∸-≤ {p} {q} {O} qr pqr = ≤-trans (≤-reflexive (+-comm p O)) pqr
eliminate-∸-≤ {p} {S q} {S r} (s≤s qr) pqr = 
  let rec = eliminate-∸-≤ {p} {q} {r} qr pqr
  in  ≤-trans (≤-reflexive (! (+-left p r))) (≤-up2 rec)


introduce-∸-≤l : {p q r : ℕ} -> (r ≤ p) -> (p ≤ q + r) -> (p ∸ r ≤ q)
introduce-∸-≤l {p} {q} {O} rp pqr = ≤-trans pqr (≤-reflexive (+-comm q O))
introduce-∸-≤l {S p} {q} {S r} (s≤s rq) pqr = introduce-∸-≤l {p} {q} {r} rq (≤-down2 (≤-trans pqr (≤-reflexive (! (+-left q r)))))


eliminate-∸-≤l : {p q r : ℕ} -> (r ≤ p) -> (p ∸ r ≤ q) -> (p ≤ q + r)
eliminate-∸-≤l {p} {q} {O} rp pqr = ≤-trans pqr (≤-reflexive (! (+-comm q O)))
eliminate-∸-≤l {S p} {q} {S r} (s≤s rp) pqr = 
  let rec = eliminate-∸-≤l {p} {q} {r} rp pqr
  in  ≤-trans (≤-up2 rec) (≤-reflexive (+-left q r))


∸-to-zero : {p q : ℕ} -> (p == q) -> (p ∸ q == 0)
∸-to-zero {O} {O} pq = idp
∸-to-zero {S p} {S q} pq = ∸-to-zero (≡-down2 pq)

minus-plus : {p q : ℕ} -> {q ≤ p} -> p ∸ q + q == p
minus-plus {p} {q} {qp} = eliminate-∸ qp idp

∸-down2 : {n r : ℕ} -> {r ≤ n} -> ((S n) ∸ (S r)) == n ∸ r
∸-down2 = idp

≤-≡ : {n k : ℕ} -> (n ≤ k) -> (k ≤ n) -> (n == k)
≤-≡ z≤n z≤n = idp
≤-≡ (s≤s pnk) (s≤s pkn) = ap S (≤-≡ pnk pkn)

plus-minus : {p q : ℕ} -> (p ≤ q) -> p + (q ∸ p) == q
plus-minus {.0} {q} z≤n = idp
plus-minus {.(S _)} {.(S _)} (s≤s pq) = ap S (plus-minus pq)

plus-minus-l : {p q : ℕ} -> (p + q) ∸ p == q
plus-minus-l {O} {q} = idp
plus-minus-l {S p} {q} = plus-minus-l {p} {q}


zero-∸ : (n : ℕ) -> (0 ∸ n == 0)
zero-∸ 0 = idp
zero-∸ (S n) = idp

∸-anti-≤ : {p q r : ℕ} -> (q ≤ p) -> (r ∸ p) ≤ (r ∸ q)
∸-anti-≤ {p} {.0} {r} z≤n = ∸-implies-≤ {r ∸ p} {r} {p} idp
∸-anti-≤ {S p} {S q} {O} (s≤s qp) = z≤n
∸-anti-≤ {S p} {S q} {S r} (s≤s qp) = ∸-anti-≤ {p} {q} {r} qp

≰⇒> : {m n : ℕ} -> ¬ (m ≤ n) -> n < m
≰⇒> {O} {n} p = ⊥-elim (p z≤n)
≰⇒> {S m} {O} p = s≤s z≤n
≰⇒> {S m} {S n} p = 
  let rec = ≰⇒> {m} {n} (λ x → p (s≤s x))
  in  s≤s rec

∸-∸-+ : {p q r : ℕ} -> (r ≤ q) -> (q ≤ p + r) -> p ∸ (q ∸ r) == (p + r) ∸ q
∸-∸-+ {p} {0} {0} rq qpr = +-comm 0 p
∸-∸-+ {p} {S q} {0} rq qpr rewrite +-comm p 0 = idp
∸-∸-+ {p} {S q} {S r} (s≤s rq) qpr =
  let rec = ∸-∸-+ {p} {q} {r} rq (≤-down2 (≤-trans qpr (≤-reflexive (+-three-assoc {p} {1} {r}))))
      lemma : (p + r) ∸ q == (p + S r) ∸ S q
      lemma = cong (λ x -> x ∸ S q) (≡-sym (+-three-assoc {p} {1} {r}))
  in ≡-trans rec lemma

∸-up : {n r : ℕ} -> (r < n) -> (n ∸ r) == S (n ∸ (S r))
∸-up {S 0} {0} p = idp
∸-up {S 0} {S r} (s≤s p) = ≤-abs p
∸-up {S (S n)} {0} p = idp
∸-up {S (S n)} {S r} (s≤s p) = ∸-up {S n} {r} p

∸-up-r : {n m : ℕ} -> (m ≤ n) -> S (n ∸ m) == S n ∸ m
∸-up-r {n} {O} q = idp
∸-up-r {n} {S m} q = ! ((∸-up q))

nowhere : {n k : ℕ} -> (¬ (n < k)) -> (¬ (n == k)) -> (¬ (n == 1 + k)) -> (¬ (1 + k < n)) -> ⊥
nowhere {0} {0} p1 p2 p3 p4 = p2 idp
nowhere {0} {S k} p1 p2 p3 p4 = p1 (s≤s z≤n)
nowhere {S 0} {0} p1 p2 p3 p4 = p3 idp
nowhere {S (S n)} {0} p1 p2 p3 p4 = p4 (s≤s (s≤s z≤n))
nowhere {S n} {S k} p1 p2 p3 p4 = nowhere (λ x → p1 (s≤s x)) (λ x → p2 (cong S x)) (λ x → p3 (cong S x)) (λ x → p4 (s≤s x))

≤-≠-≤ : {n m : ℕ} -> (n ≤ S m) -> ¬ (n == S m) -> (n ≤ m)
≤-≠-≤ {0} {0} p q = z≤n
≤-≠-≤ {0} {S m} p q = z≤n
≤-≠-≤ {S 0} {0} p q = ⊥-elim (q idp)
≤-≠-≤ {S (S n)} {0} (s≤s ()) q
≤-≠-≤ {S n} {S m} (s≤s p) q = s≤s (≤-≠-≤ p λ x → q (cong S x))

≤-∃ : (n m : ℕ) -> (n ≤ m) -> Σ ℕ (λ t -> t + n == m)
≤-∃ .0 m z≤n = m , +-unit
≤-∃ (S n) (S m) (s≤s p) =
  let rec-t , rec-p = ≤-∃ n m p
  in  rec-t , ≡-trans (+-three-assoc {rec-t} {1} {n}) (cong S rec-p)

rrr : {k : ℕ} -> k ≤ k
rrr = ≤-reflexive idp

squeeze : {n k : ℕ} -> (n < k) -> (k ≤ S n) -> (k == S n)
squeeze {.0} {.1} (s≤s {n = .0} z≤n) (s≤s z≤n) = idp
squeeze {.(S _)} {.(S (S _))} (s≤s (s≤s pn)) (s≤s (s≤s pnn)) = ap S (squeeze (s≤s pn) (s≤s pnn))