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!