(* 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.