Delta Cheatsheet

Goal

This document aims to be a complete reference for when definitions do and do not get unfolded in Lean. It will take several weeks until it even begins to resemble such a document.

Different styles of unfolding

• A definition can be unfolded eagerly during is_def_eq.

  Example: is_def_eq(a, b) could in principle unfold all [reducible] layers of both a and b eagerly before proceeding. This is not currently done.

• A definition can be unfolded lazily during is_def_eq.

  Example: if g := f, then is_def_eq(f a, g a) could detect that the depth of g is larger than the depth of f and so unfold g first before proceeding.

• A definition can be unfolded because a Pi type or a Sort is expected or required.

• A definition can be unfolded if it matches a particular pattern.

  Example: we might have reflexivity-simplification rules for definitions that wrap recursors that only trigger if it is known which pattern in the definition matches.

• A definition can be unfolded because of a unification hint.

  Example: In is_def_eq(f, g), it might be the case that neither f nor g would normally be unfolded but that the pair (f, g) triggers a unification hint that causes one or both of them to be unfolded.

• A definition can be unfolded during normalization if it is fully applied.

  Example: compose has the [unfold_full] tag, and is unfolded during normalization if it is applied to all 3 arguments (i.e. compose f g x normalizes to f (g x)). Note that the number of arguments is not well defined in general and depends on the delta/normalization strategy being used. Also note that we can simulate this behaviour easily with a single reflexivity-simplification rule.

• A definition can be unfolded during normalization if a specified argument is a constructor.

  Example: pred : nat -> nat has the [unfold 1] tag and gets unfolded during normalization if its argument is zero or succ.

• A definition can be unfolded during normalization if it is if an outer application is expecting a constructor at that position.

  Example: pair has the [constructor] tag and so gets unfolded during normalization if an application of pair occurs in the major premise of pair.rec.

• A definition can be unfolded eagerly and permanently by blast.

  Example: blast currently unfolds every [reducible] definition appearing in the context during initialization. Most blast modules that track lemmas in the environment (e.g. the simplifier) also unfold [reducible] definitions eagerly in the lemmas that they track.

• A definition can be unfolded "monotonically" by blast.

  Example: given H : f x and f x := g x x, blast might add the hypotheses H' : g x x := H and HH' : H = H' := rfl. We call this monotonic because we have not lost the original folded version. Note that we can use reflexivity-simplification rules monotonically as well.

Complications

• Some data structures may be indexed by constant names or head symbols, and are hence inherently not robust to delta reduction.

  Example: if f := g but f is not eagerly reduced by blast, then a [backward] lemma H with result g would not be considered for a backwards action for goal f even if is_def_eq(f, g). Note that H would not be tried even if f were monotonically unfolded so that the context contained Hfg : f = g. However, H would fire if e.g. a subst action replaced the goal with g.

is_def_eq scenarios

• Sometimes we may expect is_def_eq to fail and want to prevent a lot of wasted unfolding.

  Example: if we are doing search

• Sometimes the user may say "I am willing to suffer a long delay if it turns out I am wrong about `is_def_eq(_, _) being true"

  Example: exact tactic

• Sometimes we know something is going to work, but we don't know what.

  Example: even though we know something is going to work, the assumption tactic might still not want to unfold aggressively in H1 : P (fact 100), H2 : P 0 |- P 0, or else risk wasting time computing fact 100. I think assumption should be probably conservative and the user should use exact if reductions are needed, or blast if the hypothesis in question contains system-generated names.