I’ve used a few tactics in the
Crypto.v theory that I did not discuss in class. You do not need to understand any of them to use the theory. If you’re curious, all of them are in the Coq definition and/or used in Pierce or Chlipala. Here’s a list of basic descriptions to get you started if you want to learn more:
exists- like intro, but for existential quantifiers.
tauto- a tautology solver. Like omega, but for propositional logic statements.
refine- tell Coq to set up and attempt proofs that fill in holes (i.e.
_) in the associated definition.
You’ll also see significant usage of
; as presented in class. you don’t need to understand either one, but I did go through them briefly in class.