Recitation 22

  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)\)