opentheory-divides 1.57 → 1.61

raw patch · 3 files changed

+76/−10 lines, 3 filesdep ~opentheoryPVP ok

version bump matches the API change (PVP)

Dependency ranges changed: opentheory

API changes (from Hackage documentation)

Files

• opentheory-divides.cabal +4/−4
• src/OpenTheory/Natural/Divides.hs +13/−3
• src/Test.hs +59/−3

@@ -1,5 +1,5 @@ name: opentheory-divides-version: 1.57+version: 1.61 category: Number Theory synopsis: The divides relation on natural numbers license: MIT@@ -10,14 +10,14 @@ maintainer: Joe Leslie-Hurd <joe@gilith.com> description:   The divides relation on natural numbers - this package was automatically-  generated from the OpenTheory package natural-divides-1.57+  generated from the OpenTheory package natural-divides-1.61  library   build-depends:     base >= 4.0 && < 5.0,     QuickCheck >= 2.4.0.1 && < 3.0,     opentheory-primitive >= 1.5 && < 2.0,-    opentheory >= 1.195 && < 1.198+    opentheory >= 1.198 && < 1.199   hs-source-dirs: src   ghc-options: -Wall   exposed-modules:@@ -29,7 +29,7 @@     base >= 4.0 && < 5.0,     QuickCheck >= 2.4.0.1 && < 3.0,     opentheory-primitive >= 1.5 && < 2.0,-    opentheory >= 1.195 && < 1.198+    opentheory >= 1.198 && < 1.199   hs-source-dirs: src   ghc-options: -Wall   main-is: Test.hs

@@ -13,9 +13,6 @@  import qualified OpenTheory.Primitive.Natural as Natural -divides :: Natural.Natural -> Natural.Natural -> Bool-divides a b = if a == 0 then b == 0 else b `mod` a == 0- egcd ::   Natural.Natural -> Natural.Natural ->     (Natural.Natural, (Natural.Natural, Natural.Natural))@@ -28,3 +25,16 @@       let (g, (s, t)) = egcd c (b `mod` c) in       let u = s + b `div` c * t in       (g, (u, t + a `div` b * u))++chineseRemainder ::+  Natural.Natural -> Natural.Natural -> Natural.Natural ->+    Natural.Natural -> Natural.Natural+chineseRemainder a b =+  let (_, (s, t)) = egcd a b in+  let ab = a * b in+  let sa = s * a in+  let tb = (a - t) * b in+  \x y -> (x * tb + y * sa) `mod` ab++divides :: Natural.Natural -> Natural.Natural -> Bool+divides a b = if a == 0 then b == 0 else b `mod` a == 0

@@ -38,9 +38,60 @@  proposition6 ::   Primitive.Natural.Natural -> Primitive.Natural.Natural -> Bool-proposition6 a b =-  let (g, (s, t)) = Divides.egcd (a + 1) b in t * b + g == s * (a + 1)+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@@ -49,5 +100,10 @@        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  !a b. let (g, s, t) <- egcd (a + 1) b in t * b + g = s * (a + 1)\n  " proposition6+       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 ()