My.SetTheory.Nat.TvD

module My.SetTheory.Nat.TvD where

-- §──────────────────────────────────────────────────────────────────
-- Required modules
-- §──────────────────────────────────────────────────────────────────

import Algebra as A
import Data.Empty as DE
import Data.Nat as DN
import Data.Nat.Properties as DNP
import Data.Sum as DS
import Function as F
import Relation.Binary as RB
import Relation.Binary.PropositionalEquality as RBPE
import Relation.Nullary as RN

open DN using (_+_ ; _*_ ; _∸_ ; _≤_ ; _≰_ ; _<_ ; _>_ ; _≟_)
open DS using (_⊎_)
open F using (_$_ ; _∘_)
open RBPE using (_≡_ ; _≢_)

import My.SetTheory.Relation.Decidable as MySTRD
import My.SetTheory.Relation.Trichotomy as MySTRT
import My.SetTheory.Sum.Misc as MySTSM

-- §──────────────────────────────────────────────────────────────────
-- Some propositions from A. S. Troelstra and D. van Dalen,
-- `Constructivism in mathematics', vol. I, Chapter 3, Section 2.
-- §──────────────────────────────────────────────────────────────────

-- 2.1 Definitions

n∸0≡n : (n : DN.ℕ) → n ∸ 0 ≡ n
n∸0≡n n = RBPE.refl

m∸sn≡pred⌈m∸n⌉ : (m n : DN.ℕ) → m ∸ DN.suc n ≡ DN.pred (m ∸ n)
m∸sn≡pred⌈m∸n⌉ 0 0 = RBPE.refl
m∸sn≡pred⌈m∸n⌉ 0 (DN.suc n) = RBPE.refl
m∸sn≡pred⌈m∸n⌉ (DN.suc m) 0 = RBPE.refl
m∸sn≡pred⌈m∸n⌉ (DN.suc m) (DN.suc n) = m∸sn≡pred⌈m∸n⌉ m n

n+0≡n : (n : DN.ℕ) → n + 0 ≡ n
n+0≡n n = CSR.+-comm n 0
  where
    module CSR = A.CommutativeSemiring DNP.commutativeSemiring

m+sn≡s⌈m+n⌉ : (m n : DN.ℕ) → m + DN.suc n ≡ DN.suc (m + n)
m+sn≡s⌈m+n⌉ m n =
  begin
    m + DN.suc n   ≡⟨ CSR.+-comm m (DN.suc n) ⟩
    DN.suc n + m   ≡⟨⟩
    DN.suc (n + m) ≡⟨ RBPE.cong DN.suc $ CSR.+-comm n m ⟩
    DN.suc (m + n) ∎
  where
    module CSR = A.CommutativeSemiring DNP.commutativeSemiring
    open RBPE.≡-Reasoning

n*0≡0 : (n : DN.ℕ) → n * 0 ≡ 0
n*0≡0 n = CSR.*-comm n 0
  where
    module CSR = A.CommutativeSemiring DNP.commutativeSemiring

m*sn≡m*n+m : (m n : DN.ℕ) → m * DN.suc n ≡ m * n + m
m*sn≡m*n+m m n =
  begin
    m * DN.suc n ≡⟨ CSR.*-comm m (DN.suc n) ⟩
    DN.suc n * m ≡⟨⟩
    m + n * m    ≡⟨ RBPE.cong (λ x → m + x) $ CSR.*-comm n m ⟩
    m + m * n    ≡⟨ CSR.+-comm m (m * n) ⟩
    m * n + m    ∎
  where
    module CSR = A.CommutativeSemiring DNP.commutativeSemiring
    open RBPE.≡-Reasoning

sm≡sn⇒m≡n : {m n : DN.ℕ} → DN.suc m ≡ DN.suc n → m ≡ n
sm≡sn⇒m≡n sm≡sn = DNP.cancel-+-left 1 sm≡sn

-- 2.4 Proposition

0∸n≡0 : (n : DN.ℕ) → 0 ∸ n ≡ 0
0∸n≡0 0 = RBPE.refl
0∸n≡0 (DN.suc n) = RBPE.refl

sm∸sn≡m∸n : (m n : DN.ℕ) → DN.suc m ∸ DN.suc n ≡ m ∸ n
sm∸sn≡m∸n m n = RBPE.refl

sn∸n≡1 : (n : DN.ℕ) → DN.suc n ∸ n ≡ 1
sn∸n≡1 0 = RBPE.refl
sn∸n≡1 (DN.suc n) = sn∸n≡1 n

n∸n≡0 : (n : DN.ℕ) → n ∸ n ≡ 0
n∸n≡0 0 = RBPE.refl
n∸n≡0 (DN.suc n) = n∸n≡0 n

n≡0⊎n≡s⌈predN⌉ : (n : DN.ℕ) → n ≡ 0 ⊎ n ≡ DN.suc (DN.pred n)
n≡0⊎n≡s⌈predN⌉ 0 = DS.inj₁ RBPE.refl
n≡0⊎n≡s⌈predN⌉ (DN.suc n) = DS.inj₂ RBPE.refl

n≢0⇒n≡s⌈predN⌉ : {n : DN.ℕ} → n ≢ 0 → n ≡ DN.suc (DN.pred n)
n≢0⇒n≡s⌈predN⌉ {0}  n≢0 = DE.⊥-elim $ n≢0 RBPE.refl
n≢0⇒n≡s⌈predN⌉ {DN.suc n} n≢0 = RBPE.refl

n≡s⌈predN⌉⇒n≢0 : {n : DN.ℕ} → n ≡ DN.suc (DN.pred n) → n ≢ 0
n≡s⌈predN⌉⇒n≢0 {0} ()
n≡s⌈predN⌉⇒n≢0 {DN.suc n} RBPE.refl ()

m≡sn⇒m≡s⌈predM⌉ : {m n : DN.ℕ} → m ≡ DN.suc n → m ≡ DN.suc (DN.pred m)
m≡sn⇒m≡s⌈predM⌉ {0} {n} ()
m≡sn⇒m≡s⌈predM⌉ {DN.suc m} {n} m≡sn = RBPE.refl

-- 2.7 Definition

m≤n⇒m∸n≡0 : {m n : DN.ℕ} → m ≤ n → m ∸ n ≡ 0
m≤n⇒m∸n≡0 {0} {0} m≤n = RBPE.refl
m≤n⇒m∸n≡0 {0} {DN.suc n} m≤n = RBPE.refl
m≤n⇒m∸n≡0 {DN.suc m} {0} ()
m≤n⇒m∸n≡0 {DN.suc m} {DN.suc n} (DN.s≤s m≤n) = m≤n⇒m∸n≡0 m≤n

m∸n≡0⇒m≤n : {m n : DN.ℕ} → m ∸ n ≡ 0 → m ≤ n
m∸n≡0⇒m≤n {0} {n} m∸n≡0 = DN.z≤n
m∸n≡0⇒m≤n {DN.suc m} {0} ()
m∸n≡0⇒m≤n {DN.suc m} {DN.suc n} m∸n≡0 = DN.s≤s $ m∸n≡0⇒m≤n m∸n≡0

m<n⇒sm∸n≡0 : {m n : DN.ℕ} → m < n → DN.suc m ∸ n ≡ 0
m<n⇒sm∸n≡0 m<n = m≤n⇒m∸n≡0 m<n

sm∸n≡0⇒m<n : {m n : DN.ℕ} → DN.suc m ∸ n ≡ 0 → m < n
sm∸n≡0⇒m<n m∸n≡0 = m∸n≡0⇒m≤n m∸n≡0

-- 2.8 Proposition

m≡n⊎m≢n : (m n : DN.ℕ) → m ≡ n ⊎ m ≢ n
m≡n⊎m≢n m n = MySTRD.decA⇒A⊎¬A (m ≟ n)

≤-antisymmetric : {m n : DN.ℕ} → m ≤ n → n ≤ m → m ≡ n
≤-antisymmetric = DTO.antisym
  where
    module DTO = RB.DecTotalOrder DN.decTotalOrder

≤-total : (m n : DN.ℕ) → m ≤ n ⊎ n ≤ m
≤-total = DTO.total
  where
    module DTO = RB.DecTotalOrder DN.decTotalOrder

m≤n⇒sm≤sn : {m n : DN.ℕ} → m ≤ n → DN.suc m ≤ DN.suc n
m≤n⇒sm≤sn m≤n = DN.s≤s m≤n

m<n⇒sm<sn : {m n : DN.ℕ} → m < n → DN.suc m < DN.suc n
m<n⇒sm<sn m<n = m≤n⇒sm≤sn m<n

m≤n⇒m<n⊎m≡n : {m n : DN.ℕ} → m ≤ n → m < n ⊎ m ≡ n
m≤n⇒m<n⊎m≡n {0} {0} m≤n = DS.inj₂ RBPE.refl
m≤n⇒m<n⊎m≡n {0} {DN.suc n} m≤n = DS.inj₁ $ DN.s≤s DN.z≤n
m≤n⇒m<n⊎m≡n {DN.suc m} {0} ()
m≤n⇒m<n⊎m≡n {DN.suc m} {DN.suc n} (DN.s≤s m≤n) = DS.map m<n⇒sm<sn
  (λ m≡n → RBPE.cong DN.suc m≡n) $ m≤n⇒m<n⊎m≡n m≤n

m<n⇒m≤n : {m n : DN.ℕ} → m < n → m ≤ n
m<n⇒m≤n {0} {_} _ = DN.z≤n
m<n⇒m≤n {DN.suc m} {0} ()
m<n⇒m≤n {DN.suc m} {DN.suc n} (DN.s≤s m<n) = DN.s≤s $ m<n⇒m≤n m<n

m<n⊎m≡n⇒m≤n : {m n : DN.ℕ} → m < n ⊎ m ≡ n → m ≤ n
m<n⊎m≡n⇒m≤n (DS.inj₁ x) = m<n⇒m≤n x
m<n⊎m≡n⇒m≤n (DS.inj₂ y) = DTO.reflexive y
  where
    module DTO = RB.DecTotalOrder DN.decTotalOrder

≡-<-trich : RB.Trichotomous _≡_ _<_
≡-<-trich = STO.compare
  where
    module STO = RB.StrictTotalOrder DNP.strictTotalOrder

m<n⊎m≡n⊎m>n : (m n : DN.ℕ) → m < n ⊎ m ≡ n ⊎ m > n
m<n⊎m≡n⊎m>n m n = MySTRT.trichABC⇒A⊎B⊎C $ ≡-<-trich m n

m≰n⇒m>n : {m n : DN.ℕ} → m ≰ n → m > n
m≰n⇒m>n {m} {n} m≰n =
  MySTSM.¬⌈A⊎B⌉⇒A⊎B⊎C⇒C (m≰n ∘ m<n⊎m≡n⇒m≤n) $ m<n⊎m≡n⊎m>n m n

¬⌈m<n⊎m≡n⌉⇒m≰n : {m n : DN.ℕ} → RN.¬ (m < n ⊎ m ≡ n) → m ≰ n
¬⌈m<n⊎m≡n⌉⇒m≰n ¬⌈m<n⊎m≡n⌉ = ¬⌈m<n⊎m≡n⌉ ∘ m≤n⇒m<n⊎m≡n

m>n⇒m≰n : {m n : DN.ℕ} → m > n → m ≰ n
m>n⇒m≰n {m} {n} = ¬⌈m<n⊎m≡n⌉⇒m≰n ∘ (MySTRT.trichABC⇒C⇒¬⌈A⊎B⌉ $ ≡-<-trich m n)

-- 2.10 Proposition

n+1≡sn : (n : DN.ℕ) → n + 1 ≡ DN.suc n
n+1≡sn n =
  begin
    n + 1          ≡⟨ CSR.+-comm n 1 ⟩
    1 + n          ≡⟨⟩
    DN.suc (0 + n) ≡⟨⟩
    DN.suc n       ∎
  where
    module CSR = A.CommutativeSemiring DNP.commutativeSemiring
    open RBPE.≡-Reasoning

1+n≡sn : (n : DN.ℕ) → 1 + n ≡ DN.suc n
1+n≡sn n = RBPE.refl

0+n≡n : (n : DN.ℕ) → 0 + n ≡ n
0+n≡n n = RBPE.refl

+-assocʳ : (m n p : DN.ℕ) → m + (n + p) ≡ (m + n) + p
+-assocʳ m n p = RBPE.sym $ CSR.+-assoc m n p
  where
    module CSR = A.CommutativeSemiring DNP.commutativeSemiring

m+n≡n+m : (m n : DN.ℕ) → m + n ≡ n + m
m+n≡n+m m n = CSR.+-comm m n
  where
    module CSR = A.CommutativeSemiring DNP.commutativeSemiring

-- 2.11 Proposition

sn≢0 : (n : DN.ℕ) → DN.suc n ≢ 0
sn≢0 n ()

m∸n≡sp⇒m∸n≢0 : {m n p : DN.ℕ} → m ∸ n ≡ DN.suc p → m ∸ n ≢ 0
m∸n≡sp⇒m∸n≢0 {m} {n} {p} m∸n≡sp m∸n≡0 = sn≢0 p sp≡0
  where
    sp≡0 : DN.suc p ≡ 0
    sp≡0 =
      begin
        DN.suc p ≡⟨ RBPE.sym m∸n≡sp ⟩
        m ∸ n    ≡⟨ m∸n≡0 ⟩
        0        ∎
      where
        open RBPE.≡-Reasoning

m∸n≡sp⇒m≰n : {m n p : DN.ℕ} → m ∸ n ≡ DN.suc p  → m ≰ n
m∸n≡sp⇒m≰n {m} {n} m∸n≡sp m≤n =
  (m∸n≡sp⇒m∸n≢0 {m} {n} m∸n≡sp)(m≤n⇒m∸n≡0 m≤n)

m∸n≡sp⇒n<m : {m n p : DN.ℕ} → m ∸ n ≡ DN.suc p → n < m
m∸n≡sp⇒n<m m∸n≡sp = m≰n⇒m>n (m∸n≡sp⇒m≰n m∸n≡sp)

m∸n≡sp⇒n≤m : {m n p : DN.ℕ} → m ∸ n ≡ DN.suc p → n ≤ m
m∸n≡sp⇒n≤m m∸n≡sp = m<n⇒m≤n (m∸n≡sp⇒n<m m∸n≡sp)

m∸n≡sp⇒m≡n+sp : {m n p : DN.ℕ} → m ∸ n ≡ DN.suc p → m ≡ n + DN.suc p
m∸n≡sp⇒m≡n+sp {m} {n} {p} m∸n≡sp = RBPE.sym s
  where
    s : n + DN.suc p ≡ m
    s =
      begin
        n + DN.suc p ≡⟨ RBPE.cong (λ x → n + x) (RBPE.sym m∸n≡sp) ⟩
        n + (m ∸ n)  ≡⟨ DNP.m+n∸m≡n (m∸n≡sp⇒n≤m {m} {n} m∸n≡sp) ⟩
        m            ∎
      where
        open RBPE.≡-Reasoning

m≡n+sp⇒m∸n≡sp : {m n p : DN.ℕ} → m ≡ n + DN.suc p → m ∸ n ≡ DN.suc p
m≡n+sp⇒m∸n≡sp {m} {n} {p} m≡n+sp =
  begin
    m ∸ n              ≡⟨ RBPE.cong (λ x → x ∸ n) m≡n+sp ⟩
    (n + DN.suc p) ∸ n ≡⟨ RBPE.cong (λ x → x ∸ n) (CSR.+-comm n (DN.suc p)) ⟩
    (DN.suc p + n) ∸ n ≡⟨ DNP.m+n∸n≡m (DN.suc p) n ⟩
    DN.suc p           ∎
  where
    module CSR = A.CommutativeSemiring DNP.commutativeSemiring
    open RBPE.≡-Reasoning

<-transitive : {m n p : DN.ℕ} → m < n → n < p → m < p
<-transitive = DNP.<-trans

≤-transitive : {m n p : DN.ℕ} → m ≤ n → n ≤ p → m ≤ p
≤-transitive = DTO.trans
  where
    module DTO = RB.DecTotalOrder DN.decTotalOrder