1.10. Definitional equality

dsimp

The dsimp tactic is the definitional simplifier. It is similar to simp but only applies theorems that hold by reflexivity. Thus, the result is guaranteed to be definitionally equal to the input.

change

• change tgt' will change the goal from tgt to tgt', assuming these are definitionally equal.

• change t' at h will change hypothesis h : t to have type t', assuming assuming t and t' are definitionally equal.

unfold

• unfold id unfolds all occurrences of definition id in the target.

• unfold id1 id2 ... is equivalent to unfold id1; unfold id2; ....

• unfold id at h unfolds at the hypothesis h.

Definitions can be either global or local definitions.

For non-recursive global definitions, this tactic is identical to delta. For recursive global definitions, it uses the "unfolding lemma" id.eq_def, which is generated for each recursive definition, to unfold according to the recursive definition given by the user. Only one level of unfolding is performed, in contrast to simp only [id], which unfolds definition id recursively.

show

show t finds the first goal whose target unifies with t. It makes that the main goal, performs the unification, and replaces the target with the unified version of t.