{- |
module: Main
description: The divides relation on natural numbers - testing
license: MIT

maintainer: Joe Leslie-Hurd <joe@gilith.com>
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 ()