[Coq-Club] Does Coq support higher-order rewrite of lambda terms?

[Alex Meyer]

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

[Pierre Courtieu]

Hi,

Below an example about uncurrying: a (trivial) proof that from any
function is we can build IS that takes a pair of arguments instead of
two arguments and returns the same result. An example of rewriting
(inside a proof) follows.

You seem to be willing to use the coq typing system as the typing
system of your expressions (shallow embedding). Are ou aware that you
can also define a deep embedding of your semantics?

What is your goal with this semantics?

Best regards,
Pierre

---------------------------8X---------------------------
Section uncurry.
Variable e t:Type.

Variable is:(e->t)->(e->t).

Definition IS (arg: (e*(e -> t))): t := let (x,f) := arg in is f x.

Lemma is_is_IS: forall x f, is f x = IS (x,f).
Proof.
reflexivity.
Qed.

(* After that in proofs you can always use tactic "rewrite is_is_IS"
to replace (is a b) by IS (b,a) and (or "rewrite <- is_is_IS" for the
reverse).
Example: *)

Variable P: t -> Prop.

Lemma foo: forall x f, P (is x f).
Proof.
intros x f.
rewrite is_is_IS.
...

End uncurry.
---------------------------8X---------------------------

Post by Alex Meyer
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