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: a =?= b could in principle unfold all [reducible] layers of both a and b eagerly before proceeding. This is not currently done. Use-case: id (xs ++ ys) =?= id (id (xs ++ ys)) might just always unfold all the ids before proceeding, regardless of definitional depth or any other heuristic.

• A definition can be unfolded lazily during is_def_eq.

  Example: if g := f, then 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. Use-case: f1 (f2 ... (fN x)...) =?= f2 (f3 ... (fN x)) would only need to unfold f1 to confirm that the two are definitionally equal. This idiom is ubiquitous with type-class instances.

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

  Example: we may need to extract the universe level of a Sort in the app-builder.

• 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 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. Use-case: we want n + 1 =?= succ n to succeed even if + would never otherwise get reduced.

• 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 _ =?= _ 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 probably be conservative and the user should use exact if reductions are needed, or blast if the hypothesis in question contains system-generated names.

High-level desiderata

• Above all we want the delta strategy to be simple and stable enough that this cheat-sheet can exist, can be maintained, and can be understood.

• We want the strategy to be flexibly robust -- that is, we want the user to be able to say "I'll pay for the compute time, just please don't fail for some stupid reason relating to delta".

• When running in more performance-stingy contexts, we want it to be easy for the user to figure out what went wrong (what did not get unfolded in the right place) and figure out what annotations need to be tweaked or hints provided to address the problem.

Specific properties we want

• Any unification problem that can be solved in conservative mode should be solvable in liberal mode as well.

  Explanation: if liberal mode started unfolding things more aggressively from the beginning, it might no longer trigger an essential unification hint. Note that unification hints can involve "magic" solutions and are not subsumed by more aggressive unfolding. Solution: we keep an enum {conservative, liberal-next, liberal-now}. In various parts of the unifier, we check if (liberal-now) ..., and at the end of on_is_def_eq_failure, if we are liberal-next, we recurse with liberal-now. We may want to make this more graded, so that there are e.g. many different levels of liberalness.