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.