load "misc.quox";
load "bool.quox";
load "either.quox";

namespace nat {

def elim-0-1 :
    0.(P : ℕ → ★) →
    ω.(P 0) → ω.(P 1) →
    ω.(0.(n : ℕ) → P n → P (succ n)) →
    (n : ℕ) → P n =
  λ P p0 p1 ps n ⇒
  case n return n' ⇒ P n' of {
    zero    ⇒ p0;
    succ n' ⇒
      case n' return n'' ⇒ P (succ n'') of {
        zero         ⇒ p1;
        succ n'', IH ⇒ ps (succ n'') IH
      }
  }

def elim-pair :
    0.(P : ℕ → ℕ → ★) →
    ω.(P 0 0) →
    ω.(0.(n : ℕ)   → P 0 n → P 0 (succ n)) →
    ω.(0.(m : ℕ)   → P m 0 → P (succ m) 0) →
    ω.(0.(m n : ℕ) → P m n → P (succ m) (succ n)) →
    ω.(m : ℕ) → (n : ℕ) → P m n =
  λ P zz zs sz ss m ⇒
    caseω m return m' ⇒ (n : ℕ) → P m' n of {
      0 ⇒ λ n ⇒ case n return n' ⇒ P 0 n' of {
        0            ⇒ zz;
        succ n', ihn ⇒ zs n' ihn
      };
      succ m', ω.ihm ⇒ λ n ⇒ case n return n' ⇒ P (succ m') n' of {
        0       ⇒ sz m' (ihm 0);
        succ n' ⇒ ss m' n' (ihm n')
      }
    }

#[compile-scheme "(lambda (n) (cons n 'erased))"]
def dup! : (n : ℕ) → [ω. Sing ℕ n] =
  λ n ⇒
  case n return n' ⇒ [ω. Sing ℕ n'] of {
    zero ⇒ [(zero, [δ _ ⇒ zero])];
    succ n, d ⇒
      appω (Sing ℕ n) (Sing ℕ (succ n))
        (λ n' ⇒ sing.app ℕ ℕ n (λ n ⇒ succ n) n') d
  };

def dup : ℕ → [ω.ℕ] =
  λ n ⇒ appω (Sing ℕ n) ℕ (λ n' ⇒ sing.val ℕ n n') (dup! n);

#[compile-scheme "(lambda% (m n) (+ m n))"]
def plus : ℕ → ℕ → ℕ =
  λ m n ⇒
  case m return ℕ of {
    zero      ⇒ n;
    succ _, p ⇒ succ p
  };

#[compile-scheme "(lambda% (m n) (* m n))"]
def timesω : ℕ → ω.ℕ → ℕ =
  λ m n ⇒
  case m return ℕ of {
    zero      ⇒ zero;
    succ _, t ⇒ plus n t
  };

def times : ℕ → ℕ → ℕ =
  λ m n ⇒ case dup n return ℕ of { [n] ⇒ timesω m n };

def pred : ℕ → ℕ = λ n ⇒ case n return ℕ of { zero ⇒ zero; succ n ⇒ n };

def pred-succ : ω.(n : ℕ) → pred (succ n) ≡ n : ℕ =
  λ n ⇒ δ 𝑖 ⇒ n;

def0 succ-inj : (m n : ℕ) → succ m ≡ succ n : ℕ → m ≡ n : ℕ =
  λ m n eq ⇒ δ 𝑖 ⇒ pred (eq @𝑖);

#[compile-scheme "(lambda% (m n) (max 0 (- m n)))"]
def minus : ℕ → ℕ → ℕ =
  λ m n ⇒
  (case n return ℕ → ℕ of {
    zero      ⇒ λ m ⇒ m;
    succ _, f ⇒ λ m ⇒ f (pred m)
  }) m;


def0 IsSucc : ℕ → ★ =
  λ n ⇒ case n return ★ of { zero ⇒ False; succ _ ⇒ True };

def isSucc? : ω.(n : ℕ) → Dec (IsSucc n) =
  λ n ⇒
  caseω n return n' ⇒ Dec (IsSucc n') of {
    zero   ⇒ No  (IsSucc zero)      (λ v ⇒ v);
    succ n ⇒ Yes (IsSucc (succ n)) 'true
  };

def zero-not-succ : 0.(m : ℕ) → Not (zero ≡ succ m : ℕ) =
  λ m eq ⇒ coe (𝑖 ⇒ IsSucc (eq @𝑖)) @1 @0 'true;

def succ-not-zero : 0.(m : ℕ) → Not (succ m ≡ zero : ℕ) =
  λ m eq ⇒ coe (𝑖 ⇒ IsSucc (eq @𝑖)) 'true;


def0 not-succ-self : (m : ℕ) → Not (m ≡ succ m : ℕ) =
  λ m ⇒
  case m return m' ⇒ Not (m' ≡ succ m' : ℕ) of {
    zero         ⇒ zero-not-succ 0;
    succ n, ω.ih ⇒ λ eq ⇒ ih (succ-inj n (succ n) eq)
  }


#[compile-scheme "(lambda% (m n) (if (= m n) Yes No))"]
def eq? : DecEq ℕ =
  λ m ⇒
  caseω m
  return m' ⇒ ω.(n : ℕ) → Dec (m' ≡ n : ℕ)
  of {
    zero ⇒ λ n ⇒
      caseω n return n' ⇒ Dec (zero ≡ n' : ℕ) of {
        zero    ⇒ Yes (zero ≡ zero    : ℕ) (δ _ ⇒ zero);
        succ n' ⇒ No  (zero ≡ succ n' : ℕ) (λ eq ⇒ zero-not-succ n' eq)
      };
    succ m', ω.ih ⇒ λ n ⇒
      caseω n return n' ⇒ Dec (succ m' ≡ n' : ℕ) of {
        zero    ⇒ No (succ m' ≡ zero : ℕ) (λ eq ⇒ succ-not-zero m' eq);
        succ n' ⇒
          dec.elim (m' ≡ n' : ℕ) (λ _ ⇒ Dec (succ m' ≡ succ n' : ℕ))
            (λ y ⇒ Yes (succ m' ≡ succ n' : ℕ) (δ 𝑖 ⇒ succ (y @𝑖)))
            (λ n ⇒ No  (succ m' ≡ succ n' : ℕ) (λ eq ⇒ n (succ-inj m' n' eq)))
            (ih n')
      }
  };


def0 Ordering : ★ = {lt, eq, gt}

def from-ordering : 0.(A : ★) → ω.A → ω.A → ω.A → Ordering → A =
  λ A lt eq gt o ⇒
  case o return A of { 'lt ⇒ lt; 'eq ⇒ eq; 'gt ⇒ gt }

def drop-ordering : 0.(A : ★) → Ordering → A → A =
  λ A o x ⇒ case o return A of { 'lt ⇒ x; 'eq ⇒ x; 'gt ⇒ x }

def compareω : ω.ℕ → ℕ → Ordering =
  elim-pair (λ _ _ ⇒ Ordering)
    'eq
    (λ _ o   ⇒ drop-ordering Ordering o 'lt)
    (λ _ o   ⇒ drop-ordering Ordering o 'gt)
    (λ _ _ x ⇒ x)

def compare : ℕ → ℕ → Ordering =
  λ m n ⇒
  case dup m return Ordering of { [m] ⇒
  case dup n return Ordering of { [n] ⇒ compareω m n } }

def lt : ω.ℕ → ω.ℕ → Bool =
  λ m n ⇒ from-ordering Bool 'true 'false 'false (compare m n)

def le : ω.ℕ → ω.ℕ → Bool =
  λ m n ⇒ from-ordering Bool 'true 'true 'false (compare m n)

def eq : ω.ℕ → ω.ℕ → Bool =
  λ m n ⇒ from-ordering Bool 'false 'true 'false (compare m n)

def gt : ω.ℕ → ω.ℕ → Bool =
  λ m n ⇒ from-ordering Bool 'false 'false 'true (compare m n)

def ge : ω.ℕ → ω.ℕ → Bool =
  λ m n ⇒ from-ordering Bool 'false 'true 'true (compare m n)


def0 plus-zero : (m : ℕ) → m ≡ plus m 0 : ℕ =
  λ m ⇒
  case m return m' ⇒ m' ≡ plus m' 0 : ℕ of {
    zero        ⇒ δ _ ⇒ 0;
    succ m', ih ⇒ δ 𝑖 ⇒ succ (ih @𝑖)
  };

def0 plus-succ : (m n : ℕ) → succ (plus m n) ≡ plus m (succ n) : ℕ =
  λ m n ⇒
  case m return m' ⇒ succ (plus m' n) ≡ plus m' (succ n) : ℕ of {
    zero       ⇒ δ _ ⇒ succ n;
    succ _, ih ⇒ δ 𝑖 ⇒ succ (ih @𝑖)
  };

def0 times-zero : (m : ℕ) → 0 ≡ timesω m 0 : ℕ =
  λ m ⇒
  case m return m' ⇒ 0 ≡ timesω m' 0 : ℕ of {
    zero        ⇒ δ _ ⇒ zero;
    succ m', ih ⇒ ih
  };

}