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

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

{-# OPTIONS_GHC -Wall -Werror #-}

module Documentation.SBV.Examples.KnuckleDragger.Sqrt2IsIrrational where

import Prelude hiding (even, odd)

import Data.SBV
import Data.SBV.Tools.KnuckleDragger

-- | 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 KnuckleDragger 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
sqrt2IsIrrational :: IO Proof
sqrt2IsIrrational :: IO Proof
sqrt2IsIrrational = KD Proof -> IO Proof
forall a. KD a -> IO a
runKD (KD Proof -> IO Proof) -> KD Proof -> IO Proof
forall a b. (a -> b) -> a -> b
$ do
    let even, odd :: SInteger -> SBool
        even :: SInteger -> SBool
even = (Integer
2 Integer -> SInteger -> SBool
`sDivides`)
        odd :: SInteger -> SBool
odd  = SBool -> SBool
sNot (SBool -> SBool) -> (SInteger -> SBool) -> SInteger -> SBool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SInteger -> SBool
even

        sq :: SInteger -> SInteger
        sq :: SInteger -> SInteger
sq SInteger
x = SInteger
x SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* SInteger
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 <- String
-> (Forall "a" Integer -> SBool)
-> (SInteger -> (SBool, KDProofRaw SInteger))
-> KD Proof
forall a steps.
(CalcLemma a steps, Proposition a) =>
String -> a -> steps -> KD Proof
calc String
"oddSquaredIsOdd"
                             (\(Forall @"a" SInteger
a) -> SInteger -> SBool
odd SInteger
a SBool -> SBool -> SBool
.=> SInteger -> SBool
odd (SInteger -> SInteger
sq SInteger
a)) ((SInteger -> (SBool, KDProofRaw SInteger)) -> KD Proof)
-> (SInteger -> (SBool, KDProofRaw SInteger)) -> KD Proof
forall a b. (a -> b) -> a -> b
$
                             \SInteger
a -> [SInteger -> SBool
odd SInteger
a] [SBool] -> KDProofRaw SInteger -> (SBool, KDProofRaw SInteger)
forall a. [SBool] -> KDProofRaw a -> (SBool, KDProofRaw a)
|- SInteger -> SInteger
sq SInteger
a
                                           SInteger -> ChainsTo SInteger -> ChainsTo SInteger
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: let k :: SInteger
k = String -> (SInteger -> SBool) -> SInteger
forall a.
(SymVal a, HasKind a) =>
String -> (SBV a -> SBool) -> SBV a
some String
"k" ((SInteger -> SBool) -> SInteger)
-> (SInteger -> SBool) -> SInteger
forall a b. (a -> b) -> a -> b
$ \SInteger
_k -> SInteger
a SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
2SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
*SInteger
_k SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger
1  -- Grab the witness that a is odd
                                           in SInteger -> SInteger
sq (SInteger
2 SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* SInteger
k SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger
1)
                                           SInteger -> String -> Hinted SInteger
forall a b. HintsTo a b => a -> b -> Hinted a
?? String
"expand square"
                                           KDProofRaw SInteger
-> ChainsTo (KDProofRaw SInteger) -> ChainsTo (KDProofRaw SInteger)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SInteger
4SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
*SInteger
kSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
*SInteger
k SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger
4SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
*SInteger
k SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger
1
                                           SInteger -> ChainsTo SInteger -> ChainsTo SInteger
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: ChainsTo SInteger
KDProofRaw SInteger
forall a. KDProofRaw a
qed

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

    -- Prove that if @a@ is an even number, then its square is four times the square of another.
    evenSquaredIsMult4 <- calc "evenSquaredIsMult4"
                               (\(Forall @"a" SInteger
a) -> SInteger -> SBool
even SInteger
a SBool -> SBool -> SBool
.=> Integer
4 Integer -> SInteger -> SBool
`sDivides` SInteger -> SInteger
sq SInteger
a) $
                               \SInteger
a -> [SInteger -> SBool
even SInteger
a] [SBool] -> KDProofRaw SInteger -> (SBool, KDProofRaw SInteger)
forall a. [SBool] -> KDProofRaw a -> (SBool, KDProofRaw a)
|- SInteger -> SInteger
sq SInteger
a
                                              SInteger -> ChainsTo SInteger -> ChainsTo SInteger
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: let k :: SInteger
k = String -> (SInteger -> SBool) -> SInteger
forall a.
(SymVal a, HasKind a) =>
String -> (SBV a -> SBool) -> SBV a
some String
"k" ((SInteger -> SBool) -> SInteger)
-> (SInteger -> SBool) -> SInteger
forall a b. (a -> b) -> a -> b
$ \SInteger
_k -> SInteger
a SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
2SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
*SInteger
_k -- Grab the witness that a is even
                                              in SInteger -> SInteger
sq (SInteger
2 SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* SInteger
k)
                                              SInteger -> String -> Hinted SInteger
forall a b. HintsTo a b => a -> b -> Hinted a
?? String
"expand square"
                                              KDProofRaw SInteger
-> ChainsTo (KDProofRaw SInteger) -> ChainsTo (KDProofRaw SInteger)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SInteger
4SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
*(SInteger
kSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
*SInteger
k)
                                              SInteger -> ChainsTo SInteger -> ChainsTo SInteger
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: ChainsTo SInteger
KDProofRaw SInteger
forall a. KDProofRaw a
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 SInteger
x SInteger
y = (Forall "z" Integer -> SBool) -> SBool
forall a. QuantifiedBool a => a -> SBool
quantifiedBool (\(Forall @"z" SInteger
z) -> (SInteger
x SInteger -> SInteger -> SInteger
`sEMod` SInteger
z SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
0 SBool -> SBool -> SBool
.&& SInteger
y SInteger -> SInteger -> SInteger
`sEMod` SInteger
z SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
0) SBool -> SBool -> SBool
.=> SInteger
z SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
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@ are not be co-prime:
    lemma "sqrt2IsIrrational"
        (\(Forall @"a" SInteger
a) (Forall @"b" SInteger
b) -> (SInteger -> SInteger
sq SInteger
a SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
2 SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* SInteger -> SInteger
sq SInteger
b) SBool -> SBool -> SBool
.=> SBool -> SBool
sNot (SInteger -> SInteger -> SBool
coPrime SInteger
a SInteger
b))
        [squareEvenImpliesEven, evenSquaredIsMult4]