0 | ||| Implementation  of ordering relations for `Fin`ite numbers
 1 | module Data.Fin.Order
 2 |
 3 | import Control.Relation
 4 | import Control.Order
 5 | import Data.Fin
 6 | import Data.Fun
 7 | import Data.Rel
 8 | import Data.Nat
 9 | import Decidable.Decidable
10 |
11 | %default total
12 |
13 | using (k : Nat)
14 |
15 |   public export
16 |   data FinLTE : Fin k -> Fin k -> Type where
17 |     FromNatPrf : {m, n : Fin k} -> LTE (finToNat m) (finToNat n) -> FinLTE m n
18 |
19 |   public export
20 |   Transitive (Fin k) FinLTE where
21 |     transitive (FromNatPrf xy) (FromNatPrf yz) =
22 |       FromNatPrf $ transitive xy yz
23 |
24 |   public export
25 |   Reflexive (Fin k) FinLTE where
26 |     reflexive = FromNatPrf $ reflexive
27 |
28 |   public export
29 |   Preorder (Fin k) FinLTE where
30 |
31 |   public export
32 |   Antisymmetric (Fin k) FinLTE where
33 |     antisymmetric {x} {y} (FromNatPrf xy) (FromNatPrf yx) =
34 |       finToNatInjective x y $
35 |         antisymmetric xy yx
36 |
37 |   public export
38 |   PartialOrder (Fin k) FinLTE where
39 |
40 |   public export
41 |   Connex (Fin k) FinLTE where
42 |     connex {x = FZ} _ =  Left $ FromNatPrf LTEZero
43 |     connex {y = FZ} _ = Right $ FromNatPrf LTEZero
44 |     connex {x = FS k} {y = FS j} prf =
45 |       case connex {rel = FinLTE} $ \c => prf $ cong FS c of
46 |         Left  (FromNatPrf p) => Left  $ FromNatPrf $ LTESucc p
47 |         Right (FromNatPrf p) => Right $ FromNatPrf $ LTESucc p
48 |
49 |   public export
50 |   Decidable 2 [Fin k, Fin k] FinLTE where
51 |     decide m n with (isLTE (finToNat m) (finToNat n))
52 |       decide m n | Yes prf    = Yes (FromNatPrf prf)
53 |       decide m n | No  disprf = No (\ (FromNatPrf prf) => disprf prf)
54 |