Tutorial Equations : Dealing with indexed inductive types

Main contributors

• Thomas Lamiaux
• Matthieu Sozeau

Summary:

Equations is a plugin for Coq that offers a powerful support for writing functions by dependent pattern matching. In this tutorial, we focus on the facilities provided by Equations to define function by dependent pattern matching on indexed inductive types, and reason about them. In Section 1, we discuss indexed inductive types on the particularities of defining and reasoning about functions defined by pattern matching over them. In section 2, we discuss the no confusion property and how it enables to automatically discard impossible cases for indexed inductive types. In section 3, we discuss the particularity that indexed types have to particularise indices when matching, and issues that can arise.

Table of content

• 1. Basic Reasoning on Indexed Inductive Types
• 2. Advanced Dependent Pattern Matching
  • 2.1 Discarding Automatically Impossible Cases
  • 2.2 The No-Confusion Properties
  • 2.3 The Tactic Depelim
• 3. Unifying Indices and Inaccessible Patterns

Prerequisites:

Needed:

• We assume basic knowledge of Coq, of and defining functions by recursion
• We assume basic knowledge of the plugin Equations, e.g, as presented in the tutorial Equations : Basics

Not needed:

• We discuss here indexed inductives but we recall the concept so previous knowledge about them is not needed

Installation:

• Equations is available by default in the Coq Platform
• Otherwise, it is available via opam under the name coq-equations

1. Basic Reasoning on Indexed Inductive Types

Indexed inductive types are particular kind of inductive definitions Given a fixed parameter A : Type, vectors define a family of linked inductive types. One of the most well-known examples of indexed inductive types are vectors. Given a fixed parameter A : Type, vectors define a family of inductive types vec A n : Type indexed by natural numbers n : nat representing the lengths of the vectors. The Vector type has two constructors. The first constructor vnil : vec A 0 represent the empty vector, logically of size 0. Given an element a:A and a vector v : vec A n of size n, the second constructor vcons constructs a vector of size n+1 vcons a n v : vec A (S n), intuitively by adding a at the beginning of v.

The difference between a parameter and an index is that a parameter is constant accros all the return types of the constructors, whereas an index changes in at least one of the return types. For instance, in the definition of vectors the type A is a parameter as it is constant across all the return types: vec A 0 and vec A (S n). However, n:nat is an index as it is not constant in the returns types: in the return type of vnil it is fixed to 0, and in the return type of vcons it is S n. Indices always appear after the : in an inductive type declaration. Reasoning about indexed inductive types like vectors is a bit more involved than for basic inductive types like lists as the indices can matter. Noticeably pattern matching on constructors of indexed inductive types like vec A n may particularise the indices. For instance, matching a vector v : vec A n to vnil forces the value n to be 0 while for vcons if forces n to be of the form S m for some integer m. Consequently, when writing a function on an indexed inductive type, pattern-matching on the inductive type has an effect on other arguments of the function, specializing them. For instance, consider the definition of vmap and vapp :

Reasoning on indexed inductive is not very different from reasoning on regular inductive types except that we have to account for indices, which can in some cases cause some overheads. For basic properties as below, it makes no differences:

However, it can make some differences when operations on indices are involved as indices are relevant for simplification. For instance, if we try to prove that vmap respects vapp as below, in the vcons case simplification fails to simplify vmap f (S n + m) .... The reason is that the simplification rule associated to vcons is vmap f (S n) (vcons a n v) = vcons (f a) n (vmap f n v). Hence, simp can not simplify vmap until S n + m has been simplified to S (n+m) using cbn. It then behaves as usual.

This is not a limitation of Equations itself. It is due to how the rewrite tactic behind simp unifies terms. In practice, indices are mostly inferable, so it is usually possible to make them implicit. It has the advantage to make the code much more concise. For instance, for vec, it enables to write much shorter definitions of vmap and vapp:

Setting indices to be implicit also makes them implicit in proofs. Doing so is not an issue even in the case of vmap_vapp where we need to simplify indices to reduce. If we think a term should have been reduced but hasn't been because of indices, we can always make them temporally explicit to check. We can do so by defining an alias for the functions using the tactic set (name_function_ex := @(name_function _ _ _)) with an underscore for the arguments we do not want to make explicit. After inspecting the goal, you can just erase the tactic or unfold the notations. As an example, let's reprove vmap_vapp :

An alternative is to change the way rewrite looks for matching subterms in the goal, using the keyed unification strategy. With this setting, rewrite (e : t = u) looks for a syntactic match for the head of t in the goal but allows full conversion between arguments of t and the arguments of the matched application in the goal. This makes simp work up-to conversion of the indices. We can then directly call congruence to solve the induction case.

2. Advanced Dependent Pattern Matching

2.1 Discarding Automatically Impossible Cases

Having information directly part of typing, like the length for vector, can have advantages. Most noticeably, it can be used to exclude invalid cases automatically. For instance, consider the function tail that returns the last element. In the case of list, the tail function has to return a term of type option A as there is no guarantee that the input is not the empty list. This is not necessary for vectors as we can use the index to ensure there is at least one element by defining tail as a function of type vec A (S n) → vec A n. This can be implemented very directly with Equations as Equations can deduce on its own that the vnil case is impossible :

Similarly, we can give a very short definition of a function computing the diagonal of a square matrix of size n × n represented as a vector of vector v : vector (vector A n) n). On the empty matrix it returns the empty list. On a matrix (vcons (vcons a v) v') of size (S n) x (S n) representing
              | a | v |
              |---------------|
              | v' |
              | |

it returns a added to the diagonal of vmap vtail v', that is v' where the first column has been forgotten. Note, that in this case, pattern matching on n needs to be added to help Coq see it is a strictly decreasing structurally recursive definition on the index. vmap vtail v' can otherwise not be recognized as a syntactic subterm of v'. An alternative definition using well founded-recursion is presented below.

Thanks to funelim, reasoning for this kind of programs is as usual to the difference that, as for function definitions, we only need to deal with the cases that are possible:

2.2 The No-Confusion Properties

To do so, the elaboration procedure behind Equations relies crucially on no-confusion properties to deduce which cases are impossible, enabling to write concise code where all uninteresting cases are handled automatically. No-confusion properties basically embodies both discrimination and injectivity of constructors: they assert which equations are impossible because the head constructors do not match, or if they do match, simplify to equations between the constructor arguments. The cases above rely on the no-confusion property for nat, that given n, m returns True if n and m are both 0, n = m if they are both of the form S n, S m, and False otherwise. Equations provides a Derive command to generate this notion automatically for each inductive type. For instance, for nat, it suffices to write:

You may have noticed that we have derived the no-confusion property for nat after defining tail and diag, even though it is supposed to be necessary. This is because it is already defined for nat by default, so there was actually no need to do derive it in this particular case. nat is a very simple inductive type. In the general case, for indexed inductive types, there are two kind of no-confusion properties that can be derived by Equations:

• The NoConfusion property that enables to distinguish object with different indices. It takes as argument objects in the total space {n : nat & vec A n} which is generated once and for all with `Derive Signature for vec`. It enables to solve general equations between objects in potentially different instances of the inductive family:

• The NoConfusionHom property that enables to distinguish objects with the same indices (i.e., in the same instance of the inductive family), which is useful for simplifying homogeneous equations:

Note that you can also derive all of them at once using Derive Signature NoConfusion NoConfusionHom for vec. While the NoConfusionHom property is derivable for many indexed inductive types, it is not the case that is derivable for all indexed inductive types. It is derivable only when equality of constructors can be reduced to equality of the non-forced constructor arguments. A forced argument of a constructor is a constructor argument (say of variable name x) that appears in a pattern position in an index of the constructor's type conclusion. Patterns are generated from variables and constructor applications in this case. For example on vectors, this corresponds to the fact that for vcons a n v : vec A (S n), n appears in a pattern position in S n. Intuitively, the value of the *forced* constructor argument n can be inverted from the type vec A (S n). NoConfusionHom for vcons proves that vcons a n v = vcons a' n v' :> vec A (S n) ↔ a = a' ∧ v = v' :> vec A n, i.e. we can eliminate the trivial n = n equality on the forced argument n. This ultimately relies on the UIP property for nat which shows that ∀ e : n = n, e = eq_refl n. If it is not possible to derive it, then Equations may need the indices to satisfy Uniqueness of Identity Proofs, asserting that all equality proofs are equal, i.e. UIP : ∀ (A : Type) (a b : A) (p q : a = b), p = q, to be able to elaborate the definition to a Coq term. UIP holds for types like nat where equality is decidable, but it is not provable for all types. In particular, it is not provable for Type itself. It can be assumed as an axiom, but be mindful that while this is consistent with Coq's vanilla theory and classical logic axioms, it is inconsistent with univalence, so you may not want to admit it globally in your development. Also, as for any axiom, it will result in stuck computations: Equations definitions relying on it will only be simplifiable using simp but no longer compute using e.g. Eval compute. Consequently, Equations offers both options: you can declare it only for the types for which you can prove it or need it, or assume it globally: Assuming you can prove it, from e.g. decidability of equality

Dangerous, incompatible with univalence, and results in stuck computations.

2.3 No-confusion and Dependent Elimination Tactics

Equations provides tactics to access the pattern-matching and simplification engines directly inside proofs. When indexed inductive types are involved, it often provides better simplification tactics than the default injection and inversion tactics, that can handle dependent cases. To explicit pattern-matching and control the naming of variables/hypotheses introduced by an elimination, it is possible to use the dependent elimination tactic, which provides access to the Equations pattern-matching notation inside proofs. Note that the syntax of the patterns for dependent elimination follows the syntax of Equation definitions clauses, rather than the Ltac tactics as clauses.

As for Equations definitions, the patterns should cover solely the possible values of the hypothesis.

x : vec nat 2, so the only possible case to consider is two vcons applications ending with vnil.

H : vcons a ... = vcons b ... which implies a = b. noconf H applies no-confusion and substitution properties recursively to the type of H to simplify it, resulting in a substitution of b by a in the goal.

x : vec nat 2, so the only possible case to consider is two vcons applications ending with vnil.

3. Unifying Indices and Inaccessible Patterns

A particularity of indexed inductive types is that during pattern-matching indices may be particularised to values like variables or terms of the form (f (...)), where f is not a constructor of an inductive type like O or S. The most well-known of example of that is equality | eq A x : A → Prop | that is parameterized by a value x of type A and indexed by another value of type A. Its single constructor states that equality is reflexive, so the only way to build an object of eq x y (in the empty context) is if x is definitionally equal to the term y.
      Inductive eq (A : Type) (x : A) : A → Prop :=
      | eq_refl : eq A x x.
    

Pattern-matching on the equality then unifies the index y with the parameter x, that is to a variable. Consequently, we have determined the value of the pattern y to be x, and it is no longer a candidate for refinement with available constructors like 0 or S n. Such a pattern is said to be "inaccessible", and needs to be indicated by writing ?(t) to tell Equations not to refine it but rather check its inferrability. As an example, to prove the symmetry of equality we pattern match on an equality H : x = y, which unify y the variable x that we indicate by writing eq_sym x ?(x) eq_refl. The goal now being x = x, it holds by eq_refl.

In practice, when the values determined are variables as in eq_sym, the inaccessibility annotation is optional and we can simply write x or a wild card _ rather than ?(x).

For an example, where the ?(t) notation is needed, consider this inductive definition of the image. It has one constructor that for all elements a:A generates an element in its image by f, Imf f (f a). Intuitively, it means that there is an object in Imf f x provided that x is of the form f a for some a.

Pattern-matching on im : Imf f t particularise t to be of the form f a for some a. As f is not a constructor, f a is inaccessible and we need to write as ?(f a) in the pattern matching to prevent Equations to try to interpret f as a constructor. As an example, we can write a function returning the a associated to an object in the image :

Be careful that if you forget to mark inaccessible patterns, then Equations will try to match on the patterns, creating potentially pointless branches. It is fine in theory as the definition obtained will be logically equivalent provided elaboration succeeded, but annoying if you want to extract the code as the definition will be more involved. For instance, if we define vmap'' by matching on n without marking the pattern associated to n as inaccessible, we can see at extraction that Equations matched n and end up with absurd branch to eliminates, yielding a more complicated definition than the original vmap:

Using inaccessible patterns hence allows to separate explicitely the subjects of pattern-matchings and the inferred indices in definitions. The following alternative definition of the square matrix diagonal pattern-matches only on the vec argument, but uses well-founded recursion on the index n to justify termination, as vmap vtail v' is not a subterm of v'.