# Library extraction

# Extracting programs from proofs

# Ackermann relation

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!

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.

Admitted.

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.

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.

Admitted.

We can now extract something interesting from the totality proof.

Extraction ack_total_sig.

# Ackermann function

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.

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.

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.

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

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.

Admitted.