Как сделать переписывание терминов высшего порядка в Coq?

Question

Этот вопрос основан на моем вопросе https://cs.stackexchange.com/questions/96533/how-to-transform-lambda-function-to-multi-argument-lambda-function-and-how-to-re В этом вопросе есть две функции и два термина:

Функции:

is: (e->t)->(e->t)
IS: e->(e->t)->t

Условия:

(is(boss))(John): t
IS(John, boss): t

У меня такой вопрос: как переписать термины, включающие is, в термины, которые имеют только IS? Есть ли у Coq (или сторонних инструментов) такие возможности переписывания? Есть ли у Coq возможности проверить равенство переписанных терминов?

Может быть, такое переписывание может быть сделано за пределами мира Coq, может быть, есть другие инструменты чисто лямбда-исчисления только с синтаксической манипуляцией?

Answer 1

Не существует инструмента, который выполняет тот вид текстового преобразования кода Coq, который вы описываете напрямую. Не зная много о GrammaticFramework, я полагаю, что вам лучше всего написать сценарий Sed, который ищет вхождения is, примененные к аргументам, и заменяет эти вхождения эквивалентными выражениями IS.

Вторая форма «IS» может быть легче преобразована в предикат is-boss, поэтому я стремлюсь к ней прийти.

Я думаю, что если бы вы использовали скрипт Sed, вы могли бы так же легко перейти к форме IS_BOSS напрямую, без использования IS.