# Library mtac_tutorial

# Tutorial for Mtac.

# Introduction

*maybe*A, so, for instance, a function of type T nat

*may*return a natural number. It can also fail or loop forever, but it can never produce a value of a different type (that is, it is sound). We call functions of type T A

*Mtactics*, to distinguish them from the usual tactics provided by Coq.

*exactly the same*. These new features are:

- Exceptions,
- Unbounded fixpoints,
- Unification match,
- Fresh name generation.

# Simple examples

Require Import mtac.

In addition, we import a couple of modules from the standard
library that we are going to use in some examples.

Require Import Arith.Arith Arith.Div2.

Require Import Lists.List.

Require Import Strings.String.

Set Implicit Arguments.

Notation "x == y" := (beq_nat x y) (at level 60).

We start by showing the standard

*unit*and*bind*operators, which in our language are called ret (for return) and bind. The language also defines the standard notation x <- a; b for bind. This example computes the value 1 by passing the result of computing 0 to the successor.
We check the type of the definition. It has type T nat.

Let's execute it using the new keyword run and print the
result.

The result should be the_value = 1 : nat. As you can see,
run produces_a_value was replaced by the effect of computing the
code in produces_a_value. Mathematically, run is a partial
function from type T A to type A.

## Exceptions

The monad includes exceptions, like the following silly example illustrates. Exceptions are constructed with the constructor exception. In order to make distinguishable exceptions we make them opaque, sealing the definition with the Qed word.Definition AnException : Exception.

exact exception.

Qed.

Definition MyException (s : string) : Exception.

exact exception.

Qed.

Note how they are equal to exception, but we can still
differentiate them.

Definition test_ex e :=

mtry raise e

with

| AnException => ret ""%string

| MyException "hello"%string => ret "world"%string

| [s] MyException s => ret s

end.

Definition empty_string := run test_ex AnException.

Definition world_string := run test_ex (MyException "hello"%string).

Definition other_string := run test_ex (MyException "other"%string).

Print empty_string.

Print world_string.

Print other_string.

Results should be the empty string, the string "world" and the
string "other" respectively.
If an exception is not caught, then we get a meaningful error.
The Fail command below will show the exception thrown by the code:

## Unbounded fixpoints

Notice the notation we used for the arguments: we delimit them
using square brackets. Also, in this definition we decided to add the
type annotation T False, since otherwise it is impossible for the
type inference mechanism to guess the type. It is important to note
that the body of mfix should always be of type T.
Uncomment the code below and execute it: it will loop forever! You
will have to interrupt the proof assistant (C-c C-c in Emacs).
Check (run (endless_loop 0)).
The key to understanding why it is perfectly safe to allow for
such effects is to notice that run is not a function living in the
kernel typechecker of Coq. That is, for t of type T A, run t
constructs a witness for A only if it's safe to do so, but
As an exercise, we can try to break soundness of Coq by constructing an
element of type False without any further hypothesis. Take the
function endless_loop above, which has type nat -> T False. To
get an element of type False we have to execute it through run as
in the commented code. Since it will not terminate, run
(endless_loop 0) doesn't produce an offending witness.
To show the use of this unbounded fixpoint we define a function
computing the Collatz
sequence, which cannot be defined in vanilla Coq since its
termination is a conjecture.

### Endless loop... Is it still safe?

*it itself is not a witness for A*. Take as example the definitions we constructed so far: we used run but when we printed them we saw no run in their proof terms.### Constructing Collatz sequences

Definition collatz :=

mfix f [n] :=

let rest :=

if n == 1 then

ret nil

else if is_even n then

f (div2 n)

else

f (3 * n + 1)

in

s <- rest;

ret (n :: s).

We try it with the value 6.

Result: (6 :: 3 :: 10 :: 5 :: 16 :: 8 :: 4 :: 2 :: 1 :: nil) : list nat
Mtac provides a powerful new construct: the unification
match. Unlike the native Coq pattern matching, the unification match
let us specify any term as a pattern, even patterns containing
variables bound in the context.
For instance, the code below shows a function that searches for an
element in a list.

## Unification match

Definition NotFound : Exception.

exact exception.

Qed.

Definition inlist A (x : A) :=

mfix f [s : list A] :=

mmatch s as s' return T (In x s') with

| [s'] (x :: s') => ret (in_eq _ _)

| [y s'] (y :: s') =>

r <- f s';

ret (in_cons y _ _ r)

| _ => raise NotFound

end.

Check inlist.

We also depart from the standard notation for patterns: since they
may now refer to variables in the context, we need to specify a list
of pattern variables, like [s'] in the first pattern. All the
variables not included in this list should be bound by the context,
like x in the same pattern, which is bound to the argument of the
definition. That is, this pattern matches a list containing the
element x in the head.
So far we have constructed the proof terms directly, without using
the interactive mode of Coq. We can use any standard tactic (apply,
refine, exact, set, ...) with run, although not all of them
are suitable if we want to avoid writing inferable arguments. For
instance, if we have to prove a goal of the form In x s for some
list s and some element x, then we would like to use run (inlist
_ _), that is, without specifying the arguments. This will help us
build more robust proof scripts, since tomorrow we may replace x by
some other element in the list and still get a valid proof script. In
order to avoid writing the arguments, we use the tactic refine,
which provides run with the goal to prove, unlike apply, as the
following examples show:

Example x_in_zyx (x y z : nat) : In x (z :: y :: x :: nil).

Proof.

refine (run (inlist _ _)).

Qed.

Example y_in_zyx (x y z : nat) : In y (z :: y :: x :: nil).

Proof.

Fail apply (run (inlist _ (z :: y :: x :: nil))).

Abort.

Fail above shows that indeed it has failed to apply the Mtactic.
Of course, we can always provide the proof term directly instead
of going into interactive mode. In this case we don't need to
explicitly provide the arguments.

Ssreflect[5] users can use the apply: tactic, which is better
than refine. An alternative is to use eval, which is similar to
run, except that it performs the execution of the Mtactic after the
type inference mechanism of Coq has done its job:

### Interaction with Program

Program

Definition inlist' A (x : A) :=

mfix f [s : list A] :=

mmatch s as s' return T (In x s') with

| [l r] l ++ r =>

mtry

il <- f l;

ret _

with _ =>

ir <- f r;

ret _

end

| [s'] (x :: s') => ret (in_eq _ _)

| [y s'] (y :: s') =>

r <- f s';

ret (in_cons y _ _ r)

| _ => raise NotFound

end.

Next Obligation.

intros A x _ _ l r H.

apply in_or_app.

left; exact H.

Qed.

Next Obligation.

intros A x _ _ l r _ _ H.

apply in_or_app.

right; exact H.

Qed.

If the list is a concatenation of two lists l and r, we first
try to search for the element on l and, if it fails, on r. Notice
that the pattern is not a constructor, but the application of the
function ++ to two lists. As mentioned before, we can use
One problem with Program is that it generates big proof terms.
Let's look at the proof terms generated in the obligations and plug
those terms into the holes.

*any*Coq term as a pattern! It is important to make this case the first case of the match, as the unification of the scrutinee with the pattern takes into account beta delta iota zeta reductions. That is, if the concatenation case were put third in the match, then the list (x :: nil) ++ (z :: nil) will be matched against the pattern (x :: s'), by reducing it to (x :: z :: nil).Print inlist'_obligation_1.

Print inlist'_obligation_2.

The important bits are in_or_app l r x (or_introl H) and
in_or_app l r x (or_intror H). We write our function again filling
in the holes with these two terms.

Definition inlist'' A (x : A) :=

mfix f [s : list A] :=

mmatch s as s' return T (In x s') with

| [l r] l ++ r =>

mtry

il <- f l;

ret (in_or_app l r x (or_introl il))

with _ =>

ir <- f r;

ret (in_or_app l r x (or_intror ir))

end

| [s'] (x :: s') => ret (in_eq _ _)

| [y s'] (y :: s') =>

r <- f s';

ret (in_cons y _ _ r)

| _ => raise NotFound

end.

Let's prove an example using the three functions just created to
compare the proof terms they generate.

Example ex_inlist (x y z : nat) : In x ((y :: z :: nil)++(x :: z :: nil)).

Proof.

refine (run (inlist _ _)).

Qed.

Example ex_inlist' (x y z : nat) : In x ((y :: z :: nil)++(x :: z :: nil)).

Proof.

refine (run (inlist' _ _)).

Qed.

Example ex_inlist'' (x y z : nat) : In x ((y :: z :: nil)++(x :: z :: nil)).

Proof.

refine (run (inlist'' _ _)).

Qed.

Print ex_inlist.

Print ex_inlist'.

Print ex_inlist''.

Inspect the result. The last example has the shortest proof term.
We show by example some useful constructs for dealing with Higher
Order Abstract Syntax (HOAS). As the driving example we will write a
rudimentary tautology prover similar to that found in VeriML [1] and
CPDT [2]. Compared to VeriML, our approach has the benefit that it
doesn't require any special context treatment, since for us a context is
nothing more than a Coq list. And unlike in the Ltac version
presented in [2], we have meaningful types to prevent ourselves from
shooting ourselves in the foot.
We start with a very simple propositional prover. It considers
only three cases:

# A simple tautology prover

## Warming the engine: a simple propositional prover

- The proposition is True. In this case, it returns the trivial proof I.
- The proposition is a conjunction of p1 and p2. In this case, it proves both propositions and returns the introduction form of the conjunction.
- The proposition is a disjunction of p1 and p2. In this case, it tries to prove the proposition p1, and if it fails it tries to prove the proposition p2. The corresponding introduction form of the disjunction is returned.
- In any other case, it raises an exception, since no proof could be found.

Definition simpl_prop_auto :=

mfix f [p : Prop] : T p :=

mmatch p with

| True => ret I

| [ p1 p2 ] p1 /\ p2 =>

r1 <- f p1 ;

r2 <- f p2 ;

ret (conj r1 r2)

| [p1 p2] p1 \/ p2 =>

mtry

r1 <- f p1 ;

ret (or_introl r1)

with _ =>

r2 <- f p2 ;

ret (or_intror r2)

end

| _ => raise NotFound

end.

Given this definition we can easily discharge the following example.

The proof term is exactly what we would have written by hand:
ex1 = conj I (or_intror I)
Our previous function is very limited since it cannot prove
tautologies as simple as P -> P. To handle implications we need a
list of hypotheses where we can search for a proof of the atom we are
considering. We create a record type containing a proposition and a
witness for the proposition.

## Adding a context

We will need to search a list of dyns to find a witness for some
proposition. The search function below is similar to the inlist above,
but keying on the prop projector of the record. We have to prepend Program
because it calls a more agressive typechecker, otherwise it fails to notice
that the element in the body of the first case should return a P.

Program

Definition search (P : Prop) :=

mfix f [s:list dyn] : T P :=

mmatch s with

| [(x:P) s'] (Dyn x) :: s' => ret x

| [d s'] d :: s' => f s'

| _ => raise NotFound

end.

The proposition in the Dyn constructor is implicit, since it can
be inferred from the element, so we write Dyn x instead of Dyn A
x.
The tautology prover takes a context c (e.g., a list of dyns)
and a proposition. The first three cases are the same as before.

Program

Definition prop_auto' :=

mfix f [c : list dyn; p : Prop] : T p :=

mmatch p as p' return T p' with

| True => ret I

| [ p1 p2 ] p1 /\ p2 =>

r1 <- f c p1 ;

r2 <- f c p2 ;

ret (conj r1 r2)

| [p1 p2] p1 \/ p2 =>

mtry

r1 <- f c p1 ;

ret (or_introl r1)

with _ =>

r2 <- f c p2 ;

ret (or_intror r2)

end

| [(p1 p2 : Prop)] p1 -> p2 =>

nu (x:p1),

r <- f (Dyn x :: c) p2;

abs x r

| [p':Prop] p' => search p' c

end.

Let's look at the new case for handling the implication. We need
to return an element of type T (p1 -> p2), that is,
ret (fun x:p1 => f (Dyn x :: c) p2)
since this code has type T (p1 -> T p2) which is not what we
want. Instead, we use two new operators: nu and abs. The first one
is analogous to the nu operator in [3] and [4].
nu has type forall A B, (A -> T B) -> T B where A and B are
left implicit. The effect of computing nu (fun x=>b), where b : T
B, is the result of executing b, replacing any occurrence of x
with a fresh
abs abstracts over parameters created by nu. It has type forall A
P (x : A), P x -> T (forall x, P x) where A and P are left
implicit. If a is a parameter created by nu and t is a term with
a appearing free in it, then abs a t is replaced by ret
(fun x=>r), where r is t with a replaced by x. That is, a
is abstracted from t.
Coming back to the implication case, we use nu to create a parameter
x as a witness for p1. Then we add it to the list of hypothesis to
prove p2 and get the result r, which may refer to x. Therefore,
we use abs x r to abstract x from the result. We encourage the
reader to check that the type of the whole expression returned in the
implication case has type T (p1 -> p2).
Finally, we changed the last case of the algorithm: instead of throwing
an error, now we search for a witness for the proposition in the list
using the search function defined before.
We create a definition to avoid passing the empty list

*maybe*a function from p1 to p2. Of course, we cannot simply write*parameter*a. If the execution results in a term ret t for some t with a not appearing free in it, then the value ret t is used as result for nu (fun x => b). Otherwise, a failure is raised. Intuitively, the idea is that it is safe to execute the body of a function as long as it doesn't get stuck (i.e., it shouldn't inspect its argument), and the returning value doesn't return the argument (i.e., it shouldn't violate the context).
We can now easily prove this tautology.

Example ex_with_implication (p q : Prop) : p -> q -> p /\ q.

Proof.

refine (run (prop_auto _)).

Qed.

Proof.

refine (run (prop_auto _)).

Qed.

Again, the proof term generated is exactly what we would expect
for such a proof.

Print ex_with_implication.

Result:
ex_with_implication = fun (p q : Prop) (H : p) (H0 : q) => conj H H0
We can generalize our algorithm very easily to deal with forall and
exists. Below is the code, where the first four cases and the last one
are the same as before.

# Getting first order

Program

Definition tauto' :=

mfix f [c : list dyn; p : Prop] : T p :=

mmatch p as p' return T p' with

| True => ret I

| [p1 p2] p1 /\ p2 =>

r1 <- f c p1 ;

r2 <- f c p2 ;

ret (conj r1 r2)

| [p1 p2] p1 \/ p2 =>

mtry

r1 <- f c p1 ;

ret (or_introl r1)

with _ =>

r2 <- f c p2 ;

ret (or_intror r2)

end

| [(p1 p2 : Prop)] p1 -> p2 =>

nu (x:p1),

r <- f (Dyn x :: c) p2;

abs x r

| [A (q:A -> Prop)] (forall x:A, q x) =>

nu (x:A),

r <- f c (q x);

abs x r

| [A (q:A -> Prop)] (exists x:A, q x) =>

X <- evar A;

r <- f c (q X) ;

b <- is_evar X;

if b then

raise NotFound

else

ret (ex_intro q X r)

| [p':Prop] p' => search p' c

end.

The forall case is similar to the implication case from before but taking
into account the following:
As before, we create a definition to avoid passing the empty list:

- The type of x is any type A, not just Prop.
- The possible dependency of x in q, the body of the forall. This dependency is marked by making q a function from A to Prop. The unification algorithm used to unify the pattern with the proposition p will take care of instantiating q with a function taking an element of type A and returning the body of the forall.
- The context is not extended.

Here is an example to test tauto:

Example ex_first_order (p q : nat -> Prop) :

forall x, p x -> q x -> exists y, p y /\ q y.

Proof.

refine (run (tauto _)).

Qed.

forall x, p x -> q x -> exists y, p y /\ q y.

Proof.

refine (run (tauto _)).

Qed.

If we cannot instantiate an existential, then an error is thrown.

Example ex_fail (p q : nat -> Prop) :

exists y, p y /\ q y.

Proof.

Fail refine (run (tauto _)).

Abort.

exists y, p y /\ q y.

Proof.

Fail refine (run (tauto _)).

Abort.

Actually, we can omit the check for the existential and let the
user come up with the witness by itself.
We mentioned brefly that with eval we can delay the execution of
the Mtactic in order to get arguments from the goal. However, one
must use it with care, as the proof term generated is bigger than with
run:

# Delayed execution via eval

Print y_in_zyx.

Note how the procedure executed inlist ... is included in the proof
term.
The function eval is particularly useful when rewriting
procedures returning equalities. Here is an example using boolean
equality of natural numbers.

Program

Definition eq_nats :=

mfix f [x : nat; y : nat] : T (x == y = true) :=

r <-

mmatch (x, y) as p return T ((x, y) = p -> x == y = true) with

| (x, x) => ret (fun H=>_)

| [x1 x2] (x1 + x2, x2 + x1) =>

ret (fun H =>_)

end;

ret (r (eq_refl _)).

Next Obligation.

intros _ x y H.

inversion H.

symmetry.

apply beq_nat_refl.

Qed.

Next Obligation.

intros _ x y x1 x2 H.

inversion H.

rewrite beq_nat_true_iff.

apply plus_comm.

Qed.

Example plus_S n m : n + m == m + n = true /\ m == m = true /\ n == n = true.

Proof.

rewrite !(eval (eq_nats _ _)).

auto.

Qed.