在 Coq 中使用“apply with”而不给出参数名称？
Using `apply with` without giving names of parameters in Coq?
在使用 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.
谢谢。
您可以使用正确的参数专门化引理。 _ 用于我们不想特化的所有参数（因为它们可以被推断）。 @ 是专门化隐式参数所必需的。
Example test: forall n m: nat,
n = 1 -> 1 = m -> n = m.
Proof.
intros n m.
apply (@trans_eq _ _ 1).
Qed.
您可以在 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.
我对你原来的例子做了一些改动以结束证明。
为什么这有效
要了解其工作原理，check the manual under Bindings：
Tactics that take a term as an argument may also accept bindings to
instantiate some parameters of the term by name or position. The
general form of a term with bindings is termtac with bindings where
bindings can take two different forms:
bindings::= (ident | natural := term)+
| one_term+
本例显示的是one_term形式，说明如下：
in the case of apply, or of constructor and its variants, only instances for the dependent products that are not bound in the conclusion of termtac are required.
这就是为什么只需要提供一个术语。
在使用 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.
谢谢。
您可以使用正确的参数专门化引理。 _ 用于我们不想特化的所有参数（因为它们可以被推断）。 @ 是专门化隐式参数所必需的。
Example test: forall n m: nat,
n = 1 -> 1 = m -> n = m.
Proof.
intros n m.
apply (@trans_eq _ _ 1).
Qed.
您可以在 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.
我对你原来的例子做了一些改动以结束证明。
为什么这有效
要了解其工作原理，check the manual under Bindings：
Tactics that take a term as an argument may also accept bindings to instantiate some parameters of the term by name or position. The general form of a term with bindings is termtac with bindings where bindings can take two different forms:
bindings::= (ident | natural := term)+ | one_term+
本例显示的是one_term形式，说明如下：
in the case of apply, or of constructor and its variants, only instances for the dependent products that are not bound in the conclusion of termtac are required.
这就是为什么只需要提供一个术语。