autoParam cause `rw` not to unify

Stream: lean4

[Jireh Loreaux]

The following is a consequence of autoParam, and it can be a bit inconvenient. Is this a bug, or intentional for some reason? This affects both rw and simp.

theorem foo (m : Nat) (h : m.succ = 1 := by assumption) : m.succ = 1 := h

theorem foo' (m : Nat) (h : m.succ = 1) : m.succ = 1 := h

example (m : Nat) (h : m.succ = 1) : m.succ = 1 := by
  rw [foo'] -- succeeds, leaving the goal `⊢ m.succ = n`
  exact h

example (m : Nat) (h : m.succ = 1) : m.succ = 1 := by
  rw [foo _] -- succeeds, the autoParam fills the proof obligation

example (m : Nat) (h : m.succ = 1) : m.succ = 1 := by
  rw [foo]
  /-
  tactic 'assumption' failed

  m✝: Nat
  h: Nat.succ m✝ = 1
  m: Nat
  ⊢ Nat.succ m = 1
  -/

example (m : Nat) (h : m.succ = 1) : m.succ = 1 := by
  simp [foo _] -- succeeds, the autoParam fills the proof obligation

example (m : Nat) (h : m.succ = 1) : 1 + m.succ = 2 := by
  simp [foo] -- simp made no progress

[Jireh Loreaux]

bumping this thread because it seems it got lost in the weeds yesterday.

[Jannis Limperg]

Leo recently fixed some issues with autoParams in simp, so if you haven't tried this with a very recent nightly yet, that could be worth a shot.

[Kyle Miller]

I just tried it on a master branch from today, and it has the same errors

[Jireh Loreaux]

I updated the example because Leo pointed out that the right hand side has a metavariable

[Jireh Loreaux]

@Kyle Miller did you try it with the updated example above?

[Matthew Ballard]

I second Kyle’s findings.