Using `apply with` without giving names of parameters in Coq?

Question

In using the Coq apply ... with tactic, the examples I have seen all involve explicitly giving the names of variables to instantiate. For example, given a theorem about the transitivity of equality.

Theorem trans_eq : forall (X:Type) (n m o : X),
  n = m -> m = o -> n = o.

To apply it:

Example test: forall n m: nat,
  n = 1 -> 1 = m -> n = m.
Proof.
  intros n m. 
  apply trans_eq with (m := 1). Qed.

Note that in the last line apply trans_eq with (m := 1)., I have to remember that the name of the variable to instantiate is m, rather than o or n or some other names y.

To me, whether m n o or x y z are used in the original statement of the theorem shouldn't matter, because they are like dummy variables or formal parameters of a function. And sometimes I can't remember the specific names I used or somebody else put down in a different file when defining the theorem.

Is there a way by which I can refer to the variables e.g. by their position and use something like:

apply trans_eq with (@1 := 1)

in the above example?

By the way, I tried: apply trans_eq with (1 := 1). and got Error: No such binder.

Thanks.

Answer 1

You can specialize the lemma with the right arguments. The _ is used for all arguments that we don't want to specialize (because they can be inferred). The @ is required to specialize implicit arguments.

Example test: forall n m: nat,
  n = 1 -> 1 = m -> n = m.
Proof.
  intros n m. 
  apply (@trans_eq _ _ 1). 
Qed.

Answer 2

You can omit the binder names after with, so in your case do apply trans_eq with 1.

Example test: forall n m: nat,
  n = 1 -> 1 = m -> n = m.
Proof.
  intros n m.
  apply trans_eq with 1; auto.
Qed.

I've changed your original example a little to conclude the proof.

Why this works

To understand why this works, check the manual under Bindings:

Tactics that take a term as an argument may also accept bindings to instantiate some parameters of the term by name or position. The general form of a term with bindings is termtac with bindings where bindings can take two different forms:

bindings::= (ident | ​natural := term)+
           | one_term+

What is shown in this example is the form one_term, which is described as follows:

in the case of apply, or of constructor and its variants, only instances for the dependent products that are not bound in the conclusion of termtac are required.

Which is why only one term needs to be supplied.