BiNat.idr

module BiNat

import Data.Vect

%default total

public export
data BiNat : Type where
  I  : BiNat
  N0 : BiNat -> BiNat
  N1 : BiNat -> BiNat

public export
Uninhabited (I = N0 _) where
  uninhabited Refl impossible
public export
Uninhabited (N0 _ = I) where
  uninhabited Refl impossible
public export
Uninhabited (I = N1 _) where
  uninhabited Refl impossible
public export
Uninhabited (N1 _ = I) where
  uninhabited Refl impossible
public export
Uninhabited (N0 _ = N1 _) where
  uninhabited Refl impossible
public export
Uninhabited (N1 _ = N0 _) where
  uninhabited Refl impossible

public export
Eq BiNat where
  I      == I      = True
  I      == (N0 n) = False
  I      == (N1 n) = False
  (N0 m) == I      = False
  (N0 m) == (N0 n) = m == n
  (N0 m) == (N1 n) = False
  (N1 m) == I      = False
  (N1 m) == (N0 n) = False
  (N1 m) == (N1 n) = m == n

public export
Ord BiNat where
  compare I      I      = EQ
  compare I      _      = LT
  compare (N0 m) I      = GT
  compare (N0 m) (N0 n) = compare m n
  compare (N0 m) (N1 n) = case compare m n of
    LT => LT
    EQ => LT
    GT => GT
  compare (N1 m) I      = GT
  compare (N1 m) (N0 n) = case compare m n of
    LT => LT
    EQ => GT
    GT => GT
  compare (N1 m) (N1 n) = compare m n

public export
data LTE : (m, n: BiNat) -> Type where
  LTEI : LTE I n
  LTERefl : (n : BiNat) -> LTE n n
  LTETail00 : {m, n : BiNat} -> LTE m n -> LTE (N0 m) (N0 n)
  LTETail01 : {m, n : BiNat} -> LTE m n -> LTE (N0 m) (N1 n)
  LTETail10 : {m, n : BiNat} -> LTE m n -> Not (m = n) -> LTE (N1 m) (N0 n)
  LTETail11 : {m, n : BiNat} -> LTE m n -> LTE (N1 m) (N1 n)

public export
Uninhabited (LTE (N0 _) I) where
  uninhabited LTEI impossible
  uninhabited (LTERefl _) impossible
  uninhabited (LTETail00 lte) impossible
  uninhabited (LTETail01 lte) impossible
  uninhabited (LTETail10 lte notEq) impossible
  uninhabited (LTETail11 lte) impossible
public export
Uninhabited (LTE (N1 _) I) where
  uninhabited LTEI impossible
  uninhabited (LTERefl _) impossible
  uninhabited (LTETail00 lte) impossible
  uninhabited (LTETail01 lte) impossible
  uninhabited (LTETail10 lte notEq) impossible
  uninhabited (LTETail11 lte) impossible

lteAntisynmetric : {a, b : BiNat} -> LTE a b -> LTE b a -> a = b
lteAntisynmetric                       (LTERefl _)             _                       = Refl
lteAntisynmetric                       _                       (LTERefl _)             = Refl
lteAntisynmetric {a = I}    {b = I}    LTEI                    LTEI                    = Refl
lteAntisynmetric {a = I}    {b = N0 b} LTEI                    lteBA                   = absurd (uninhabited lteBA)
lteAntisynmetric {a = I}    {b = N1 b} LTEI                    lteBA                   = absurd (uninhabited lteBA)
lteAntisynmetric {a = N0 a} {b = I}    lteAB                   LTEI                    = absurd (uninhabited lteAB)
lteAntisynmetric {a = N0 a} {b = N0 b} (LTETail00 lteAB)       (LTETail00 lteBA)       = rewrite lteAntisynmetric lteAB lteBA in Refl
lteAntisynmetric {a = N0 a} {b = N1 b} (LTETail01 lteAB)       (LTETail10 lteBA notEq) = absurd (notEq (lteAntisynmetric lteBA lteAB))
lteAntisynmetric {a = N1 a} {b = I}    lteAB                   LTEI                    = absurd (uninhabited lteAB)
lteAntisynmetric {a = N1 a} {b = N0 b} (LTETail10 lteAB notEq) (LTETail01 lteBA)       = absurd (notEq (lteAntisynmetric lteAB lteBA))
lteAntisynmetric {a = N1 a} {b = N1 b} (LTETail11 lteAB)       (LTETail11 lteBA)       = rewrite lteAntisynmetric lteAB lteBA in Refl

lteTransitive : {a, b, c : BiNat} -> LTE a b -> LTE b c -> LTE a c
lteTransitive {a = I}                          LTEI                    _                       = LTEI
lteTransitive {a}        {b = a}    {c}        (LTERefl _)             lteBC                   = lteBC
lteTransitive {a = N0 a} {b = N0 b} {c = N0 b} (LTETail00 lteAB)       (LTERefl _)             = LTETail00 lteAB
lteTransitive {a = N0 a} {b = N0 b} {c = N0 c} (LTETail00 lteAB)       (LTETail00 lteBC)       = LTETail00 (lteTransitive lteAB lteBC)
lteTransitive {a = N0 a} {b = N0 b} {c = N1 c} (LTETail00 lteAB)       (LTETail01 lteBC)       = LTETail01 (lteTransitive lteAB lteBC)
lteTransitive {a = N0 a} {b = N1 b} {c = N1 b} (LTETail01 lteAB)       (LTERefl _)             = LTETail01 lteAB
lteTransitive {a = N0 a} {b = N1 b} {c = N0 c} (LTETail01 lteAB)       (LTETail10 lteBC notEq) = LTETail00 (lteTransitive lteAB lteBC)
lteTransitive {a = N0 a} {b = N1 b} {c = N1 c} (LTETail01 lteAB)       (LTETail11 lteBC)       = LTETail01 (lteTransitive lteAB lteBC)
lteTransitive {a = N1 a} {b = N0 b} {c = N0 b} (LTETail10 lteAB notEq) (LTERefl (N0 _))        = LTETail10 lteAB notEq
lteTransitive {a = N1 a} {b = N0 b} {c = N0 c} (LTETail10 lteAB notEq) (LTETail00 lteBC)       =
  let acNotEq = \eq => notEq (lteAntisynmetric lteAB (replace {p = \x => LTE b x} (sym eq) lteBC)) in
  LTETail10 (lteTransitive lteAB lteBC) acNotEq
lteTransitive {a = N1 a} {b = N0 b} {c = N1 c} (LTETail10 lteAB notEq) (LTETail01 lteBC)       = LTETail11 (lteTransitive lteAB lteBC)
lteTransitive {a = N1 a} {b = N1 b} {c = N0 c} (LTETail11 lteAB)       (LTETail10 lteBC notEq) =
  let acNotEq = \eq => notEq (lteAntisynmetric lteBC (replace {p = \x => LTE x b} eq lteAB)) in
  LTETail10 (lteTransitive lteAB lteBC) acNotEq
lteTransitive {a = N1 a} {b = N1 b} {c = N1 b} (LTETail11 lteAB)       (LTERefl _) = LTETail11 lteAB
lteTransitive {a = N1 a} {b = N1 b} {c = N1 c} (LTETail11 lteAB)       (LTETail11 lteBC)       = LTETail11 (lteTransitive lteAB lteBC)

data LT : BiNat -> BiNat -> Type where
  LTC : {m, n : BiNat} -> LTE m n -> Not (m = n) -> LT m n

ltTransitive : {a, b, c : BiNat} -> LT a b -> LT b c -> LT a c
ltTransitive {a} {b} {c} (LTC lteAB notEqAB) (LTC lteBC notEqBC) =
  let lteAC = lteTransitive lteAB lteBC in
  let notEqAC = \eq => notEqAB (lteAntisynmetric lteAB (replace {p = \x => LTE b x} eq lteBC)) in
  LTC lteAC (\eq => notEqAC (sym eq))

public export
succ : BiNat -> BiNat
succ I      = N0 I
succ (N0 n) = N1 n
succ (N1 n) = N0 (succ n)

public export
pred : BiNat -> BiNat
pred I           = I
pred (N0 I)      = I
pred (N0 (N0 n)) = N1 (pred (N0 n))
pred (N0 (N1 n)) = N1 (N0 n)
pred (N1 n)      = N0 n

succNotI : (n : BiNat) -> Not (succ n = I)
succNotI I prf impossible
succNotI (N0 n) prf impossible
succNotI (N1 n) prf impossible

succNotEq : (n : BiNat) -> Not (n = succ n)
succNotEq I prf impossible
succNotEq (N0 n) prf impossible
succNotEq (N1 n) prf impossible

N0Injective : (m, n : BiNat) -> N0 m = N0 n -> m = n
N0Injective m n prf = case prf of Refl => Refl

N1Injective : (m, n : BiNat) -> N1 m = N1 n -> m = n
N1Injective m n prf = case prf of Refl => Refl

succInjective : (m, n : BiNat) -> succ m = succ n -> m = n
succInjective I      I      Refl = Refl
succInjective I      (N0 n) prf impossible
succInjective I      (N1 n) prf  = absurd $ succNotI n (sym $ N0Injective I (succ n) prf)
succInjective (N0 m) I      prf impossible
succInjective (N0 m) (N0 n) prf  = rewrite N1Injective m n prf in Refl
succInjective (N0 m) (N1 n) prf impossible
succInjective (N1 m) I      prf  = absurd $ succNotI m (N0Injective (succ m) I prf)
succInjective (N1 m) (N0 n) prf impossible
succInjective (N1 m) (N1 n) prf  = rewrite succInjective m n (N0Injective (succ m) (succ n) prf) in Refl

predOfSucc : (n : BiNat) -> pred (succ n) = n
predOfSucc I                = Refl
predOfSucc (N0 n)           = Refl
predOfSucc (N1 I)           = Refl
predOfSucc (N1 (N0 n))      = Refl
predOfSucc (N1 (N1 I))      = Refl
predOfSucc (N1 (N1 (N0 n))) = Refl
predOfSucc (N1 (N1 (N1 n))) = rewrite predOfSucc (N1 n) in Refl

succOfPred : (n : BiNat) -> Not (n = I) -> succ (pred n) = n
succOfPred I           notI = absurd (notI Refl)
succOfPred (N0 I)      _    = Refl
succOfPred (N0 (N0 n)) _    = rewrite succOfPred (N0 n) uninhabited in Refl
succOfPred (N0 (N1 n)) _    = Refl
succOfPred (N1 n)      _    = Refl

public export
plus : BiNat -> BiNat -> BiNat
plus I      n      = succ n
plus (N0 m) I      = N1 m
plus (N0 m) (N0 n) = N0 (plus m n)
plus (N0 m) (N1 n) = N1 (plus m n)
plus (N1 m) I      = N0 (succ m)
plus (N1 m) (N0 n) = N1 (plus m n)
plus (N1 m) (N1 n) = N0 (succ (plus m n))

plusCommutes : (m, n : BiNat) -> plus m n = plus n m
plusCommutes I      I      = Refl
plusCommutes I      (N0 n) = Refl
plusCommutes I      (N1 n) = Refl
plusCommutes (N0 m) I      = Refl
plusCommutes (N0 m) (N0 n) = rewrite plusCommutes m n in Refl
plusCommutes (N0 m) (N1 n) = rewrite plusCommutes m n in Refl
plusCommutes (N1 m) I      = Refl
plusCommutes (N1 m) (N0 n) = rewrite plusCommutes m n in Refl
plusCommutes (N1 m) (N1 n) = rewrite plusCommutes m n in Refl

plusISucc : (n : BiNat) -> plus n I = succ n
plusISucc n = rewrite plusCommutes I n in Refl

plusBySucc : (m, n : BiNat) -> plus m (succ n) = succ (plus m n)
plusBySucc I      n      = Refl
plusBySucc (N0 m) I      = rewrite plusISucc m in Refl
plusBySucc (N0 m) (N0 n) = Refl
plusBySucc (N0 m) (N1 n) = rewrite plusBySucc m n in Refl
plusBySucc (N1 m) I      = rewrite plusISucc m in Refl
plusBySucc (N1 m) (N0 n) = Refl
plusBySucc (N1 m) (N1 n) = rewrite plusBySucc m n in Refl

n0IsDouble : (n : BiNat) -> N0 n = plus n n
n0IsDouble I      = Refl
n0IsDouble (N0 n) = rewrite n0IsDouble n in Refl
n0IsDouble (N1 n) = rewrite sym $ n0IsDouble n in Refl

plusAssociative : (a, b, c : BiNat) -> plus (plus a b) c = plus a (plus b c)
plusAssociative I      b c =
  rewrite plusCommutes (succ b) c in
  rewrite plusCommutes b c in
  plusBySucc c b
plusAssociative (N0 a) b c =
  rewrite n0IsDouble a in
  rewrite plusAssociative a a b in
  rewrite plusAssociative a (plus a b) c in
  rewrite plusAssociative a a (plus b c) in
  rewrite plusAssociative a b c in Refl
plusAssociative (N1 a) b c =
  rewrite plusCommutes (N1 a) b in
  rewrite plusBySucc b (N0 a) in
  rewrite plusCommutes (succ (plus b (N0 a))) c in
  rewrite plusBySucc c (plus b (N0 a)) in
  rewrite plusCommutes (N1 a) (plus b c) in
  rewrite plusBySucc (plus b c) (N0 a) in
  rewrite plusCommutes b c in
  rewrite n0IsDouble a in
  rewrite plusCommutes b (plus a a) in
  rewrite plusAssociative a a b in
  rewrite plusCommutes c (plus a (plus a b)) in
  rewrite plusCommutes (plus c b) (plus a a) in
  rewrite plusCommutes c b in
  rewrite plusAssociative a a (plus b c) in
  rewrite sym $ plusAssociative a b c in
  rewrite plusAssociative a (plus a b) c in Refl

composeFunctions : {T : BiNat -> Type} ->
  ((k : BiNat) -> T k -> T (succ k)) ->
  (m, n : BiNat) -> T m -> T (plus m n)
composeFunctions f m I      pm = rewrite plusISucc m in f m pm
composeFunctions f m (N0 n) pm =
  rewrite n0IsDouble n in
  rewrite sym $ plusAssociative m n n in
  let pmn = composeFunctions f m n pm in
  composeFunctions f (plus m n) n pmn
composeFunctions f m (N1 n) pm =
  rewrite plusBySucc m (N0 n) in
  rewrite n0IsDouble n in
  rewrite sym $ plusAssociative m n n in
  let pmn = composeFunctions f m n pm in
  let pmnn = composeFunctions f (plus m n) n pmn in
  f (plus (plus m n) n) pmnn

public export
induction : {P : BiNat -> Type} ->
            P I ->
            ((n : BiNat) -> P n -> P (succ n)) ->
            (n : BiNat) -> P n
induction pI pSucc I      = pI
induction pI pSucc (N0 n) =
  rewrite n0IsDouble n in
  composeFunctions pSucc n n (induction pI pSucc n)
induction pI pSucc (N1 n) =
  let l1 = composeFunctions pSucc n n (induction pI pSucc n) in
  let l2 = replace {p = P} (sym $ n0IsDouble n) l1 in
  pSucc (N0 n) l2

lteFromLt : {m, n : BiNat} -> LT m n -> LTE m n
lteFromLt (LTC lte notEq) = lte

ltSucc : (n : BiNat) -> LT n (succ n)
ltSucc I      = LTC LTEI (\eq => absurd (uninhabited eq))
ltSucc (N0 n) = LTC (LTETail01 (LTERefl n)) uninhabited
ltSucc (N1 n) = LTC (LTETail10 (lteFromLt (ltSucc n)) (succNotEq n)) uninhabited

plusLt : (m, n : BiNat) -> LT m (plus m n)
plusLt m I      = rewrite plusISucc m in ltSucc m
plusLt m (N0 n) =
  rewrite n0IsDouble n in
  rewrite sym $ plusAssociative m n n in
  ltTransitive (plusLt m n) (plusLt (plus m n) n)
plusLt m (N1 n) =
  rewrite plusBySucc m (N0 n) in
  rewrite n0IsDouble n in
  rewrite sym $ plusAssociative m n n in
  let l1 = ltTransitive (plusLt m n) (plusLt (plus m n) n) in
  ltTransitive l1 (ltSucc _)

succPlusLeft : (m, n : BiNat) -> succ (plus m n) = plus (succ m) n
succPlusLeft m n =
  rewrite plusCommutes (succ m) n in
  rewrite plusBySucc n m in
  rewrite plusCommutes m n in Refl

complement : (m, n : BiNat) -> LT m n -> (k : BiNat ** plus m k = n)
complement = induction
  {P = \m => (n : BiNat) -> LT m n -> (k : BiNat ** plus m k = n)}
  (\n => \(LTC _ notEq) => (pred n ** rewrite succOfPred n (\x => notEq (sym x)) in Refl))
  $ \m, pm, n, lt =>
    let lt2 = ltTransitive (ltSucc m) lt in
    let (k ** eq) = pm n lt2 in
    case k of
      I => case lt of LTC _ notEq => absurd (notEq (replace {p = \x => x = n} (plusISucc m) eq))
      N0 I =>
        let eq2 = replace {p = \x => x = n} (plusBySucc m I) eq in
        let eq3 = replace {p = \x => x = n} (succPlusLeft m I) eq2 in
        (I ** eq3)
      N0 (N0 k2) =>
        let eq2 = replace {p = \x => plus m x = n} (sym $ succOfPred (N0 (N0 k2)) uninhabited) eq in
        let eq3 = replace {p = \x => x = n} (plusBySucc m (N1 (pred (N0 k2)))) eq2 in
        let eq4 = replace {p = \x => x = n} (succPlusLeft m (N1 (pred (N0 k2)))) eq3 in
        (N1 (pred (N0 k2)) ** eq4)
      N0 (N1 k2) =>
        let eq2 = replace {p = \x => x = n} (plusBySucc m (N1 (N0 k2))) eq in
        let eq3 = replace {p = \x => x = n} (succPlusLeft m (N1 (N0 k2))) eq2 in
        (N1 (N0 k2) ** eq3)
      N1 k2 =>
        let eq2 = replace {p = \x => x = n} (plusBySucc m (N0 k2)) eq in
        let eq3 = replace {p = \x => x = n} (succPlusLeft m (N0 k2)) eq2 in
        (N0 k2 ** eq3)