Использование `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. 

Я немного изменил исходный пример, чтобы применить запрос на отсутствие привязки.