The Coq mailing list

[Alex Meyer <alex153 AT outlook.lv>]

Hello!

I have 2 questions that are based on the problem mentioned in my stackexchage question https://cs.stackexchange.com/questions/96533/how-to-transform-lambda-function-to-multi-argument-lambda-function-and-how-to-re which tries to implement in Coq the formal semantics of the natural language.

1) I have two functions with types is:(e->t)->(e->t) and IS:e->(e->t)->t and I wanted to know how can I rewrite lambda terms that uses 'is' into lambda terms, that uses 'IS'. The first reply to my stackexchange question gave answer that it is just re-currying. But I have great doubts that simple recurrying can change the type of functions in so important manner how it is required if one goes from 'is' to 'IS'. So - the question is - do I need there full higher-order rewrite of just currying is sufficient?

2) And the second question is - does Coq have some facilities to do such term rewrite as was mentioned in my first questions? As far as I know Coq, then Coq just compiles and confirms the proofs (terms) that were written by users, no code generation happens, at least in CoqIDE. But maybe there are some tools for higher-order term rewrite in Coq? Of course, the example (e.g. involving 'is' and 'IS') would be helpful.

Alex