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 unfolding heuristics 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 ge [reducible] {A : Type} [s : has_le A] (a b : A) : Prop := le b a

  Suggested annotation: [eager] Reason: we want to "normalize" arithmetic expressions to only use le, and want to think about ge as notational convenience alone. Possible alternative: special purpose normalization for arithmetic expressions.

• 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 at least monotonically unfold it to expose the Pi.

  Issue: even if we wanted blast to monotonically unfold it, we may still want the unifier to eagerly unfold it. There might be benefits to being able to set the blast behaviour and the unifier behaviour separately, though the working hypothesis is that it would not be worth the extra complexity in annotations.

• definition weak_order.to_has_le : Π (A : Type) [s : weak_order A], has_le A

  Suggested annotation: [lazy]

  Comments: instances are the main use-case for lazy unfolding in the unifier.

  Issue: we don't want blast to monotonically unfold this. We floated the idea above of a no-blast tag for this purpose, though this may not be a great solution.

• definition id : Π {A : Type}, A → A

  Suggested annotation: [liberal], but with an [unfold_full] lemma tagged as [eager].

  Comments: we never want to see @id A a, we always want that simplified to a. On the other hand, we don't want to unfold @id A to fun a, a unnecessarily, yet still don't want unification to fail in liberal mode on @id A =?= fun a:A, a.

• definition add : Π {A : Type} [s : has_add A], A → A → A

  Suggested annotation: [never], but with unfold hints for concrete cases, e.g. add ?n ?m =?= succ ?k, and with a ton of special-purpose support for reasoning about add in other parts of the system.

  Comment: I doubt it but we may want more flexible unification hints. If all but one of the four arguments are constructor applications and the instance of add is computable, then we can solve the unification constraint with some cleverness.

• definition confluent := ∀ {x y1 y2 : A}, rtc R x y1 → rtc R x y2 → joinable R y1 y2

  Suggested annotation: [lazy]

  Reason: similar to left_inverse

• definition compact := ...

  Suggested annotation: [liberal]

  Reason: it is similar to confluent, except there are probably more useful properties that compact sets satisfy, so it makes sense to try to reason at the higher level of abstraction first before even bothering to monotonically unfold.

Issues

• For blast, the distinction between [lazy] and [liberal] is too close a call. They both get monotonically instantiated if necessary, and the only question is whether you try working with it unexpanded first, which you may as well always do. The right heuristic seems to be: if you have run out of things to instantiate at the unexpanded level, monotonically unfold. I think we will need to use learning to make more fine-grained ordering decisions.

• The tension between the unifier's interpretations of the annotations and blast's is awkward.

Second attempt at a strategy

Approach

• Still use the same annotations with the same meanings for definitions, refl-simp lemmas and [unfold <pos>] hints.

• Different (orthogonal) annotations for the unifier and for blast.

• Unifier annotations

  • definitional-depth (heuristic for lazy unfolding, example: instances)
  • aggressive (lazy unfold first despite low depth, example: id.unfold_full)
  • expensive (do not unfold unless some non-default flag is set; possibly in addition to one of the first two annotations)

• Blast annotations

  • unfold eagerly and permanently (example: ge)
  • monotonically unfold (treat .def as any other [simp?] lemma, example: right_inverse)

• Use learning to deal with the deluge of lemmas to instantiate in blast.

Issues

• These unifier annotations may not give us enough flexibility for "fast is_def_eq" as needed in search, e.g. type-class resolution. There is only one bit -- expensive vs not-expensive. We may want cheap / normal / expensive.

• There may still be some confusion due to indexing data structures. The trick discussed above for [backwards] mitigates the problem in some cases but not others. This seems unavoidable to me.

• Since blast would no longer be able to distinguish between "expensive" unfoldings and cheap ones, we would need to rely heavily on learning. A simple fix is to make the cheap vs normal vs expensive that we need for the unifier interpreted by blast as well, so that e.g. the cheap ones are always monotonically unfolded, the normal ones are considered regular lemmas for instantiation, and the expensive ones are not considered unless a flag is set.

• Question: does the unifier aggressive annotation correspond (almost) exactly to the blast eager annotation?

• What are the definitions we never want to unfold in blast, monotonically or otherwise? I want to say instances, but only because we normalize these in the simplifier, and because e-matching and other modules treat instances specially so cc doesn't need to match them.

Third attempt at a strategy

• Cost: cheap vs normal vs expensive
• Lazy strategy: depth-based vs aggressive
• Blast: eager vs monotonic