-----------------------------------------------------------------------------
-- |
-- Module    : Documentation.SBV.Examples.TP.Sqrt2IsIrrational
-- Copyright : (c) Levent Erkok
-- License   : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- Prove that square-root of 2 is irrational.
-----------------------------------------------------------------------------

{-# LANGUAGE DataKinds        #-}
{-# LANGUAGE TypeAbstractions #-}

{-# OPTIONS_GHC -Wall -Werror #-}

module Documentation.SBV.Examples.TP.Sqrt2IsIrrational where

import Prelude hiding (even, odd)

import Data.SBV
import Data.SBV.TP

-- | Prove that square-root of @2@ is irrational. That is, we can never find @a@ and @b@ such that
-- @sqrt 2 == a / b@ and @a@ and @b@ are co-prime.
--
-- In order not to deal with reals and square-roots, we prove the integer-only alternative:
-- If @a^2 = 2b^2@, then @a@ and @b@ cannot be co-prime. We proceed by establishing the
-- following helpers first:
--
--   (1) An odd number squared is odd: @odd x -> odd x^2@
--   (2) An even number that is a perfect square must be the square of an even number: @even x^2 -> even x@.
--   (3) If a number is even, then its square must be a multiple of 4: @even x .=> x*x % 4 == 0@.
--
--  Using these helpers, we can argue:
--
--   (4)  Start with the premise @a^2 = 2b^2@.
--   (5)  Thus, @a^2@ must be even. (Since it equals @2b^2@ by (4).)
--   (6)  Thus, @a@ must be even. (Using (2) and (5).)
--   (7)  Thus, @a^2@ must be divisible by @4@. (Using (3) and (6). That is, @2b^2 == 4K@ for some @K@.)
--   (8)  Thus, @b^2@ must be even. (Using (7), and @b^2 = 2K@.)
--   (9)  Thus, @b@ must be even. (Using (2) and (8).)
--   (10) Since @a@ and @b@ are both even, they cannot be co-prime. (Using (6) and (9).)
--
-- Note that our proof is mostly about the first 3 facts above, then z3 and TP fills in the rest.
--
-- We have:
--
-- >>> sqrt2IsIrrational
-- Lemma: oddSquaredIsOdd
--   Step: 1                               Q.E.D.
--   Step: 2 (expand square)               Q.E.D.
--   Result:                               Q.E.D.
-- Lemma: squareEvenImpliesEven            Q.E.D.
-- Lemma: evenSquaredIsMult4
--   Step: 1                               Q.E.D.
--   Step: 2 (expand square)               Q.E.D.
--   Result:                               Q.E.D.
-- Lemma: sqrt2IsIrrational                Q.E.D.
-- [Proven] sqrt2IsIrrational :: Bool
sqrt2IsIrrational :: IO (Proof SBool)
sqrt2IsIrrational = runTP $ do
    let even, odd :: SInteger -> SBool
        even = (2 `sDivides`)
        odd  = sNot . even

        sq :: SInteger -> SInteger
        sq x = x * x

    -- Prove that an odd number squared gives you an odd number.
    -- We need to help the solver by guiding it through how it can
    -- be decomposed as @2k+1@.
    --
    -- Interestingly, the solver doesn't need the analogous theorem that even number
    -- squared is even, possibly because the even/odd definition above is enough for
    -- it to deduce that fact automatically.
    oddSquaredIsOdd <- calc "oddSquaredIsOdd"
                             (\(Forall @"a" a) -> odd a .=> odd (sq a)) $
                             \a -> [odd a] |- sq a
                                           =: let k = some "k" $ \_k -> a .== 2*_k + 1  -- Grab the witness that a is odd
                                           in sq (2 * k + 1)
                                           ?? "expand square"
                                           =: 4*k*k + 4*k + 1
                                           =: qed

    -- Prove that if a perfect square is even, then it has to be the square of an even number. For z3, the above proof
    -- is enough to establish this.
    squareEvenImpliesEven <- lemma "squareEvenImpliesEven"
                                   (\(Forall @"a" a) -> even (sq a) .=> even a)
                                   [proofOf oddSquaredIsOdd]

    -- Prove that if @a@ is an even number, then its square is four times the square of another.
    evenSquaredIsMult4 <- calc "evenSquaredIsMult4"
                               (\(Forall @"a" a) -> even a .=> 4 `sDivides` sq a) $
                               \a -> [even a] |- sq a
                                              =: let k = some "k" $ \_k -> a .== 2*_k -- Grab the witness that a is even
                                              in sq (2 * k)
                                              ?? "expand square"
                                              =: 4*(k*k)
                                              =: qed

    -- Define what it means to be co-prime. Note that we use euclidian notion of modulus here
    -- as z3 deals with that much better. Two numbers are co-prime if 1 is their only common divisor.
    let coPrime :: SInteger -> SInteger -> SBool
        coPrime x y = quantifiedBool (\(Forall z) -> (x `sEMod` z .== 0 .&& y `sEMod` z .== 0) .=> z .== 1)

    -- Prove that square-root of 2 is irrational. We do this by showing for all pairs of integers @a@ and @b@
    -- such that @a*a == 2*b*b@, it must be the case that @a@ and @b@ can not be co-prime:
    lemma "sqrt2IsIrrational"
          (quantifiedBool (\(Forall a) (Forall b) -> sq a .== 2 * sq b .=> sNot (coPrime a b)))
          [proofOf squareEvenImpliesEven, proofOf evenSquaredIsMult4]