rw works with defs but not with lets

Stream: new members

[Klaus Gy]

im trying to move a series of defs and lemmas inside a theorem. i noticed that the rw tactic can work with defs (it treats def N x := T as equality N x = T), but when turning the defs into lets, this no longer works. note that unfold also is not of help here, bc this unfolds the name everywhere, but i just need it to unfold the lhs. what does work is let N_eq : N x = T := rfl and then use N_eq inside rw instead, would it be possible to improve rw on that?

[Kyle Miller]

#mwe please?

[Robin Arnez]

I assume

example : let x := 5; x = 5 := by
  intro x
  rw [x] -- fails

right?

[Robin Arnez]

This works but isn't nice:

example : let x := 5; x = 5 := by
  intro x
  rw [show x = value_of% x from rfl] -- works

[Klaus Gy]

I think I understand now why it's tricky. rw tries to fill in placeholder arguments, so foo is already treated as e.g. foo _ _ if it takes two arguments, now if we have something like foo x : x = y := bar x y then foo in rw already expands to foo _, making it additionally expand to the equation foo x = bar x y would overload it I fear.

[Kyle Miller]

Still, could you give a #mwe? Especially one with an example that illustrates why unfold does not help?

[Klaus Gy]

/-- doesnt work -/
def myDef : Nat :=
  let foo x y := x + y
  let bar x y := x + y
  have {x y : Nat} : foo x y = bar x y := by rw[foo, ← bar]
  1

/-- works -/
def myDef' : Nat :=
  let foo x y := x + y
  let fooEq x y : foo x y = x + y := rfl
  let bar x y := x + y
  let barEq x y : bar x y = x + y := rfl
  have {x y : Nat} : foo x y = bar x y := by rw[fooEq, ← barEq]
  1

def foo (x y : Nat) := x + y
def bar (x y : Nat) := x + y

/-- this works as well -/
def fooEqBar (x y : Nat) : foo x y = bar x y := by
  rw[foo, ← bar]

[Klaus Gy]

in this case i could use unfold, but i had a more complicated situation where i didnt want to unfold the term on the rhs, just on the lhs.

[Kyle Miller]

If you want to isolate where you unfold, you can always use conv mode, like conv => enter [1]; unfold foo

[Klaus Gy]

thank you, that is helpful!

[Kyle Miller]

There's also a new feature you can use to make equations for your lets:

def myDef' : Nat :=
  let (eq := fooEq) foo x y := x + y
  let (eq := barEq) bar x y := x + y
  have {x y : Nat} : foo x y = bar x y := by rw[fooEq, ← barEq]
  1

[Klaus Gy]

aah very sweet!