rewrite and simp fail to guess function argument

Stream: lean4

[Bhavik Mehta]

This is an instance in which Lean 3 rewrite and simp are able to close a goal, whereas neither succeed in Lean 4. This came up in the exponential ramsey project.
Lean 4:

theorem test {f : Nat → Nat} {c : Nat} : c ≠ 2 ∧ f c = 1 ↔ c = 1 ∧ f c ≠ 2 := sorry
example {n m : Nat} : m ≠ 2 ∧ n = 1 ↔ m = 1 ∧ n ≠ 2 := by simp [test] --succeeds, but fails to close the goal
example {n m : Nat} : m ≠ 2 ∧ n = 1 ↔ m = 1 ∧ n ≠ 2 := by rw [test] --fails

Lean 3:

theorem test {f : ℕ → ℕ} {c : ℕ} : c ≠ 2 ∧ f c = 1 ↔ c = 1 ∧ f c ≠ 2 := sorry
example {n m : ℕ} : m ≠ 2 ∧ n = 1 ↔ m = 1 ∧ n ≠ 2 := by simp [test] --succeeds
example {n m : ℕ} : m ≠ 2 ∧ n = 1 ↔ m = 1 ∧ n ≠ 2 := by rw [test] -- succeeds

[Bhavik Mehta]

It's unclear if this counts as a regression, since the "problem" is in some way that the theorem test isn't stated in the best way. But I'm recording it here anyway, in case the actual cause of this is more serious.

[Kevin Buzzard]

Are you suggesting that in Lean 3, rw [test] would succeed in actually manufacturing a function which sends m to n? Does just simp work in Lean 3? You don't need test to prove this of course.(you do now)

[Bhavik Mehta]

Oops, just simp does work in Lean 3, I think that's a sign I over minimised!

[Bhavik Mehta]

Amended, thanks for that. But, in Lean 3, rw [test] succeeds in making the function which is constantly m, which is enough to close the goal.

[Patrick Massot]

There are two separate issues. The first one is that simp and rw are not able to infer the f argument. The workaround is

example {n m : Nat} : m ≠ 2 ∧ n = 1 ↔ m = 1 ∧ n ≠ 2 := by
  simp [test (f := fun _ ↦ n)]

example {n m : Nat} : m ≠ 2 ∧ n = 1 ↔ m = 1 ∧ n ≠ 2 := by
  rw [test (f := fun _ ↦ n)]
  exact Iff.rfl

which both succeed. Then a completely separate issue is that rw calls the rfl tactic but that tactic works only for equalities, not iff. A workaround is to do:

macro_rules | `(tactic| rfl) => `(tactic| exact Iff.rfl)

example {n m : Nat} : m ≠ 2 ∧ n = 1 ↔ m = 1 ∧ n ≠ 2 := by
  rw [test (f := fun _ ↦ n)]

I think both issues should be raised (independently) on the Lean 4 repository, after checking they aren't already reported. Maybe Leo will say this shouldn't be fixed because that would be too slow or unpredicatable, but at least it would be documented.

[Bhavik Mehta]

Ah, I hadn't realised that even if f were guessed correctly, the rw would fail. I suppose I'm not so worried about the latter problem, seeing as in mathlib rfl already knows to try Iff.rfl. But I agree entirely with your analysis of the former problem.