Skip to content

Instantly share code, notes, and snippets.

@roehst roehst/Direction.idr
Last active Dec 9, 2018

What would you like to do?
Simple verification in Idris

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
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.