Coq Equality III
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
return clauses of the match
statement, which types the expression using the right hand side of the equality
instead of the left.
P is a predicate, i.e. it maps the value in the equality to a
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
Set-valued functions, and the fully general
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 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”
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
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!
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!