git.iko.soy/Idris-dev
on master help sign in
Order on Fin
426730fJan Bessai
libs/base/Decidable/Order.idr+19
compare with master
unifiedsplit
@@ -111,3 +111,22 @@ maximum x y with (order x y)
111 | Left _ = y
111 | Left _ = y
112 | Right _ = x
112 | Right _ = x
113
113
114+using (k : Nat)
115+ data FinLTE : Fin k -> Fin k -> Type where
116+ FromNatPrf : {m : Fin k} -> {n : Fin k} -> NatLTE (finToNat m) (finToNat n) -> FinLTE m n
117+
118+ instance Preorder (Fin k) FinLTE where
119+ transitive m n o (FromNatPrf p1) (FromNatPrf p2) =
120+ FromNatPrf (NatLTEIsTransitive (finToNat m) (finToNat n) (finToNat o) p1 p2)
121+ reflexive n = FromNatPrf (NatLTEIsReflexive (finToNat n))
122+
123+ instance Poset (Fin k) FinLTE where
124+ antisymmetric m n (FromNatPrf p1) (FromNatPrf p2) =
125+ finToNatInjective m n (NatLTEIsAntisymmetric (finToNat m) (finToNat n) p1 p2)
126+
127+ instance Ordered (Fin k) FinLTE where
128+ order m n =
129+ either (Left . FromNatPrf)
130+ (Right . FromNatPrf)
131+ (order (finToNat m) (finToNat n))
132+
libs/prelude/Prelude/Fin.idr+10
@@ -9,6 +9,9 @@ data Fin : Nat -> Type where
9 fZ : Fin (S k)
9 fZ : Fin (S k)
10 fS : Fin k -> Fin (S k)
10 fS : Fin k -> Fin (S k)
11
11
12+fSInjective : (m : Fin k) -> (n : Fin k) -> fS m = fS n -> m = n
13+fSInjective left _ refl = refl
14+
12instance Eq (Fin n) where
15instance Eq (Fin n) where
13 (==) fZ fZ = True
16 (==) fZ fZ = True
14 (==) (fS k) (fS k') = k == k'
17 (==) (fS k) (fS k') = k == k'
@@ -24,6 +27,13 @@ finToNat : Fin n -> Nat
24finToNat fZ = Z
27finToNat fZ = Z
25finToNat (fS k) = S (finToNat k)
28finToNat (fS k) = S (finToNat k)
26
29
30+finToNatInjective : (fm : Fin k) -> (fn : Fin k) -> (finToNat fm) = (finToNat fn) -> fm = fn
31+finToNatInjective fZ fZ refl = refl
32+finToNatInjective (fS m) fZ refl impossible
33+finToNatInjective fZ (fS n) refl impossible
34+finToNatInjective (fS m) (fS n) prf =
35+ cong (finToNatInjective m n (succInjective (finToNat m) (finToNat n) prf))
36+
27instance Cast (Fin n) Nat where
37instance Cast (Fin n) Nat where
28 cast x = finToNat x
38 cast x = finToNat x
29
39