@@ -10,7 +10,7 @@ import Decidable.Equality
1010--------------------------------------------------------------------------------
1111
1212--------------------------------------------------------------------------------
13−-- Preorders and Posets
13+-- Preorders, Posets and total Orders
1414--------------------------------------------------------------------------------
1515
1616class Preorder t (po : t -> t -> Type) where
@@ -20,6 +20,19 @@ class Preorder t (po : t -> t -> Type) where
2020class (Preorder t po) => Poset t (po : t -> t -> Type) where
2121 total antisymmetric : (a : t) -> (b : t) -> po a b -> po b a -> a = b
2222
23+class (Poset t to) => Ordered t (to : t -> t -> Type) where
24+ total order : (a : t) -> (b : t) -> Either (to a b) (to b a)
25+
26+minimum : (Ordered t to) => t -> t -> t
27+minimum x y with (order x y)
28+ | Left _ = x
29+ | Right _ = y
30+
31+maximum : (Ordered t to) => t -> t -> t
32+maximum x y with (order x y)
33+ | Left _ = y
34+ | Right _ = x
35+
2336--------------------------------------------------------------------------------
2437-- Natural numbers
2538--------------------------------------------------------------------------------
@@ -56,6 +69,10 @@ total zeroNeverGreater : {n : Nat} -> NatLTE (S n) Z -> _|_
5669zeroNeverGreater {n} (nLTESm _) impossible
5770zeroNeverGreater {n} nEqn impossible
5871
72+total zeroAlwaysSmaller : {n : Nat} -> NatLTE Z n
73+zeroAlwaysSmaller {n = Z } = nEqn
74+zeroAlwaysSmaller {n = S k} = nLTESm (zeroAlwaysSmaller {n = k})
75+
5976total
6077nGTSm : {n : Nat} -> {m : Nat} -> (NatLTE n m -> _|_) -> NatLTE n (S m) -> _|_
6178nGTSm disprf (nLTESm nLTEm) = FalseElim (disprf nLTEm)
@@ -74,5 +91,51 @@ decideNatLTE x (S y) with (decEq x (S y))
7491instance Decidable [Nat,Nat] NatLTE where
7592 decide = decideNatLTE
7693
94+total
7795lte : (m : Nat) -> (n : Nat) -> Dec (NatLTE m n)
7896lte m n = decide {ts = [Nat,Nat]} {p = NatLTE} m n
97+
98+total
99+shift : (m : Nat) -> (n : Nat) -> NatLTE m n -> NatLTE (S m) (S n)
100+shift Z Z _ = nEqn
101+shift Z (S Z) _ = nLTESm nEqn
102+shift Z (S (S j)) _ = nLTESm (shift Z (S j) zeroAlwaysSmaller)
103+shift (S k) Z prf = FalseElim (zeroNeverGreater prf)
104+shift (S k) (S k) nEqn = nEqn
105+shift (S k) (S j) (nLTESm prf) = nLTESm (shift (S k) j prf)
106+
107+instance Ordered Nat NatLTE where
108+ order Z n = Left zeroAlwaysSmaller
109+ order m Z = Right zeroAlwaysSmaller
110+ order (S k) (S j) with (order k j)
111+ order (S k) (S j) | Left prf = Left (shift k j prf)
112+ order (S k) (S j) | Right prf = Right (shift j k prf)
113+
114+--------------------------------------------------------------------------------
115+-- Finite numbers
116+--------------------------------------------------------------------------------
117+
118+using (k : Nat)
119+ data FinLTE : Fin k -> Fin k -> Type where
120+ FromNatPrf : {m : Fin k} -> {n : Fin k} -> NatLTE (finToNat m) (finToNat n) -> FinLTE m n
121+
122+ instance Preorder (Fin k) FinLTE where
123+ transitive m n o (FromNatPrf p1) (FromNatPrf p2) =
124+ FromNatPrf (NatLTEIsTransitive (finToNat m) (finToNat n) (finToNat o) p1 p2)
125+ reflexive n = FromNatPrf (NatLTEIsReflexive (finToNat n))
126+
127+ instance Poset (Fin k) FinLTE where
128+ antisymmetric m n (FromNatPrf p1) (FromNatPrf p2) =
129+ finToNatInjective m n (NatLTEIsAntisymmetric (finToNat m) (finToNat n) p1 p2)
130+
131+ instance Decidable [Fin k, Fin k] FinLTE where
132+ decide m n with (decideNatLTE (finToNat m) (finToNat n))
133+ | Yes prf = Yes (FromNatPrf prf)
134+ | No disprf = No (\ (FromNatPrf prf) => disprf prf)
135+
136+ instance Ordered (Fin k) FinLTE where
137+ order m n =
138+ either (Left . FromNatPrf)
139+ (Right . FromNatPrf)
140+ (order (finToNat m) (finToNat n))
141+