simp loop

Stream: mathlib4

[Kevin Buzzard]

import Mathlib.Data.Int.Basic

-- in `std` and tagged @[simp]
#check Int.ofNat_add_ofNat
/-
Int.ofNat_add_ofNat (m n : ℕ) : ↑m + ↑n = ↑(m + n)
-/
-- in `mathlib` and tagged @[simp]
#check Nat.cast_add
/-
Nat.cast_add.{u_1} {R : Type u_1} [inst✝ : AddMonoidWithOne R] (m n : ℕ) : ↑(m + n) = ↑m + ↑n
-/

example (a b : ℕ) : (a : ℤ) + (b : ℤ) = 37 := by simp -- hangs

[Kevin Buzzard]

(credit to @Bhavik Mehta who ran into this on the train from Duessoldorf and now has a flat laptop battery)

[Kevin Buzzard]

@Mario Carneiro Nat.cast_add was simp in Lean 3. Should simp be removed from Int.ofNat_add_ofNat?

[Yaël Dillies]

Or maybe the lemma should simply be turned around?

[Joachim Breitner]

Usually with simp lemmas, you want more primitive and unary operations to moved inside of less primitive and nary operations. So turning it around seems the right call, I'd say

[Kevin Buzzard]

My understanding that with lemmas like this, the simplifier is in fact ill-equipped to deal with the problem. Sometimes you want to push casts in and sometimes out. This is why we have norm_cast and push_cast. Because of this I've never quite known what to do with simp and lemmas like this. What works for one application might not work for another.

[Bhavik Mehta]

Just to be clear, is the suggestion to turn Int.ofNat_add_ofNat around, or Nat.cast_add? My vote is to turn the former around, and keep the latter as it is, and keep it simp

[Yaël Dillies]

Turn Int.ofNat_add_ofNat around. It's a distributivity lemma, and distributivity lemmas should have their RHS distributed.

[Bhavik Mehta]

Then we're in agreement :)

[Mario Carneiro]

The reason ofNat_add_ofNat is in the order it is is because this is one of four equational lemmas for Int.add

[Mario Carneiro]

so it should probably just be @[local simp]

[Jireh Loreaux]

What does local simp mean? Only until the current scope ends I guess (section, namespace or file)?

[Scott Morrison]

Haha, I had not read this thread, but had just independently decided to put local simp there, and just searched zulip thinking "surely someone has wanted this previously".

[Scott Morrison]

This gets done, amongst other things, in std4#261, with mathlib bump #7141

[Kevin Buzzard]

Thanks Scott! I was thinking of making a Std PR but realised I had no idea how to actually do this and also realised that even if I could make a change and get std compiling, this was no guarantee that I'd not broken mathlib. This and the imminent start of term stopped me from working on this...