Proofs by reflection and uses of type classes

When performing proofs about mathematical formulas, it is often enough to perform small computation on the shape of the statement rather than complex reasoning on the meaning of all its components.

These computations can be programmed directly in Coq, as long as we define a language to describe the shapes that we are interested in and write programs to compute on elements of this language.  Then, there should be a way to link computations about the language with reasoning steps and the programs that we have defined can be used for reasoning.

This is the trick used by the ring tactic.  The complicated part is to establish the link between computations about the language and reasoning steps.  This is the subject of this post.

The theory of proofs by associativity

To illustrate this, we will work on a simple example: proofs by associativity.  When an operator is associative, it is not necessary to know where parentheses occur in two complex expressions to show that they are equal, it is enough to know in which order each of the elementary formulas appears.

For instance, consider the following two expressions:

We simply know that the two expressions are equal because addition is associative and 1, x, y, and z appear in that order in both expressions.

We shall now write a Coq function that takes care of checking that two formulas do have the same elementary components in the same order.

First we define a language to describe the expressions we are interested in:

Inductive lang := var (i : nat) | bin (t1 t2 : lang).

Then we write a function that returns the same result for all inputs that have the same elementary expressions in the same order.  In this case, this is done by writing a normalizing function.   Here we call such a normalizing function norm:

Fixpoint norm_aux t1 t2 : lang :=
match t1 with
| var x => bin (var x) t2
| bin t t' => norm_aux t (norm_aux t' t2)
end.

Fixpoint norm t :=
match t with
| var x => t
| bin t1 t2 => norm_aux t1 (norm t2)
end.

For instance,

norm (bin (bin (var 1) (bin (var 2) (var 3))) (var 4)

and

norm (bin (bin (var 1) (var 2)) (bin (var 3) (var 4))

are both equal to

bin (var 1) (bin (var 2) (bin (var 3) (var 4)))

Linking the theory to practice

Now, we need to show that expression of the language lang can be related to expressions of a domain where we wish to work. For the sake of simplicity, we shall consider that we are only interested in expressions about integers (type Z), but we shall show that our approach works for any associative operator on integers.

Require Import ZArith.

Open Scope Z_scope.

We shall first define a function that maps any expression in our language to an expression in Z. We need to pick the values for all the variables occurring in the expression. We use a list of integer values for this.

Fixpoint interp (op : Z -> Z -> Z) (l : list Z) (t : lang) : Z :=
  match t with
  | var v => nth v l 0
  | bin x y => op (interp op l x) (interp op l y)
  end.

If we consider the following expression:

We see that it is the result of the following call to the interp function (assuming x, y, and z are values in type Z).

interp (1::x::y::z::nil) (bin (bin (var 0) (var 1)) (bin (var 2) (var 3)))

Now, we need to show that the norm function is sound. In other words, when op is associative, the interpretation of expressions from lang is not modified by norm. This is expressed as follows:

Section assoc_reflection_proofs.

Variable op : Z -> Z -> Z.

Hypothesis op_assoc : forall a b c, op a (op b c) = op (op a b) c.

Lemma norm_aux_c l t1 t2 :
  interp op l (norm_aux t1 t2) = op (interp op l t1) (interp op l t2).
Proof.
revert t2; induction t1 as [i | t1 IH1 t2 IH2]; intros t3.
  now auto.
now simpl; rewrite IH1, IH2, op_assoc.
Qed.

Lemma norm_c l t :  interp op l t = interp op l (norm t).
Proof.
induction t as [i | t1 IH1 t2 IH2]; auto; simpl.
now rewrite IH2, norm_aux_c.
Qed.

Lemma norm_c2 l t1 t2 : norm t1 = norm t2 -> interp op l t1 = interp op l t2.
Proof. now intros nn; rewrite (norm_c _ t1), (norm_c _ t2); apply f_equal.  Qed.

End assoc_reflection_proofs.

Arguments norm_c2 {op}.

Now we can use this theorem in an example.

Example axpypzpt x y z t : (x + y) + (z + t) = x + (y + z) + t.
Proof.
change (interp Z.add (x::y::z::t::nil)(bin (bin (var 0) (var 1))
                                           (bin (var 2) (var 3))) =
        interp Z.add (x::y::z::t::nil)
             (bin (bin (var 0) (bin (var 1) (var 2))) (var 3))).
apply (norm_c2 Z.add_assoc).
reflexivity.
Qed.

The first change step in this proof triggers the computation of the interp function on the two inputs and verify that this computation returns the two expressions compared in the equality.
The last reflexivity step in this proof triggers the computation of the norm function on the two inputs and verify that this computation returns the same value. So computation is used extensively in this proof, but only one invocation of a theorem is needed.

this example proof exhibits a problem that we still have to solve: the user needs to write the expressions in the theoretical language whose interpretation will be equal to the expressions being compared. This is treated in the next section.

From practice to theory: reification

Our objective now, is to find a way to force Coq to compute a list of values and two expressions in lang so that the interp function maps these two values to expressions appearing in our goal.

We assume that the goal has the shape of an equality u = v. Here, we will use a little trick: instead of looking for expressions in lang for u and v separately, we will look for an expression representing u + v. This expression will necessarily have the shape (bin e₁ e₂) and the expressions for u and v will be e₁ and e₂.

To force Coq to compute the needed values, we will use the proof search capability that comes with Coq’s mechanism for type classes.

We use a type class to express that the interpretation of expression from lang with respect to a list of values returns a given expression in Z. This type class is declared as follows:

Class Reify (op : Z -> Z -> Z)  (x : Z) (t : lang) (l : list Z).

Elements of this class have an empty body. Only the type of the class is meaningful here: it is used to express that we put together a value in Z, a term from the lang type, and a list .

Then we explain that to produce a value of lang corresponding to a fixed binary operator, we need to construct two sub-trees and combine them with the bin constructor of the lang type.

Instance binRf op x y l e1 e2 {_ : Reify op x e1 l} {_ : Reify op y e2 l} :
   Reify op (op x y) (bin e1 e2) l | 1 := {}.

Thus, when faced with a question to prove

Reify Z.add ((2 + x) + y) ?expr ?l

Where ?expr and ?l are still unknown, the instance binRf will push Coq to transform this question into finding two expressions ?e1 and ?e2 for (2 + x) and y respectively. When finding these expressions, it will construct the value (bin ?e1 ?e2) as the result for ?expr.

It actually works in a different way, using a notion of incomplete terms with existential variables that is introduced by logic programming (in other words, in programming languages such as Prolog). When using the
instance binRf where the second argument is unknown (represented by an existential variable written ?expr in my example), the proof search mechanism memorizes directly that ?expr should have the value (bin ?e1 ?e2) where ?e1 and ?e2 are existential variables.

Many tactics in Coq are fine-tuned to take advantage of existential variables, these tactics have a name starting with the letter e: eapply, eauto, etc. In the case of type classes, the main working tool is a tactic called typeclasses eauto, but we will not need to call it explicitly.

We need now to explain what will happen when the expression of type Z is not an application of the operator op for which interp is working. In this case, we wish to construct a term of the form of the form (var i), and make sure that the ith element in the list of values is equal to the expression of type Z we are working on.

To make sure that the ith element of the list is the right one, we define a new type class, with we call Nth (to mimick the nth function that is used in interp).

Class Nth (i : nat) (l : list Z) (e : Z).

This Nth class is used to guide proof search. We expect statements of the form Nth i l e to express that the ith element of list l is the expression e.

When the first element of a list is the expression we are looking for and the number i is 0, then we can stop
our search here and the intended meaning is obtained. This is expressed by the following class instance.

Instance nth0 e l : Nth 0 (e :: l) e | 0 := {}.

Here, something clever is happening: if in fact the we know e, but l and i are unknown, we
can still use this instance. This fixes i to be 0 and l to be (e :: ?l1) where ?l1 is a new
unknown existential variable.

Now, if we are looking at a list of the form (e’ :: l’) where e’ is different from e, we may still succeed as long as the ith element of l’ is e. This is expressed by the following instance.

Instance nthS i e l e'
   {_ : Nth i l e} : Nth (S i) (e' :: l) e | 2 := {}.

The same clever trick as above applies here. If the list l’ is partially unknown, then the process of looking whether e does appear in it will actually change its value, adding e in the list and leaving an extra unknown sublist for later completion.

For instance, we may wonder whether an existential variable ?l can be such that the two questions (Nth ?i ?l x) and (Nth ?j ?l y) receive a positive answer (in this illustrating example, x and y are fixed distinct values, not unknowns). The two questions are taken in order. Furst we look at the question (Nth ?i ?l x). Since ?l and ?i are unknown, the Instance nth0 can be used and this gives us the information

?l = x :: ?l1
?i = 0

This first question is solved. Consider now the question (Nth ?j ?l y). Because of the above information, this question actually has a new shape: (Nth ?j (x :: ?l1) y). This question cannot be solved using nth0, but nthS can be applied, leading to the following information

?j = S ?k

and the new question (Nth ?k ?l1 y). Now because ?k and ?l1 are unknown, we can apply nth0 to the sub-question and gather the following information.

?k = 0
?j = S 0 = 1
?l1 = y :: ?l2
?l = x :: y :: ?l2

So asking the two questions (Nth ?j ?l x) and (Nth ?j ?l y) resulted in ?l, ?i, ?j receiving relevant values.

Now that we have a way to make sure that unknown lists become known enough to contain fixed elements, we can use that to explain how to construct a list and a lang expression for an arbitrary value.

Instance varRf op e i l 
  {_ : Nth i l e} : Reify op e (var i) l | 100.

there is a small glitch though, neither the nth0 instance nor the nthS instances makes the list completely known, there is always a sublist that remains unknown. When doing proofs, this is unsatisfactory, and the Coq system will not let us finish a proof with a sub-part that is still unknown. The simplest thing to do is to fix the remaining unknown to nil when we know that we don’t need to add anymore information in the list. This is done with yet another type class, which we name Closed.

Class Closed (l : list Z).

Instance closed0 : Closed nil.

Instance closed1 a l {_ : Closed l} : Closed (a :: l).

To make Coq use these type classes, we define a function Reify_trigger as follows:

Definition reify_trigger op (term : Z) {expr : lang} {lvar : list Z}
 {_ : Reify op term expr lvar} `{Closed lvar} := (lvar, expr).

This function has six arguments: the first is the binary operator for which we want reification to happen, the second is the expression in type Z that we want to reify, the third one is the reification result, the fourth one is the list of values for all variables in the third one. The fifth is a value in the type class Reify and the sixth one is a value in type closed. The fifth argument guarantees that reify_trigger will only return a value when the reified expression and the list of values for variables are correct for the expression we want to reify.

The clever trick is that if we call reify_trigger with only the first two arguments, Coq will attempt to insert all other arguments. In the process of inserting the argument of type Reify, it will actually construct expr and lvar (partially for lvar) and in the process of inserting the argument of type closed, it will finish the construction of lvar. The function will then be able to return the reified value and the list of variables. Moreover, the arguments after the third one are never written by the user, because they are implicit, as expressed by the use of curly braces.
This process is used in the following tactic:

Ltac reify_step op :=
match goal with |- ?u = ?v =>
  match eval red in (reify_trigger op (op u v)) with
    (?a, bin ?b ?c) => change (interp op a b = interp op a c)
  end
end.

We can now test this tactic in the previous example.

Example axpypzpt' x y z t : (x + y) + (z + t) = x + (y + z) + t.
Proof.
reify_step Z.add.

At this stage, the goal is as follows: the reification process has taken place and the goal has the following shape.

interp Z.add (x :: y :: z :: t :: nil)
    (bin (bin (var 0) (var 1)) (bin (var 2) (var 3))) =
  interp Z.add (x :: y :: z :: t :: nil)
    (bin (bin (var 0) (bin (var 1) (var 2))) (var 3))

The proof of this theorem can be finished by calling the following command (as before):

apply (norm_c2 Z.add_assoc).
reflexivity.
Qed.

This example can then be extended to incorporate the treatment of commutativity. The fully worked example is available here.