git.iko.soy/Idris-dev
on master help sign in
Order on Fin
commit426730f261821788ee67384fe2dd508870d1dae2 authorJan Bessai <Jan.Bessai@tu-dortmund.de> dateFri 21 Feb 2014, 17:36 (13 years ago) parentd3f0024
2 files changed+29
compare with master
unifiedsplit
libs/base/Decidable/Order.idr+19 libs/prelude/Prelude/Fin.idr+10
libs/base/Decidable/Order.idr+19
@@ -111,3 +111,22 @@ maximum x y with (order x y)
111111 | Left _ = y
112112 | Right _ = x
113113
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
99 fZ : Fin (S k)
1010 fS : Fin k -> Fin (S k)
1111
12+fSInjective : (m : Fin k) -> (n : Fin k) -> fS m = fS n -> m = n
13+fSInjective left _ refl = refl
14+
1215instance Eq (Fin n) where
1316 (==) fZ fZ = True
1417 (==) (fS k) (fS k') = k == k'
@@ -24,6 +27,13 @@ finToNat : Fin n -> Nat
2427finToNat fZ = Z
2528finToNat (fS k) = S (finToNat k)
2629
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+
2737instance Cast (Fin n) Nat where
2838 cast x = finToNat x
2939