Recitation 25

1. 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?

   • implication
   • conjunction

   • disjunction

2. 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)$