Explain the correspondence between propositions and types. How is each of the following expressed in Coq, and what is a corresponding way of expressing it in OCaml?
Explain the correspondence between proofs and programs. Then, for each of the following propositions, determine its corresponding type in both OCaml and Coq, then write an OCaml and a Coq definition to give a program of that type, as we did above. Your program proves that the type is inhabited, which means there is a value of that type. It also proves the proposition holds.
- \((p \wedge q) \rightarrow (q \wedge p)\)
- \((p \vee q) \rightarrow (q \vee p)\)