(* week-04_warmup.v *)
(* LPP 2025 - CS3234 2024-2025, Sem2 *)
(* Olivier Danvy <olivier@comp.nus.edu.sg> *)
(* Version of 07 Feb 2025 *)

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

Definition curry (A B C : Type) (f : A * B -> C) (a : A) (b : B) : C :=
  f (a, b).

Definition uncurry (A B C : Type) (g : A -> B -> C) (p : A * B) : C :=
  match p with
    (a, b) =>
    g a b
  end.

Definition uncurry' (A B C : Type) (g : A -> B -> C) (p : A * B) : C :=
  let (a, b) := p
  in g a b.

Proposition uncurry_is_a_left_inverse_of_curry :
  forall (A B C : Type)
         (f : A * B -> C)
         (a : A)
         (b : B),
    uncurry A B C (curry A B C f) (a, b) = f (a, b).
Proof.
Abort.

Proposition curry_is_a_left_inverse_of_uncurry :
  forall (A B C : Type)
         (g : A -> B -> C)
         (a : A)
         (b : B),
    curry A B C (uncurry A B C g) a b = g a b.
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 pl_and_pm :
  forall A B C : Prop,
    (A -> B -> C) <-> (A /\ B -> C).
Proof.
Abort.

(* ***** *)

Check Nat.add.

Check (Nat.add 2).

Check (Nat.add 2 3).

(* ***** *)

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

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

Theorem equivalence_of_the_two_modus_ponenses :
  forall A B : Prop,
    (A /\ (A -> B) -> B) <-> (A -> (A -> B) -> B).
Proof.
Abort.

(* ***** *)

Definition uncurried_induction_principle_for_nat : Prop :=
  forall P : nat -> Prop,
    P O /\ (forall n' : nat, P n' -> P (S n')) ->
    forall n : nat,
      P n.

Definition curried_induction_principle_for_nat : Prop :=
  forall P : nat -> Prop,
    P O ->
    (forall n' : nat, P n' -> P (S n')) ->
    forall n : nat,
      P n.

Theorem equivalence_of_the_two_induction_principles :
  forall P : nat -> Prop,
    (P O /\ (forall n' : nat, P n' -> P (S n')) ->
    forall n : nat,
      P n)
    <->
    (P O ->
    (forall n' : nat, P n' -> P (S n')) ->
    forall n : nat,
      P n).
Proof.
Abort.  

Check nat_ind.
(*
nat_ind
     : forall P : nat -> Prop, P 0 -> (forall n : nat, P n -> P (S n)) -> forall n : nat, P n
*)

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

(* end of week-04_warmup.v *)