(* ASSIGNMENT 1

   Due on Gradescope by 5pm on Friday, February 12 *)

require import AllCore.

(* QUESTION 1

   prove the following lemma without using the tactics `case` or
   `smt`, and without using any lemmas from the EasyCrypt Library: *)

lemma sub (a b c : bool) :
  (a => b => c) => (a => b) => a => c.
proof.
(* BEGIN FILL IN *)
move => H1 H2 a_true.
apply H1 => //.
by apply H2.
(* END FILL IN *)
qed.

lemma sub' (a b c : bool) :
  (a => b => c) => (a => b) => a => c.
proof.
(* BEGIN FILL IN *)
move => H1 H2 a_true.
by rewrite H1 2:H2.
(* END FILL IN *)
qed.

(* QUESTION 2

   prove the following lemma without using the tactics `case` or
   `smt`, and without using any lemmas from the EasyCrypt Library: *)

lemma peirce (a b : bool) :
  (a \/ !a) => ((a => b) => a) => a.
proof.
(* BEGIN FILL IN *)
move => [// | a_false] H.
by apply H.
(* END FILL IN *)
qed.

lemma peirce' (a b : bool) :
  (a \/ !a) => ((a => b) => a) => a.
proof.
(* BEGIN FILL IN *)
move => [// | -> //].
(* END FILL IN *)
qed.

(* QUESTION 3

   prove the following lemma without using the `smt` tactic, and
   without using any lemmas from the EasyCrypt Library (you may use
   the `case` tactic): *)

lemma not_exists (P : 'a -> bool) :
  (! exists (x : 'a), P x) <=> (forall (x : 'a), ! (P x)).
proof.
(* BEGIN FILL IN *)
split => [not_ex x | all_not].
case (P x) => [P_x | //].
have // : exists x, P x.
  by exists x.
case (exists x, P x) => [[] x P_x | //].
have // : ! (P x).
  apply all_not.
(* END FILL IN *)
qed.

(* QUESTION 4

   This question is about proving the equivalence of two definitions
   of when an integer is prime. *)

require import IntDiv StdOrder. (* lemmas for integer mod and div *)
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.

(* you may use the following lemma in your proof (it should probably
   be provided by IntDiv): *)

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, this lemma 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).
*)

(* prove the following lemma without using the `smt` tactic; you
   may use the `case` tactic as well as any lemmas from the EasyCrypt
   Library

   hint: you can use your solution to QUESTION 3, and you can use
   `search` to look for needed lemmas in the EasyCrypt Library. E.g.,

     search [!] (/\)

   searches for lemmas involving negation and conjunction

   for *partial credit*, you can use `smt` or even `admit` for parts
   of your proof *)

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.
(* BEGIN FILL IN *)
move => ge2_n.
have ge1_n : 1 <= n.
  by apply (lez_trans 2).
rewrite not_exists /=.
apply forall_iff => x /=.
rewrite 2!negb_and.
split => [[] // [not_lt1_x x_div_n | not_lt_x_n x_div_n] | rhs_impl].
left; by rewrite lezNgt.
right.
have ge1_x : 1 <= x.
  rewrite -lerNgt in not_lt_x_n.
  by apply (lez_trans n).
have not_n_lt_x : ! n < x.
  by rewrite ler_gtF 1:div_le.
case (x = n) => [// | x_ne_n].
rewrite neq_ltz in x_ne_n.
by elim x_ne_n.
case (x %| n) => [x_div_n /= | //].
have [le1_x | -> //] : x <= 1 \/ x = n.
  by rewrite rhs_impl.
left; by rewrite ltzNge.
(* END FILL IN *)
qed.

(* use prime_equiv_ge2 (but not the `smt` tactic) to prove the
   following lemma asserting the equivalence of the two definitions of
   primality (you won't need `case` or lemmas from the EasyCrypt
   Library, but you may use them) *)

lemma prime_equiv (n : int) :
 is_prime1 n <=> is_prime2 n.
proof.
(* BEGIN FILL IN *)
rewrite /is_prime1 /is_prime2.
split => [[] ge2_n H | [] ge2_n H].
split => //.
by rewrite -prime_equiv_ge2.
split => //.
by rewrite prime_equiv_ge2.
(* END FILL IN *)
qed.