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

Промених малко вашия оригинален пример, така че apply да изисква липсващо обвързване.

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