weaker rfl after rw

Stream: lean4

[Kevin Buzzard]

In Lean 3, the rw closed the goal. In Lean 4 it doesn't:

example (f : Y → Z) (g g' : X → Y) (h : g = g') : (f ∘ g) x = f (g' x) := by
  rw [h]
  -- ⊢ Function.comp f g' x = f (g' x)
  sorry

I'm interested in understanding why this happens because it just came up in the mathlib port and I suspect we'll be seeing it again. Is there some rule of thumb here about the change?

[Ruben Van de Velde]

Is this a change related to rfl or Function.comp? I feel like I've hit issues with comp before

[Kevin Buzzard]

Oh I don't know! In mathlib3 rw tries a "weak rfl", not daring to unfold too much, because we don't want a performance hit when it fails.

[Richard Copley]

There's another kind of difference in rw between Lean 3 and Lean 4:

example {x a : ℕ} (h : 0 < a) : x = x * (a - (a - 1)) := by
  rw [Nat.sub_sub_self h]
  -- ⊢ x = x * Nat.succ 0
  change x = x * 1
  rw [mul_one]

• In Lean 3, after the first rewrite the goal is x = x * 1 which can be finished with either simp or rw mul_one.
• In Lean 4, the goal becomes x = x * Nat.succ 0 instead. Then simp doesn't do anything and rw [mul_one] fails to match. My solution was to add the change call, after which either simp or rw [mul_one] will close the goal.

This isn't the same as your example, because rfl (reducible or not) won't close the goal at that point, in Lean 3 or in Lean 4. It's not necessarily a bug, or even a big deal, but it's another difference that might affect porting.

[Reid Barton]

That's an interesting difference, thanks for pointing it out.

[Reid Barton]

I think Kevin's original example is due to Function.comp no longer being reducible.

[Richard Copley]

In Kevin's example, in Lean 3, the rw changes (f ∘ g) x = f (g' x) to (f ∘ g') x = f (g' x) — an exact match, nothing to reduce — but in Lean 4 the result has Function.comp instead of ∘.

[Ruben Van de Velde]

Your issue is that you're abusing the le-lt defeq; sub_sub_self needs a 1 \le a argument

[Reid Barton]

Isn't ∘ notation for Function.comp? Though I don't know why it doesn't get pretty printed that way

[Ruben Van de Velde]

This works:

example {x a : ℕ} (h : 0 < a) : x = x * (a - (a - 1)) := by
  replace h : 1 ≤ a := h
  rw [Nat.sub_sub_self h]
  rw [mul_one]

[Richard Copley]

That replacement makes for a clearer argument than the one I came up with. Thanks.

[Reid Barton]

I agree this example with le/lt is marginally defeq abuse, but there are probably similar situations, which we wouldn't consider abuse, but where the result of rw is still spelled differently in Lean 3 and Lean 4.

[Reid Barton]

It seems like Lean 3 takes the spelling from the goal, while Lean 4 takes the one from the lemma to rewrite with.

[Ruben Van de Velde]

If you're keeping this code, I'd use one of these, fwiw:

  rw [←Nat.add_one_le_iff, zero_add] at h
  rw [pos_iff_ne_zero, ←one_le_iff_ne_zero] at h

(and wonder if we should have a custom lemma for it)

[Richard Copley]

Reid Barton said:

Isn't ∘ notation for Function.comp? Though I don't know why it doesn't get pretty printed that way

Right, I see. And I said "an exact match, nothing to reduce": that's not true at all. The goal is (f ∘ g') x = f (g' x), which is rfl but not an exact equality and not with_reducible rfl.