From efd5f75c0672773341b5ca1c1d4b2ad0c0d09daa Mon Sep 17 00:00:00 2001
From: Ohad Kammar <ohad.kammar@ed.ac.uk>
Date: Sun, 7 Aug 2022 18:23:04 +0100
Subject: Initial version

---
 src/Syntax/PreorderReasoning/Setoid.idr | 53 +++++++++++++++++++++++++++++++++
 1 file changed, 53 insertions(+)
 create mode 100644 src/Syntax/PreorderReasoning/Setoid.idr

(limited to 'src/Syntax/PreorderReasoning/Setoid.idr')

diff --git a/src/Syntax/PreorderReasoning/Setoid.idr b/src/Syntax/PreorderReasoning/Setoid.idr
new file mode 100644
index 0000000..29ec715
--- /dev/null
+++ b/src/Syntax/PreorderReasoning/Setoid.idr
@@ -0,0 +1,53 @@
+||| Like Syntax.PreorderReasoning.Generic, but optimised for setoids
+module Syntax.PreorderReasoning.Setoid
+
+import Data.Setoid.Definition
+
+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.equivalence.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.equivalence.relation x y
+CalcWith a (|~ x) = a.equivalence.reflexive x
+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.equivalence.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.equivalence.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 y))
+
+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 y))
-- 
cgit v1.2.3