Recitation 21

Now that the midterm project has passed, we’re back to the usual recitation format. This recitation covers lectures 20 and 21, that is, both lectures we’ve had on Coq.

  1. Write a sentence summarizing how we have used each of these tactics or tacticals 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
    • exact
    • intros
    • left
    • right
    • simpl
    • split
    • tauto
    • trivial
    • all
    • ;
    • -

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