folding definitions

Stream: lean4

[Simon Hudon]

In Lean 3, there was a neat trick you could use to fold a definition in a proof. You could do rw [<- myDef]. In Lean 4, rw does not seem to be using equational lemmas anymore. Trying the same with simp, you could try simp only [<- myDef] which would give you:

invalid '←' modifier, 'myDef' is a declaration name to be unfolded

Furthermore, it seems like equational lemmas are now declared private so they're not readily available to reference directly in rw or simp. Is there a different way to get the same outcome?

[Leonardo de Moura]

Yes, rw is not using equational theorems yet. It is on the TODO list.

it seems like equational lemmas are now declared private

Yes, they are private, and they are generated on demand. Motivation: users that are using Lean as a programming language are not penalized with the performance overhead.

Is there a different way to get the same outcome?

You can force the equational theorems to be regenerated using the following hack.

macro "generate_eq_thms" declName:ident : command => `(section attribute [local simp] $declName end)

generate_eq_thms List.length

example {a : α} {as bs : List α} (h : bs = a::as) : as.length + 1 = bs.length := by
  rw [← List.length._eq_2]
  trace_state -- lhs was folded
  rw [h]

[Simon Hudon]

Nice, thanks! Is it legal to mention List.length._eq_2 in rw because you're in the same namespace or does become more generally available once you forced their generation?

[Leonardo de Moura]

does become more generally available once you forced their generation?

This one. The generate_eq_thms command is generating new private theorems, and they are visible in the current file.

[Simon Hudon]

Cool, thanks!

[Leonardo de Moura]

@Simon Hudon https://github.com/leanprover/lean4/commit/cf0ca026fb2ae24723f325de1cceaaeaeccf3001

[Simon Hudon]

Awesome! Thanks a lot!

[Simon Hudon]

One question about your implementation: any reason not to use getUnfoldEqnFor? as well, possibly as a fallback if getEqnsFor? doesn't turn up anything?

[Leonardo de Moura]

@Simon Hudon Not sure if people use stuff such as repeat rw [f]. If we also apply the unfold theorem, it may produce nontermination.
BTW, we have an unfold tactic in Lean 4 for applying the unfold theorems.

[Simon Hudon]

This might be a good place to borrow from ssreflect. It gives you a bunch of ascii decorations in rewrite and one of them is ! myLemma (or 3 ! myLemma). That should make repeat rw [f, g, h] less commonly necessary and gives you the opportunity, when using ! with a definition, to just refuse to use the unfold lemma.

[Leonardo de Moura]

@Simon Hudon I am bored today, but not bored enough to implement these decorations :)

[Simon Hudon]

Haha! I'm sure something better will come up! It's on my list anyway but nowhere near the top