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

```
Print eq_ind.
(* eq_ind =
fun (A : Type) (x : A) (P : A -> Prop) (f : P x) (y : A) (e : x = y) =>
match e in (_ = y0) return (P y0) with
| eq_refl => f
end
: forall (A : Type) (x : A) (P : A -> Prop),
P x -> forall y : A, x = y -> P
*)
```

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.

```
Check eq_rect.
(* eq_rect
: forall (A : Type) (x : A) (P : A -> Type),
P x -> forall y : A, x = y -> P y
*)
```

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.

```
Theorem one_gt_0: forall x, x = 1 -> x > 0.
Proof using.
intros * eq.
Fail eapply (eq_rect _ _ eq).
(* The command has indeed failed with message:
In environment
x : nat
eq : x = 1
Unable to unify "x = ?M160" with "1 <= x"
*)
```

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.

```
pattern x.
Check (eq_rect _ (fun n => n > 0)).
(* eq_rect ?x (fun n : nat => n > 0)
: ?x > 0 -> forall y : nat, ?x = y -> y > 0
where
?x : [x : nat eq : x = 1 |- nat
*)
```

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`

.

```
eapply (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.

```
Undo.
apply (fun new_goal => eq_rect_r _ new_goal eq).
```

We did it!

```
intuition.
Qed.
```

## 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?

```
Ltac is_in_goal x :=
match goal with
| |- context[x] => idtac
end.
Ltac rew_r H :=
match type of H with
| ?x = _ =>
(is_in_goal x + fail "Nothing to rewrite");
pattern x;
apply (fun new_goal => eq_rect_r _ new_goal H)
end.
Goal forall x, x = 1 -> x > 0.
intros * H.
rew_r H.
(* Looks good! *)
Abort.
```

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

```
Ltac rew_l H :=
match type of H with
| _ = ?y =>
(is_in_goal y + fail "Nothing to rewrite");
pattern y;
apply (fun new_goal => eq_rect _ _ new_goal _ H)
end.
Goal forall x, 1 = x -> x > 0.
intros * H.
rew_l H.
(* Awesome! *)
Abort.
```

The core functionality is there, now we add in some convenient notation and error messaging.

```
Ltac is_an_equality H :=
match type of H with
| _ = _ => idtac
end.
Tactic Notation "rew" "->" uconstr(H) :=
(is_an_equality H + fail "Not an equality");
rew_r H.
Tactic Notation "rew" "<-" hyp(H) :=
(is_an_equality H + fail "Not an equality");
rew_l H.
Tactic Notation "rew" hyp(H) :=
rew -> H +
rew <- H.
Goal forall x y: nat, x = y -> ~ x > y.
intros * eq.
rew eq.
Undo.
rew -> eq.
Undo.
rew <- eq.
assert (H: x = 1) by admit.
Fail rew <- H.
assert (H': x > 1) by admit.
Fail rew H'.
Abort.
```

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!