In your crash course on Coq, you have seen that Coq can do predicate logic.
You have also seen that, on top of this, the logic of Coq has the theory of equality and Peano's arithmetic built-in.
When those theories are encoded in predicate logic as in your INF412 course notes, the proof of
45*67=3015 is huge.
And this is the case, whether we do it directly with Peano's axioms, or indirectly in a stronger theory of predicate logic such as set theory (ZF) -as you have seen in lectures.
Church's theory of simple types, today known as Higher-Order Logic, addresses this issue, incorporating direct computations (of e.g.
45*67) into the logic, so that the proof of
45*67=3015 only takes a couple of steps.
The logic of Coq is an extension of Higher-Order Logic, but equality and natural numbers in Coq are not encoded the way Church suggested.
In this practical, we forget about Coq's in-built equality and natural numbers, to come back to Church's original presentation of arithmetic in Higher-Order Logic.
Open the file
church.v in Proof General.
Higher-Order Logic allows you to quantify over predicates, so that equality on type
a can be defined according to Leibniz's principle, rather than assumed axiomatically (as you do in predicate logic).
Using the definition provided,
Church's trick to represent natural numbers in higher-order logic can be illustrated by saying that the number 3 is the concept of re-iterating three times a function f over an argument x.
More generally, a number
n is represented as a function taking as arguments an element
x and a function
f, and producing the element obtained by applying
n times over
The (simple) type of natural numbers is therefore
a->(a->a)->a, which is parameterised by the type
a of the argument
We abbreviate this type by
Similarly, the number 0 (is represented by the function that) takes as arguments an element
x and a function
f, and produces the element obtained by applying
0 times over
x, in other words, producing
Look at the corresponding representation of 0 in
Now look at the definition of successor, addition, and multiplication.
To force it to hold, Church's trick is simply to restrict the notion of natural numbers to those inhabitant of
natT a that satisfy every hereditary property.
Look at the corresponding definition of
Nat a in
Now every statement of the form "for all natural number n,..." will be represented by
forall n, Nat a n ->...
Conversely, every statement of the form "there exists a natural n such that..." will be represented by
exists n, Nat a n /\...
Of course, we should check that the natural numbers we can write do satisfy
This cannot be proved for every kind of Church's numerals, but it can be proved for Church's numerals over a type
a that has two distinct inhabitants (a property defined as
two a in
Prop itself is such a type.
Finally, the last missing axiom is the injectivity of successor.
There is no trick to enforce it, the only way to have it in Higher-Order Logic (at least with Church's numerals) is to assume it as an axiom (this is what we do in predicate logic anyway, and in set theory the injectivity of successor is the consequence of other axioms...)
This is what motivated the development of Coq on an extension of Higher-Order Logic with inductive types, which have all of these properties built-in.
35*67=3015 represented in Church's arithmetic. The proof has to hold in one command.
If you have time,