Add syntax for setoid reasoning.

2 files changed, 56 insertions, 0 deletions

diff --git a/soat.ipkg b/soat.ipkg
index 7d584ac..b9972b4 100644
--- a/soat.ipkg
+++ b/soat.ipkg
@@ -14,3 +14,4 @@ modules = Data.Morphism.Indexed
         , Soat.SecondOrder.Algebra.Lift
         , Soat.SecondOrder.Signature
         , Soat.SecondOrder.Signature.Lift
+        , Syntax.PreorderReasoning.Setoid
diff --git a/src/Syntax/PreorderReasoning/Setoid.idr b/src/Syntax/PreorderReasoning/Setoid.idr
new file mode 100644
index 0000000..f0480b2
--- /dev/null
+++ b/src/Syntax/PreorderReasoning/Setoid.idr
@@ -0,0 +1,55 @@
+{- Taken from https://github.com/ohad/idris-setoid -}
+
+||| Like Syntax.PreorderReasoning.Generic, but optimised for setoids
+module Syntax.PreorderReasoning.Setoid
+
+import public Data.Setoid
+
+infixl 0  ~~
+prefix 1  |~
+infix  1  ...,..<,..>,.=.,.=<,.=>
+
+public export
+data Step : (a : Setoid) -> (lhs,rhs : U a) -> Type where
+  (...) : {0 a : Setoid} -> (0 y : U a) -> {0 x : U a} ->
+    a.relation x y -> Step a x y
+
+public export
+data FastDerivation : (a : Setoid) -> (x, y : U a) -> Type where
+  (|~) : {0 a : Setoid} -> (x : U a) -> FastDerivation a x x
+  (~~) : {0 a : Setoid} -> {x, y : U a}
+         -> FastDerivation a x y -> {z : U a} -> (step : Step a y z)
+         -> FastDerivation a x z
+
+public export
+CalcWith : (a : Setoid) -> {0 x : U a} -> {0 y : U a} -> FastDerivation a x y ->
+  a.relation x y
+CalcWith a (|~ x) = a.equivalence.reflexive
+CalcWith a ((~~) der (z ... step)) = a.equivalence.transitive
+    (CalcWith a der) step
+
+-- Smart constructors
+public export
+(..<) : {a : Setoid} -> (y : U a) -> {x : U a} ->
+    a.relation y x -> Step a x y
+(y ..<(prf)) {x} = (y ...(a.equivalence.symmetric prf))
+
+public export
+(..>) : {0 a : Setoid} -> (0 y : U a) -> {0 x : U a} ->
+    a.relation x y -> Step a x y
+(..>) = (...)
+
+public export
+(.=.) : {a : Setoid} -> (y : U a) -> {x : U a} ->
+    x === y -> Step a x y
+(y .=.(Refl)) = (y ...(a.equivalence.reflexive))
+
+public export
+(.=>) : {a : Setoid} -> (y : U a) -> {x : U a} ->
+    x === y -> Step a x y
+(.=>) = (.=.)
+
+public export
+(.=<) : {a : Setoid} -> (y : U a) -> {x : U a} ->
+    y === x -> Step a x y
+(y .=<(Refl)) = (y ...(a.equivalence.reflexive))