The last chapter highlighted a very heuristic approach to proving. In this chapter, we will study an alternative technique, proof by reflection. We will write, in Gallina, decision procedures with proofs of correctness, and we will appeal to these procedures in writing very short proofs. Such a proof is checked by running the decision procedure. The term reflection applies because we will need to translate Gallina propositions into values of inductive types representing syntax, so that Gallina programs may analyze them.

Proving Evenness

Proving that particular natural number constants are even is certainly something we would rather have happen automatically. The Ltac-programming techniques that we learned in the last chapter make it easy to implement such a procedure.

even_256 =
Even_SS
  (Even_SS
     (Even_SS
        (Even_SS
 



...and so on. This procedure always works (at least on machines with infinite resources), but it has a serious drawback, which we see when we print the proof it generates that 256 is even. The final proof term has length super-linear in the input value. Coq's implicit arguments mechanism is hiding the values given for parameter n of Even_SS, which is why the proof term only appears linear here. Also, proof terms are represented internally as syntax trees, with opportunity for sharing of node representations, but in this chapter we will measure proof term size as simple textual length or as the number of nodes in the term's syntax tree, two measures that are approximately equivalent. Sometimes apparently large proof terms have enough internal sharing that they take up less memory than we expect, but one avoids having to reason about such sharing by ensuring that the size of a sharing-free version of a term is low enough.

Superlinear evenness proof terms seem like a shame, since we could write a trivial and trustworthy program to verify evenness of constants. The proof checker could simply call our program where needed.

It is also unfortunate not to have static typing guarantees that our tactic always behaves appropriately. Other invocations of similar tactics might fail with dynamic type errors, and we would not know about the bugs behind these errors until we happened to attempt to prove complex enough goals.

The techniques of proof by reflection address both complaints. We will be able to write proofs like this with constant size overhead beyond the size of the input, and we will do it with verified decision procedures written in Gallina.

For this example, we begin by using a type from the MoreSpecif module (included in the book source) to write a certified evenness checker.

Inductive partial (P : Prop) : Set := Proved : P -> [P] | Uncertain : [P]
 



A partial P value is an optional proof of P. The notation P[] stands for partial P.

We bring into scope some notations for the partial type. These overlap with some of the notations we have seen previously for specification types, so they were placed in a separate scope that needs separate opening.

The function check_even may be viewed as a verified decision procedure, because its type guarantees that it never returns Yes for inputs that are not even.

Now we can use dependent pattern-matching to write a function that performs a surprising feat. When given a partial P, this function partialOut returns a proof of P if the partial value contains a proof, and it returns a (useless) proof of True otherwise. From the standpoint of ML and Haskell programming, it seems impossible to write such a type, but it is trivial with a return annotation.

It may seem strange to define a function like this. However, it turns out to be very useful in writing a reflective version of our earlier prove_even tactic:

We identify which natural number we are considering, and we "prove" its evenness by pulling the proof out of the appropriate check_even call. Recall that the exact tactic proves a proposition P when given a proof term of precisely type P.

even_256' = partialOut (check_even 256)
     : isEven 256



We can see a constant wrapper around the object of the proof. For any even number, this form of proof will suffice. The size of the proof term is now linear in the number being checked, containing two repetitions of the unary form of that number, one of which is hidden above within the implicit argument to partialOut.

What happens if we try the tactic with an odd number?

  prove_even_reflective.

User error: No matching clauses for match goal

Thankfully, the tactic fails. To see more precisely what goes wrong, we can run manually the body of the match.


  exact (partialOut (check_even 255)).

  Error: The term "partialOut (check_even 255)" has type
 "match check_even 255 with
  | Yes => isEven 255
  | No => True
  end" while it is expected to have type "isEven 255"

As usual, the type checker performs no reductions to simplify error messages. If we reduced the first term ourselves, we would see that check_even 255 reduces to a No, so that the first term is equivalent to True, which certainly does not unify with isEven 255.

Our tactic prove_even_reflective is reflective because it performs a proof search process (a trivial one, in this case) wholly within Gallina, where the only use of Ltac is to translate a goal into an appropriate use of check_even.

Reifying the Syntax of a Trivial Tautology Language

We might also like to have reflective proofs of trivial tautologies like this one:

true_galore =
fun H : True /\ True =>
and_ind (fun _ _ : True => or_introl (True /\ (True -> True)) I) H
     : True /\ True -> True \/ True /\ (True -> True)
 



As we might expect, the proof that tauto builds contains explicit applications of natural deduction rules. For large formulas, this can add a linear amount of proof size overhead, beyond the size of the input.

To write a reflective procedure for this class of goals, we will need to get into the actual "reflection" part of "proof by reflection." It is impossible to case-analyze a Prop in any way in Gallina. We must reify Prop into some type that we can analyze. This inductive type is a good candidate:

We write a recursive function to reflect this syntax back to Prop. Such functions are also called interpretation functions, and have used them in previous examples to give semantics to small programming languages.

It is easy to prove that every formula in the range of tautDenote is true.

To use tautTrue to prove particular formulas, we need to implement the syntax reification process. A recursive Ltac function does the job.

With tautReify available, it is easy to finish our reflective tactic. We look at the goal formula, reflect it, and apply tautTrue to the reflected formula.

We can verify that obvious solves our original example, with a proof term that does not mention details of the proof.

true_galore' =
tautTrue
  (TautImp (TautAnd TautTrue TautTrue)
     (TautOr TautTrue (TautAnd TautTrue (TautImp TautTrue TautTrue))))
     : True /\ True -> True \/ True /\ (True -> True)



It is worth considering how the reflective tactic improves on a pure-Ltac implementation. The formula reification process is just as ad-hoc as before, so we gain little there. In general, proofs will be more complicated than formula translation, and the "generic proof rule" that we apply here is on much better formal footing than a recursive Ltac function. The dependent type of the proof guarantees that it "works" on any input formula. This is all in addition to the proof-size improvement that we have already seen.

It may also be worth pointing out that our previous example of evenness testing used a function partialOut for sound handling of input goals that the verified decision procedure fails to prove. Here, we prove that our procedure tautTrue (recall that an inductive proof may be viewed as a recursive procedure) is able to prove any goal representable in taut, so no extra step is necessary.

A Monoid Expression Simplifier

Proof by reflection does not require encoding of all of the syntax in a goal. We can insert "variables" in our syntax types to allow injection of arbitrary pieces, even if we cannot apply specialized reasoning to them. In this section, we explore that possibility by writing a tactic for normalizing monoid equations.

We add variables and hypotheses characterizing an arbitrary instance of the algebraic structure of monoids. We have an associative binary operator and an identity element for it.

It is easy to define an expression tree type for monoid expressions. A Var constructor is a "catch-all" case for subexpressions that we cannot model. These subexpressions could be actual Gallina variables, or they could just use functions that our tactic is unable to understand.

Next, we write an interpretation function.

We will normalize expressions by flattening them into lists, via associativity, so it is helpful to have a denotation function for lists of monoid values.

The flattening function itself is easy to implement.

flatten has a straightforward correctness proof in terms of our denote functions.

Now it is easy to prove a theorem that will be the main tool behind our simplification tactic.

We implement reification into the mexp type.

The final monoid tactic works on goals that equate two monoid terms. We reify each and change the goal to refer to the reified versions, finishing off by applying monoid_reflect and simplifying uses of mldenote. Recall that the change tactic replaces a conclusion formula with another that is definitionally equal to it.

We can make short work of theorems like this one:

  ============================
   a + (b + (c + (d + e))) = a + (b + (c + (d + e)))
 



Our tactic has canonicalized both sides of the equality, such that we can finish the proof by reflexivity.

It is interesting to look at the form of the proof.

t1 =
fun a b c d : A =>
monoid_reflect (Op (Op (Op (Var a) (Var b)) (Var c)) (Var d))
  (Op (Op (Var a) (Op (Var b) (Var c))) (Var d))
  (refl_equal (a + (b + (c + (d + e)))))
     : forall a b c d : A, a + b + c + d = a + (b + c) + d



The proof term contains only restatements of the equality operands in reified form, followed by a use of reflexivity on the shared canonical form.

Extensions of this basic approach are used in the implementations of the ring and field tactics that come packaged with Coq.

A Smarter Tautology Solver

Now we are ready to revisit our earlier tautology solver example. We want to broaden the scope of the tactic to include formulas whose truth is not syntactically apparent. We will want to allow injection of arbitrary formulas, like we allowed arbitrary monoid expressions in the last example. Since we are working in a richer theory, it is important to be able to use equalities between different injected formulas. For instance, we cannot prove P -> P by translating the formula into a value like Imp (Var P) (Var P), because a Gallina function has no way of comparing the two Ps for equality.

To arrive at a nice implementation satisfying these criteria, we introduce the quote tactic and its associated library.

The type index comes from the Quote library and represents a countable variable type. The rest of formula's definition should be old hat by now.

The quote tactic will implement injection from Prop into formula for us, but it is not quite as smart as we might like. In particular, it interprets implications incorrectly, so we will need to declare a wrapper definition for implication, as we did in the last chapter.

Now we can define our denotation function.

The varmap type family implements maps from index values. In this case, we define an assignment as a map from variables to Props. Our reifier formulaDenote works with an assignment, and we use the varmap_find function to consult the assignment in the Atomic case. The first argument to varmap_find is a default value, in case the variable is not found.

We define some shorthand for a particular variable being true, and now we are ready to define some helpful functions based on the ListSet module of the standard library, which (unsurprisingly) presents a view of lists as sets.

We define what it means for all members of an index set to represent true propositions, and we prove some lemmas about this notion.

Now we can write a function forward which implements deconstruction of hypotheses. It has a dependent type, in the style of Chapter 6, guaranteeing correctness. The arguments to forward are a goal formula f, a set known of atomic formulas that we may assume are true, a hypothesis formula hyp, and a success continuation cont that we call when we have extended known to hold new truths implied by hyp.

A backward function implements analysis of the final goal. It calls forward to handle implications.

A simple wrapper around backward gives us the usual type of a partial decision procedure.

Our final tactic implementation is now fairly straightforward. First, we intro all quantifiers that do not bind Props. Then we call the quote tactic, which implements the reification for us. Finally, we are able to construct an exact proof via partialOut and the my_tauto Gallina function.

A few examples demonstrate how the tactic works.

mt1 = partialOut (my_tauto (Empty_vm Prop) Truth)
     : True



We see my_tauto applied with an empty varmap, since every subformula is handled by formulaDenote.

mt2 =
fun x y : nat =>
partialOut
  (my_tauto (Node_vm (x = y) (Empty_vm Prop) (Empty_vm Prop))
     (Imp (Atomic End_idx) (Atomic End_idx)))
     : forall x y : nat, x = y --> x = y



Crucially, both instances of x = y are represented with the same index, End_idx. The value of this index only needs to appear once in the varmap, whose form reveals that varmaps are represented as binary trees, where index values denote paths from tree roots to leaves.

fun x y z : nat =>
partialOut
  (my_tauto
     (Node_vm (x < S y) (Node_vm (x < y) (Empty_vm Prop) (Empty_vm Prop))
        (Node_vm (y > z) (Empty_vm Prop) (Empty_vm Prop)))
     (Imp
        (Or (And (Atomic (Left_idx End_idx)) (Atomic (Right_idx End_idx)))
           (And (Atomic (Right_idx End_idx)) (Atomic End_idx)))
        (And (Atomic (Right_idx End_idx))
           (Or (Atomic (Left_idx End_idx)) (Atomic End_idx)))))
     : forall x y z : nat,
       x < y /\ y > z \/ y > z /\ x < S y --> y > z /\ (x < y \/ x < S y)



Our goal contained three distinct atomic formulas, and we see that a three-element varmap is generated.

It can be interesting to observe differences between the level of repetition in proof terms generated by my_tauto and tauto for especially trivial theorems.

mt4 =
partialOut
  (my_tauto (Empty_vm Prop)
     (Imp
        (And Truth
           (And Truth
              (And Truth (And Truth (And Truth (And Truth Falsehood))))))
        Falsehood))
     : True /\ True /\ True /\ True /\ True /\ True /\ False --> False

mt4' =
fun H : True /\ True /\ True /\ True /\ True /\ True /\ False =>
and_ind
  (fun (_ : True) (H1 : True /\ True /\ True /\ True /\ True /\ False) =>
   and_ind
     (fun (_ : True) (H3 : True /\ True /\ True /\ True /\ False) =>
      and_ind
        (fun (_ : True) (H5 : True /\ True /\ True /\ False) =>
         and_ind
           (fun (_ : True) (H7 : True /\ True /\ False) =>
            and_ind
              (fun (_ : True) (H9 : True /\ False) =>
               and_ind (fun (_ : True) (H11 : False) => False_ind False H11)
                 H9) H7) H5) H3) H1) H
     : True /\ True /\ True /\ True /\ True /\ True /\ False -> False



The traditional tauto tactic introduces a quadratic blow-up in the size of the proof term, whereas proofs produced by my_tauto always have linear size.

Manual Reification of Terms with Variables

The action of the quote tactic above may seem like magic. Somehow it performs equality comparison between subterms of arbitrary types, so that these subterms may be represented with the same reified variable. While quote is implemented in OCaml, we can code the reification process completely in Ltac, as well. To make our job simpler, we will represent variables as nats, indexing into a simple list of variable values that may be referenced.

Step one of the process is to crawl over a term, building a duplicate-free list of all values that appear in positions we will encode as variables. A useful helper function adds an element to a list, maintaining lack of duplicates. Note how we use Ltac pattern matching to implement an equality test on Gallina terms; this is simple syntactic equality, not even the richer definitional equality. We also represent lists as nested tuples, to allow different list elements to have different Gallina types.

Now we can write our recursive function to calculate the list of variable values we will want to use to represent a term.

We will also need a way to map a value to its position in a list.

The next building block is a procedure for reifying a term, given a list of all allowed variable values. We are free to make this procedure partial, where tactic failure may be triggered upon attempting to reflect a term containing subterms not included in the list of variables. The output type of the term is a copy of formula where index is replaced by nat, in the type of the constructor for atomic formulas.

Note that, when we write our own Ltac procedure, we can work directly with the normal -> operator, rather than needing to introduce a wrapper for it.

Finally, we bring all the pieces together.

A quick test verifies that we are doing reification correctly.

Our simple tactic adds the translated term as a new variable:
f := Imp'
         (Or' (And' (Atomic' 2) (Atomic' 1)) (And' (Atomic' 1) (Atomic' 0)))
         (And' (Atomic' 1) (Or' (Atomic' 2) (Atomic' 0))) : formula'

More work would be needed to complete the reflective tactic, as we must connect our new syntax type with the real meanings of formulas, but the details are the same as in our prior implementation with quote.

Exercises

1. Implement a reflective procedure for normalizing systems of linear equations over rational numbers. In particular, the tactic should identify all hypotheses that are linear equations over rationals where the equation righthand sides are constants. It should normalize each hypothesis to have a lefthand side that is a sum of products of constants and variables, with no variable appearing multiple times. Then, your tactic should add together all of these equations to form a single new equation, possibly clearing the original equations. Some coefficients may cancel in the addition, reducing the number of variables that appear.
   
   To work with rational numbers, import module QArith and use Local Open Scope Q_scope. All of the usual arithmetic operator notations will then work with rationals, and there are shorthands for constants 0 and 1. Other rationals must be written as num # den for numerator num and denominator den. Use the infix operator == in place of =, to deal with different ways of expressing the same number as a fraction. For instance, a theorem and proof like this one should work with your tactic:
     Theorem t2 : forall x y z, (2 # 1) * (x - (3 # 2) * y) == 15 # 1
       -> z + (8 # 1) * x == 20 # 1
       -> (-6 # 2) * y + (10 # 1) * x + z == 35 # 1.
       intros; reifyContext; assumption.
     Qed.
   
   
   
   Your solution can work in any way that involves reifying syntax and doing most calculation with a Gallina function. These hints outline a particular possible solution. Throughout, the ring tactic will be helpful for proving many simple facts about rationals, and tactics like rewrite are correctly overloaded to work with rational equality ==.
   
   
   1. Define an inductive type exp of expressions over rationals (which inhabit the Coq type Q). Include variables (represented as natural numbers), constants, addition, subtraction, and multiplication.
   2. Define a function lookup for reading an element out of a list of rationals, by its position in the list.
   3. Define a function expDenote that translates exps, along with lists of rationals representing variable values, to Q.
   4. Define a recursive function eqsDenote over list exp( * Q), characterizing when all of the equations are true.
   5. Fix a representation lhs of flattened expressions. Where len is the number of variables, represent a flattened equation as ilist Q len. Each position of the list gives the coefficient of the corresponding variable.
   6. Write a recursive function linearize that takes a constant k and an expression e and optionally returns an lhs equivalent to k * e. This function returns None when it discovers that the input expression is not linear. The parameter len of lhs should be a parameter of linearize, too. The functions singleton, everywhere, and map2 from DepList will probably be helpful. It is also helpful to know that Qplus is the identifier for rational addition.
   7. Write a recursive function linearizeEqs : list exp( * Q) -> option (lhs * Q). This function linearizes all of the equations in the list in turn, building up the sum of the equations. It returns None if the linearization of any constituent equation fails.
   8. Define a denotation function for lhs.
   9. Prove that, when exp linearization succeeds on constant k and expression e, the linearized version has the same meaning as k * e.
   10. Prove that, when linearizeEqs succeeds on an equation list eqs, then the final summed-up equation is true whenever the original equation list is true.
   11. Write a tactic findVarsHyps to search through all equalities on rationals in the context, recursing through addition, subtraction, and multiplication to find the list of expressions that should be treated as variables. This list should be suitable as an argument to expDenote and eqsDenote, associating a Q value to each natural number that stands for a variable.
   12. Write a tactic reify to reify a Q expression into exp, with respect to a given list of variable values.
   13. Write a tactic reifyEqs to reify a formula that begins with a sequence of implications from linear equalities whose lefthand sides are expressed with expDenote. This tactic should build a list exp( * Q) representing the equations. Remember to give an explicit type annotation when returning a nil list, as in constr:(@nil exp( * Q)).
   14. Now this final tactic should do the job:
         Ltac reifyContext :=
           let ls := findVarsHyps in
             repeat match goal with
                      | [ H : ?e == ?num # ?den |- _ ] =>
                        let r := reify ls e in
                          change (expDenote ls r == num # den) in H;
                          generalize H
                    end;
             match goal with
               | [ |- ?g ] => let re := reifyEqs g in
                   intros;
                     let H := fresh "H" in
                     assert (H : eqsDenote ls re); [ simpl in *; tauto
                       | repeat match goal with
                                  | [ H : expDenote _ _ == _ |- _ ] => clear H
                                end;
                       generalize (linearizeEqsCorrect ls re H); clear H; simpl;
                         match goal with
                           | [ |- ?X == ?Y -> _ ] =>
                             ring_simplify X Y; intro
                         end ]
             end.