使用`apply with`而不提供Coq中的參數名稱？

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. 

Answer 2

可以with後省略粘合劑的名字，所以你的情況做apply trans_eq with (1)。

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

我已經改變了你原來的例子，以便應用程序會請求缺少綁定。