Why can't rw do unfolding?

Stream: new members

[Dan Abramov]

I suspect that it's a very common beginner mistake to do rw [Foo] to unfold a let Foo := binding.

I've gotten used to doing simp only [Foo] or unfold Foo at this point, but this got me wondering — why not just allow it?

Clearly simp can do it, why not give this ability to rw too? Is there any fundamental reason why it's a bad idea, or is it historical?

[Aaron Liu]

implementation-wise, it's a bit different from any of the other things that rw does

[Dan Abramov]

Another related question is I often want to do the inverse of unfolding. I.e. I have some existing definition let Foo := bar baz and I have bar baz somewhere in the goal, and I wish it would just say Foo instead everywhere for clarity. I (think) I can achieve that by redeclaring with set like set Foo := bar baz but that's weird. What intuitively I want to write is rw [← Foo] in this case.

[Kyle Miller]

It's on the roadmap for the new rw :-)

I'm looking forward to rw [<- Foo] for some refolding as well.

[Kyle Miller]

(You beat me to hitting enter)

[Dan Abramov]

Super nice, looking forward to it!

[Julia Scheaffer]

Would this just do the same thing as rw [Foo.eq_def] and rw [<- Foo.eq_def]?

[Aaron Liu]

well Foo doesn't have an eq_def lemma since it's a local decl

[Aaron Liu]

example : 0 ≠ 1 := by
  let Foo := 0
  -- doesn't work
  rw [← Foo.eq_def]

[Julia Scheaffer]

Ah, makes sense now. Thanks

[Kyle Miller]

I think basically any question that goes "why can simp/rw do such-and-such which rw/simp can't" right now has the answer "we're working on a unified rewrite that can do what both do". At least as far as what can be rewritten. The simp tactic is meant for applying any rewrite rules that can apply, so it's got some fundamental differences. Still, every simp call should be translatable into some rw in the future.

[Kyle Miller]

@Dan Abramov Do you know about refold_let?

[Kyle Miller]

Was it you or someone else that complained about how unfold didn't work with let definitions? It used to be only possible with unfold_let or simp, but we changed unfold to handle let definitions too.

I wonder if there ought to be a low-level refold tactic that can handle both top-level definitions and let definitions? It might not be necessary with the new rw, but specialized low-level tactics can sometimes be nice to have.

[Alfredo Moreira-Rosa]

What would be nice also, is automatic unfolding up to a custom threshold, not necessarily visibility boundaries like opaque.
For ex, if i define

@[level 3]
def Foo := ....

Then it would be nice if simp +level 3 [...] would automatically unfold everything tagged with levels 1 to 3.

[Ruben Van de Velde]

TIL about the unified rewrite :)

[Dan Abramov]

Kyle Miller said:

Do you know about refold_let?

I did not! But I'm also not sure what it does (I did read the docstring several times but the meaning eludes me without an example, and trying to apply it in a few places seems to yield no result).

[Kyle Miller]

refold_let Foo should be like "rw [<- Foo]".

It's got some limitations, for example if Foo is a function it very likely won't work. It doesn't know how to un-beta-reduce. There are also some limitations with refold_let x at h; it won't refold if x was defined after h. I think you have to revert h; refold_let x; intro h or something similar.

[Kyle Miller]

There are a few examples of it in MathlibTest/DefEqTransformations.lean

[Dan Abramov]

Ah interesting, it seems to work at h when h is a hypothesis but not at other let bindings (which is often where I want it).

[Dan Abramov]

Might be something more subtle, I'll see if I can extract it next time I can't get it working.

[Kyle Miller]

(The revert trick is a good one to remember. It's often a way to make let values accessible to such tactics.)

[Kyle Miller]

The tactic definitely doesn't affect let values. It uses Mathlib.Tactic.runDefEqTactic, which only touches types.

There's no good reason that it doesn't. This is a gap in Lean's tactic design in general — it's unclear to what extent tactics are meant to operate on let values. Or, should they operate on just the value?

[Kyle Miller]

In Rocq it's possible to specify whether you want to rewrite the value or the type. Lean's at syntax doesn't have that specificity.

[Dan Abramov]

Ohhh I get it! I guess I haven't fully conceptualized that I'm usually rewriting types.

[Robin Arnez]

I actually wrote something that allows you to rewrite on values some time ago:

add_value, simp_value and conv_value tactics

import Lean

def forall_eq_of_let {c : α → Sort _} (h : let a := b; c a) : ∀ a, b = a → c a := by
  intro val
  exact Eq.ndrec h

abbrev Eq.recr.{u, u_1} {α : Sort u_1} {a : α} {motive : (b : α) → b = a → Sort u}
    (refl : motive a (Eq.refl a)) {b : α} (t : b = a) : motive b t :=
  t ▸ refl

open Lean Parser Elab Tactic
elab "add_value " hyp:term : tactic => do
  withMainContext do
    let u ← Meta.mkFreshLevelMVar
    let α ← Meta.mkFreshExprMVar (some (.sort u))
    let lhs ← Meta.mkFreshExprMVar α
    let rhs ← Meta.mkFreshExprMVar α
    let mut eq ← elabTermEnsuringType hyp (some (mkApp3 (mkConst ``Eq [u]) α lhs rhs))
    let mut goal ← getMainGoal
    unless eq.isFVar do
      goal ← goal.assert `h (mkApp3 (mkConst ``Eq [u]) α lhs rhs) eq
      let (eqVar, goal') ← goal.intro1
      eq := .fvar eqVar
      goal := goal'
    let eqVar := eq.fvarId!
    let mut symm := false
    let mut var := default
    if let .fvar v ← Meta.whnf lhs then
      var := v
      symm := true
    else if let .fvar v ← Meta.whnf rhs then
      var := v
      symm := false
    else
      Meta.throwTacticEx `add_value goal "expected variable on lhs"
    if ← var.isLetVar then
      Meta.throwTacticEx `add_value goal "variable already has a value"
    let reverted := #[var, eqVar]
    let (_, goal') ← (← getMainGoal).withReverted reverted fun goal fvars => goal.withContext do
      if fvars[0]! != var then
        Meta.throwTacticEx `add_value goal "unexpected error"
      if fvars[1]! != eqVar then
        Meta.throwTacticEx `add_value goal "invalid dependencies"
      let .forallE varNm t (.forallE _ (mkApp3 (.const ``Eq [univ]) _ lhs rhs) b _) _ ← goal.getType |
        Meta.throwTacticEx `add_value goal "unexpected goal state"
      let value := if symm then rhs else lhs
      if value.hasLooseBVars then
        Meta.throwTacticEx `add_value goal "recursive substitution"
      let newType : Expr := .letE varNm t value (b.instantiate1 (mkApp2 (.const ``rfl [univ]) t (.bvar 0))) false
      let newGoal ← Meta.mkFreshExprMVar newType
      let lvl' ← Meta.getLevel b
      let recNm := if symm then ``Eq.recr else ``Eq.rec
      let motive : Expr := .lam varNm t (.lam `h (mkApp3 (.const ``Eq [univ]) t lhs rhs) b .default) .default
      let newValue := mkApp4 (.const recNm [lvl', univ]) t value motive newGoal
      goal.assign newValue
      return ((), (fvars.map some).eraseIdx! 1, newGoal.mvarId!)
    replaceMainGoal [goal']

#print Lean.Parser.Tactic.simp

syntax "simp_value" optConfig (discharger)? (&" only")?
  (" [" withoutPosition((simpStar <|> simpErase <|> simpLemma),*,?) "]")? " at " ident : tactic

macro_rules
  | `(tactic| simp_value $cfg:optConfig $(disch)? $[only%$o]? $[[$args,*]]? at $i:ident) =>
    `(tactic| (
      clear_value (h : $i = _)
      simp $cfg:optConfig $[$disch]? $[only%$o]? $[[$args,*]]? at h
      add_value h
    ))

macro "conv_value" &" at " a:ident arrow:" => " c:Conv.convSeq : tactic =>
  `(tactic| (
    clear_value (h : $a = _)
    conv at h => rhs; conv =>%$arrow $c
    add_value h
  ))

example : ∀ a b, (h : 25 * 3 + b = a) → a < 4 → True := by
  intro a b h
  add_value h
  intro h
  conv_value at a => simp; rw [Nat.add_comm]

[Klaus Gy]

@Dan Abramov I asked a similar question recently, maybe you find something relevant in that thread: https://leanprover.zulipchat.com/#narrow/channel/113489-new-members/topic/rw.20works.20with.20defs.20but.20not.20with.20lets