# Coq Equality III

## Rewriting

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 `in`

and `return`

clauses of the match
statement, which types the expression using the right hand side of the equality
instead of the left.

Notice that `P`

is a predicate, i.e. it maps the value in the equality to a `Prop`

.
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
“_rec” for `Set`

-valued functions, and the fully general `Type`

-recursive principle
“_rect” for `Type`

-valued functions.

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
theorem.

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”
the `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 `eq_rect`

’s
sibling, `eq_rect_r`

.

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!

# Automation

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!