Skip to content

Instantly share code, notes, and snippets.

@roehst

roehst/Direction.idr

Last active December 9, 2018 23:42
Show Gist options

  • Select an option

    Learn more about clone URLs
  • Save roehst/f87af1dabd2699762dec2657a20173f7 to your computer and use it in GitHub Desktop.

Select an option

Learn more about clone URLs
Save roehst/f87af1dabd2699762dec2657a20173f7 to your computer and use it in GitHub Desktop.
Download ZIP

Revisions

  1. roehst revised this gist Nov 28, 2018. 1 changed file with 6 additions and 2 deletions.
    8 changes: 6 additions & 2 deletions Direction.idr
    View file
    Original file line number Diff line number Diff line change
    @@ -8,7 +8,11 @@ turn South = West
    turn West = North
    turn East = South

    prop_turn : (d : Direction) -> (turn (turn (turn (turn d)))) = d
    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
    @@ -18,4 +22,4 @@ 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
    prop_not_idempotent East Refl impossible
  2. roehst created this gist Nov 28, 2018.
    21 changes: 21 additions & 0 deletions Direction.idr
    View file
    Original file line number Diff line number Diff line change
    @@ -0,0 +1,21 @@
    module Main

    data Direction = North | South | West | East

    turn : Direction -> Direction
    turn North = East
    turn South = West
    turn West = North
    turn East = South

    prop_turn : (d : Direction) -> (turn (turn (turn (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
    5 changes: 5 additions & 0 deletions README.md
    View file
    Original file line number Diff line number Diff line change
    @@ -0,0 +1,5 @@
    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.