Extracting programs from proofs

In this tutorial we will extract programs from simple proofs on natural numbers.

Ackermann relation

We define a relation ack : nat → nat → nat → Prop which is the specification of Ackermann's function: ack m n r means that the result of the function on m and n should be r.

Let us prove that the relation is total. Be careful to start your argument correctly, it is not straightforward!

In this proof you may find it useful to choose names when destructing an existential, using destruct ... as (x,H). You can also use assumption instead of explicitly using exact H when the conclusion of the goal is one of its hypotheses.

Ask Coq to extract a program from the proof ack_total. The result is disappointing: it is because the computational content of objects in Prop is erased.

The expression ∃ x:A, P x is a notation for ex A P. The type ex is defined inductively: its inhabitants (i.e. proofs of existential statements) can only be derived using ex_intro, i.e. by providing a witness x and a proof of P x.

Coq comes with a variant of ex called sig that defines existential quantification in Type rather than Prop. The expression {x : A | P x} is a notation for sig A P.

Let us prove totality using sig.

The following won't be allowed: intros. destruct (ack_total m n). Indeed we cannot use the computationally meaningless ack_total to define the computationally meaningful ack_total_sig. However, copying the proof script of ack_total should work. In particular, destruct works similarly on ex and sig. At the end, use Defined rather than Qed to avoid warnings: this informs Coq that we care about the proof contents, and not only about the fact that the statement is provable.

We can now extract something interesting from the totality proof.

Ackermann function

We have extracted Ackermann's function from a proof of totality of the Ackermann relation. It is also possible (and often convenient) to define the function explicitly in Coq. The function will essentially be defined by induction over natural numbers. Concretely, we will form a Fixpoint definition: it allows to define a recursive function as long as some argument strictly decreases in these calls, so that termination is ensured. Here, "decreasing" must be obvious: the new argument must be a strict subterm of the (finite) initial argument. For example, in the following (re)definition of the addition function, the decreasing argument is the first one: the only recursive call is one a strict subterm m' of m.

First define fack' such that, if fack_m is Ackermann's function with a first argument fixed to m, then fack' fack_m n is the result of Ackermann's function for S m and n.

Now define fack to be Ackermann's function.

Prove that fack implements the Ackermann specification.

This yields a new proof of totality.

Let's compute some values of the function.

Extraction gives us a program that we could run in OCaml.

But since we have a Coq function we can also directly evaluate it.

We can also unwrap this result from the sig type of one of our existence proofs.

Induction over a relation

So far we have not used the fact that ack is given as an Inductive definition. We will use it to prove unicity next: because ack is inductive, you have an induction scheme for it, that you can use through the induction tactic: if H : ack m n r try using induction H.

Do NOT use inductions on m and n: induct on ack m n r directly. Be careful: the ∀ r2 comes late in the formula for a reason.