> module PS1Test where
> import PS1Soln

Test of summation:

> sig1 = Sigma "x" (EInt 1) (EInt 5) (EVar "x")
> sig2 = Sigma "x" (EInt 5) (EInt 1) (EVar "x")

> ts1 = testI sig1  -- 15
> ts2 = testI sig2  -- 0

Encoding of Problem 1:

   P(a,b) == Exists m . m > 0 /\ a*m = b

> p :: (IntExp,IntExp) -> Assert
> p(a,b) = Exists "m" ( (EVar "m" :>: EInt 0)      :/\:
>                       ((a :*: EVar "m") :=: b) )

   Q(a,b,c) == P(a,b) /\ P(a,c)

> q :: (IntExp,IntExp,IntExp) -> Assert
> q(a,b,c) = p(a,b) :/\: p(a,c)

a) PRIME(b) == not Exists a . (a /= b) /\ (a /= 1) /\ P(a,b)

> prime :: IntExp -> Assert
> prime(b) = Not (Exists "a" ((EVar "a" :/=: b)      :/\: 
>                             (EVar "a" :/=: EInt 1) :/\: 
>                             p(EVar "a",b))             )

b) GCD(a,b,c) == Q(a,b,c) /\ not Exists a' . a'>a /\ Q(a',b,c)

> gcd' :: (IntExp,IntExp,IntExp) -> Assert
> gcd'(a,b,c) = q(a,b,c) :/\: 
>               Not (Exists "a'" ((EVar "a'" :>: a) :/\: q(EVar "a'",b,c)))

c) FERMAT = not (Exists a . Exists b . Exists c . Exists n . n > 2 /\ a^n + b^n = c^n) 

> fermat = Not (Exists "a" (Exists "b" (Exists "c" (Exists "n" (
>               (EVar "n" :>: EInt 2) :/\:
>               (((EVar "a" :^: EVar "n") :+: (EVar "b" :^: EVar "n")) :=: 
>                (EVar "c" :^: EVar "n")))))))  

Examples:

> ta1 = testA (p (EInt 6, EInt 42))		-- True
> ta2 = testA (p (EInt 42, EInt 42))		-- True
> ta3 = testA (p (EInt 6, EInt 43))		-- diverges (can this be avoided??)

> tb1 = testA (q (EInt 6, EInt 42, EInt 600))	-- True
> tb2 = testA (q (EInt 6, EInt 42, EInt 43))	-- diverges

> tc1 = testA (gcd' (EInt 6, EInt 42, EInt 43)) -- diverges
> tc2 = testA (gcd' (EInt 6, EInt 18, EInt 42)) -- diverges
> tc3 = testA (gcd' (EInt 3, EInt 18, EInt 42)) -- diverges

> td1 = testA (prime (EInt 4))			-- diverges
> td2 = testA (prime (EInt 7))			-- diverges