load "nat.quox"
load "either.quox"
load "maybe.quox"
load "sub.quox"


namespace nat.lt {

def0 LT : ℕ → ℕ → ★ =
  elim-pair¹ (λ _ _ ⇒ ★)
    False             -- 0      ≮ 0
    (λ   n p ⇒ True)  -- 0      < succ n
    (λ m   p ⇒ False) -- succ m ≮ 0
    (λ m n p ⇒ p)     -- succ m < succ n ⇔ m < n


def0 irr : sub.Irr2 ℕ ℕ LT =
  elim-pair (λ m n ⇒ (p q : LT m n) → p ≡ q : LT m n)
    false.irr (λ _ _ ⇒ true.irr) (λ _ _ ⇒ false.irr) (λ _ _ p ⇒ p)


-- [todo] quantities (which will need to inline and adapt elim-pair)
def elimω : 0.(P : (m n : ℕ) → LT m n → ★) →
            ω.(0.(n : ℕ) → P 0 (succ n) 'true) →
            ω.(0.(m n : ℕ) → 0.(lt : LT m n) →
               ω.(P m n lt) → P (succ m) (succ n) lt) →
            ω.(m n : ℕ) → 0.(lt : LT m n) → P m n lt =
  λ P p0s pss ⇒
    elim-pairω (λ m n ⇒ 0.(lt : LT m n) → P m n lt)
      (λ       ff ⇒ void (P 0 0 ff) ff)
      (λ   n p tt ⇒ p0s n)
      (λ m   p ff ⇒ void (P (succ m) 0 ff) ff)
      (λ m n p tt ⇒ pss m n tt (p tt))

def0 true-ty : (m n : ℕ) → LT m n → LT m n ≡ True : ★ =
  elim-pair¹ (λ m n ⇒ LT m n → LT m n ≡ True : ★)
    (λ       ff ⇒ void¹ (False ≡ True : ★) ff)
    (λ   n p tt ⇒ δ _ ⇒ True)
    (λ m   p ff ⇒ void¹ (False ≡ True : ★) ff)
    (λ n m p tf ⇒ p tf)

def0 true-val :
    (m n : ℕ) → (lt : LT m n) → Eq (𝑖 ⇒ true-ty m n lt @𝑖) lt 'true =
  let IsTrue : (m n : ℕ) → LT m n → ★ =
    λ m n lt ⇒ Eq (𝑖 ⇒ true-ty m n lt @𝑖) lt 'true in
  elim-pair (λ m n ⇒ (lt : LT m n) → IsTrue m n lt)
    (λ       ff ⇒ void (IsTrue 0 0 ff) ff)
    (λ   n p tt ⇒ δ _ ⇒ 'true)
    (λ m   p ff ⇒ void (IsTrue (succ m) 0 ff) ff)
    (λ n m p tf ⇒ p tf)

def revive : 0.(m n : ℕ) → 0.(LT m n) → LT m n =
  λ m n lt ⇒ coe (𝑘 ⇒ true-ty m n lt @𝑘) @1 @0 'true


def drop : 0.(A : ★) → 0.(m n : ℕ) → LT m n → A → A =
  λ A m n lt x ⇒ true.drop A (coe (𝑖 ⇒ true-ty m n lt @𝑖) lt) x

def0 succ-both : (m n : ℕ) → LT m n → LT (succ m) (succ n) =
  λ m n p ⇒ p

def0 succ-right : (m n : ℕ) → LT m n → LT m (succ n) =
  λ m n lt ⇒
    elimω (λ m n _ ⇒ LT m (succ n))
      (λ _        ⇒ 'true)
      (λ _ _ _ ih ⇒ ih)
      m n lt

def0 right-is-succ : (m n : ℕ) → LT m n → IsSucc n =
  λ m n lt ⇒
    elimω (λ _ n _ ⇒ IsSucc n) (λ _ ⇒ 'true) (λ _ _ _ _ ⇒ 'true) m n lt

def right-has-succ : 0.(m : ℕ) → (n : ℕ) → 0.(LT m n) → HasSucc n =
  λ m n lt ⇒
    case n return n' ⇒ 0.(LT m n') → HasSucc n' of {
      0      ⇒ λ lt ⇒ void (HasSucc 0) (right-is-succ m 0 lt);
      succ n ⇒ λ _  ⇒ (n, [δ _ ⇒ succ n])
    } lt

def0 right-not-zero : (m : ℕ) → Not (LT m 0) =
  λ m ⇒ case m return m' ⇒ Not (LT m' 0) of { 0 ⇒ λ v ⇒ v; succ _ ⇒ λ v ⇒ v }

def0 plus-right : (m n₀ n₁ : ℕ) → LT m n₀ → LT m (plus n₀ n₁) =
  λ m n₀ n₁ lt ⇒
    elimω (λ m n _ ⇒ LT m (plus n n₁)) (λ _ ⇒ 'true) (λ _ _ _ ih ⇒ ih) m n₀ lt

#[compile-scheme "(lambda% (m n) (if (< m n) dec.Yes dec.No))"]
def lt? : ω.(m n : ℕ) → Dec (LT m n) =
  elim-pairω (λ m n ⇒ Dec (LT m n))
    (No (LT 0 0) (λ v ⇒ v))
    (λ n p ⇒ Yes (LT 0 (succ n)) 'true)
    (λ m p ⇒ No  (LT (succ m) 0) (λ v ⇒ v))
    (λ m n p ⇒
      dec.elim (LT m n) (λ _ ⇒ Dec (LT (succ m) (succ n)))
        (λ yes ⇒ Yes (LT (succ m) (succ n)) yes)
        (λ no  ⇒ No  (LT (succ m) (succ n)) no) p)


def0 irrefl : (m n : ℕ) → LT m n → Not (m ≡ n : ℕ) =
  λ m n lt ⇒
    elimω (λ m n _ ⇒ Not (m ≡ n : ℕ))
      (λ n eq ⇒ zero-not-succ n eq)
      (λ m n _ ih eq ⇒ ih (succ-inj m n eq))
      m n lt

def0 asym : (m n : ℕ) → LT m n → Not (LT n m) =
  λ m n lt ⇒
    elimω (λ m n _ ⇒ Not (LT n m)) (λ _ ff ⇒ ff) (λ _ _ _ ih ff ⇒ ih ff) m n lt

def0 trans : (n₀ n₁ n₂ : ℕ) → LT n₀ n₁ → LT n₁ n₂ → LT n₀ n₂ =
  λ n₀ n₁ n₂ lt₀₁ lt₁₂ ⇒
  elimω (λ n₀ n₁ lt₀₁ ⇒ (n₂ : ℕ) → (lt₁₂ : LT n₁ n₂) → LT n₀ n₂)
    (λ n₁ n₂ ⇒
      case n₂ return n₂' ⇒ LT (succ n₁) n₂' → LT 0 n₂' of {
        0      ⇒ λ v ⇒ v;
        succ _ ⇒ λ _ ⇒ 'true
      })
    (λ n₀ n₁ lt₀₁ ih n₂ ⇒
      case n₂ return n₂' ⇒ LT (succ n₁) n₂' → LT (succ n₀) n₂' of {
        0       ⇒ λ v    ⇒ v;
        succ n₂ ⇒ λ lt₁₂ ⇒ ih n₂ lt₁₂
      })
    n₀ n₁ lt₀₁ n₂ lt₁₂

}

namespace nat {
def0 LT  = lt.LT
def  lt? = lt.lt?
}


namespace fin {

def0 Bounded : ℕ → ℕ → ★ = λ n i ⇒ nat.LT i n

def0 Fin : ℕ → ★ = λ n ⇒ Sub ℕ (Bounded n)

def fin : 0.(n : ℕ) → (i : ℕ) → 0.(Bounded n i) → Fin n =
  λ n ⇒ sub.sub ℕ (Bounded n)

def val : 0.(n : ℕ) → Fin n → ℕ =
  λ n ⇒ sub.val ℕ (Bounded n)

def0 val-eq : (n : ℕ) → (i j : Fin n) → val n i ≡ val n j : ℕ → i ≡ j : Fin n =
  λ n ⇒ sub.sub-eq ℕ (Bounded n) (λ i ⇒ nat.lt.irr i n)

def0 proof : (n : ℕ) → (i : Fin n) → nat.LT (val n i) n =
  λ n ⇒ sub.proof ℕ (Bounded n)


def0 no-fin0 : Not (Fin 0) =
  λ f0 ⇒ case f0 return False of { (i, lt) ⇒
    nat.lt.right-not-zero i (get0 (nat.LT i 0) lt)
  }


def fin? : ω.(n i : ℕ) → Maybe (Fin n) =
  λ n ⇒ sub.sub? ℕ (Bounded n) (λ i ⇒ nat.lt? i n)

def F0 : 0.(n : ℕ) → Fin (succ n) =
  λ n ⇒ fin (succ n) 0 'true
def FS : 0.(n : ℕ) → Fin n → Fin (succ n) =
  λ n i ⇒ fin (succ n) (succ (val n i)) (proof n i)

def weak : 0.(m n : ℕ) → 0.(nat.LT m n) → Fin m → Fin n =
  λ m n mn i' ⇒
    let i = val m i'; 0.im = proof m i' in
    fin n i (nat.lt.trans i m n im mn)


def bound-has-succ : (n : ℕ) → 0.(Fin n) → nat.HasSucc n =
  λ n i ⇒ nat.lt.right-has-succ (fst i) n (get0 (nat.LT (fst i) n) (snd i))

def elim' :
    0.(P : (n i : ℕ) → nat.LT i n → ★) →
    1.(pz : 0.(n : ℕ) → P (succ n) 0 'true) →
    ω.(ps : 0.(n i : ℕ) → 0.(lt : nat.LT i n) →
            P n i lt → P (succ n) (succ i) lt) →
    0.(n : ℕ) → (i : ℕ) → 0.(lt : nat.LT i n) → P n i lt =
  λ P pz ps n i lt ⇒
    case i return i' ⇒ 0.(n : ℕ) → 0.(lt : nat.LT i' n) → P n i' lt of {
      0 ⇒ λ n lt ⇒
        let0 npp = nat.lt.right-has-succ 0 n lt;
             p   = nat.has-succ.val n npp;
             np  = nat.has-succ.proof n npp in
        coe (𝑘 ⇒ P (np @𝑘) 0 (coe (𝑙 ⇒ nat.LT 0 (np @𝑙)) @0 @𝑘 lt)) @1 @0
            (pz p);
      succ i, ih ⇒ λ n lt ⇒
        let 0.npp = nat.lt.right-has-succ (succ i) n lt;
            0.p   = nat.has-succ.val n npp;
            0.np  = nat.has-succ.proof n npp;
            0.lt' : nat.LT i p = coe (𝑘 ⇒ nat.LT (succ i) (np @𝑘)) lt;
            0.lteq : Eq (𝑘 ⇒ nat.LT (succ i) (np @𝑘)) lt lt' =
              δ 𝑘 ⇒ coe (𝑙 ⇒ nat.LT (succ i) (np @𝑙)) @0 @𝑘 lt;
            1.almost : P (succ p) (succ i) lt' = ps p i lt' (ih p lt') in
        coe (𝑘 ⇒ P (np @𝑘) (succ i) (lteq @𝑘)) @1 @0 almost;
    } n lt

def elim : 0.(P : (n : ℕ) → Fin n → ★) →
           (pz : 0.(n : ℕ) → P (succ n) (F0 n)) →
           (ps : 0.(n : ℕ) → 0.(i : Fin n) →
                 P n i → P (succ n) (FS n i)) →
           0.(n : ℕ) → (i : Fin n) → P n i =
  λ P pz ps n ilt ⇒
    case ilt return ilt' ⇒ P n ilt' of { (i, lt) ⇒
      let0 lt = get0 (nat.LT i n) lt in
      drop0 (nat.LT i n) (P n (i, [lt])) lt
      (elim' (λ n i lt ⇒ P n (i, [lt])) pz (λ n i lt ⇒ ps n (i, [lt])) n i lt)
    }

{-
def elim : 0.(P : (n : ℕ) → Fin n → ★) →
           (pz : 0.(n : ℕ) → P (succ n) (F0 n)) →
           (ps : 0.(n : ℕ) → 0.(i : Fin n) →
                 P n i → P (succ n) (FS n i)) →
           0.(n : ℕ) → (i : Fin n) → P n i =
  λ P pz ps n ilt ⇒
    let i = val n ilt; 0.lt : nat.LT i n = proof n ilt;
        0.pp = nat.lt.right-has-succ i n lt;
        0.p  = nat.has-succ.val n pp; 0.np = nat.has-succ.proof n pp;
        0.RES : ℕ → ℕ → ★ =
          λ i n ⇒ (lt : nat.LT i n) × P n (i, [lt]);
        res : RES i (succ p) =
          case i
          return i' ⇒ 0.(p : ℕ) → 0.(nat.LT i' (succ p)) → RES i' (succ p)
          of {
            0 ⇒ λ p _ ⇒ ('true, pz p);
            succ i, IH ⇒ λ p lt ⇒
              let 0.qq = nat.lt.right-has-succ i p lt;
                  0.q  = nat.has-succ.val p qq; 0.pq = nat.has-succ.proof p qq;
                  0.lt : nat.LT i (succ q) = coe (𝑘 ⇒ nat.LT i (pq @𝑘)) lt;
              in
              case IH q lt return RES (succ i) (succ p) of { (lt', ih') ⇒
                let lt : nat.LT (succ i) (succ p) =
                      coe (𝑘 ⇒ nat.LT i (pq @𝑘)) @1 @0 lt';
                    ih : P p (i, [lt]) =
                      coe (𝑘 ⇒ P (pq @𝑘) (i, [coe (𝑙 ⇒ nat.LT i (pq @𝑙)) @1 @𝑘 lt']))
                          @1 @0 ih';
                    res : P (succ p) (succ i, [lt]) =
                      ps p (i, [lt]) ih;
                in
                (lt, res)
              }
          } p (coe (𝑘 ⇒ nat.LT i (np @𝑘)) lt);
    in
    case coe (𝑘 ⇒ RES i (np @𝑘)) @1 @0 res
    return P n ilt
    of { (lt', res) ⇒
      nat.lt.drop (P n ilt) i n lt' res
    }
-}

}


def0 Fin = fin.Fin
def  F0  = fin.F0
def  FS  = fin.FS