Last time, we showed how to use
eq_ind to manually prove inequalities.
eq_ind is the
inductive principle automatically generated by Coq based on the inductive definition of
eq. In the spirit of our deep dive, let’s take a look at the underlying definition.
As we can see, the definition is actually quite trivial. We are only returning the
f argument. The “magic” is done by the
return clauses of the match
statement, which types the expression using the right hand side of the equality
instead of the left.
P is a predicate, i.e. it maps the value in the equality to a
There is no reason this must be the case. In addition to generating the inductive
principle “_ind”, Coq will also generate the corresponding recursive principle
Set-valued functions, and the fully general
If you squint at this type just right, it may start to look like substitution. Indeed,
we can use
eq_rect to perform rewriting by hand. Let’s try our hand at a simple
The problem is that Coq cannot deduce the argument
P: nat -> Type. We can easily solve
this by making it apparent in the goal. We do this with the
pattern tactic, “factoring out”
x by β-expansion.
Note that eq_rect doesn’t quite do what we want here, because it expects a hypothesis
of the form
?x = y, when our’s is in the form
y = ?x. Instead, we use
This is almost what we want, but the order of the arguments prevents us from giving the rewrite equality. We solve the problem by instead passing a function with the “new goal” argument stubbed out.
We did it!
Now that we think we know the general approach to rewriting, why don’t we try to properly generalize it by writing our own rewrite tactic?
To rewrite in the other direction, we return to
eq_rect. Note that
eq_rect has less
implicit arguments then
eq_rect_r, so confusingly we must add more holes
The core functionality is there, now we add in some convenient notation and error messaging.
This is almost just as good as the standard
rewrite tactic! The one thing we
haven’t done is handled rewriting in a hypothesis. This involves forward instead
of backwards reasoning, but the key ideas are the same. I’ll leave it as my first
suggested exercise to the reader.
Up next, inversion!