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

Question

在使用 Coq apply ... 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 , 而不是 o或 n或其他一些名字 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.