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.
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.