module Decidable.Order

import Decidable.Decidable
import Decidable.Equality
import Data.Fin
import Data.Fun
import Data.Rel

%access public export

--------------------------------------------------------------------------------
-- Utility Lemmas
--------------------------------------------------------------------------------

--------------------------------------------------------------------------------
-- Preorders, Posets, total Orders, Equivalencies, Congruencies
--------------------------------------------------------------------------------

interface Preorder t (po : t -> t -> Type) where
  total transitive : (a : t) -> (b : t) -> (c : t) -> po a b -> po b c -> po a c
  total reflexive : (a : t) -> po a a

interface (Preorder t po) => Poset t (po : t -> t -> Type) where
  total antisymmetric : (a : t) -> (b : t) -> po a b -> po b a -> a = b

interface (Poset t to) => Ordered t (to : t -> t -> Type) where
  total order : (a : t) -> (b : t) -> Either (to a b) (to b a)

interface (Preorder t eq) => Equivalence t (eq : t -> t -> Type) where
  total symmetric : (a : t) -> (b : t) -> eq a b -> eq b a

interface (Equivalence t eq) => Congruence t (f : t -> t) (eq : t -> t -> Type) where
  total congruent : (a : t) -> 
                    (b : t) -> 
                    eq a b -> 
                    eq (f a) (f b)

minimum : (Ordered t to) => t -> t -> t
minimum {to} x y with (order {to} x y)
  | Left _ = x
  | Right _ = y

maximum : (Ordered t to) => t -> t -> t
maximum {to} x y with (order {to} x y)
  | Left _ = y
  | Right _ = x

--------------------------------------------------------------------------------
-- Syntactic equivalence (=)
--------------------------------------------------------------------------------

implementation Preorder t ((=) {A = t} {B = t}) where
  transitive a b c = trans {a = a} {b = b} {c = c}
  reflexive a = Refl

implementation Equivalence t ((=) {A = t} {B = t}) where
  symmetric a b prf = sym prf

implementation Congruence t f ((=) {A = t} {B = t}) where
  congruent a b = cong {a = a} {b = b} {f = f}

--------------------------------------------------------------------------------
-- Natural numbers
--------------------------------------------------------------------------------

total LTEIsTransitive : (m : Nat) -> (n : Nat) -> (o : Nat) ->
                           LTE m n -> LTE n o ->
                           LTE m o
LTEIsTransitive Z n o                 LTEZero                  nlteo   = LTEZero
LTEIsTransitive (S m) (S n) (S o) (LTESucc mlten)    (LTESucc nlteo)   = LTESucc (LTEIsTransitive m n o mlten nlteo)

total LTEIsReflexive : (n : Nat) -> LTE n n
LTEIsReflexive Z      = LTEZero
LTEIsReflexive (S n)  = LTESucc (LTEIsReflexive n)

implementation Preorder Nat LTE where
  transitive = LTEIsTransitive
  reflexive  = LTEIsReflexive

total LTEIsAntisymmetric : (m : Nat) -> (n : Nat) ->
                              LTE m n -> LTE n m -> m = n
LTEIsAntisymmetric Z Z         LTEZero LTEZero = Refl
LTEIsAntisymmetric (S n) (S m) (LTESucc mLTEn) (LTESucc nLTEm) with (LTEIsAntisymmetric n m mLTEn nLTEm)
   LTEIsAntisymmetric (S n) (S n) (LTESucc mLTEn) (LTESucc nLTEm)    | Refl = Refl           


implementation Poset Nat LTE where
  antisymmetric = LTEIsAntisymmetric

total zeroNeverGreater : {n : Nat} -> LTE (S n) Z -> Void
zeroNeverGreater {n} LTEZero     impossible
zeroNeverGreater {n} (LTESucc _) impossible

total zeroAlwaysSmaller : {n : Nat} -> LTE Z n
zeroAlwaysSmaller = LTEZero

total ltesuccinjective : {n : Nat} -> {m : Nat} -> (LTE n m -> Void) -> LTE (S n) (S m) -> Void
ltesuccinjective {n} {m} disprf (LTESucc nLTEm) = void (disprf nLTEm)
ltesuccinjective {n} {m} disprf LTEZero         impossible


total decideLTE : (n : Nat) -> (m : Nat) -> Dec (LTE n m)
decideLTE    Z      y  = Yes LTEZero
decideLTE (S x)     Z  = No  zeroNeverGreater
decideLTE (S x)   (S y) with (decEq (S x) (S y))
  | Yes eq      = rewrite eq in Yes (reflexive (S y))
  | No _ with (decideLTE x y)
    | Yes nLTEm = Yes (LTESucc nLTEm)
    | No  nGTm  = No (ltesuccinjective nGTm)

implementation Decidable [Nat,Nat] LTE where
  decide = decideLTE

total
lte : (m : Nat) -> (n : Nat) -> Dec (LTE m n)
lte m n = decide {ts = [Nat,Nat]} {p = LTE} m n

total
shift : (m : Nat) -> (n : Nat) -> LTE m n -> LTE (S m) (S n)
shift m n mLTEn = LTESucc mLTEn
      
implementation Ordered Nat LTE where
  order Z      n = Left LTEZero
  order m      Z = Right LTEZero
  order (S k) (S j) with (order {to=LTE} k j)
    order (S k) (S j) | Left  prf = Left  (shift k j prf)
    order (S k) (S j) | Right prf = Right (shift j k prf)

----------------------------------------------------------------------------------
---- Finite numbers
----------------------------------------------------------------------------------

using (k : Nat)
  data FinLTE : Fin k -> Fin k -> Type where
    FromNatPrf : {m : Fin k} -> {n : Fin k} -> LTE (finToNat m) (finToNat n) -> FinLTE m n

  implementation Preorder (Fin k) FinLTE where
    transitive m n o (FromNatPrf p1) (FromNatPrf p2) = 
      FromNatPrf (LTEIsTransitive (finToNat m) (finToNat n) (finToNat o) p1 p2)
    reflexive n = FromNatPrf (LTEIsReflexive (finToNat n))

  implementation Poset (Fin k) FinLTE where
    antisymmetric m n (FromNatPrf p1) (FromNatPrf p2) =
      finToNatInjective m n (LTEIsAntisymmetric (finToNat m) (finToNat n) p1 p2)
  
  implementation Decidable [Fin k, Fin k] FinLTE where
    decide m n with (decideLTE (finToNat m) (finToNat n))
      | Yes prf    = Yes (FromNatPrf prf)
      | No  disprf = No (\ (FromNatPrf prf) => disprf prf)

  implementation Ordered (Fin k) FinLTE where
    order m n =
      either (Left . FromNatPrf) 
             (Right . FromNatPrf)
             (order (finToNat m) (finToNat n))