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