Использование `apply with` без указания имен параметров в Coq?

При использовании тактики Coq apply ... with все примеры, которые я видел, включают явное указание имен переменных для создания экземпляров. Например, дана теорема о транзитивности равенства.

Theorem trans_eq : forall (X:Type) (n m o : X),
  n = m -> m = o -> n = o.

To apply it:

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.

Спасибо.


coq coq-tactic
person tinlyx    schedule 06.10.2015    source источник

Ответы (2)


arrow_upward
6
arrow_downward

Вы можете конкретизировать лемму с помощью правильных аргументов. _ используется для всех аргументов, которые мы не хотим специализировать (потому что они могут быть выведены). @ требуется для специализации неявных аргументов.

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

arrow_upward
2
arrow_downward

Вы можете опустить имена подшивок после 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.

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

person Tiago Cogumbreiro    schedule 07.10.2015
comment
Спасибо. Это работает с одной промежуточной переменной. Но я также пробовал это с двумя промежуточными переменными apply ... with (x:=XX) (y:=YY). Но как только я удалю имена переменных x:=, y:=, (apply ... with (XX) (YY)), это больше не работает. Любые идеи? - person tinlyx; 08.10.2015