(* Assignment 1 - EasyCrypt's Ambient Logic (100 points)

   Due Friday, October 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.

   If you use AI to solve a question, you must add a comment
   explaining the process you followed, including what prompts you
   used. Whether or not you use AI, you must understand your
   answers, and be able to explain them orally. *)

require import AllCore.

(* the following two lemmas are already proved, and may be used freely
   in answering the following questions *)

(* if you want to prove a goal whose conclusion is !P, running the
   tactic apply not_intro will reduce this goal to showing P => false *)

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

(* if you want to prove a goal whose conclusion is P, running the
   tactic apply contradiction will reduce this goal to showing
   !P => false *)

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

(* end of already proved lemmas *)

(* Question 1 (25 points)

   You may *not* use the `smt` or `case` tactics, nor 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 form either. There are some other ways to do
   proofs using truth tables in EasyCrypt; you may *not* use such
   approaches. *)

lemma lem1 (x y z : bool) :
  (x \/ y) /\ (x => z) /\ (y => z) => z.
proof.
(* BEGIN FILL IN *)
move => [] [x_true | y_true] [x_implies_z y_implies_z].
by apply x_implies_z.
by apply y_implies_z.
(* END FILL IN *)
qed.

(* Question 2 (25 points)

   You may *not* use the `smt` or `case` tactics, nor 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 form either. There are some other ways to do
   proofs using truth tables in EasyCrypt; you may *not* use such
   approaches. *)

lemma lem2 (x y : bool) :
  (x => ! y) <=> (y => ! x).
proof.
(* BEGIN FILL IN *)
split => [x_imply_not_y y_true | y_imply_not_x x_true].
apply not_intro => x_true.
have // : ! y by apply x_imply_not_y.
apply not_intro => y_true.
have // : ! x by apply y_imply_not_x.
(* END FILL IN *)
qed.

(* Question 3 (25 points)

   You may *not* use the `smt` or `case` tactics, nor 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 form either. There are some other ways to do
   proofs using truth tables in EasyCrypt; you may *not* use such
   approaches. *)

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

(* Question 4 (25 points)

   In this question, there are three lemmas to prove, and you must
   prove them in order. Earlier lemmas can be used to prove later
   ones.

   You *may* use any of the lemmas of the EasyCrypt Library, but you
   may not use `smt`, even in the `/#` form. You *may* use `case`.

   Hint: run these commands:

     print Int.odd.
     search Int.odd.

   Int.odd is EasyCrypt's test for an integer being odd.  There is no
   Int.even. We have defined our own version of `odd`, as well
   `even`. *)

require import IntDiv.

op even (k : int) = k %% 2 = 0.
op odd (k : int) = ! even k.

lemma odd_iff_even_minus1 (k : int) :
  odd k <=> even (k - 1).
proof.
(* BEGIN FILL IN *)
rewrite /odd /even -oddP -oddPn.
have -> : k = (k - 1) + 1 by trivial.
by rewrite oddS.
(* END FILL IN *)
qed.

lemma even_eq (k : int) :
  even k => k = 2 * (k %/ 2).
proof.
(* BEGIN FILL IN *)
rewrite /even => eq0_k_mod2.
have -> : 2 * (k %/ 2) = k %/ 2 * 2 + k %% 2 by rewrite {1}mulrC eq0_k_mod2.
apply divz_eq.
(* END FILL IN *)
qed.

lemma odd_eq (k : int) :
  odd k => k = 2 * ((k - 1) %/ 2) + 1.
proof.
(* BEGIN FILL IN *)
move => odd_k.
by rewrite -subr_eq {1}(even_eq (k - 1)) 1:-odd_iff_even_minus1.
(* END FILL IN *)
qed.