Rocq Cheat Sheet

Basic formulas, expressions and tactics

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

Tactic index

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

Inductive types

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:

When a parameter is always the same, including in arguments to a constructor then we say it is a uniform parameter.