(* Q1: Implementing Propositional Logic *)

(* Implement the below function using only &&, ||, and `not`. 
   (You do not need to use all three of these primitives.) 
*)
let implies (p : bool) (q : bool) : bool = failwith "TODO"

(* Next, implement implies using only `if/then/else` expressions -- no `&&`, `||`, or `not`. You can also use `true` and `false`. *)
let implies_if (p : bool) (q : bool) : bool = failwith "TODO"

(* Q2: Translating propositional logic *)

(* (P /\ Q) \/ (not (R /\ S)) *)
let p1 (p : bool) (q : bool) (r : bool) (s : bool) : bool = failwith "TODO"


(* (P \/ Q) ==> (not R) *)
let p2 (p : bool) (q : bool) (r : bool) : bool = failwith "TODO"

(* not (P /\ (Q \/ R)) *)
let p3 (p : bool) (q : bool) (r : bool) : bool = failwith "TODO"

(* (P ==> Q) /\ (Q ==> P) *)
let p4 (p : bool) (q : bool) : bool = failwith "TODO"

(* Q3: Forall, Exists on Booleans  *)

let forallb (f : bool -> bool) : bool = failwith "TODO"

let existsb (f : bool -> bool) : bool = failwith "TODO"



(* Q4: Verifying Equivalences *)

(* Calculate the truth value of:
  forall p,
    (p && p) = p
*)
let lemma_1 () : bool = failwith "TODO"

(* Calculate the truth value of:
  forall p, exists q, 
    (p && q) = p
  *)

let lemma_2 () : bool = failwith "TODO"

(* Calulate the truth value of:
  forall p, forall q, 
    ((not p) ==> q) = (p \/ q).
*)
let lemma_3 () : bool = failwith "TODO"

(* Q5: Simplifying Propositions *)

(* Simplify (not p) || q || p, and use forallb to verify that your simplification is correct. *)

let prop_complex (p : bool) (q : bool) : bool = 
    (not p) || q || p

let prop_simple (p : bool) (q : bool) : bool = failwith "TODO"

(* forall q : bool, forall q : bool,  prop_complex p q = prop_simple p q *)
let prop_simple_lemma () : bool = failwith "TODO"


(* Q5: Forall, Exists on [0..5] *)

(* Do the same as Q3, but instead of over bool, over the set of integers from 0
to 5 (inclusive). *)
let forall_0_5 (f : int -> bool) : bool = failwith "TODO"
let exists_0_5 (f : int -> bool) : bool = failwith "TODO"

(* Q6: Formalizing properties on integers *)

(* forall x \in [0..5], exists y \in [0..5], x - y = 0 *)
(* Use forall_0_5 and exists_0_5. *)

let lemma_4 () : bool = failwith "TODO"

(* forall x \in [0..5],
  (x mod 2) = 0 ==> 
    exists k \in [0..5],
      x = 2 * k

  (Hint: mod is an infix operator that can go between numbers in OCaml, 
    just like +, *, or -.)
*)

let lemma_5 () : bool = failwith "TODO"