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


namespace fin {

def0 LT : ℕ → ℕ → ★ =
  λ m n ⇒
    nat.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
      m n


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

def0 lt-irr-het :
    (m m' n n' : ℕ) → (mm : m ≡ m' : ℕ) → (nn : n ≡ n' : ℕ) →
    (p : LT m n) → (q : LT m' n') →
    Eq (𝑖 ⇒ LT (mm @𝑖) (nn @𝑖)) p q =
  λ m m' n n' mm nn p q ⇒ δ 𝑖 ⇒
    lt-irr (mm @𝑖) (nn @𝑖)
           (coe (𝑗 ⇒ LT (mm @𝑗) (nn @𝑗)) @0 @𝑖 p)
           (coe (𝑗 ⇒ LT (mm @𝑗) (nn @𝑗)) @1 @𝑖 q) @𝑖

def0 lt-irr-het-left :
    (m m' n : ℕ) → (mm : m ≡ m' : ℕ) → (p : LT m n) → (q : LT m' n) →
    Eq (𝑖 ⇒ LT (mm @𝑖) n) p q =
  λ m m' n mm ⇒ lt-irr-het m m' n n mm (δ _ ⇒ n)


def0 lt-true : (m n : ℕ) → LT m n → LT m n ≡ True : ★ =
  λ m n p ⇒
    nat.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)
      m n p


#[compile-scheme "(lambda% (m n) (if (< m n) dec.Yes dec.No))"]
def lt? : ω.(m n : ℕ) → Dec (LT m n) =
  nat.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 Fin : ℕ → ★ =
  λ n ⇒ (i : ℕ) × [0.LT i n]


def to-ℕ : 0.(n : ℕ) → Fin n → ℕ =
  λ n i ⇒ case i return ℕ of { (i, p) ⇒ drop0 (LT i n) ℕ p i }

def0 to-ℕ-fst : (n : ℕ) → (i : Fin n) → to-ℕ n i ≡ fst i : ℕ =
  λ n i ⇒ drop0-eq (LT (fst i) n) ℕ (snd i) (fst i)

def0 to-ℕ-eq : (n : ℕ) → (i j : Fin n) →
               to-ℕ n i ≡ to-ℕ n j : ℕ → i ≡ j : Fin n =
  λ n i' j' ij' ⇒
    let i = fst i'; ilt = get0 (LT i n) (snd i');
        j = fst j'; jlt = get0 (LT j n) (snd j');
        ij : (i ≡ j : ℕ) =
          coe (𝑘 ⇒ to-ℕ-fst n i' @𝑘 ≡ j : ℕ)
            (coe (𝑘 ⇒ to-ℕ n i' ≡ to-ℕ-fst n j' @𝑘 : ℕ) ij');
        ltt : Eq (𝑘 ⇒ LT (ij @𝑘) n) ilt jlt =
          lt-irr-het-left i j n ij ilt jlt in
    δ 𝑘 ⇒ (ij @𝑘, [ltt @𝑘])


def fin? : ω.(n i : ℕ) → Maybe (Fin n) =
  λ n i ⇒
    dec.elim (LT i n) (λ _ ⇒ Maybe (Fin n))
      (λ yes ⇒ Just (Fin n) (i, [yes]))
      (λ no  ⇒ Nothing (Fin n))
      (lt? i n)


def F0 : 0.(n : ℕ) → Fin (succ n) = λ _ ⇒ (0, ['true])
def FS : 0.(n : ℕ) → Fin n → Fin (succ n) =
  λ n i ⇒ case i return Fin (succ n) of { (i, p) ⇒ (succ i, p) }

def dup! : 0.(n : ℕ) → (i : Fin n) → Dup (Fin n) i =
  λ n ilt ⇒
    case ilt        return ilt' ⇒ Dup (Fin n) ilt'     of { (i, lt0) ⇒
    case lt0        return ilt' ⇒ Dup (Fin n) (i, lt0) of { [lt] ⇒
    case nat.dup! i return        Dup (Fin n) (i, lt0) of { (iω, ii0) ⇒
      case iω
      return iω' ⇒ 0.(iω' ≡ iω : [ω.ℕ]) → Dup (Fin n) (i, lt0)
      of { [i!] ⇒ λ iiω ⇒
        let 0.iωi : iω ≡ [i] : [ω.ℕ] = get0 (iω ≡ [i] : [ω.ℕ]) ii0;
        in
        0
      } (δ _ ⇒ iω)
    }}}

{-
    case ilt return ilt' ⇒ Dup (Fin n) ilt'      of { (i, lt0) ⇒
    case lt0 return lt0' ⇒ Dup (Fin n) (i, lt0') of { [lt] ⇒
    case nat.dup! i return Dup (Fin n) (i, [lt]) of { (iω, eq0) ⇒
      let ω.i! = fst ieq!;
          0.ii  : i! ≡ i : ℕ = get0 (i! ≡ i : ℕ) (snd ieq!);
          0.lt! : LT i! n    = coe (𝑘 ⇒ LT (ii @𝑘) n) @1 @0 lt;
          0.ltt : Eq (𝑘 ⇒ LT (ii @𝑘) n) lt! lt =
            lt-irr-het-left i! i n ii lt! lt;
          ω.ilt! : Fin n = (i!, [lt!]);
          0.iltt : ilt! ≡ ilt : Fin n =
            δ 𝑘 ⇒ [(ii @𝑘, [ltt @𝑘])];
      in
      ([ilt!], [iltt])
      -- [((i!, [lt!]), [δ 𝑘 ⇒ (ii @𝑘, [ltt @𝑘])])]
    }}}
-}

{-
def dup : 0.(n : ℕ) → Fin n → [ω.Fin n] =
  λ n i ⇒ appω (Sing (Fin n) i) (Fin n) (λ p ⇒ fst p) (dup! n i)
-}

{-
def0 dup-ok : (n : ℕ) → (i : Fin n) → dup n i ≡ [i] : [ω.Fin n] =
  λ n i ⇒

    appω (Sing (Fin n) i) [0.dup n i ≡ [i] : [ω.Fin n]]
         (λ p ⇒ snd p) (dup! n i)
-}

{-
def0 dup-ok : (n : ℕ) → (i : Fin n) → dup n i ≡ [i] : [ω.Fin n] =
  λ n i ⇒
    case dup! n i return i' ⇒ fst i' ≡ [i] : 
-}

{-
def dup : 0.(n : ℕ) → Fin n → [ω.Fin n] =
  λ n ilt ⇒
  case ilt return [ω.Fin n] of { (i, lt0) ⇒
  case lt0 return [ω.Fin n] of { [lt] ⇒
    case nat.dup i
    return i' ⇒ 0.(i' ≡ [i] : [ω.ℕ]) → [ω.Fin n]
    of { [i!] ⇒ λ iiω ⇒
      let0 ii  : i! ≡ i : ℕ = boxω-inj ℕ i! i iiω;
           lt! : LT i! n    = coe (𝑘 ⇒ LT (ii @𝑘) n) @1 @0 lt in
      [(i!, [lt!])]
    } (nat.dup-ok i)
  }}
-}

{-
def0 dup-ok : (n : ℕ) → (i : Fin n) → dup n i ≡ [i] : [ω.Fin n] =
  λ n ilt ⇒ δ 𝑘 ⇒
    let i = fst ilt; lt = get0 (LT i n) (snd ilt);
    in
-}

{-
def dup-ok : 0.(n : ℕ) → (i : Fin n) → dup n i ≡ [i] : [ω.Fin n] =
  λ n i ⇒
  case i return i' ⇒ dup n i' ≡ [i'] : [ω.Fin n] of { (i, lt0) ⇒
  case lt0 return lt' ⇒ dup n (i, lt') ≡ [(i, lt')] : [ω.Fin n] of { [lt] ⇒
    case nat.dup i
    return i' ⇒ (i' ≡ [i] : [ω.ℕ]) →
                dup n (i, [lt]) ≡ [(i, [lt])] : [ω.Fin n]
    of { [i!] ⇒ λ iiω ⇒
      let0 ii  : i! ≡ i : ℕ = boxω-inj ℕ i! i iiω;
           lt! : LT i! n    = coe (𝑘 ⇒ LT (ii @𝑘) n) @1 @0 lt;
           ltt : Eq (𝑘 ⇒ LT (ii @𝑘) n) lt! lt =
             lt-irr-het i! i n n ii (δ _ ⇒ n) lt! lt
      in
      δ 𝑘 ⇒ [(ii @𝑘, [ltt @𝑘])]
    } (nat.dup-ok i)
  }}
-}


{-
def0 dup-ok : (n : ℕ) → (i : Fin n) → dup n i ≡ [i] : [ω.Fin n] =
  λ n ilt ⇒
    case ilt return i' ⇒ dup n i' ≡ [i'] : [ω.Fin n] of { (i, lt0) ⇒
    case lt0 return lt' ⇒ dup n (i, lt') ≡ [(i, lt')] : [ω.Fin n] of { [lt] ⇒
      let i! = getω ℕ (nat.dup i);
          ii  : i! ≡ i : ℕ = δ 𝑘 ⇒ getω ℕ (nat.dup-ok i @𝑘);
          lt! : LT i! n = coe (𝑘 ⇒ LT (ii @𝑘) n) @1 @0 lt;
          ltt : Eq (𝑘 ⇒ LT (ii @𝑘) n) lt! lt =
            lt-irr-het i! i n n ii (δ _ ⇒ n) lt! lt
      in
      δ 𝑘 ⇒ [(ii @𝑘, [ltt @𝑘])]
  }}
-}

}

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