Когда сопоставление с образцом (с match goal with) в определенной пользователем тактике, мы можем использовать ?x, чтобы связать термин Галлина, чтобы позже мы могли обратиться к нему. Мы можем использовать несколько таких идентификаторов в одном предложении (... ?x ... ?y ...) или даже использовать один и тот же идентификатор (... ?x ... ?x ...), чтобы указать, что для совпадения предложения в этих двух позициях должен присутствовать один и тот же термин Gallina. В некотором смысле это ограничивает возможные совпадения с требованием «одинаковости». Это удобно, но было бы удобнее (так), чтобы иметь возможность выставить «другое» требование. Есть ли способ написать предложение соответствия в форме ... ?x ... ?y ..., где мы требуем, чтобы термины, связанные с ?x и ?y, различались?
Под различимым я не обязательно подразумеваю не равное, а просто другое (их имена [или представления] не совпадают). Например, скажем, у меня есть два условия a,b:C. Эти два термина могут быть равны в том смысле, что мы можем доказать утверждение a = b, но это не имеет значения для моих целей. Что отличает a и b друг от друга, так это то, что их имена разные.
Итак, могу ли я сопоставить с шаблоном, задав требование, что две мета-переменные ?x и ?y должны связывать разные термины?
Чтобы поместить это в некоторый контекст, скажем, мы определили пары, проекции и пусть R будет некоторым (соответствующим образом типизированным) двоичным отношением. Предположим, я каким-то образом в результате предположил следующие два.
H : R (proj1 (pair a b)) c
H' : R (proj1 (pair a b)) a
Я бы хотел написать в своей тактике предложение о совпадении, которое будет соответствовать только H, а не H'. Есть ли уловка для этого?
Если нет способа сопоставить только H, то, возможно, я мог бы сопоставить оба, где я связываю a с ?x и c (или снова a) с ?y. Но затем в правой части предложения о совпадении я хотел бы выполнить проверку " are-они-разные? " между x и y и выполнить idtac in В случае, если два связывают буквально одинаковые термины.