Author: Beta Ziliani
Use Alt-N/P to move back and forward, Alt-Enter go to the point. F8 or the start button will toggle the panel.
Mtac is a typechecked language for proof automation. It consists of a monadic type M A for a type A, which is interpreted via the new operator Mrun. The best way of understanding the type M A is as maybe A, so, for instance, a function of type M 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 M A Mtactics, to distinguish them from the usual tactics provided by Coq.
One of the key aspects of Mtac is that it subsumes Gallina, the language of Coq, and it inherits from Coq the beta delta iota zeta reduction rules. This makes programming tactics very pleasant, since developers only need to learn the new features and their semantics, since the rest is exactly the same. These new features are:
In this tutorial we illustrate some of these features, building up from simple examples. In order to execute the code in this file you will need to install Mtac's plugin. For details on how to do that, follow the link: Mtac home page
To begin working with the new language we need to import the M type.
In addition, we import a couple of modules from the standard library that we are going to use in some examples.
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 M nat.
Let's execute it using the new keyword Mrun and print the result.
The result should be the_value = 1 : nat. As you can see, Mrun produces_a_value was replaced by the effect of computing the code in produces_a_value. Mathematically, Mrun is a partial function from type M A to type A.
Note how they are equal to exception, but we can still differentiate them.
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:
Note that we have to specify the returning type (we put the arbitrary type nat).
Fixpoints in Coq should terminate to ensure soundness. Checking termination is hard, so Coq relies on a pretty restrictive syntactic condition to ensure termination. We allow non-termination in our language via an unbounded fixpoint, which we call mfix1, mfix2, ... where the number specifies the number of arguments of the function. For instance, an endless loop can be written simply as:
In this definition we decided to add the type annotation M False, since otherwise it is impossible for the type inference mechanism to guess the type. It is important to note that the body of mfix1 should always be of type M.
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 (Mrun (endless_loop 0)).
The key to understanding why it is perfectly safe to allow for such effects is to notice that Mrun is not a function living in the kernel typechecker of Coq. That is, for t of type M A, Mrun t constructs a witness for A only if it's safe to do so, but 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 Mrun in their proof terms.
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 -> M False. To get an element of type False we have to execute it through Mrun as in the commented code. Since it will not terminate, Mrun (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.
We try it with the value 5.
Result: (6 :: Nat.div2 6 :: 3 * Nat.div2 6 + 1 :: Nat.div2 (3 * Nat.div2 6 + 1) :: 3 * Nat.div2 (3 * Nat.div2 6 + 1) + 1 :: Nat.div2 (3 * Nat.div2 (3 * Nat.div2 6 + 1) + 1) :: Nat.div2 (Nat.div2 (3 * Nat.div2 (3 * Nat.div2 6 + 1) + 1)) :: Nat.div2 (Nat.div2 (Nat.div2 (3 * Nat.div2 (3 * Nat.div2 6 + 1) + 1))) :: Nat.div2 (Nat.div2 (Nat.div2 (Nat.div2 (3 * Nat.div2 (3 * Nat.div2 6 + 1) + 1)))) :: nil) : list nat
That doesn't look nice. We'd like to have a list of numbers, not a list of
computations. We have two alternatives, eiter we compute
the result, or
we produce the values in the Mtactic already simplified. The first one is done
with the standard compute tactic.
Result: (6 :: 3 :: 10 :: 5 :: 16 :: 8 :: 4 :: 2 :: 1 :: nil) : list nat
The second option, to simplify the results on the fly, requires a small change in the original tactic:
Can you spot the difference?
Result: (6 :: 3 :: 10 :: 5 :: 16 :: 8 :: 4 :: 2 :: 1 :: nil) : list nat
Mtac defines different unit operators, each operating on the term prior to its return:
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.
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 Mrun, although Mrun is not always 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 Mrun (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 can use the tactic rrun already imported with the Mtac package:
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. Mrun is in fact notation for the application of the tactic rrun with the $(...)$ extension in Coq 8.5 to use tactics to build terms.
An alternative is to use eval, which is similar to Mrun, except that it performs the execution of the Mtactic after the type inference mechanism of Coq has done its job:
When writing tactics, we can use Program to avoid having to write the proof terms ourselves. As an example, we will extend our inlist function to handle list concatenation in order to handle more cases and get shorter proof terms. By using Program, Coq will ask us to provide (interactively) the proof terms for the cases where there is a hole (_) and it cannot guess what to fill in that hole.
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 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).
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.
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.
Let's prove an example using the three functions just created to compare the proof terms they generate.
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:
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.
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.
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.
Let's look at the new case for handling the implication. We need to return an element of type M (p1 -> p2), that is, maybe a function from p1 to p2. Of course, we cannot simply write
ret (fun x:p1 => f (Dyn x :: c) p2)
since this code has type M (p1 -> M 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 -> M B) -> M 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 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).
abs abstracts over parameters created by nu. It has type forall A P (x : A), P x -> M (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 M (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
We can now easily prove this tautology.
Again, the proof term generated is exactly what we would expect for such a proof.
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.
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:
Here is an example to test tauto:
If we cannot instantiate an existential, then an error is thrown.
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 Mrun:
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. Notice how we use the [H] notation after the right arrow in the pattern. The name H will be instantiated with a proof of equality of the scrutinee with the pattern.
You've seen the main characteristics of Mtac, but this doesn't include all what you can do. Moreover, Mtac is still being developed, with new ideas being incorporated all the time. You're invited to visit the web page and to follow Mtac on Twitter or Facebook to keep updated.
[1] VeriML: Typed Computation of Logical Terms inside a Language with Effects. Antonis Stampoulis and Zhong Shao. In Proc. 2010 ACM SIGPLAN International Conference on Functional Programming (ICFP'10).
[2] http://adam.chlipala.net/cpdt/
[3] Aleksandar Nanevski. Meta-programming with names and necessity. In Proceedings of the seventh ACM SIGPLAN international conference on Functional programming, ICFP'02, pages 206-217, New York, NY, USA, 2002. ACM.
[4] Carsten Schuermann, Adam Poswolsky, and Jeffrey Sarnat. The nabla-calculus. functional programming with higher-order encodings. In Proceedings of the 7th international conference on Typed Lambda Calculi and Applications, TLCA'05, pages 339-353, Berlin, Heidelberg, 2005. Springer-Verlag.
[5] http://www.msr-inria.inria.fr/Projects/math-components