(* proving the equivalence of two definitions of when an integer is
   prime *)

require import AllCore.   (* core theories *)
require import IntDiv.    (* lemmas for integer mod and div *)
require import StdOrder.  (* orderings *)
import IntOrder.          (* lemmas about <, <= on int *)

(* n %/ x is the integer division of n by x, discarding any remainder

   n %% x is the remainder of integer division of n by x

   x %| n tests whether x divides n, i.e., n %% x = 0

   %/ and %% are actually abbreviations, defined in terms of edivz;
   consequently, when using `search` to look for lemmas involving
   these abbreviations, one must search for `edivz` instead. But we've
   provided (below) the lemma that needs such facts *)

(* here are two ways of defining when an integer is prime, which
   you will prove are equivalent: *)

op is_prime1 (n : int) : bool =
  2 <= n /\
  ! exists (x : int),
    x %| n /\ 1 < x /\ x < n.

op is_prime2 (n : int) : bool =
   2 <= n /\
   forall (x : int),
   x %| n => x <= 1 \/ x = n.

lemma div_le (x n : int) :
  1 <= x => 1 <= n => x %| n => x <= n.
proof.
move => ge1_x ge1_n x_div_n.
have n_eq : n = (n %/ x) * x.
  by rewrite eq_sym -dvdz_eq.
rewrite n_eq -{1}mul1z ler_pmul // (lez_trans 1) //.
case (1 <= n %/ x) => //.
rewrite -ltrNge => lt1_n_div_x.
have le0_n : n <= 0.
  by rewrite n_eq mulr_le0_ge0 1:-ltzS // (lez_trans 1).
have // : 1 <= 0.
  by apply (lez_trans n).
qed.

(* When proving the following lemma, these lemmas from the EasyCrypt
   Library will be helpful:

lemma forall_iff (P P' : 'a -> bool) :
  (forall x, P x <=> P' x) =>
  (forall (x : 'a), P x) <=> (forall (x : 'a), P' x).

lemma nosmt negb_exists (P : 'a -> bool) :
  !(exists a, P a) <=> forall a, !P a.
*)

(* let's prove the following lemma without using the `smt` tactic *)

lemma prime_equiv_ge2 (n : int) :
  2 <= n =>
  (! (exists (x : int), x %| n /\ 1 < x /\ x < n) <=>
   (forall (x : int), x %| n => x <= 1 \/ x = n)).
proof.

qed.

(* use prime_equiv_ge2 (but not the `smt` tactic) to prove the
   following lemma asserting the equivalence of the two definitions of
   primality *)

lemma prime_equiv (n : int) :
 is_prime1 n <=> is_prime2 n.
proof.

qed.