Recitation 24

  1. Write a sentence summarizing some of the tactics we’ve seen so far. All of them can be found in the notes, as well as in the Coq cheatsheet. (Note: it is notoriously hard to explain exactly what Coq tactics do. The point is to start developing your understanding, not to get a perfect or complete answer.)

    • apply
    • assumption
    • auto
    • contradiction
    • destruct [as]
    • discriminate
    • intros
    • left
    • right
    • simpl
    • trivial
    • all

  2. Explain in your own words the difference between classical and constructive logic.