module Peano where
import Test.QuickCheck

data Nat = Z | S Nat deriving Show

(+@) :: Nat -> Nat -> Nat
Z +@ y = y
(S x) +@ y = S (x +@ y)

(*@) :: Nat -> Nat -> Nat
x *@ Z = Z 
x *@ S y = (x *@ y) +@ x 

sqr x = x *@ x 

(=@) :: Nat -> Nat -> Bool
Z =@ Z  = True
(S m) =@  (S n) = m =@ n 
_=@ _  = False 


(<@) :: Nat -> Nat -> Bool
Z <@ Z = False 
Z <@ x | not(x =@ Z) = True 
x <@ Z | not(x =@ Z) = False 
(S x) <@ (S y) = x <@ y 



(<=@) :: Nat -> Nat -> Bool
x <=@ y = if (x =@ y) || (x <@ y) then True else False



isqrt Z = Z
isqrt (S x) | (sqr (S (isqrt x))) <=@  (S x) = (S (isqrt x))
            | (S x) <@ (sqr (S (isqrt x))) = isqrt x


instance Arbitrary Nat where
 arbitrary = oneof [return Z, (S  <$>  arbitrary) ]

isqrtPostCondition :: Nat  -> Bool
isqrtPostCondition x  = (sqr (isqrt x) <=@ x) && (x <@ sqr(S (isqrt x)))
check = quickCheck isqrtPostCondition
-- +++ OK, passed 100 tests.

module Peano where
import Test.QuickCheck

data Nat = Z | S Nat deriving Show
-- addition
(+@) :: Nat -> Nat -> Nat
Z +@ y = y
(S x) +@ y = S (x +@ y)
-- multiplication
(*@) :: Nat -> Nat -> Nat
x *@ Z = Z 
x *@ S y = (x *@ y) +@ x 
-- square
sqr x = x *@ x 
-- equality
(=@) :: Nat -> Nat -> Bool
Z =@ Z  = True
(S m) =@  (S n) = m =@ n 
_=@ _  = False 

-- lesst than
(<@) :: Nat -> Nat -> Bool
Z <@ Z = False 
Z <@ x | not(x =@ Z) = True 
x <@ Z | not(x =@ Z) = False 
(S x) <@ (S y) = x <@ y 


-- less than or equal
(<=@) :: Nat -> Nat -> Bool
x <=@ y = if (x =@ y) || (x <@ y) then True else False


-- Integer square root function
isqrt Z = Z
isqrt (S x) | (sqr (S (isqrt x))) <=@  (S x) = (S (isqrt x))
            | (S x) <@ (sqr (S (isqrt x))) = isqrt x

-- test with Quickcheck
instance Arbitrary Nat where
 arbitrary = oneof [return Z, (S  <$>  arbitrary) ]

isqrtPostCondition :: Nat  -> Bool
isqrtPostCondition x  = (sqr (isqrt x) <=@ x) && (x <@ sqr(S (isqrt x)))
check = quickCheck isqrtPostCondition
-- +++ OK, passed 100 tests.

module Peano where
import Test.QuickCheck

data Nat = Z | S Nat deriving Show

(+@) :: Nat -> Nat -> Nat
Z +@ y = y
(S x) +@ y = S (x +@ y)

(*@) :: Nat -> Nat -> Nat
x *@ Z = Z 
x *@ S y = (x *@ y) +@ x 

sqr x = x *@ x 

(=@) :: Nat -> Nat -> Bool
Z =@ Z  = True
(S m) =@  (S n) = m =@ n 
_=@ _  = False 


(<@) :: Nat -> Nat -> Bool
Z <@ Z = False 
Z <@ x | not(x =@ Z) = True 
x <@ Z | not(x =@ Z) = False 
(S x) <@ (S y) = x <@ y 



(<=@) :: Nat -> Nat -> Bool
x <=@ y = if (x =@ y) || (x <@ y) then True else False



isqrt Z = Z
isqrt (S x) | (sqr (S (isqrt x))) <=@  (S x) = (S (isqrt x))
            | (S x) <@ (sqr (S (isqrt x))) = isqrt x


instance Arbitrary Nat where
 arbitrary = oneof [return Z, (S  <$>  arbitrary) ]

isqrtPostCondition :: Nat  -> Bool
isqrtPostCondition x  = (sqr (isqrt x) <=@ x) && (x <@ sqr(S (isqrt x)))
check = quickCheck isqrtPostCondition

Is there a technical name for this form of proof to program relation? I would be grateful for an explanation or pointer to the literature.

module Peano where
import Test.QuickCheck

data Nat = Z | S Nat deriving Show

(+@) :: Nat -> Nat -> Nat
Z +@ y = y
(S x) +@ y = S (x +@ y)

(*@) :: Nat -> Nat -> Nat
x *@ Z = Z 
x *@ S y = (x *@ y) +@ x 

sqr x = x *@ x 

(=@) :: Nat -> Nat -> Bool
Z =@ Z  = True
(S m) =@  (S n) = m =@ n 
_=@ _  = False 


(<@) :: Nat -> Nat -> Bool
Z <@ Z = False 
Z <@ x | not(x =@ Z) = True 
x <@ Z | not(x =@ Z) = False 
(S x) <@ (S y) = x <@ y 



(<=@) :: Nat -> Nat -> Bool
x <=@ y = if (x =@ y) || (x <@ y) then True else False



isqrt Z = Z
isqrt (S x) | (sqr (S (isqrt x))) <=@  (S x) = (S (isqrt x))
            | (S x) <@ (sqr (S (isqrt x))) = isqrt x


instance Arbitrary Nat where
 arbitrary = oneof [return Z, (S  <$>  arbitrary) ]

isqrtPostCondition :: Nat  -> Bool
isqrtPostCondition x  = (sqr (isqrt x) <=@ x) && (x <@ sqr(S (isqrt x)))
check = quickCheck isqrtPostCondition
-- +++ OK, passed 100 tests.