The Coq mailing list

[Pierre Courtieu <pierre.courtieu AT gmail.com>]

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---------------------------
Le jeu. 23 août 2018 à 22:18, Alex Meyer 
<alex153 AT outlook.lv>
 a écrit :
>
> 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