How to do higher-order term rewriting in Coq?

Question

This question is based on my question https://cs.stackexchange.com/questions/96533/how-to-transform-lambda-function-to-multi-argument-lambda-function-and-how-to-re There are two functions and two terms in that question:

Functions:

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

Terms:

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

My question is this: how to rewrite terms involving is with terms that have only IS? Does Coq (or third party tools) has such rewriting facilities? Does Coq have facilities to check the equality of rewrittern terms?

Maybe such rewriting can be done outside the Coq world, maybe there are other purely lambda calculus tools with syntactic manipulation only?

Answer 1

There is no tool that performs the kind of textual transformation of Coq code you are describing directly. Without knowing much about GrammaticalFramework, I imagine that your best bet would be to write a Sed script that looks for occurrences of is applied to arguments and replaced those occurrences by equivalent expressions with IS.

The second “IS“ form can be more easily converted to is-boss predicate, that is why I am striving to arrive at it.

I think that if you used a Sed script you could just as easily go to the IS_BOSS form directly, without using IS.