# Extracting programs from proofs

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

Require Extraction.

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

Inductive ack : nat nat nat Prop :=
| ack_m_O : n, ack O n (S n)
| ack_n_O : m r, ack m (S O) r ack (S m) O r
| ack_m_n : m n r r',
ack (S m) n r ack m r r' ack (S m) (S n) r'.

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

Lemma ack_total : m n, r, ack m n r.
Proof.
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.

Extraction ack_total.

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.

Print ex.

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.

Check { r : nat | ack 2 3 r }.
Print sig.

Let us prove totality using sig.

Lemma ack_total_sig : m n, { r | ack m n r }.
Proof.
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.

Extraction ack_total_sig.

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

Fixpoint addition (m:nat) (n:nat) : nat :=
match m with
| On
| S m'S (addition m' n)
end.

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.

Fixpoint fack' (fack_m : natnat) (n:nat) : nat := match n with
| O ⇒ 12
| S n' ⇒ 3456
end.

Now define fack to be Ackermann's function.

Fixpoint fack (m:nat) (n:nat) : nat.

Prove that fack implements the Ackermann specification.

Lemma fack_correct : m n, ack m n (fack m n).

This yields a new proof of totality.

Lemma ack_total_fun : m n, { r | ack m n r }.
Proof.
intros. (fack m n). apply fack_correct.
Defined.

Recursive Extraction ack_total_fun.

Let's compute some values of the function.

Lemma ack_3_3 : { x : nat | ack 3 3 x }.
Proof.
apply ack_total_fun.
Defined.

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

Recursive Extraction ack_3_3.

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

Eval compute in fack 3 3.

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

Eval compute in ack_total_fun 3 3.
Eval compute in let (x,_) := ack_total_fun 3 3 in x.
Eval compute in let (x,_) := ack_total_sig 3 3 in x.

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

Check ack_ind.

Lemma ack_unicity : m n r1,
ack m n r1 r2, ack m n r2 r1 = r2.
Proof.
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.