Church's arithmetic in Coq

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.

# Equality as a defined notion of Higher-Order Logic

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,
prove the usual properties of equality stated in `church.v`.

# Representing natural numbers, addition and multiplication

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 `f`, `n` times over `x`.

The (simple) type of natural numbers is therefore `a->(a->a)->a`, which is parameterised by the type `a` of the argument `x`. We abbreviate this type by `natT a`.

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 `f`, `0` times over `x`, in other words, producing `x`.
Look at the corresponding representation of 0 in `church.v`.

Now look at the definition of successor, addition, and multiplication.

Prove Peano's axioms about addition and multiplication.

# Induction

Other axioms of Peano's arithmetic are missing. An important one is the induction principle, which states that every hereditary property is true of every natural number.

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 `church.v`

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 `Nat a`.

Prove that they do, by providing proofs of the next two theorems in `church.v`

Now prove the induction principle.

# Missing axioms of Peano's arithmetic

Another axiom that is missing is the fact that 0 is the successor of noone.

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 `church.v`).

`Prop` itself is such a type.
Prove it (it can be useful to consider `True` and `not True`).

Now prove that for such a type, 0 is the successor of noone.

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.

# For the road

We provide a way to convert Coq's in-built numerals into Church's.

Prove the theorem `35*67=3015` represented in Church's arithmetic. The proof has to hold in one command.

If you have time, prove the last theorem.