(* week-03_exercises.v *)
(* LPP 2025 - CS3234 2024-2025, Sem2 *)
(* Olivier Danvy <olivier@comp.nus.edu.sg> *)
(* Version of 07 Feb 2025, with True instead of unit in the exercise about propositions *)
(* was: *)
(* Version of 31 Jan 2025 *)

(* ********** *)

(* Exercises about types: *)

(*
Definition ta : forall A : Type, A -> A * A :=
  ...
*)

(*
Definition tb : forall A B : Type, A -> B -> A * B :=
  ...
*)

(*
Definition tc : forall A B : Type, A -> B -> B * A :=
  ...
*)

Check (tt : unit).

(*
Definition td : forall (A : Type), (unit -> A) -> A :=
  ...
*)

(*
Definition te : forall A B : Type, (A -> B) -> A -> B :=
  ...
*)

(*
Definition tf : forall A B : Type, A -> (A -> B) -> B :=
  ...
*)

(*
Definition tg : forall A B C : Type, (A -> B -> C) -> A -> B -> C :=
  ...
*)

(*
Definition th : forall A B C : Type, (A -> B -> C) -> B -> A -> C :=
  ...
*)

(*
Definition ti : forall A B C D : Type, (A -> C) -> (B -> D) -> A -> B -> C * D :=
  ...
*)

(*
Definition tj : forall A B C : Type, (A -> B) -> (B -> C) -> A -> C :=
  ...
*)

(*
Definition tk : forall A B : Type, A * B -> B * A :=
  ... (* Hint: use a match expression to destructure the input pair. *)
*)

(*
Definition tl : forall A B C : Type, (A * B -> C) -> A -> B -> C :=
  ...
*)

(*
Definition tm : forall A B C : Type, (A -> B -> C) -> A * B -> C :=
  ...
*)

(*
Definition tn : forall A B C : Type, A * (B * C) -> (A * B) * C :=
  ...
*)

(* ********** *)

(* Exercises about propositions: *)

Proposition pa :
  forall A : Prop,
    A -> A /\ A.
Proof.
Abort.

Proposition pb :
  forall A B : Prop,
    A -> B -> A /\ B.
Proof.
Abort.

Proposition pc :
  forall A B : Prop,
    A -> B -> B /\ A.
Proof.
Abort.

Check I.

Proposition pd :
  forall (A : Prop),
    (True -> A) -> A.
Proof.
Abort.

Proposition pe :
  forall A B : Prop,
    (A -> B) -> A -> B.
Proof.
Abort.

Proposition pf :
  forall A B : Prop,
    A -> (A -> B) -> B.
Proof.
Abort.

Proposition pg :
  forall A B C : Prop,
    (A -> B -> C) -> A -> B -> C.
Proof.
Abort.

Proposition ph :
  forall A B C : Prop,
    (A -> B -> C) -> B -> A -> C.
Proof.
Abort.

Proposition pi :
  forall A B C D : Prop,
    (A -> C) -> (B -> D) -> A -> B -> C /\ D.
Proof.
Abort.

Proposition pj :
  forall A B C : Prop,
    (A -> B) -> (B -> C) -> A -> C.
Proof.
Abort.

Proposition pk :
  forall A B : Prop,
    A /\ B -> B /\ A.
Proof.
Abort.

Proposition pl :
  forall A B C : Prop,
    (A /\ B -> C) -> A -> B -> C.
Proof.
Abort.

Proposition pm :
  forall A B C : Prop,
    (A -> B -> C) -> A /\ B -> C.
Proof.
Abort.

Proposition pn :
  forall A B C : Prop,
    (A /\ (B /\ C)) -> (A /\ B) /\ C.
Proof.
Abort.

(* ********** *)

(* end of week-03_exercises.v *)