enthusiastic `push_cast`

Stream: mathlib4

[Heather Macbeth]

The following is resolved by push_cast in mathlib4, but not by push_cast in mathlib3. It would be convenient for me for teaching to have the mathlib3 behaviour, but before engaging in serious advocacy, I'd just like to understand it -- what is the reason for the difference?

example : (3:ℤ) ≤ 3 := by push_cast

[Moritz Doll]

Lean 4 is so fast that the tactics happily do more work:

example : (3 : ℤ) ≤ (3 : ℕ) := by
  simp only

[Moritz Doll]

push_cast is essentially a macro on top of simp

[Heather Macbeth]

Hmm, but simp only doesn't solve that in Lean 3 (where push_cast is also implemented on top of simp, IIRC).

I wonder if it's the decidability-checking feature of simp that is dealing with this? I'll try turning it off ...

[Heather Macbeth]

Yup!

push_cast (config := { decide := false })

has the mathlib3 behaviour.

[Moritz Doll]

ah that came up when Scott was using zify for linarith as well

[Heather Macbeth]

I even opened an issue for this (lean4#2068) after being surprised by it some other time.