Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
Agda-style preorder reasoning in Idris
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
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.