RFC: f.eq_unfold lemmas

Proposal

For a function definition like Option.map we currently (well, for non-recursive only after #4154) create two kinds of rewrite lemmas 👍🏻

map.eq_<n>: Matches when map is fully applied and there are constructors (map f none = …)
map.eq_def: Matches when map is fully applied (map f x = match x with …)

Users can use this with simp or rw to control how aggressive the function should be unfolded. For example, rw [Option.map] will leave map x in place, but rw [Option.map.eq_def] will unfold it.

In this “algebra of rewrite specificity” there is a spot that we are missing and that might be useful:

map.eq_unfold: Matches every map, even under applied or under binders (map = fun f x => match x with …).

One particular use-case for this is to rewrite with rw under binders where that isn't possible with f.eq_def:


theorem Option.map.eq_unfold : @Option.map = fun {α : Type u1} {β : Type u2} (f : α → β) x => match x with | .some x => some (f x) | .none => none := by
  rfl

example : List.map (fun x => Option.map f x) xs = xs := by
  fail_if_success rw [Option.map]
  fail_if_success rw [Option.map.eq_def]
  rw [Option.map.eq_unfold]
  trace_state
  /-
  ⊢ List.map
    (fun x =>
      (fun {α β} f x =>
          match x with
          | some x => some (f x)
          | none => none)
        f x)
    xs =
  xs
  -/
  sorry

This would probably also have helped with #5026.

Naming

As always, naming is hard. Some options:

f.unfold -- clashes with too many existing theorems
f.const_eq
f.eq_spec -- goes well with .eq_def and .eq_n
f.def -- probably not, we had this name for what’s now f.eq_def and it broke too much.

Implementation

Various ways to skin the cat, specially with regard to the existing getUnfoldFor? machinery.

One plausible path of least disruption is to have a single (non-extensible) generator for f.eq_unfold that looks at f.eq_def to compute the lemma statement (by moving binders to the RHS), and then proves it by rfl if possible and else using funext and f.eq_def.

Future steps

Once this is in, I imagine it might be a worthwhile refactoring to make it so that only the generation of f.unfold is extensible (wf, structural, non-rec, maybe #3119), and then f.eq_def and f.eq_1 are generated by lean from that definition. More uniform, less code. This should not prevent those theorems to be proven by Eq.rfl if possible.

Community Feedback

Ideas should be discussed on the Lean Zulip prior to submitting a proposal. Summarize all prior discussions and link them here.

Impact

Add :+1: to issues you consider important. If others benefit from the changes in this proposal being added, please ask them to add :+1: to it.

leanprover / lean4