A very simple example of verification in Idris.
Try changing the turn
function and see how it fails to typecheck.
There are 2 other ways to make the properties pass.
module Main | |
data Direction = North | South | West | East | |
turn : Direction -> Direction | |
turn North = East | |
turn South = West | |
turn West = North | |
turn East = South | |
iter : (n: Nat) -> (f: a -> a) -> a -> a | |
iter Z _ x = x | |
iter (S k) f x = iter k f (f x) | |
prop_turn : (d : Direction) -> (iter 4 Main.turn d) = d | |
prop_turn North = Refl | |
prop_turn South = Refl | |
prop_turn West = Refl | |
prop_turn East = Refl | |
prop_not_idempotent : (d : Direction) -> Not (turn d = d) | |
prop_not_idempotent North Refl impossible | |
prop_not_idempotent South Refl impossible | |
prop_not_idempotent West Refl impossible | |
prop_not_idempotent East Refl impossible |