COQ definition curry howard (A -> B -> C) -> (B -> A -> C) using sets

1
votes

I've been staring this in the face for hours not understanding :(

I need to solve some definitions using coq, and I am supposed to do it via the Curry Howard isomorphism. I have read up and still have no clue what I am doing. I have looked at other examples and tried doing it those ways and I always get errors.

For example, here I need to define this:

Variables A B C : Set.

Definition c01 : (A -> B -> C) -> (B -> A -> C) :=

this was my attempt:

fun g => fun p => g (snd p) (fst p).
end.

I also tried

fun f => fun b => fun a => f (b , a)
end.

Eventually it just says it was expecting a different type than what I gave, and sometimes it says things like: "expected to have type "?9 * ?10"."

Really struggling to grasp this after reading everything I could find.

Please could somebody explain :(

1
coqcurry-howard

1 Answers

1
votes

Well I guess you do not know how to read the types correctly.

c01's type is (A -> B -> C) -> (B -> A -> C). That means it is a function, which takes a function as argument and returns a function.

It takes "a function with two arguments" (I mean in the Haskell sense of "a function with two arguments", not in the Scala or Java sense), of type A and B, which returns a value of type C.

It must return a function with two arguments, of type A and B (but in the other order), which returns a value of type C.

So what must this function, c01, do?

It must take a function, and turn it into the same function with the order of its arguments reversed.

So:

fun f => fun b => fun a => f a b

Or equivalently (just adding some parentheses to make it clearer):

fun f => (fun b => fun a => f a b)