| 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 |
| Exercises 1 | assert, specialize, unfold,
contradiction, symmetry, lia |
| Lesson 2 Part 1 | change, discriminate, intros,
assumption, inversion,
generalize |
| Exercises 2 — 1 | constructor |
| Lesson 2 Part 2 | remember, subst,
induction … using, exists |
| Exercises 2 — 2 | replace |
| Lesson 3 Part 1 | refine |
| Lesson 3 Part 2 | exact, pose, cbn,
cbv |
| Exercises 3 | pattern |
| Lesson 4 | instantiate, repeat, auto,
tauto, eexists, eapply,
eassumption, eauto |
| Lesson 5 | congruence, now, erewrite,
revert, fix, clear,
firstorder |
Here is a summary of what an inductive type is, what are parameters and what are indices (singular: index).
Inductive ind (par1 : type1) (par2 : type2) : index_type1 -> index_type2 -> Sort :=
| ctor1 (arg1 : arg_type1_1) (arg2 : arg_type1_2) : ind par1 par2 val_index1_1 val_index1_2
| ctor2 (arg1 : arg_type2_1) (arg2 : arg_type2_2) (arg3 : arg_type2_3) : ind par1 par2 val_index2_1 val_index2_2.An inductive type has:
ind,par1 and par2, to the left of the colon
(:),index_type1 and
index_type2, to the right of the colon,Type or
Prop),ind p1 p2 i1 i2
where potentially the parameters p1 and p2
differ from par1 and par2,ind par1 par2 i1 i2 where
the parameters have to be the same as those in the declaration,
namely par1 and par2.When a parameter is always the same, including in arguments to a constructor then we say it is a uniform parameter.