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