Curry-Howard isomorphism definitions in Coq using fun

0
votes

I'm having some issues with defining in Coq, more specifically when defining using the CHI. I have managed to gain the understanding of basic principals but when I try to define this"

((A -> (A -> C)) * ((A -> C) -> A)) -> C :=

I get nowhere due to the fact it keeps telling me:
"Error: The type of this term is a product while it is expected to be "C".
I have already tried the usual tactics I have used earlier in my script and I'm convinced this has to be solved using the same methods (fun) however everything I seem to be trying ends in that error message. Any tips?

1
setdefinitioncoqisomorphismcurry-howard
It is hard to say what the problem could be; could you put the rest of your script in here, or a simplified version thereof? – Arthur Azevedo De Amorim
More infos would be great. It might be a problem of notation scope where * is interpreted as the multiplication on natural numbers. – Vinz
Are you looking for the selectors fst and snd defined on a product type? – Alexander Kogtenkov

1 Answers

0
votes

It seems you are defining a function that takes as input:

  • a function of type A -> (A -> C): given an object of type A, it gives back a function of type A -> C.
  • a function of type (A -> C) -> A: given a function of type A -> C, it gives back an object of type A.

You are trying to build an object of type C which I don't see how you will managed to do it. However you can build an object of type A by combining the two functions you have as input.

Hope it helps,

V.