(* Assignment 1 - EasyCrypt's Ambient Logic

   Due Friday, February 2, at 11:59pm on Gradescope

   In this assignment, you should (for full credit) make good use of
   the advanced proof features illustrated in the labs and described
   in the slides on the Ambient Logic, with the goal of producing
   concise, elegant proofs.

   If you have trouble with a lemma or a part of a lemma, you may
   use `admit` for the proof of that lemma or lemma part. You can
   always come back later to these steps and try to complete them. *)

require import AllCore.

(* QUESTION 1 (34 Points)

   In this question, two of the lemmas are proved for you, but you
   must prove the remaining four. You must prove the lemmas in order,
   as later lemmas may use earlier ones. You may not introduce
   additional lemmas.

   You may not use the `smt` or `case` tactics, or any of the lemmas
   of the EasyCrypt Library. (`smt` can also be invoked using `/#` in
   an introduction pattern or application of `rewrite`; you may not
   use that either. There is a version of `elim` that, like `case`,
   lets one work with truth tables; you may not use that version of
   `elim` either. You may use the version of `elim` for eliminating
   hypotheses (assumptions), as we did in the labs). *)

(* trivial proves this; you may use it below *)

lemma not_intro (a : bool) :
  (a => false) => ! a.
proof. trivial. qed.

(* we proved the following lemma in lab, but by using `case`, which
   you may not use *)

lemma negb_or (a b : bool) :
  ! (a \/ b) <=> ! a /\ ! b.
proof.
(* BEGIN FILL IN *)
(* END FILL IN *)
qed.

(* trivial proves this; you may use it below *)

lemma by_contradiction (a : bool) :
  (! a => false) => a.
proof. trivial. qed.

lemma excluded_middle (a : bool) :
  a \/ !a.
proof.
(* BEGIN FILL IN *)
(* END FILL IN *)
qed.

lemma negb_and (a b : bool) :
  ! (a /\ b) <=> ! a \/ ! b.
proof.
(* BEGIN FILL IN *)
(* END FILL IN *)
qed.

lemma negb_imply (a b : bool) :
  ! (a => b) <=> a /\ ! b.
proof.
(* BEGIN FILL IN *)
(* END FILL IN *)
qed.

(* QUESTION 2 (33 Points)

   In this question, you may not use `smt` (or `/#`) or any lemmas
   from the EasyCrypt Library, but you may use all other tactics. *)

lemma exists_or_iff (P Q : 'a -> bool) :
  (exists (x : 'a), P x \/ Q x) <=>
  (exists (x : 'a), P x) \/ (exists (x : 'a), Q x).
proof.
(* BEGIN FILL IN *)
(* END FILL IN *)
qed.

lemma forall_and_iff (P Q : 'a -> bool) :
  (forall (x : 'a), P x /\ Q x) <=>
  (forall (x : 'a), P x) /\ (forall (x : 'a), Q x).
proof.
(* BEGIN FILL IN *)
(* END FILL IN *)
qed.

(* QUESTION 3 (33 Points)

   In this problem, you may not use `smt` (or `/#'), but you may use
   all other tactics as well as all lemmas of the EasyCrypt Library.

   You may prove whatever auxiliary lemmas you need.

   (Hint: do a `print` of the operator `odd`, and then search for
   related lemmas.) *)

(* operators and lemmas about integer division, and lemmas about the
   standard ordering on the integers *)

require import IntDiv StdOrder.
import IntOrder.

(* definition of being a prime number *)

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

(* BEGINNING OF AUXILIARY LEMMAS *)
(* END OF AUXILIARY LEMMAS *)

(* if n and n + 1 are both prime, then n = 2 *)

lemma adjacent_primes_uniq_2 (n : int) :
  is_prime n => is_prime (n + 1) => n = 2.
proof.
(* BEGIN FILL IN *)
(* END FILL IN *)
qed.