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

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.