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.

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
;



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