Librairie lib_arith (.sats)

(supprimer le menu, télécharger, aller au .dats)

(****************************************)
(*                                      *)
(*        Arithmetical functions        *)
(*                                      *)
(****************************************)

// Used in dans lib_prime

propdef Mod (x : int, y : int, r : int) = [y <> 0] [q : int] MUL (q, y, x - r)
propdef Div (p : int, q : int) = [k : int] MUL (k, p, q)

prfun mul_incr {x, y, z : nat; t, t' : int | y <= z} (pf : MUL (x, y, t), pf2 : MUL (x, z, t'))
        :<> [t <= t'] void

prfun square_incr {x, y : nat; t, t' : int | x <= y} (pf : MUL (x, x, t), pf2 : MUL (y, y, t'))
        : [t <= t'] void

prfun div_nat_nat_nat {x, y, z : int | x > 0; z > 0} (pf : MUL (x, y, z))
        : [y > 0] void

prfun div_less {k, m : pos} (pf : Div (k, m))
        : [k <= m] void

prfun zero_div {k : nat} (pf : Div (0, k))
        : [k == 0] void

(***********************)
(*     Gcd and lcm     *)
(***********************)

propdef Gcd (m : int, n : int, gcd : int) =
  (Div (gcd, m), Div (gcd, n), {k : pos} (Div (k, m), Div (k, n)) -<> [gcd >= k] void)

propdef Lcm (m : int, n : int, lcm : int) =
  (Div (m, lcm), Div (n, lcm), {k : nat} (Div (m, k), Div (n, k)) -<> [lcm <= k] void)

fun gcd_commute {m, n, gcd : int} (pf : Gcd (m, n, gcd))
        : Gcd (n, m, gcd)

fun gcd {m, n : nat | m <> 0 || n <> 0} (m : int m, n : int n)
        : [r : int] (Gcd (m, n, r) | int r)