Agda-style preorder reasoning in Idris

PreorderReasoning.idr

module PreOrderReasoning


-- QED is first to get the precedence to work out. It's just refl with an explicit argument.
syntax [expr] "QED" = qed expr
-- foo ={ prf }= bar ={ prf' }= fnord QED
-- is a proof that foo is related to fnord, with the intermediate step being bar, justified by prf and prf'
syntax [from] "={" [prf] "}=" [to] = step from prf to

--These are the components for using the syntax with equality
namespace Equal
  using (a : Type, x : a, y : a, z : a)
    qed : (x : a) -> x = x
    qed x = the (x = x) refl
    step : (x : a) -> x = y -> (y = z) -> x = z
    step x refl refl = refl


-- stupid proofs showing it in action
oneplusone : (S Z) + 1 = (S (S Z))
oneplusone = ((S Z) + 1) ={ refl }= (S (S Z)) QED

demo2 : (n : Nat) -> n + 0 = n
demo2 Z = refl
demo2 (S k) = let ih = demo2 k in
              ((S k) + 0) ={ cong ih }= (S k) QED


-- Now the same syntax can be used for proofs of isomorphism
data Iso : Type -> Type -> Type where
  MkIso : (to : a -> b) ->
          (from : b -> a) ->
          (toFrom : (y : b) -> to (from y) = y) ->
          (fromTo : (x : a) -> from (to x) = x) ->
          Iso a b

-- Isomorphism properties

isoRefl : Iso a a
isoRefl = MkIso id id (\x => refl) (\x => refl)

isoTrans : Iso a b -> Iso b c -> Iso a c
isoTrans (MkIso to from toFrom fromTo) (MkIso to' from' toFrom' fromTo') =
  MkIso (\x => to' (to x))
        (\y => from (from' y))
        (\y => (to' (to (from (from' y))))  ={ cong (toFrom (from' y)) }=
               (to' (from' y))              ={ toFrom' y }=
               y QED)
        (\x => (from (from' (to' (to x))))  ={ cong (fromTo' (to x)) }=
               (from (to x))                ={ fromTo x }=
               x QED)

-- Isomorphism reasoning


namespace Iso
  qed : (a : Type) -> Iso a a
  qed a = isoRefl

  step : (a : Type) -> Iso a b -> Iso b c -> Iso a c
  step a iso1 iso2 = isoTrans iso1 iso2


swap : Either a b -> Either b a
swap (Left x) = Right x
swap (Right x) = Left x

eitherComm : Iso (Either a b) (Either b a)
eitherComm = MkIso swap swap swapSwap swapSwap
  where swapSwap : (e : Either a b) -> swap (swap e) = e
        swapSwap (Left x) = refl
        swapSwap (Right x) = refl


-- Sorry, no time to find a realistic example.

stupidProof : Iso (Either a b) (Either a b)
stupidProof {a} {b} = (Either a b) ={ eitherComm }=
                      (Either b a) ={ eitherComm }=
                      (Either a b) QED