{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# 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
sqrt2IsIrrational :: IO (Proof SBool)
sqrt2IsIrrational :: IO (Proof SBool)
sqrt2IsIrrational = TP (Proof SBool) -> IO (Proof SBool)
forall a. TP a -> IO a
runTP (TP (Proof SBool) -> IO (Proof SBool))
-> TP (Proof SBool) -> IO (Proof SBool)
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
Proof (Forall "a" Integer -> SBool)
oddSquaredIsOdd <- String
-> (Forall "a" Integer -> SBool)
-> StepArgs (Forall "a" Integer -> SBool) Integer
-> TP (Proof (Forall "a" Integer -> SBool))
forall t.
(Proposition (Forall "a" Integer -> SBool), SymVal t,
EqSymbolic (SBV t)) =>
String
-> (Forall "a" Integer -> SBool)
-> StepArgs (Forall "a" Integer -> SBool) t
-> TP (Proof (Forall "a" Integer -> SBool))
forall a t.
(Calc a, Proposition a, SymVal t, EqSymbolic (SBV t)) =>
String -> a -> StepArgs a t -> TP (Proof a)
calc String
"oddSquaredIsOdd"
(\(Forall @"a" SInteger
a) -> SInteger -> SBool
odd SInteger
a SBool -> SBool -> SBool
.=> SInteger -> SBool
odd (SInteger -> SInteger
sq SInteger
a)) (StepArgs (Forall "a" Integer -> SBool) Integer
-> TP (Proof (Forall "a" Integer -> SBool)))
-> StepArgs (Forall "a" Integer -> SBool) Integer
-> TP (Proof (Forall "a" Integer -> SBool))
forall a b. (a -> b) -> a -> b
$
\SInteger
a -> [SInteger -> SBool
odd SInteger
a] [SBool] -> TPProofRaw SInteger -> (SBool, TPProofRaw SInteger)
forall a. [SBool] -> TPProofRaw a -> (SBool, TPProofRaw 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
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"
TPProofRaw SInteger
-> ChainsTo (TPProofRaw SInteger) -> ChainsTo (TPProofRaw 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
TPProofRaw SInteger
forall a. TPProofRaw a
qed
Proof (Forall "a" Integer -> SBool)
squareEvenImpliesEven <- String
-> (Forall "a" Integer -> SBool)
-> [ProofObj]
-> TP (Proof (Forall "a" Integer -> SBool))
forall a.
Proposition a =>
String -> a -> [ProofObj] -> TP (Proof a)
lemma String
"squareEvenImpliesEven"
(\(Forall @"a" SInteger
a) -> SInteger -> SBool
even (SInteger -> SInteger
sq SInteger
a) SBool -> SBool -> SBool
.=> SInteger -> SBool
even SInteger
a)
[Proof (Forall "a" Integer -> SBool) -> ProofObj
forall a. Proof a -> ProofObj
proofOf Proof (Forall "a" Integer -> SBool)
oddSquaredIsOdd]
Proof (Forall "a" Integer -> SBool)
evenSquaredIsMult4 <- String
-> (Forall "a" Integer -> SBool)
-> StepArgs (Forall "a" Integer -> SBool) Integer
-> TP (Proof (Forall "a" Integer -> SBool))
forall t.
(Proposition (Forall "a" Integer -> SBool), SymVal t,
EqSymbolic (SBV t)) =>
String
-> (Forall "a" Integer -> SBool)
-> StepArgs (Forall "a" Integer -> SBool) t
-> TP (Proof (Forall "a" Integer -> SBool))
forall a t.
(Calc a, Proposition a, SymVal t, EqSymbolic (SBV t)) =>
String -> a -> StepArgs a t -> TP (Proof a)
calc String
"evenSquaredIsMult4"
(\(Forall @"a" SInteger
a) -> SInteger -> SBool
even SInteger
a SBool -> SBool -> SBool
.=> Integer
4 Integer -> SInteger -> SBool
`sDivides` SInteger -> SInteger
sq SInteger
a) (StepArgs (Forall "a" Integer -> SBool) Integer
-> TP (Proof (Forall "a" Integer -> SBool)))
-> StepArgs (Forall "a" Integer -> SBool) Integer
-> TP (Proof (Forall "a" Integer -> SBool))
forall a b. (a -> b) -> a -> b
$
\SInteger
a -> [SInteger -> SBool
even SInteger
a] [SBool] -> TPProofRaw SInteger -> (SBool, TPProofRaw SInteger)
forall a. [SBool] -> TPProofRaw a -> (SBool, TPProofRaw 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
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"
TPProofRaw SInteger
-> ChainsTo (TPProofRaw SInteger) -> ChainsTo (TPProofRaw 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
TPProofRaw SInteger
forall a. TPProofRaw a
qed
let coPrime :: SInteger -> SInteger -> SBool
coPrime :: SInteger -> SInteger -> SBool
coPrime SInteger
x SInteger
y = (Forall Any Integer -> SBool) -> SBool
forall a. QuantifiedBool a => a -> SBool
quantifiedBool (\(Forall 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)
String -> SBool -> [ProofObj] -> TP (Proof SBool)
forall a.
Proposition a =>
String -> a -> [ProofObj] -> TP (Proof a)
lemma String
"sqrt2IsIrrational"
((Forall Any Integer -> Forall Any Integer -> SBool) -> SBool
forall a. QuantifiedBool a => a -> SBool
quantifiedBool (\(Forall SInteger
a) (Forall 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)))
[Proof (Forall "a" Integer -> SBool) -> ProofObj
forall a. Proof a -> ProofObj
proofOf Proof (Forall "a" Integer -> SBool)
squareEvenImpliesEven, Proof (Forall "a" Integer -> SBool) -> ProofObj
forall a. Proof a -> ProofObj
proofOf Proof (Forall "a" Integer -> SBool)
evenSquaredIsMult4]