Permalink
Switch branches/tags
Nothing to show
Find file Copy path
Fetching contributors…
Cannot retrieve contributors at this time
93 lines (80 sloc) 3.66 KB
(* begin hide *)
Require Import Omega.
(* end hide *)
(** Whenever a user doesn't name a variable in an Ltac script, Coq
will automatically generate a fresh name for it. After doing some
proofs, however, you start to realize that this behavior is more of a
nuisance than a feature. The heuristics used by Coq when choosing new
names are hard to predict and depend on the current proof state,
making proofs likely to break whenever a small change is
introduced. As every experienced Coq user knows, trying to figure out
whether hypothesis [H22] now corresponds to [H9] or [H24] when fixing
a complicated proof script cannot exactly be described as a pleasant
experience, specially when the proof script is 2000 lines long and
you've spent hours dealing with similar horrors.
When writing robust proof scripts, one must ensure that the code
doesn't depend on weird automatically chosen names. Here are some tips
for making the naming problem disappear.
*** Name variables explicitly
Most of the times, you can get rid of this problem by not being lazy
and naming everything explicitly. Avoid using tactics like [intros] or
[destruct] in their unnamed form; instead, use [intros v1 v2 v3 ...]
or [destruct v as [a1 a2|a1 a2 a3|...]]. You can also name hypothesis
in the statement of your lemma, using a [forall] instead of a plain
implication arrow (remember, in Coq, these are actually the same
thing). If you don't pass any names to [intros], it will try to keep
the same names that appear in the current goal: *)
Lemma l1 : forall (A : Prop) (HYP : A), A.
Proof. intros. exact HYP. Qed.
(** This also works when reintroducing a variable from the context
into the goal, for instance with [generalize dependent].
*** Name constructor arguments
When working with complicated inductive predicates, naming all new
variables explicitly on every [destruct] or [inversion] can be
cumbersome. A reasonable compromise is to name all the arguments to
your constructors in inductive definitions. This makes the names that
are generated by those tactics meaningful, more stable and
predictable. Here's an example of a simple inductively defined
relation with explicit argument names: *)
Inductive collatz : nat -> nat -> Prop :=
| collatz_even (n m : nat)
(EVEN : 2 * m = n) : collatz n m
| collatz_odd (n m : nat)
(ODD : 2 * m + 1 = n) : collatz n (3 * n + 1)
| collatz_trans (n m p : nat)
(COLLATZnm : collatz n m)
(COLLATZmp : collatz m p) : collatz n p.
(** *** Don't refer to names in proofs
Weird automatically generated names are not a problem if they do not
appear in Ltac scripts. Automated proofs can obviously help here, but
there are small things you can do even if you're not an automation
expert. By using [match], you can avoid mentioning automatically
generated names without having to convert an unnamed [inversion] or
[destruct] into a named one: *)
Lemma collatz_cycle :
forall n m,
(n = 1 \/ n = 4 \/ n = 2) ->
collatz n m ->
m = 1 \/ m = 4 \/ m = 2.
Proof.
intros.
match goal with
| H : collatz _ _ |- _ => induction H
end.
- omega.
- repeat match goal with
| H : _ \/ _ |- _ => destruct H
end; omega.
- match goal with
| H1 : ?P,
H2 : ?P -> ?Q,
H3 : ?Q -> ?R |- ?R =>
apply H3; apply H2; apply H1
end.
Qed.
(** In the above (admittedly artificial) example, we were able to
refer exactly to what we wanted in the context without having to
resort to the names that Coq chose. Notice how in the third case we
were able to specify how premises and conclusions should match when
picking the hypotheses. In most cases, a simple [match] suffices to
remove explicit names from proofs. *)