| Expression | Meaning | Prove it | Use it |
|---|---|---|---|
P -> Q |
implication | intro |
apply |
P /\ Q |
conjunction | split |
destruct |
P \/ Q |
disjunction | left, right |
destruct |
~ P |
negation | intro |
apply |
x = y |
equality | reflexivity, f_equal |
rewrite |
0 + 2 |
addition | simpl |
- |
n : nat |
natural numbers | constructor, exact 12 |
induction |
forall (x : A), B |
universal quantifier | intro |
apply, specialize |
exists (x : A), B |
existential quantifier | exists |
destruct |
Go to the corresponding lecture and do something like Ctrl + F to find where we introduce it and hopefully an explanation. If that isn’t enough (because we don’t explain it in enough detail), then please ask!
| Introduced in … | Tactics |
|---|---|
| Lesson 1 | intro, split, destruct,
apply, left, right,
exfalso, reflexivity, simpl,
induction, f_equal, assumption,
rewrite, specialize, intros |