在 Coq 中使用 `apply with` 而不给出参数名称？

Question

在使用 Coqapply ... with策略时，我看到的所有示例都涉及明确给出要实例化的变量的名称。例如，给定一个关于等式传递性的定理。

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

给apply它：

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

请注意，在最后一行中apply trans_eq with (m := 1).，我必须记住要实例化的变量的名称是m，而不是oorn或其他一些名称y。

对我来说，在定理的原始陈述中是否使用m n o或x y z是否使用应该无关紧要，因为它们就像虚拟变量或函数的形式参数。有时我不记得我在定义定理时使用的特定名称或其他人在不同文件中放置的名称。

有没有一种方法可以让我引用变量，例如通过它们的位置并使用类似的东西：

apply trans_eq with (@1 := 1)

在上面的例子中？

顺便说一句，我试过：apply trans_eq with (1 := 1).并得到Error: No such binder.

谢谢。

Answer 1

您可以使用正确的参数专门化引理。将_用于所有参数，我们不希望专攻（因为他们可以推断）。在@需要专门隐含参数。

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