blob: f0480b2ee60056f37e8c7b7ebdc36c72c7f1db51 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
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))
|
