# rewriting is induction

When you have a type *T* and two elements *x, y : T* of the type, you can make a type, so called, equality (identity) type *eq T x y*. If you find a term of the type *t : eq T x y*, the term *t* will be an evidence that the two elements *x* and *y* are equal (hence called to be propositional equality). Equality is an inductive type with a constructor that gives a single rule making the evidence called reflexivity.

Being an inductive type, you can define your own equality type. In Coq:

```
Inductive myeq {T : Type} : T -> T -> Type :=
myrefl : forall x, myrefl x : myeq x x.
```

*myeq* is an inductive type that *depends* on a given type $T$ and two elements of the type. Its constructor is called *myrefl* that *depends* on the given type *T* and an element of it *x : T*. Hence, when such arguments are given, *myrefl* is used to construct the term *myrefl T x : myeq T x*.

For example, *myeq nat 42 42* is the type which represents the proposition *42 = 42* of natural numbers and a proof of the proposition is *myrefl nat 42 : myeq nat 42 42*.

Being an inductive type, *myeq* comes with an induction principle. The below is what Coq says for the type *myeq*:

```
myeq_ind
: forall (T : Type) (P : forall t t0 : T, myeq t t0 -> Prop),
(forall x : T, P x x (myrefl x)) -> forall (y y0 : T) (m : myeq y y0), P y y0 m
```

It roughly says that given any predicate on triples *(x, y, t)* where *x, y : T* and *t* is a proof that *x* and *y* are equal (*myeq x y* holds), in order to prove that the predicate is satisfied for all such triples, it suffices to only prove the case where the predicate acts on triples in form $(x, x, myrefl x)$.

If it isn’t clear why this is the induction principle for our equality, let us recall what the induction principle for natural numbers says. *nat* is an inductive type with two constructors *zero : nat* and *succ : nat -> nat*. The induction principle says that to prove a predicate *P* on all *x : nat*, it suffices only to prove the case where *x* is *zero* and the case where *x* is *succ n* assuming *P n* for any *n*.

Now, let us see how the induction principle works for rewriting. Rewriting for a predicate is in this form

```
forall (T : Type) (Q : T -> Prop) (x y : T) , myeq x y -> Q x -> Q y
```

and we want to prove it using the induction principle for *myeq*. Assuming a type *T : Type* and a predicate on it *Q : T -> Prop*, it is to prove *R := forall x y : T, myeq x y -> (Q x -> Q y)* where *(Q x -> Q y)* is a proposition. Hence, the *R* is a predicate on triples *(x, y, t)* where *t : myeq x y*. The induction principle on *myeq* says that in order to prove the predicate on such triples, it suffices to prove only the case where the predicate acts on *(x, x, myrefl x)* which is to prove *Q x -> Q x*.

In Coq, you can also check this either by

```
fun (T : Type) (Q : T -> Prop) (x y : T) (X : myeq x y) (H : Q x) =>
myeq_ind T (fun (x0 y0 : T) (_ : myeq x0 y0) => Q x0 -> Q y0) (fun (x0 : T) (H0 : Q x0) => H0) x y X H
: forall (T : Type) (Q : T -> Prop) (x y : T), myeq x y -> Q x -> Q y
```

or

```
Lemma myrewrite : forall (T:Type) (Q : T -> Prop) (x y : T), myeq x y -> Q x -> Q y.
Proof.
intros T Q x y t X.
induction t.
exact X.
Qed.
```

The HoTT book has a great explanation about identity types.