{- | module: Main description: The divides relation on natural numbers - testing license: MIT maintainer: Joe Leslie-Hurd stability: provisional portability: portable -} module Main ( main ) where import qualified OpenTheory.Natural as Natural import qualified OpenTheory.Natural.Divides as Divides import qualified OpenTheory.Primitive.Natural as Primitive.Natural import OpenTheory.Primitive.Test proposition0 :: Primitive.Natural.Natural -> Bool proposition0 a = Divides.divides a 0 proposition1 :: Primitive.Natural.Natural -> Bool proposition1 a = Divides.divides a a proposition2 :: Primitive.Natural.Natural -> Bool proposition2 a = Divides.divides 1 a proposition3 :: Primitive.Natural.Natural -> Primitive.Natural.Natural -> Bool proposition3 a b = Divides.divides (fst (Divides.egcd a b)) a proposition4 :: Primitive.Natural.Natural -> Primitive.Natural.Natural -> Bool proposition4 a b = Divides.divides (fst (Divides.egcd a b)) b proposition5 :: Primitive.Natural.Natural -> Bool proposition5 a = Divides.divides 2 a == Natural.naturalEven a proposition6 :: Primitive.Natural.Natural -> Primitive.Natural.Natural -> Bool proposition6 ap b = let a = ap + 1 in let (_, (_, t)) = Divides.egcd a b in t < a proposition7 :: Primitive.Natural.Natural -> Primitive.Natural.Natural -> Bool proposition7 ap b = let a = ap + 1 in let (_, (s, _)) = Divides.egcd a b in s < max b 2 proposition8 :: Primitive.Natural.Natural -> Primitive.Natural.Natural -> Bool proposition8 ap b = let a = ap + 1 in let (g, (s, t)) = Divides.egcd a b in t * b + g == s * a proposition9 :: Primitive.Natural.Natural -> Primitive.Natural.Natural -> Primitive.Natural.Natural -> Primitive.Natural.Natural -> Bool proposition9 ap bp xp yp = let aq = ap + 1 in let bq = bp + 1 in let g = fst (Divides.egcd aq bq) in let a = aq `div` g in let b = bq `div` g in let x = xp `mod` a in let y = yp `mod` b in Divides.chineseRemainder a b x y < a * b proposition10 :: Primitive.Natural.Natural -> Primitive.Natural.Natural -> Primitive.Natural.Natural -> Primitive.Natural.Natural -> Bool proposition10 ap bp xp yp = let aq = ap + 1 in let bq = bp + 1 in let g = fst (Divides.egcd aq bq) in let a = aq `div` g in let b = bq `div` g in let x = xp `mod` a in let y = yp `mod` b in Divides.chineseRemainder a b x y `mod` a == x proposition11 :: Primitive.Natural.Natural -> Primitive.Natural.Natural -> Primitive.Natural.Natural -> Primitive.Natural.Natural -> Bool proposition11 ap bp xp yp = let aq = ap + 1 in let bq = bp + 1 in let g = fst (Divides.egcd aq bq) in let a = aq `div` g in let b = bq `div` g in let x = xp `mod` a in let y = yp `mod` b in Divides.chineseRemainder a b x y `mod` b == y main :: IO () main = do check "Proposition 0:\n !a. divides a 0\n " proposition0 check "Proposition 1:\n !a. divides a a\n " proposition1 check "Proposition 2:\n !a. divides 1 a\n " proposition2 check "Proposition 3:\n !a b. divides (fst (egcd a b)) a\n " proposition3 check "Proposition 4:\n !a b. divides (fst (egcd a b)) b\n " proposition4 check "Proposition 5:\n !a. divides 2 a <=> even a\n " proposition5 check "Proposition 6:\n !ap b. let a <- ap + 1 in let (g, s, t) <- egcd a b in t < a\n " proposition6 check "Proposition 7:\n !ap b. let a <- ap + 1 in let (g, s, t) <- egcd a b in s < max b 2\n " proposition7 check "Proposition 8:\n !ap b. let a <- ap + 1 in let (g, s, t) <- egcd a b in t * b + g = s * a\n " proposition8 check "Proposition 9:\n !ap bp xp yp.\n let aq <- ap + 1 in\n let bq <- bp + 1 in\n let g <- fst (egcd aq bq) in\n let a <- aq div g in\n let b <- bq div g in\n let x <- xp mod a in\n let y <- yp mod b in\n chineseRemainder a b x y < a * b\n " proposition9 check "Proposition 10:\n !ap bp xp yp.\n let aq <- ap + 1 in\n let bq <- bp + 1 in\n let g <- fst (egcd aq bq) in\n let a <- aq div g in\n let b <- bq div g in\n let x <- xp mod a in\n let y <- yp mod b in\n chineseRemainder a b x y mod a = x\n " proposition10 check "Proposition 11:\n !ap bp xp yp.\n let aq <- ap + 1 in\n let bq <- bp + 1 in\n let g <- fst (egcd aq bq) in\n let a <- aq div g in\n let b <- bq div g in\n let x <- xp mod a in\n let y <- yp mod b in\n chineseRemainder a b x y mod b = y\n " proposition11 return ()