Warmup

The exercise about types and the exercise about proposition offer a lot to reflect about.

Currying and uncurrying are inverses of each other

Among the 14 types in search of a term of that type, in the Exercise about types from last week, one could find the type of the curry function and of the uncurry function:

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.

We now know enough to prove that they are inverses of each other:

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

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.

The propositions that correspond to these types could be found in the Exercise about propositions from last week:

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

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

Logically, the inverseness of curry and uncurry corresponds to the following equivalence:

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

Resources

• The Gallina code for the present lecture note (latest version: 01 Feb 2024).

Version

Created [01 Feb 2024]