`Equations` is a plugin for that comes with a few support modules defining
classes and tactics for running it. We will introduce its main
features through a handful of examples. We start our Coq primer
session by importing the `Equations` module.

In its simplest form, `Equations` allows to define functions on inductive datatypes.
Take for example the booleans defined as an inductive type with two constructors `true` and `false`:

Inductive bool : Set := true : bool | false : boolWe can define the boolean negation as follows:

`Equations` declarations are formed by a signature definition and a set of *clauses*
that must form a *covering* of this signature. The compiler is then expected to
automatically find a corresponding case-splitting tree that implements the function.
In this case, it simply needs to split on the single variable `b` to
produce two new *programming problems* `neg true` and `neg false` that are directly
handled by the user clauses. We will see in more complex examples that this search
for a splitting tree may be non-trivial.

In the setting of a proof assistant like Coq, we need not only the ability to define complex functions but also get good reasoning support for them. Practically, this translates to the ability to simplify applications of functions appearing in the goal and to give strong enough proof principles for (recursive) definitions.

`Equations` provides this through an automatic generation of proofs related to
the function. Namely, each defining equation gives rise to a lemma stating the
equality between the left and right hand sides. These equations can be used as
rewrite rules for simplification during proofs, without having to rely on the
fragile simplifications implemented by raw reduction. We can also generate the
inductive graph of any `Equations` definition, giving the strongest elimination
principle on the function.

I.e., for `neg` the inductive graph is defined as:

Inductive neg_ind : bool -> bool -> Prop := | neg_ind_equation_1 : neg_ind true false | neg_ind_equation_2 : neg_ind false trueAlong with a proof of

b : bool ============================ neg (neg b) = bAn application of the tactic

In the following sections we will show how these ideas generalize to more complex types and definitions involving dependencies, overlapping clauses and recursion.

Coq's inductive types can be parameterized by types, giving polymorphic datatypes. For example the list datatype is defined as:

No special support for polymorphism is needed, as type arguments are treated
like regular arguments in dependent type theories. Note however that one cannot
match on type arguments, there is no intensional type analysis.
We can write the polymorphic `tail` function as follows:

Note that the argument `{A}` is declared implicit and must hence be
omitted in the defining clauses. In each of the branches it is named
`A`. To specify it explicitely one can use the syntax `(A:=B)`,
renaming that implicit argument to `B` in this particular case

Of course with inductive types comes recursion. Coq accepts a subset of the structurally recursive definitions by default (it is incomplete due to its syntactic nature). We will use this as a first step towards a more robust treatment of recursion via well-founded relations. A classical example is list concatenation:

Recursive definitions like `app` can be unfolded easily so proving the
equations as rewrite rules is direct. The induction principle associated
to this definition is more interesting however. We can derive from it the
following *elimination* principle for calls to `app`:

app_elim : forall P : forall (A : Type) (l l' : list A), list A -> Prop, (forall (A : Type) (l' : list A), P A nil l' l') -> (forall (A : Type) (a : A) (l l' : list A), P A l l' (app l l') -> P A (a :: l) l' (a :: app l l')) -> forall (A : Type) (l l' : list A), P A l l' (app l l')Using this eliminator, we can write proofs exactly following the structure of the function definition, instead of redoing the splitting by hand. This idea is already present in the

The structure of real programs is richer than a simple case tree on the original arguments in general. In the course of a computation, we might want to scrutinize intermediate results (e.g. coming from function calls) to produce an answer. This literally means adding a new pattern to the left of our equations made available for further refinement. This concept is know as with clauses in the Agda community and was first presented and implemented in the Epigram language .

The compilation of with clauses and its treatment for generating equations and the induction principle are quite involved in the presence of dependencies, but the basic idea is to add a new case analysis to the program. To compute the type of the new subprogram, we actually abstract the discriminee term from the expected type of the clause, so that the type can get refined in the subprogram. In the non-dependent case this does not change anything though.

Each `with` node generates an auxiliary definition from the clauses
in the curly brackets, taking the additional object as argument. The
equation for the with node will simply be an indirection to the
auxiliary definition and simplification will continue as usual with
the auxiliary definition's rewrite rules.

By default, equations makes definitions opaque after definition,
to avoid spurious unfoldings, but this can be reverted on a case by case
basis, or using the global `Set Equations Transparent` option.

A common use of with clauses is to scrutinize recursive results like the following:

The real power of with however comes when it is used with dependent types.

Coq supports writing dependent functions, in other words, it gives the ability to
make the results *type* depend on actual *values*, like the arguments of the function.
A simple example is given below of a function which decides the equality of two
natural numbers, returning a sum type carrying proofs of the equality or disequality
of the arguments. The sum type `{ A } + { B }` is a constructive variant of disjunction
that can be used in programs to give at the same time a boolean algorithmic information
(are we in branch `A` or `B`) and a *logical* information (a proof witness of `A` or `B`).
Hence its constructors `left` and `right` take proofs as arguments. The `eq_refl` proof
term is the single proof of `x = x` (the `x` is generaly infered automatically).

Of particular interest here is the inner program refining the recursive result.
As `equal n m` is of type `{ n = m } + { n <> m }` we have two cases to consider:

- Either we are in the
`left p`case, and we know that`p`is a proof of`n = m`, in which case we can do a nested match on`p`. The result of matching this equality proof is to unify`n`and`m`, hence the left hand side patterns become`S n`and`S ?(n)`and the return type of this branch is refined to`{ n = n } + { n <> n }`. We can easily provide a proof for the left case. - In the right case, we mark the proof unfilled with an underscore. This will
generate an obligation for the hole, that can be filled automatically by a
predefined tactic or interactively by the user in proof mode (this uses the
same obligation mechanism as the Program extension
). In this case the automatic tactic
is able to derive by itself that
`n <> m -> S n <> S m`.

We decompose the list and are faced with two cases:

- In the first case, the list is empty, hence the proof
`pf`of type`nil <> nil`allows us to derive a contradiction by applying it to reflexivity. We make use of another category of right-hand sides, which we call*empty*nodes to inform the compiler that a contradiction is derivable in this case. In general we cannot expect the compiler to find by himself that the context contains a contradiction, as it is undecidable .However, in this case, one could also write an empty set of clauses for the

`with`subprogram, as Equations applies a heuristic in case of an empty set of clause: it tries to split each of the variables in the context to find an empty type. - In the second case, we simply return the head of the list, disregarding the proof.

The next step is to make constraints such as non-emptiness part of the datatype itself. This capability is provided through inductive families in Coq , which are a similar concept to the generalization of algebraic datatypes to GADTs in functional languages like Haskell . Families provide a way to associate to each constructor a different type, making it possible to give specific information about a value in its type.

Inductive eq (A : Type) (x : A) : A -> Prop := eq_refl : eq A x x.]]

Equality is a polymorphic relation on `A`. (The `Prop` sort (or kind) categorizes
propositions, while the `Set` sort, equivalent to $$ $$ in Haskell categorizes
computational types.) Equality 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` is if
`x ~= y`, that is if `x` is definitionaly equal to `y`.

Now what is the elimination principle associated to this inductive family? It is the good old Leibniz substitution principle:

forall (A : Type) (x : A) (P : A -> Type), P x -> forall y : A, x = y -> P yProvided a proof that

Let us explain the meaning of the non-linear patterns here that we
slipped through in the `equal` example. By pattern-matching on the
equalities, we have unified `x`, `y` and `z`, hence we determined the
*values* of the patterns for the variables to be `x`. The `?(x)`
notation is essentially denoting that the pattern is not a candidate
for refinement, as it is determined by another pattern. This
particular patterns are called inaccessible

. When they are variables
the inaccessibility annotation is optional.

Functions on `vector`s provide more stricking examples of this
situation. The `vector` family is indexed by a natural number
representing the size of the vector: `[ Inductive vector (A : Type) :
nat -> Type := | Vnil : vector A O | Vcons : A -> forall n : nat,
vector A n -> vector A (S n) ]`

The empty vector `Vnil` has size `O` while the cons operation
increments the size by one. Now let us define the usual map on
vectors:

Here the value of the index representing the size of the vector
is directly determined by the constructor, hence in the case tree
we have no need to eliminate `n`. This means in particular that
the function `vmap` does not do any computation with `n`, and
the argument could be eliminated in the extracted code.
In other words, it provides only *logical* information about
the shape of `v` but no computational information.

The `vmap` function works on every member of the `vector` family,
but some functions may work only for some subfamilies, for example
`vtail`:

The type of `v` ensures that `vtail` can only be applied to
non-empty vectors, moreover the patterns only need to consider
constructors that can produce objects in the subfamily `vector A (S n)`,
excluding `Vnil`. The pattern-matching compiler uses unification
with the theory of constructors to discover which cases need to
be considered and which are impossible. In this case the failed
unification of `0` and `S n` shows that the `Vnil` case is impossible.
This powerful unification engine running under the hood permits to write
concise code where all uninteresting cases are handled automatically.

For this to work smoothlty, the package requires some derived definitions
on each (indexed) family, which can be generated automatically using
the generic `Derive` command. Here we ask to generate the signature,
heterogeneous no-confusion and homogeneous no-confusion principles for vectors:

The precise specification of these derived definitions can be found in the manual
section . Signature is used to pack

a value in an inductive family
with its index, e.g. the total space

of every index and value of the family. This
can be used to derive the heterogeneous no-confusion principle for the family, which
allows to discriminate between objects in potentially different instances/fibers of the family,
or deduce injectivity of each constructor. The `NoConfusionHom` variant derives
the homogeneous no-confusion principle between two objects in the *same* instance
of the family, e.g. to simplify equations of the form `Vnil = Vnil :> vector A 0`.
This last principle can only be defined when pattern-matching on the inductive family
does not require the `K` axiom and will otherwise fail.

Back to our example, of course the equations and the induction principle are simplified in a
similar way. If we encounter a call to `vtail` in a proof, we can
use the following elimination principle to simplify both the call and the
argument which will be automatically substituted by an object of the form
`Vcons _ _ _`:

forall P : forall (A : Type) (n : nat), vector A (S n) -> vector A n -> Prop, (forall (A : Type) (n : nat) (a : A) (v : vector A n), P A n (Vcons a v) v) -> forall (A : Type) (n : nat) (v : vector A (S n)), P A n v (vtail v)As a witness of the power of the unification, consider the following function which computes the diagonal of a square matrix of size

Here in the second equation, we know that the elements of the vector
are necessarily of size `S n` too, hence we can do a nested refinement
on the first one to find the first element of the diagonal.

Notice how in the `diag` example above we explicitely pattern-matched
on the index `n`, even though the `Vnil` and `Vcons` pattern matching
would have been enough to determine these indices. This is because the
following definition also fails:

Indeed, Coq cannot guess the decreasing argument of this fixpoint
using its limited syntactic guard criterion: `vmap vtail v'` cannot
be seen to be a (large) subterm of `v'` using this criterion, even
if it is clearly smaller

. In general, it can also be the case that
the compilation algorithm introduces decorations to the proof term
that prevent the syntactic guard check from seeing that the
definition is structurally recursive.

To aleviate this problem, `Equations` provides support for
*well-founded* recursive definitions which do not rely on syntactic
checks.

The simplest example of this is using the `lt` order on natural numbers
to define a recursive definition of identity:

Here `id` is defined by well-founded recursion on `lt` on the (only)
argument `n` using the `by wf` annotation. At recursive calls of
`id`, obligations are generated to show that the arguments
effectively decrease according to this relation. Here the proof
that `n' < S n'` is discharged automatically.

Wellfounded recursion on arbitrary dependent families is not as easy
to use, as in general the relations on families are *heterogeneous*,
as they must relate inhabitants of potentially different instances of
the family. `Equations` provides a `Derive` command to generate the
subterm relation on any such inductive family and derive the
well-foundedness of its transitive closure. This provides
course-of-values or so-called mathematical

induction on these
objects, reflecting the structural recursion criterion in the logic.

For vectors for example, the relation is defined as:

Inductive t_direct_subterm (A : Type) : forall n n0 : nat, vector A n -> vector A n0 -> Prop := t_direct_subterm_1_1 : forall (h : A) (n : nat) (H : vector A n), t_direct_subterm A n (S n) H (Vcons h H)That is, there is only one recursive subterm, for the subvector in the

The relation is actually called `t_subterm` as `vector` is just
a notation for `Vector.t`.
`t_subterm` itself is the transitive closure of the relation seen as
an homogeneous one by packing the indices of the family with the
object itself. Once this is derived, we can use it to define
recursive definitions on vectors that the guard condition couldn't
handle. The signature provides a `signature_pack` function to pack a
vector with its index. The well-founded relation is defined on the
packed vector type.

We can use the packed relation to do well-founded recursion on the vector.
Note that we do a recursive call on a substerm of type `vector A n` which
must be shown smaller than a `vector A (S n)`. They are actually compared
at the packed type `{ n : nat & vector A n}`. The default obligation
tactic defined in `Equations.Init` includes a proof-search
for `subterm` proofs which can resolve the recursive call obligation
automatically in this case.

For the diagonal, it is easier to give `n` as the decreasing argument
of the function, even if the pattern-matching itself is on vectors:

One can check using `Extraction diag'` that the computational behavior of `diag'`
is indeed not dependent on the index `n`.

To use the K axiom or UIP with `Equations`, one *must* first set an option
allowing its use during dependenet pattern-matching compilation.

By default we disallow the user of UIP, but it can be set.

The user must declare this axiom itself, as an instance of the `UIP` class.

In this case the following definition uses the `UIP` axiom just declared.

Note that the definition loses its computational content: it will get stuck on an axiom. We hence do not recommend its use.

Equations allows however to use constructive proofs of UIP for types
enjoying decidable equality. The following example relies on an
instance of the `EqDec` typeclass for natural numbers, from which
we can automatically derive a `UIP nat` instance. Note that
the computational behavior of this definition on open terms is not
to reduce to `p` but pattern-matches on the decidable equality
proof. However the defining equation still holds as a
*propositional* equality, and the definition of K' is axiom-free.