Librairie lib_prime (.sats)

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

(***********************************************)
(*                                             *)
(*        Functions about prime numbers        *)
(*                                             *)
(***********************************************)

staload A = "lib_arith.sats"

propdef Prime (p : int) =
  (() -<> [p >= 2] void, ({x, y : pos | x <= y} MUL (x, y, p) -<> [x == 1] void))

(** A number is prime iff it is not evenly divisible by any number less than it’s square root *)
prfun is_prime_pf {p : int | p >= 2} (pf : {n : pos; k : int | k <= p}
                                           (MUL (n, n, k), $A.Div (n, p)) -<> [n == 1] void)
       : Prime p

// Logical if
dataprop L_if (bool, prop,  prop) =
  | {b : bool | b == true} {T, E : prop}  L_then (b, T, E) of (bool b, T)
  | {b : bool | b == false} {T, E : prop} L_else (b, T, E) of (bool b, E)

propdef prime (b : bool, p : int) = // prime(b, p) is true iff either b == true and p is
                                    // prime, or b == false and p is composite
  L_if (b, Prime p, Prime p -<> [0 == 1] void)

fun is_prime {p : int} (p : int p) : [b : bool] (prime (b, p) | bool b)

////
propdef Smallest_prime_factor (n : int, p : int) = // true iff p is the smallest prime factor
                                                   // of n
  (() -<> [n >= 2] void
   , Prime p
   , $A.Div (p, n)
   , {l : int} ($A.Div (l, n), Prime l) -<> [l >= p] void)

fun less_prime_factor {n : int | n >= 2} (n : int n)
        : [p : int] (Smallest_prime_factor (n, p) | int p)