Curry and uncurry

The fourth wall: You look thoughtful.

Pablito: I am. Why is the induction principle for Peano numbers stated with an arrow and read with a conjunction?

The fourth wall: Pray elaborate.

Pablito: Here is how it is stated, look:

forall P : nat -> Prop,
  P 0 ->
  (forall n' : nat, P n' -> P (S n')) ->
  forall n : nat,
    P n.

The fourth wall: Yes.

Pablito: And here is how it is read:

forall P : nat -> Prop,
  P 0 /\ (forall n' : nat, P n' -> P (S n')) ->
  forall n : nat,
    P n.

The fourth wall: Ah, you mean “if the base case holds then if the induction step holds” vs. “if the base case holds and if the induction step holds”?

Pablito: Yes, precisely.

The fourth wall: That would be because of the curry-uncurry isomorphism.

Pablito: Could you elaborate?

The fourth wall: Certainly. Remember these two propositions, in the exercise about propositions from Week 02:

Proposition currying :
  forall A B C : Prop,
    (A /\ B -> C) -> (A -> B -> C).

Proposition uncurrying :
  forall A B C : Prop,
    (A -> B -> C) -> (A /\ B -> C).

Pablito: Yes. I even remember their proofs:

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.

The fourth wall: Well, the form A -> B -> C is said to be “curried”, and the form A /\ B -> C is said to be “uncurried”.

Pablito: OK.

The fourth wall: And these two forms are equivalent. Behold the curry-uncurry isomorphism:

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.

Pablito: OK. And so?

The fourth wall: Just a second. Remember the two types, in the exercise about types from Week 02:

Definition curry (A B C : Type) (uf : A * B -> C) : A -> B -> C :=
  ...

Definition uncurry (A B C : Type) (cf : A -> B -> C) : A * B -> C :=
  ...

Pablito: Yes. I even remember their definienses:

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.

The fourth wall: Well, the form A -> B -> C is said to be “curried”, and the form A * B -> C is said to be “uncurried”.

Pablito: OK.

The fourth wall: And these two forms are equivalent, look:

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.

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).

Pablito: OK, I buy that – the two proofs are the same:

Proof.
  intros A B C f a b.
  unfold uncurry, curry.
  reflexivity.
Qed.

The fourth wall: Almost, yes. In actuality, the proof of curry_is_a_left_inverse_of_uncurry is:

fun (A B C : Type) (cf : A -> B -> C) (a : A) (b : B) => eq_refl

The fourth wall: ..whereas the proof of uncurry_is_a_left_inverse_of_curry is:

fun (A B C : Type) (uf : A * B -> C) (a : A) (b : B) => eq_refl

Pablito: OK, OK. And I do understand that proofs are programs. Oh. You mean I should look at the proofs of the currying theorem and of the uncurrying theorem?

The fourth wall: That would not be a waste of time, but let’s move forward and look at the uncurried version of nat_ind:

Lemma uncurried_nat_ind :
  forall P : nat -> Prop,
    P 0 /\ (forall n' : nat, P n' -> P (S n')) ->
    forall n : nat,
      P n.

Pablito: Let me prove it:

intros P [base_case induction_step] n.
induction n as [ | n' IHn'].
- exact base_case.
- exact (induction_step n' IHn').

Pablito: ...which was a piece of cake.

The fourth wall: So much a piece of cake that you could state this proof using nat_ind, no?

Pablito: Let me see. Ah, yes:

Restart.

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

The fourth wall: Now let’s look at the curried version of nat_ind:

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

Pablito: This one is totally simple to prove, because it literally is nat_ind:

Proof.
  exact nat_ind.

The fourth wall: Indeed it is. But can you indulge me and prove it, say, using uncurried_nat_ind?

Pablito: Let me see. Ah, yes:

Restart.

intros P base_case induction_step n.
exact (uncurried_nat_ind P (conj base_case induction_step) n).

The fourth wall: Good. Now for your initial point:

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).

Pablito: Yes, that was my point, and you are saying that for any given P, the uncurried version and the curried version of nat_ind are equivalent?

The fourth wall: Yes. And that is a corollary of the curry-uncurry isomorphism:

Proof.
  intro P.
  exact (curry_and_uncurry (P 0) (forall n' : nat, P n' -> P (S n')) (forall n : nat, P n)).
Qed.

Resources

• The code for the present lecture note (latest version: 14 Apr 2024).

Version

Created [14 Apr 2024]