Simple verification in Idris

README.md

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.

Direction.idr

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