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
   : 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
   ?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.

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

We did it!



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

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)

Goal forall x, x = 1 -> x > 0.
  intros * H.
  rew_r H.
(* Looks good! *)

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)
Goal forall x, 1 = x -> x > 0.
  intros * H.
  rew_l H.
(* Awesome! *)

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

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.
  rew -> eq.
  rew <- eq.
  assert (H: x = 1) by admit.
  Fail rew <- H.
  assert (H': x > 1) by admit.
  Fail rew H'.

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!