coq - 在 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，而不是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.

谢谢。

score 6 · Accepted Answer

您可以使用正确的论点专门化引理。_用于我们不想专门化的所有参数（因为可以推断它们）。@需要专门化隐式参数。

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

score 3 · Accepted Answer

您可以在之后省略活页夹名称with，所以在您的情况下这样做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.

我已经稍微改变了你原来的例子来总结证明。

将术语作为参数的策略也可以接受绑定以通过名称或位置实例化术语的某些参数。带有绑定的术语的一般形式是带有绑定的 termtac，其中绑定可以采用两种不同的形式：
bindings::= (ident | natural := term)+
           | one_term+

本例所示为形式one_term，描述如下：

在 apply 或构造函数及其变体的情况下，只需要在 termtac 的结论中不受约束的依赖产品的实例。

这就是为什么只需要提供一个术语的原因。

2 回答 2