The previous chapter introduced the most common form of de Bruijn indices, without essential use of dependent types. In earlier chapters, we used dependent de Bruijn indices to illustrate tricks for working with dependent types. This chapter presents one complete case study with dependent de Bruijn indices, focusing on producing the most maintainable proof possible of a classic theorem about lambda calculus.

The proof that follows does not provide a complete guide to all kinds of formalization with de Bruijn indices. Rather, it is intended as an example of some simple design patterns that can make proving standard theorems much easier.

We will prove commutativity of capture-avoiding substitution for basic untyped lambda calculus:

x1 <> x2 => [e1/x1][e2/x2]e = [e2/x2][[e2/x2]e1/x1]e

Defining Syntax and Its Associated Operations

Our definition of expression syntax should be unsurprising. An expression of type exp n may refer to n different free variables.

The classic implementation of substitution in de Bruijn terms requires an auxiliary operation, lifting, which increments the indices of all free variables in an expression. We need to lift whenever we "go under a binder." It is useful to write an auxiliary function liftVar that lifts a variable; that is, liftVar x y will return y + 1 if y >= x, and it will return y otherwise. This simple description uses numbers rather than our dependent fin family, so the actual specification is more involved.

Combining a number of dependent types tricks, we wind up with this concrete realization.

Now it is easy to implement the main lifting operation.

To define substitution itself, we will need to apply some explicit type casts, based on equalities between types. A single equality will suffice for all of our casts. Its statement is somewhat strange: it quantifies over a variable f of type fin n, but then never mentions f. Rather, quantifying over f is useful because fin is a dependent type that is inhabited or not depending on its index. The body of the theorem, S pred( n) = n, is true only for n , but we can prove it by contradiction when n = 0, because we have around a value f of the uninhabited type fin 0.

Now we define a notation to streamline our cast expressions. The code f[ return n, r for e] denotes a cast of expression e whose type can be obtained by substituting some number n1 for n in r. f should be a proof that n1 = n2, for any n2. In that case, the type of the cast expression is r with n2 substituted for n.

This notation is useful in defining a variable substitution operation. The idea is that substVar x y returns None if x = y; otherwise, it returns a "squished" version of y with a smaller fin index, reflecting that variable x has been substituted away. Without dependent types, this would be a simple definition. With dependency, it is reasonably intricate, and our main task in automating proofs about it will be hiding that intricacy.

It is now easy to define our final substitution function. The abstraction case involves two casts, where one uses the sym_eq function to convert a proof of n1 = n2 into a proof of n2 = n1.

Our final commutativity theorem is about subst, but our proofs will rely on a few more auxiliary definitions. First, we will want an operation more that increments the index of a fin while preserving its interpretation as a number.

Second, we will want a kind of inverse to liftVar.

Custom Tactics

Less than a page of tactic code will be sufficient to automate our proof of commutativity. We start by defining a workhorse simplification tactic simp, which extends crush in a few ways.


Ltac simp := repeat progress (crush; try discriminate;
 



We enter an inner loop of applying hints specific to our domain.


  repeat match goal with
 



Our first two hints find places where equality proofs are pattern-matched on. The first hint matches pattern-matches in the conclusion, while the second hint matches pattern-matches in hypotheses. In each case, we apply the library theorem UIP_refl, which says that any proof of a fact like e = e is itself equal to refl_equal. Rewriting with this fact enables reduction of the pattern-match that we found.


           | [ |- context[match ?pf with refl_equal => _ end] ] =>
           rewrite (UIP_refl _ _ pf)
           | [ _ : context[match ?pf with refl_equal => _ end] |- _ ] =>
           rewrite (UIP_refl _ _ pf) in *
 



The next hint finds an opportunity to invert a fin equality hypothesis.


           | [ H : Next _ = Next _ |- _ ] => injection H; clear H
 



If we have two equality hypotheses that share a lefthand side, we can use one to rewrite the other, bringing the hypotheses' righthand sides together in a single equation.


           | [ H : ?E = _, H' : ?E = _ |- _ ] => rewrite H in H'
 



Finally, we would like automatic use of quantified equality hypotheses to perform rewriting. We pattern-match a hypothesis H asserting proposition P. We try to use H to perform rewriting everywhere in our goal. The rewrite succeeds if it generates no additional hypotheses, and, to prevent infinite loops in proof search, we clear H if it begins with universal quantification.


           | [ H : ?P |- _ ] => rewrite H in *; [match P with
                                                   | forall x, _ => clear H
                                                   | _ => idtac
                                                 end]
         end).
 



In implementing another level of automation, it will be useful to mark which free variables we generated with tactics, as opposed to which were present in the original theorem statement. We use a dummy marker predicate Generated to record that information. A tactic not_generated fails if and only if its argument is a generated variable, and a tactic generate records that its argument is generated.

A tactic destructG performs case analysis on fin values. The built-in case analysis tactics are not smart enough to handle all situations, and we also want to mark new variables as generated, to avoid infinite loops of case analysis. Our destructG tactic will only proceed if its argument is not generated.

Our most powerful workhorse tactic will be dester, which incorporates all of simp's simplifications and adds heuristics for automatic case analysis and automatic quantifier instantiation.


Ltac dester := simp;
  repeat (match goal with
 



The first hint expresses our main insight into quantifier instantiation. We identify a hypothesis IH that begins with quantification over fin values. We also identify a free fin variable x and an arbitrary equality hypothesis H. Given these, we try instantiating IH with x. We know we chose correctly if the instantiated proposition includes an opportunity to rewrite using H.


            | [ x : fin _, H : _ = _, IH : forall f : fin _, _ |- _ ] =>
              generalize (IH x); clear IH; intro IH; rewrite H in IH
 



This basic idea suffices for all of our explicit quantifier instantiation. We add one more variant that handles cases where an opportunity for rewriting is only exposed if two different quantifiers are instantiated at once.


            | [ x : fin _, y : fin _, H : _ = _,
                IH : forall (f : fin _) (g : fin _), _ |- _ ] =>
              generalize (IH x y); clear IH; intro IH; rewrite H in IH
 



We want to case-analyze on any fin expression that is the discriminee of a match expression or an argument to more.


            | [ |- context[match ?E with First _ => _ | Next _ _ => _ end] ] =>
              destructG E
            | [ _ : context[match ?E with First _ => _ | Next _ _ => _ end] |- _ ] =>
              destructG E
            | [ |- context[more ?E] ] => destructG E
 



Recall that simp will simplify equality proof terms of facts like e = e. The proofs in question will either be of n = S pred( n) or S pred( n) = n, for some n. These equations do not have syntactically equal sides. We can get to the point where they do have equal sides by performing case analysis on n. Whenever we do so, the n = 0 case will be contradictory, allowing us to discharge it by finding a free variable of type fin 0 and performing inversion on it. In the n = S n' case, the sides of these equalities will simplify to equal values, as needed. The next two hints identify n values that are good candidates for such case analysis.


            | [ x : fin ?n |- _ ] =>
              match goal with
                | [ |- context[nzf x] ] =>
                  destruct n; [ inversion x | ]
              end
            | [ x : fin (pred ?n), y : fin ?n |- _ ] =>
              match goal with
                | [ |- context[nzf x] ] =>
                  destruct n; [ inversion y | ]
              end
 



Finally, we find match discriminees of option type, enforcing that we do not destruct any discriminees that are themselves match expressions. Crucially, we do these case analyses with case_eq instead of destruct. The former adds equality hypotheses to record the relationships between old variables and their new deduced forms. These equalities will be used by our quantifier instantiation heuristic.


            | [ |- context[match ?E with None => _ | Some _ => _ end] ] =>
              match E with
                | match _ with None => _ | Some _ => _ end => fail 1
                | _ => case_eq E; firstorder
              end
 



Each iteration of the loop ends by calling simp again, and, after no more progress can be made, we finish by calling eauto.


          end; simp); eauto.
 

Theorems

We are now ready to prove our main theorem, by way of a progression of lemmas.

The first pair of lemmas characterizes the interaction of substitution and lifting at the variable level.

Next, we define a notion of "greater-than-or-equal" for fin values, prove an inversion theorem for it, and add that theorem as a hint.

A congruence lemma for the fin constructor Next is similarly useful.

We prove a crucial lemma about liftVar in terms of fin_ge.

We suggest a particular way of changing the form of a goal, so that other hints are able to match.

We suggest applying the f_equal tactic to simplify equalities over expressions. For instance, this would reduce a goal App f1 x1 = App f2 x2 to two goals f1 = f2 and x1 = x2.

Our consideration of lifting in isolation finishes with another hint lemma. The auxiliary lemma with a strengthened induction hypothesis is where we put fin_ge to use, and we do not need to mention that predicate again afteward.

Now we characterize the interaction of substitution and lifting on variables. We start with a more general form substVar_lift' of the final lemma substVar_lift, with the latter proved as a direct corollary of the former.

We follow a similar decomposition for the expression-level theorem about substitution and lifting.

Our last auxiliary lemma characterizes a situation where substitution can undo the effects of lifting.

Finally, we arrive at the substitution commutativity theorem.

The final theorem is specialized to the case of substituting in an expression with exactly two free variables, which yields a statement that is readable enough, as statements about de Bruijn indices go.

This proof script is resilient to specification changes. It is easy to add new constructors to the language being treated. The proofs adapt automatically to the addition of any constructor whose subterms each involve zero or one new bound variables. That is, to add such a constructor, we only need to add it to the definition of exp and add (quite obvious) cases for it in the definitions of lift and subst.