@@ -15,7 +15,7 @@ import Decidable.Equality
1515
1616class Preorder t (po : t -> t -> Type) where
1717 total transitive : (a : t) -> (b : t) -> (c : t) -> po a b -> po b c -> po a c
18− total Reflexive : (a : t) -> po a a
18+ total reflexive : (a : t) -> po a a
1919
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
@@ -48,7 +48,7 @@ maximum x y with (order x y)
4848
4949instance Preorder t ((=) {A = t} {B = t}) where
5050 transitive a b c = trans {a = a} {b = b} {c = c}
51− Reflexive a = Refl
51+ reflexive a = Refl
5252
5353instance Equivalence t ((=) {A = t} {B = t}) where
5454 symmetric a b prf = sym prf
@@ -60,99 +60,88 @@ instance Congruence t f ((=) {A = t} {B = t}) where
6060-- Natural numbers
6161--------------------------------------------------------------------------------
6262
63−data NatLTE : Nat -> Nat -> Type where
64− nEqn : NatLTE n n
65− nLTESm : NatLTE n m -> NatLTE n (S m)
63+total LTEIsTransitive : (m : Nat) -> (n : Nat) -> (o : Nat) ->
64+ LTE m n -> LTE n o ->
65+ LTE m o
66+LTEIsTransitive Z n o LTEZero nlteo = LTEZero
67+LTEIsTransitive (S m) (S n) (S o) (LTESucc mlten) (LTESucc nlteo) = LTESucc (LTEIsTransitive m n o mlten nlteo)
6668
67−total NatLTEIsTransitive : (m : Nat) -> (n : Nat) -> (o : Nat) ->
68− NatLTE m n -> NatLTE n o ->
69− NatLTE m o
70−NatLTEIsTransitive m n n mLTEn (nEqn) = mLTEn
71−NatLTEIsTransitive m n (S o) mLTEn (nLTESm nLTEo)
72− = nLTESm (NatLTEIsTransitive m n o mLTEn nLTEo)
69+total LTEIsReflexive : (n : Nat) -> LTE n n
70+LTEIsReflexive Z = LTEZero
71+LTEIsReflexive (S n) = LTESucc (LTEIsReflexive n)
7372
74−total NatLTEIsReflexive : (n : Nat) -> NatLTE n n
75−NatLTEIsReflexive _ = nEqn
73+instance Preorder Nat LTE where
74+ transitive = LTEIsTransitive
75+ reflexive = LTEIsReflexive
7676
77−instance Preorder Nat NatLTE where
78− transitive = NatLTEIsTransitive
79− Reflexive = NatLTEIsReflexive
77+total LTEIsAntisymmetric : (m : Nat) -> (n : Nat) ->
78+ LTE m n -> LTE n m -> m = n
79+LTEIsAntisymmetric Z Z LTEZero LTEZero = Refl
80+LTEIsAntisymmetric (S n) (S m) (LTESucc mLTEn) (LTESucc nLTEm) with (LTEIsAntisymmetric n m mLTEn nLTEm)
81+ LTEIsAntisymmetric (S n) (S n) (LTESucc mLTEn) (LTESucc nLTEm) | Refl = Refl
8082
81−total NatLTEIsAntisymmetric : (m : Nat) -> (n : Nat) ->
82− NatLTE m n -> NatLTE n m -> m = n
83−NatLTEIsAntisymmetric n n nEqn nEqn = Refl
84−NatLTEIsAntisymmetric n m nEqn (nLTESm _) impossible
85−NatLTEIsAntisymmetric n m (nLTESm _) nEqn impossible
86−NatLTEIsAntisymmetric n m (nLTESm _) (nLTESm _) impossible
8783
88−instance Poset Nat NatLTE where
89− antisymmetric = NatLTEIsAntisymmetric
84+instance Poset Nat LTE where
85+ antisymmetric = LTEIsAntisymmetric
9086
91−total zeroNeverGreater : {n : Nat} -> NatLTE (S n) Z -> _|_
92−zeroNeverGreater {n} (nLTESm _) impossible
93−zeroNeverGreater {n} nEqn impossible
87+total zeroNeverGreater : {n : Nat} -> LTE (S n) Z -> _|_
88+zeroNeverGreater {n} LTEZero impossible
89+zeroNeverGreater {n} (LTESucc _) impossible
9490
95−total zeroAlwaysSmaller : {n : Nat} -> NatLTE Z n
96−zeroAlwaysSmaller {n = Z } = nEqn
97−zeroAlwaysSmaller {n = S k} = nLTESm (zeroAlwaysSmaller {n = k})
91+total zeroAlwaysSmaller : {n : Nat} -> LTE Z n
92+zeroAlwaysSmaller = LTEZero
9893
99−total
100−nGTSm : {n : Nat} -> {m : Nat} -> (NatLTE n m -> _|_) -> NatLTE n (S m) -> _|_
101−nGTSm disprf (nLTESm nLTEm) = FalseElim (disprf nLTEm)
102−nGTSm {n} {m} disprf (nEqn) impossible
94+total ltesuccinjective : {n : Nat} -> {m : Nat} -> (LTE n m -> _|_) -> LTE (S n) (S m) -> _|_
95+ltesuccinjective {n} {m} disprf (LTESucc nLTEm) = FalseElim (disprf nLTEm)
96+ltesuccinjective {n} {m} disprf LTEZero impossible
10397
104−total
105−decideNatLTE : (n : Nat) -> (m : Nat) -> Dec (NatLTE n m)
106−decideNatLTE Z Z = Yes nEqn
107−decideNatLTE (S x) Z = No zeroNeverGreater
108−decideNatLTE x (S y) with (decEq x (S y))
109− | Yes eq = rewrite eq in Yes nEqn
110− | No _ with (decideNatLTE x y)
111− | Yes nLTEm = Yes (nLTESm nLTEm)
112− | No nGTm = No (nGTSm nGTm)
113−
114−instance Decidable [Nat,Nat] NatLTE where
115− decide = decideNatLTE
98+
99+total decideLTE : (n : Nat) -> (m : Nat) -> Dec (LTE n m)
100+decideLTE Z y = Yes LTEZero
101+decideLTE (S x) Z = No zeroNeverGreater
102+decideLTE (S x) (S y) with (decEq (S x) (S y))
103+ | Yes eq = rewrite eq in Yes (reflexive x)
104+ | No _ with (decideLTE x y)
105+ | Yes nLTEm = Yes (LTESucc nLTEm)
106+ | No nGTm = No (ltesuccinjective nGTm)
107+
108+instance Decidable [Nat,Nat] LTE where
109+ decide = decideLTE
116110
117111total
118−lte : (m : Nat) -> (n : Nat) -> Dec (NatLTE m n)
119−lte m n = decide {ts = [Nat,Nat]} {p = NatLTE} m n
112+lte : (m : Nat) -> (n : Nat) -> Dec (LTE m n)
113+lte m n = decide {ts = [Nat,Nat]} {p = LTE} m n
120114
121115total
122−shift : (m : Nat) -> (n : Nat) -> NatLTE m n -> NatLTE (S m) (S n)
123−shift Z Z _ = nEqn
124−shift Z (S Z) _ = nLTESm nEqn
125−shift Z (S (S j)) _ = nLTESm (shift Z (S j) zeroAlwaysSmaller)
126−shift (S k) Z prf = FalseElim (zeroNeverGreater prf)
127−shift (S k) (S k) nEqn = nEqn
128−shift (S k) (S j) (nLTESm prf) = nLTESm (shift (S k) j prf)
129−
130−instance Ordered Nat NatLTE where
131− order Z n = Left zeroAlwaysSmaller
132− order m Z = Right zeroAlwaysSmaller
116+shift : (m : Nat) -> (n : Nat) -> LTE m n -> LTE (S m) (S n)
117+shift m n mLTEn = LTESucc mLTEn
118+
119+instance Ordered Nat LTE where
120+ order Z n = Left LTEZero
121+ order m Z = Right LTEZero
133122 order (S k) (S j) with (order k j)
134123 order (S k) (S j) | Left prf = Left (shift k j prf)
135124 order (S k) (S j) | Right prf = Right (shift j k prf)
136125
137−--------------------------------------------------------------------------------
138−-- Finite numbers
139−--------------------------------------------------------------------------------
126+----------------------------------------------------------------------------------
127+---- Finite numbers
128+----------------------------------------------------------------------------------
140129
141130using (k : Nat)
142131 data FinLTE : Fin k -> Fin k -> Type where
143− FromNatPrf : {m : Fin k} -> {n : Fin k} -> NatLTE (finToNat m) (finToNat n) -> FinLTE m n
132+ FromNatPrf : {m : Fin k} -> {n : Fin k} -> LTE (finToNat m) (finToNat n) -> FinLTE m n
144133
145134 instance Preorder (Fin k) FinLTE where
146135 transitive m n o (FromNatPrf p1) (FromNatPrf p2) =
147− FromNatPrf (NatLTEIsTransitive (finToNat m) (finToNat n) (finToNat o) p1 p2)
148− Reflexive n = FromNatPrf (NatLTEIsReflexive (finToNat n))
136+ FromNatPrf (LTEIsTransitive (finToNat m) (finToNat n) (finToNat o) p1 p2)
137+ reflexive n = FromNatPrf (LTEIsReflexive (finToNat n))
149138
150139 instance Poset (Fin k) FinLTE where
151140 antisymmetric m n (FromNatPrf p1) (FromNatPrf p2) =
152− finToNatInjective m n (NatLTEIsAntisymmetric (finToNat m) (finToNat n) p1 p2)
141+ finToNatInjective m n (LTEIsAntisymmetric (finToNat m) (finToNat n) p1 p2)
153142
154143 instance Decidable [Fin k, Fin k] FinLTE where
155− decide m n with (decideNatLTE (finToNat m) (finToNat n))
144+ decide m n with (decideLTE (finToNat m) (finToNat n))
156145 | Yes prf = Yes (FromNatPrf prf)
157146 | No disprf = No (\ (FromNatPrf prf) => disprf prf)
158147