git.iko.soy/Idris-dev
on master help sign in
Equivalence and congruence relations
bd93226Jan Bessai
libs/base/Decidable/Order.idr+25−1
compare with master
unifiedsplit
@@ -10,7 +10,7 @@ import Decidable.Equality
10--------------------------------------------------------------------------------
10--------------------------------------------------------------------------------
11
11
12--------------------------------------------------------------------------------
12--------------------------------------------------------------------------------
13−-- Preorders, Posets and total Orders
13+-- Preorders, Posets, total Orders, Equivalencies, Congruencies
14--------------------------------------------------------------------------------
14--------------------------------------------------------------------------------
15
15
16class Preorder t (po : t -> t -> Type) where
16class Preorder t (po : t -> t -> Type) where
@@ -23,6 +23,16 @@ class (Preorder t po) => Poset t (po : t -> t -> Type) where
23class (Poset t to) => Ordered t (to : t -> t -> Type) where
23class (Poset t to) => Ordered t (to : t -> t -> Type) where
24 total order : (a : t) -> (b : t) -> Either (to a b) (to b a)
24 total order : (a : t) -> (b : t) -> Either (to a b) (to b a)
25
25
26+class (Preorder t eq) => Equivalence t (eq : t -> t -> Type) where
27+ total symmetric : (a : t) -> (b : t) -> eq a b -> eq b a
28+
29+class (Equivalence t eq) => Congruence t (eq : t -> t -> Type) where
30+ total congruent : (a : t) ->
31+ (b : t) ->
32+ (f : t -> t) ->
33+ eq a b ->
34+ eq (f a) (f b)
35+
26minimum : (Ordered t to) => t -> t -> t
36minimum : (Ordered t to) => t -> t -> t
27minimum x y with (order x y)
37minimum x y with (order x y)
28 | Left _ = x
38 | Left _ = x
@@ -33,6 +43,20 @@ maximum x y with (order x y)
33 | Left _ = y
43 | Left _ = y
34 | Right _ = x
44 | Right _ = x
35
45
46+--------------------------------------------------------------------------------
47+-- Syntactic equivalence (=)
48+--------------------------------------------------------------------------------
49+
50+instance Preorder t ((=) {A = t} {B = t}) where
51+ transitive a b c = trans {a = a} {b = b} {c = c}
52+ reflexive a = refl
53+
54+instance Equivalence t ((=) {A = t} {B = t}) where
55+ symmetric a b prf = sym prf
56+
57+instance Congruence t ((=) {A = t} {B = t}) where
58+ congruent a b f = cong {a = a} {b = b} {f = f}
59+
36--------------------------------------------------------------------------------
60--------------------------------------------------------------------------------
37-- Natural numbers
61-- Natural numbers
38--------------------------------------------------------------------------------
62--------------------------------------------------------------------------------