prop-tests.disco

||| This is a foozle function.

!!! foo 3 == 5
!!! foo 9 == 28

||| We can have more documentation before more tests.

!!! foo 12 == 25
!!! ∀ n:Nat. foo (n+10) == 2n+21

foo : N -> N
foo 3 = 5
foo 9 = 28
foo n = 2n + 1

||| Reverse a list.
!!! reverse [3,6,7] == [7,6,3]
!!! ∀ a:N, b:N. reverse [a,b] == [b,a]
!!! ∀ xs:List(N). reverse (reverse xs) == xs

reverse : List(a) -> List(a)
reverse = revHelper []

revHelper : List(a) -> List(a) -> List(a)
revHelper rev [] = rev
revHelper rev (x :: xs) = revHelper (x :: rev) xs

toBin : N -> List(Bool)
toBin 0 = []
toBin 1 = []
toBin n = {? false if 2 divides n, true otherwise ?} :: toBin (n // 2)

fromBin : List(Bool) -> N
fromBin [] = 1
fromBin (false :: bs) = 2 (fromBin bs)
fromBin (true  :: bs) = 2 (fromBin bs) + 1

plusIso : N + N -> N
plusIso (left n) = 2n
plusIso (right n) = 2n + 1

plusIsoR : N -> N + N
plusIsoR n =
  {? left  (n // 2)   if 2 divides n
   , right (n // 2)   otherwise
  ?}

!!! ∀ v:Void. 2 == 3    -- this is true!
!!! ∀ u:Unit. u == u    -- there is only one Unit value
!!! ∀ l:List(Void). l == l
-- !!! ∀ l:List(Unit). l == reverse l    -- too slow!
!!! ∀ bs : List(Bool). toBin (fromBin bs) == bs
!!! ∀ q : F. q >= 0
!!! ∀ p : N * N. {? x + y when p is (x,y) ?} >= 0
!!! ∀ bs : Bool * Bool. {? b1 when bs is (b1,b2) if b2, false otherwise ?}
                     == {? b1 and b2 when bs is (b1,b2) ?}
!!! ∀ x : N + N. plusIsoR (plusIso x) == x

!!! ∀ x : Void + N. {? true when x is right _, false otherwise ?}

x : N
x = 0

  -- x is just here to give us something to attach arbitrary test
  -- properties to.