content: -- Properties of Natural numbers, with recursion at "double speed",
  -- but production in normal speed
  module NatDoubleSlow where
  
  import Hip.Prelude
  import Prelude (Eq,Ord,Show,iterate,(!!),fmap,Bool(..))
  
  data Nat = Z | S Nat
    deriving (Eq,Ord,Show)
  
  instance Arbitrary Nat where
    arbitrary =
      let nats = iterate S Z
      in  (nats !!) `fmap` choose (0,25)
  
  Z       + y = y
  S Z     + y = S y
  S (S x) + y = S (S x + y)
  
  Z       * _ = Z
  S Z     * y = y
  S (S x) * y = y + (S x * y)
  
  Z       - _       = Z
  x       - Z       = x
  S Z     - S x     = Z
  S x     - S Z     = x
  S (S x) - S (S y) = S x - S y
  
  Z   <= _   = True
  _   <= Z   = False
  S x <= S y = x <= y
  
  _   < Z   = False
  Z   < _   = True
  S x < S y = x < y
  
  -- Only properties directly or indirectly regarding +
  
  prop_assoc_plus :: Nat -> Nat -> Nat -> Prop Nat
  prop_assoc_plus x y z
    = x + (y + z) =:= (x + y) + z
  
  prop_assoc_mul :: Nat -> Nat -> Nat -> Prop Nat
  prop_assoc_mul x y z
    = x * (y * z) =:= (x * y) * z
  
  prop_right_identity_plus :: Nat -> Prop Nat
  prop_right_identity_plus x
    = x + Z =:= x
  
  prop_left_identity_plus :: Nat -> Prop Nat
  prop_left_identity_plus x
    = Z + x =:= x
  
  prop_right_identity_mul :: Nat -> Prop Nat
  prop_right_identity_mul x
    = x * S Z =:= x
  
  prop_left_identity_mul :: Nat -> Prop Nat
  prop_left_identity_mul x
    = S Z * x =:= x
  
  prop_add_comm :: Nat -> Nat -> Prop Nat
  prop_add_comm x y
    = x + y =:= y + x
  
  prop_mul_comm :: Nat -> Nat -> Prop Nat
  prop_mul_comm x y
    = x * y =:= y * x
  
  prop_left_distrib :: Nat -> Nat -> Nat -> Prop Nat
  prop_left_distrib x y z
    = x * (y + z) =:= (x * y) + (x * z)
  
  prop_right_distrib :: Nat -> Nat -> Nat -> Prop Nat
  prop_right_distrib x y z
    = (x + y) * z =:= (x * z) + (y * z)
  
  prop_minus_zeroish :: Nat -> Nat -> Prop Nat
  prop_minus_zeroish n m
    = n - (n + m) =:= Z
  
  prop_minus_absorbish  :: Nat -> Nat -> Prop Nat
  prop_minus_absorbish n m
    = (n + m) - n =:= m
  
  prop_minus_distribish :: Nat -> Nat -> Nat -> Prop Nat
  prop_minus_distribish k m n
    = (k + m) - (k + n) =:= m - n
  
  prop_le_succ_plus :: Nat -> Nat -> Prop Bool
  prop_le_succ_plus i m
    = proveBool (i < S (i + m))
  
  prop_le_plus :: Nat -> Nat -> Prop Bool
  prop_le_plus n m
    = proveBool (n <= (n + m))
  
  prop_le_plus_sym :: Nat -> Nat -> Prop Bool
  prop_le_plus_sym n m
    = proveBool (n <= (m + n))
  
  prop_minus_plus :: Nat -> Nat -> Prop Nat
  prop_minus_plus n m
    = (m + n) - n =:= m
  
  prop_lt_suc  :: Nat -> Nat -> Prop Bool
  prop_lt_suc i m
    = proveBool (i < S (m + i))
  
  main = do
    quickCheck (printTestCase "prop_assoc_plus" prop_assoc_plus)
    quickCheck (printTestCase "prop_assoc_mul" prop_assoc_mul)
    quickCheck (printTestCase "prop_right_identity_plus" prop_right_identity_plus)
    quickCheck (printTestCase "prop_left_identity_plus" prop_left_identity_plus)
    quickCheck (printTestCase "prop_right_identity_mul" prop_right_identity_mul)
    quickCheck (printTestCase "prop_left_identity_mul" prop_left_identity_mul)
    quickCheck (printTestCase "prop_add_comm" prop_add_comm)
    quickCheck (printTestCase "prop_mul_comm" prop_mul_comm)
    quickCheck (printTestCase "prop_left_distrib" prop_left_distrib)
    quickCheck (printTestCase "prop_right_distrib" prop_right_distrib)
    quickCheck (printTestCase "prop_minus_zeroish" prop_minus_zeroish)
    quickCheck (printTestCase "prop_minus_absorbish" prop_minus_absorbish)
    quickCheck (printTestCase "prop_minus_distribish" prop_minus_distribish)
    quickCheck (printTestCase "prop_le_succ_plus" prop_le_succ_plus)
    quickCheck (printTestCase "prop_le_plus" prop_le_plus)
    quickCheck (printTestCase "prop_le_plus_sym" prop_le_plus_sym)
    quickCheck (printTestCase "prop_minus_plus" prop_minus_plus)
    quickCheck (printTestCase "prop_lt_suc" prop_lt_suc)
  