diff options
| -rw-r--r-- | soat.ipkg | 3 | ||||
| -rw-r--r-- | src/Data/Setoid.idr | 55 | ||||
| -rw-r--r-- | src/Soat/Relation.idr | 47 |
3 files changed, 59 insertions, 46 deletions
@@ -2,7 +2,8 @@ package soat authors = "Greg Brown" sourcedir = "src" -modules = Soat.Data.Product +modules = Data.Setoid + , Soat.Data.Product , Soat.Data.Sublist , Soat.FirstOrder.Algebra , Soat.FirstOrder.Signature diff --git a/src/Data/Setoid.idr b/src/Data/Setoid.idr new file mode 100644 index 0000000..8014bac --- /dev/null +++ b/src/Data/Setoid.idr @@ -0,0 +1,55 @@ +module Data.Setoid + +import public Control.Relation + +%default total + +public export +record Equivalence a (rel : Rel a) where + constructor MkEquivalence + refl : Reflexive a rel + sym : Symmetric a rel + trans : Transitive a rel + +public export +record Setoid where + constructor MkSetoid + 0 U : Type + 0 relation : Rel U + equivalence : Data.Setoid.Equivalence U relation + +public export +equiv : Control.Relation.Equivalence a rel => Data.Setoid.Equivalence a rel +equiv = MkEquivalence (MkReflexive reflexive) (MkSymmetric symmetric) (MkTransitive transitive) + +public export +[refl'] (eq : Data.Setoid.Equivalence a rel) => Reflexive a rel where + reflexive = reflexive @{eq.refl} + +public export +[sym'] (eq : Data.Setoid.Equivalence a rel) => Symmetric a rel where + symmetric = symmetric @{eq.sym} + +public export +[trans'] (eq : Data.Setoid.Equivalence a rel) => Transitive a rel where + transitive = transitive @{eq.trans} + +public export +[equiv'] Data.Setoid.Equivalence a rel => Control.Relation.Equivalence a rel + using refl' sym' trans' where + +public export +(.reflexive) : Data.Setoid.Equivalence a rel -> {x : a} -> rel x x +(.reflexive) eq = reflexive @{eq.refl} + +public export +(.symmetric) : Data.Setoid.Equivalence a rel -> {x, y : a} -> rel x y -> rel y x +(.symmetric) eq = symmetric @{eq.sym} + +public export +(.transitive) : Data.Setoid.Equivalence a rel -> {x, y, z : a} -> rel x y -> rel y z -> rel x z +(.transitive) eq = transitive @{eq.trans} + +public export +(.equalImpliesEq) : Data.Setoid.Equivalence a rel -> {x, y : a} -> x = y -> rel x y +(.equalImpliesEq) eq Refl = eq.reflexive diff --git a/src/Soat/Relation.idr b/src/Soat/Relation.idr index 6d6b691..9826d60 100644 --- a/src/Soat/Relation.idr +++ b/src/Soat/Relation.idr @@ -1,53 +1,10 @@ module Soat.Relation -import Control.Relation +import public Data.Setoid %default total public export -record Equivalence a (rel : Rel a) where - constructor MkEquivalence - refl : Reflexive a rel - sym : Symmetric a rel - trans : Transitive a rel - -public export -equiv : Control.Relation.Equivalence a rel => Soat.Relation.Equivalence a rel -equiv = MkEquivalence (MkReflexive reflexive) (MkSymmetric symmetric) (MkTransitive transitive) - -public export -[refl'] (eq : Soat.Relation.Equivalence a rel) => Control.Relation.Reflexive a rel where - reflexive = reflexive @{eq.refl} - -public export -[sym'] (eq : Soat.Relation.Equivalence a rel) => Control.Relation.Symmetric a rel where - symmetric = symmetric @{eq.sym} - -public export -[trans'] (eq : Soat.Relation.Equivalence a rel) => Control.Relation.Transitive a rel where - transitive = transitive @{eq.trans} - -public export -[equiv'] Soat.Relation.Equivalence a rel => Control.Relation.Equivalence a rel - using refl' sym' trans' where - -public export -(.reflexive) : Soat.Relation.Equivalence a rel -> {x : a} -> rel x x -(.reflexive) eq = reflexive @{eq.refl} - -public export -(.symmetric) : Soat.Relation.Equivalence a rel -> {x, y : a} -> rel x y -> rel y x -(.symmetric) eq = symmetric @{eq.sym} - -public export -(.transitive) : Soat.Relation.Equivalence a rel -> {x, y, z : a} -> rel x y -> rel y z -> rel x z -(.transitive) eq = transitive @{eq.trans} - -public export -(.equalImpliesEq) : Soat.Relation.Equivalence a rel -> {x, y : a} -> x = y -> rel x y -(.equalImpliesEq) eq Refl = eq.reflexive - -public export IRel : {a : Type} -> (a -> Type) -> Type IRel {a = a} x = (i : a) -> x i -> x i -> Type @@ -65,7 +22,7 @@ ITransitive x rel = (i : a) -> Transitive (x i) (rel i) public export IEquivalence : {a : Type} -> (x : a -> Type) -> IRel x -> Type -IEquivalence x rel = (i : a) -> Soat.Relation.Equivalence (x i) (rel i) +IEquivalence x rel = (i : a) -> Setoid.Equivalence (x i) (rel i) public export record ISetoid (a : Type) where |