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 :(
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)