The exercise about types and the exercise about propositions offer a lot to reflect about.
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.
And incidentally, when a match-expression has only one branch, it can be written as a deconstructing let-expression:
Definition uncurry' (A B C : Type) (g : A -> B -> C) (p : A * B) : C :=
let (a, b) := p
in g a b.
At any rate, we now know enough to prove that curry and uncurry are inverses of each other, using the unfold tactic to replace the names curry and uncurry by their denotation and inline their definitions:
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.
And 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).
In Gallina, as in OCaml, functions are curried by default. For example, the resident addition function, Nat.add, has type nat -> nat -> nat. So when we apply it to a given number, the result is another function that we then apply to a second given number, and then the result is a third number that is the sum of the two given numbers.
Having curried functions is a language-design choice. For another choice, in Lisp and in Scheme for example, functions are uncurried by default.
Consider the modus ponens. Informally, we write it as the following induction rule where A and B denote propositions:
| MODUS-PONENS | A | A -> B | |
| B | |||
We read this rule as “if A holds and if A -> B holds, then B holds.
And we can formalize this rule either in an uncurried way, i.e., using a conjunction, or in a curried way, i.e., using an implication:
Proposition uncurried_modus_ponens :
forall A B : Prop,
A /\ (A -> B) -> B.
Proposition curried_modus_ponens :
forall A B : Prop,
A -> (A -> B) -> B.
This choice does not matter because the two are equivalent:
Theorem equivalence_of_the_two_modus_ponenses :
forall A B : Prop,
(A /\ (A -> B) -> B) <-> (A -> (A -> B) -> B).
Consider mathematical induction. In tCPA, it is formalized as structural induction over Peano numbers, where P denotes a function mapping a Peano number to a proposition:
| IND | P O | forall n' : nat, P n' -> P (S n') | |
| forall n : nat, P n | |||
We read this rule as “if the base case hold and if the induction step holds, then the conclusion holds”.
And we can formalize this rule either in an uncurried way, i.e., using a conjunction, or in a curried way, i.e., using an implication:
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.
This choice does not matter because the two are equivalent:
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).
In tCPA, the choice is that the resident induction principle for nat, i.e., nat_ind, is curried:
nat_ind
: forall P : nat -> Prop, P 0 -> (forall n : nat, P n -> P (S n)) -> forall n : nat, P n
At any point during a proof, we can type:
Show Proof.
TCPA then unparses the proof tree that we have constructed so far into the syntax of a Gallina expression, exploiting the Curry-Howard isomorphism between proofs and programs. This feature can be fruitfully used when revisiting the fourteen propositions in need of a proof in Week 03.
For example, consider the modus ponens:
Theorem modus_ponens :
forall A B C : Prop,
A -> (A -> B) -> B.
Proof.
intros A B C.
intros H_A H_A_implies_B.
apply H_A_implies_B.
exact H_A.
Show Proof.
The *response* window then contains the following Gallina expression that represents the proof of Theorem modus ponens:
(fun (A B _ : Prop) (H_A : A) (H_A_implies_B : A -> B) => H_A_implies_B H_A)
And indeed the proof rule associated to the intro tactic coincides with the program rule associated to function abstractions, and the proof rule associated to the apply tactic coincides with the program rule associated to applications.
But let us re-do the proof of Theorem modus_ponens with simpler names:
Restart. (* with simpler names *)
intros A B C.
intros a f.
exact (f a).
Show Proof.
The *response* window then contains the following Gallina expression:
(fun (A B _ : Prop) (a : A) (f : A -> B) => f a)
The point of writing Theorem is that it makes tCPA shift into proof mode, to be exited when we write Qed, Admitted, or Abort. Here – now that we know the proof of Theorem modus_ponens – we can directly declare a name, modus_ponens_as_a_definition, whose type is forall A B C : Prop, A -> (A -> B) -> B and whose denotation is fun (A B _ : Prop) (a : A) (f : A -> B) => f a:
Definition modus_ponens_as_a_definition : forall A B C : Prop, A -> (A -> B) -> B :=
(fun (A B _ : Prop) (a : A) (f : A -> B) => f a).
And in tCPA, the type and the proposition are represented in the same way, and the Gallina function and the proof are also represented in the same way, which is totally awesome.
In fact, we can use the exact tactic to supply the proof by giving it the Gallina representation of the proof:
Theorem modus_ponens_revisited :
forall A B C : Prop,
A -> (A -> B) -> B.
Proof.
exact (fun (A B _ : Prop) (a : A) (f : A -> B) => f a).
Qed.
And if we use the tCPA Print, namely:
Print modus_ponens.
Print modus_ponens_as_a_definition.
Print modus_ponens_revisited.
the result is the same (modulo the three names):
modus_ponens =
fun (A B _ : Prop) (a : A) (f : A -> B) => f a
: forall A B : Prop, Prop -> A -> (A -> B) -> B
modus_ponens_as_a_definition =
fun (A B _ : Prop) (a : A) (f : A -> B) => f a
: forall A B : Prop, Prop -> A -> (A -> B) -> B
modus_ponens_revisited =
fun (A B _ : Prop) (a : A) (f : A -> B) => f a
: forall A B : Prop, Prop -> A -> (A -> B) -> B
which illustrates
The logical question: Why do we even have a language of tactics when we can directly write proofs as programs?
The pragmatic answer: Because the said programs get really complicated really quick. Against this backdrop, the language of tactics was designed to account for the way informal proofs are written.
Added Section The Coq Proof Assistant in essence and Section A logical question and a pragmatic answer [15 Feb 2025]
Created [07 Feb 2025]