0 | ||| Until Idris2 starts supporting the 'syntax' keyword, here's a
 1 | ||| poor-man's equational reasoning
 2 | module Syntax.PreorderReasoning
 3 |
 4 | import public Syntax.PreorderReasoning.Ops
 5 |
 6 | |||Slightly nicer syntax for justifying equations:
 7 | |||```
 8 | ||| |~ a
 9 | ||| ~~ b ...( justification )
10 | |||```
11 | |||and we can think of the `...( justification )` as ASCII art for a thought bubble.
12 | public export
13 | data Step : a -> b -> Type where
14 |   (...) : (0 y : a) -> (0 step : x ~=~ y) -> Step x y
15 |
16 | public export
17 | data FastDerivation : (x : a) -> (y : b) -> Type where
18 |   (|~) : (0 x : a) -> FastDerivation x x
19 |   (~~) : FastDerivation x y -> (step : Step y z) -> FastDerivation x z
20 |
21 | public export
22 | Calc : {0 x : a} -> {0 y : b} -> (0 der : FastDerivation x y) -> x ~=~ y
23 | Calc der = irrelevantEq $ Calc' der
24 |   where
25 |     Calc' : {0 x : c} -> {0 y : d} -> FastDerivation x y -> x ~=~ y
26 |     Calc' (|~ x) = Refl
27 |     Calc' ((~~) der (_ ...(Refl))) = Calc' der
28 |
29 | {- -- requires import Data.Nat
30 | 0
31 | example : (x : Nat) -> (x + 1) + 0 = 1 + x
32 | example x =
33 |   Calc $
34 |    |~ (x + 1) + 0
35 |    ~~ x+1  ...( plusZeroRightNeutral $ x + 1 )
36 |    ~~ 1+x  ...( plusCommutative x 1          )
37 | -}
38 |
39 | -- Smart constructors
40 | public export
41 | (..<) : (0 y : a) -> {0 x : b} -> (0 step : y ~=~ x) -> Step x y
42 | (y ..<(prf)) {x} = (y ...(sym prf))
43 |
44 | public export
45 | (..>) : (0 y : a) -> (0 step : x ~=~ y) -> Step x y
46 | (..>) = (...)
47 |
48 | ||| Use a judgemental equality but is not trivial to the reader.
49 | public export
50 | (~=) : FastDerivation x y -> (0 z : dom) -> {auto 0 xEqy : y = z} -> FastDerivation x z
51 | (~=) der y {xEqy = Refl} = der ~~ y ... Refl
52 |