mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-12-01 09:49:24 +03:00
43 lines
995 B
Idris
43 lines
995 B
Idris
||| Until Idris2 starts supporting the 'syntax' keyword, here's a
|
|
||| poor-man's equational reasoning
|
|
module Syntax.PreorderReasoning
|
|
|
|
||| Deep embedding of equation derivation sequences.
|
|
||| Using the Nil, (::) constructors lets us use list syntax.
|
|
public export
|
|
data Derivation : (x : a) -> (y : b) -> Type where
|
|
Nil : Derivation x x
|
|
(::) : (x = y) -> Derivation y z -> Derivation x z
|
|
|
|
infix 1 ==|
|
|
|
|
||| Explicate the term under consideration and the justification for
|
|
||| the next step.
|
|
export
|
|
(==|) : (x : a) -> (x = y) -> x = y
|
|
(==|) x pf = pf
|
|
|
|
||| Finishg the derivation.
|
|
||| A bit klunky, but this /is/ a poor-man's version.
|
|
export
|
|
QED : {x : a} -> x = x
|
|
QED = Refl
|
|
|
|
export
|
|
Calculate : Derivation x y -> x = y
|
|
Calculate [] = Refl
|
|
Calculate (Refl :: der) = Calculate der
|
|
|
|
{--
|
|
||| Requires Data.Nata
|
|
example : (x : Nat) -> (x + 1) + 0 = 1 + x
|
|
example x = Calculate [
|
|
(x + 1) + 0
|
|
==| plusZeroRightNeutral (x + 1) ,
|
|
x + 1
|
|
==| plusCommutative x 1 ,
|
|
1 + x
|
|
==| QED
|
|
]
|
|
--}
|