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 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. This still seems brittle though. It would be more robust to lookup the [backward] rules for every term in the CC equivalence class of the goal.

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.

• Rely on lazy unfolding in the unifier as little as possible, and rely on eager unfolding + "monotonic" unfolding (+ cc) in blast as much as possible.

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.

First attempt at a strategy

Approach

• Four levels of reducibility, as there are now (not suggesting these names):

  • eager
  • lazy
  • liberal
  • never

• These reducibility levels can be associated with definitions as well as with reflexivity-simplification lemmas, and perhaps with [unfold <i1> ... <im>] annotations as well.

• The unifier does eager unfolding with the eager annotated definitions and reflexivity-simplification lemmas, and lazy unfolding with the lazy ones. In liberal mode, if it fails it considers lazy-unfolding/normalizing things with the liberal tag.

• Blast eagerly (and permanently) unfolds the eager ones, and monotonically unfolds the lazy ones. In liberal mode, if it fails it considers monotonically unfolding the liberal ones.

  Issue: there are many definitions that are likely to be tagged as lazy that blast has no business monotonically unfolding, e.g. those related to instances. There may need to be a [no-blast] annotation or something like it that means "don't bother monotonically instantiating me".

  Issue: If hints are provided, does blast still monotonically instantiate? That is, is monotonic instantiation treated as if the .def lemmas were tagged as [simp?] for ematching, and are ignored as are all other [simp?] lemmas when specific lemmas are passed as hints?

• relaxed-whnf is used as it is now, so that when Pi or Sort is needed we find it no matter what the annotations.

• [constructor] and recursor-normalization is done in tactics and blast actions and not in unification, details TBD.

• We may also need a conservative mode for unification (to be used during search, e.g. type class resolution) that does not even do lazy unfolding, and only considers the eager rules.

Example annotations

• definition left_inverse (g : B → A) (f : A → B) : Prop := ∀x, g (f x) = x

  Comments: it seems weird to make this [eager] and not allow blast to ever see it, because it is obviously a useful abstraction to humans. There is also useful lexical information in the name, that (a) makes the analogy to other variants of inverses more clear and (b) makes it much easier to locate informal proofs online. Suggested annotation: [lazy] Reason: There are not that many lemmas that use it, and the property it hides is not that complicated and very likely to be useful. We will very often want to atleast monotonically unfold it to expose the Pi.