(* week-11_curry-and-uncurry.v *)
(* LPP 2025 - CS3234 2024-2025, Sem2 *)
(* Olivier Danvy <olivier@comp.nus.edu.sg> *)
(* Version of 04 Apr 2025 *)

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

(* Propositions: *)

Proposition currying :
  forall A B C : Prop,
    (A /\ B -> C) -> (A -> B -> C).
Proof.
  intros A B C H H_A H_B.
  exact (H (conj H_A H_B)).
Qed.

Proposition uncurrying :
  forall A B C : Prop,
    (A -> B -> C) -> (A /\ B -> C).
Proof.
  intros A B C H [H_A H_B].
  exact (H H_A H_B).
Qed.

Theorem curry_and_uncurry :
  forall A B C : Prop,
    (A /\ B -> C) <-> (A -> B -> C).
Proof.
  intros A B C.
  split.
  - exact (currying A B C).
  - exact (uncurrying A B C).
Qed.

(* ***** *)

(* Types: *)

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

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

Proposition curry_is_a_left_inverse_of_uncurry :
  forall (A B C : Type)
         (cf : A -> B -> C)
         (a : A)
         (b : B),
    curry A B C (uncurry A B C cf) a b = cf a b.
Proof.
  intros A B C cf a b.
  unfold uncurry, curry.
  reflexivity.
  Show Proof.
(*
  (fun (A B C : Type) (cf : A -> B -> C) (a : A) (b : B) => eq_refl)
*)
Qed.

Proposition uncurry_is_a_left_inverse_of_curry :
  forall (A B C : Type)
         (uf : A * B -> C)
         (a : A)
         (b : B),
    uncurry A B C (curry A B C uf) (a, b) = uf (a, b).
Proof.
  intros A B C uf a b.
  unfold curry, uncurry.
  reflexivity.
  Show Proof.
(*
  (fun (A B C : Type) (uf : A * B -> C) (a : A) (b : B) => eq_refl)
*)
Qed.

(* ***** *)

(* Propositions, revisited: *)

Theorem currying_revisited :
  forall A B C : Prop,
    (A /\ B -> C) -> (A -> B -> C).
Proof.
  intros A B C H H_A H_B.
  exact (H (conj H_A H_B)).
  Show Proof.
(*
  (fun (A B C : Prop) (H : A /\ B -> C) (H_A : A) (H_B : B) => H (conj H_A H_B))
 *)

  Restart.

  intros A B C uf a b.
  exact (uf (conj a b)).
  Show Proof.
(*
  (fun (A B C : Prop) (uf : A /\ B -> C) (a : A) (b : B) => uf (conj a b))
 *)

  Restart.

  exact (fun (A B C : Prop) (uf : A /\ B -> C) (a : A) (b : B) => uf (conj a b)).
Qed.

Theorem uncurrying_revisited :
  forall A B C : Prop,
    (A -> B -> C) -> (A /\ B -> C).
Proof.
  intros A B C H [H_A H_B].
  exact (H H_A H_B).
  Show Proof.
(*
  (fun (A B C : Prop) (H : A -> B -> C) (H0 : A /\ B) =>
     match H0 with
     | conj H_A H_B => H H_A H_B
     end)
 *)

  Restart.

  intros A B C H P.
  destruct P as [H_A H_B].
  exact (H H_A H_B).
  Show Proof.
(*
  (fun (A B C : Prop) (H : A -> B -> C) (P : A /\ B) =>
     match P with
     | conj H_A H_B => H H_A H_B
     end)
 *)

  Restart.

  intros A B C uf p.
  destruct p as [a b].
  exact (uf a b).
  Show Proof.
(*
  (fun (A B C : Prop) (uf : A -> B -> C) (p : A /\ B) =>
   match p with
   | conj a b => uf a b
   end)
 *)

  Restart.

  exact (fun (A B C : Prop) (uf : A -> B -> C) (p : A /\ B) =>
           match p with
           | conj a b => uf a b
           end).
Qed.

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

Lemma uncurried_nat_ind :
  forall P : nat -> Prop,
    P 0 /\ (forall n' : nat, P n' -> P (S n')) ->
    forall n : nat,
      P n.
Proof.
  intros P [base_case induction_step] n.
  induction n as [ | n' IHn'].
  - exact base_case.
  - exact (induction_step n' IHn').

  Restart.

  intros P [base_case induction_step] n.
  exact (nat_ind P base_case induction_step n).
Qed.

Lemma curried_nat_ind :
  forall P : nat -> Prop,
    P 0 ->
    (forall n' : nat, P n' -> P (S n')) ->
    forall n : nat,
      P n.
Proof.
  exact nat_ind.

  Restart.

  intros P base_case induction_step n.
  exact (uncurried_nat_ind P (conj base_case induction_step) n).
Qed.
  
Proposition curried_nat_ind_and_uncurried_nat_ind :
  forall P : nat -> Prop,
    (P 0 /\ (forall n' : nat, P n' -> P (S n')) -> forall n : nat, P n)
    <->
    (P 0 -> (forall n' : nat, P n' -> P (S n')) -> forall n : nat, P n).
Proof.
  intro P.
  exact (curry_and_uncurry (P 0) (forall n' : nat, P n' -> P (S n')) (forall n : nat, P n)).
Qed.

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

(* end of week-11_curry-and-uncurry.v *)