unknown identifier `iff_self`, even without the lemma

Stream: lean4

[Jeremy Tan]

In lean4#5317 I rename 13 simp lemmas, including iff_self, to resolve a TODO in Mathlib.Init.Logic. But I am getting this error even though iff_self_eq (the renamed iff_self) is not in the lemma list:
Init/Data/Nat/Basic.lean:321:17: error: unknown constant 'iff_self'
| succ c ih => simp only [Nat.add_succ, Nat.sub_succ, ih]
Do I need to update stage0? If so, how can I do this locally?

[Jeremy Tan]

(The Mathlib TODO says -- FIXME: remove _iff and add _eq for the lean 4 core versions. Versions with _iff appended are in Mathlib.Init.Logic)

[Jeremy Tan]

More saliently @Kim Morrison: do you think the core simp lemmas should have the _eq appended or not? If the latter, then I should be able to simply deprecate the 13 lemmas under the TODO

[Kim Morrison]

I'm skeptical these really need a rename. Let's just deprecate in mathlib.

[Mario Carneiro]

The lean 4 core lemmas here are not written in the standard style, so I think they should not be squatting the nice names for the respective lemmas

[Mario Carneiro]

@Jeremy Tan yes this is a stage0 issue. simp contains a reference to iff_self directly in its code, via the simpOnlyBuiltins list. When you rename the theorem and try to compile lean core, you are still using the stage0 simp tactic to compile the Init library and this tactic doesn't realize that the theorem has been renamed. You might be able to do this in two stages where in the first stage you have iff_self and iff_self_eq both defined, and in the second stage (after compilation of the compiler is complete and simp is updated to use the new name) you can remove iff_self or change its statement

[Yaël Dillies]

Mario Carneiro said:

The lean 4 core lemmas here are not written in the standard style, so I think they should not be squatting the nice names for the respective lemmas

Same problem with docs#forall_congr which I would like to see renamed to forall_congr_eq so that we can unprime docs#forall_congr'

[Jeremy Tan]

Mario Carneiro said:

The lean 4 core lemmas here are not written in the standard style, so I think they should not be squatting the nice names for the respective lemmas

Kim said that the core lemmas should not be renamed, and I've already got #16721 in mathlib which deprecates the mathlib versions. Now what? Should I still press on with my core PR and rename forall_congr?

[Mario Carneiro]

it looks like most of #16721 can stand as is because when it is used in simp it doesn't matter if you use an equality or iff

[Mario Carneiro]

but in general I would say hold please until discussion is concluded

[Kim Morrison]

Some general principles for proposing renamings in the Lean repo:

1. Yes, I would like to know about things that are clearly named incorrectly, and I would like to fix them.
2. But I really don't want to spend time personally on discussions about whether things are named correctly.
3. So I'd prefer that renaming requests only happen when it is absolutely clear that #naming says the current name is wrong, and specifies what the name should be. (If this motivates improvements to #naming first, great!)
4. For now at least, I don't want to touch the Lean/elsewhere disagreement about "what constitutes a name fragment", so in particular let's not revisit the congr_arg / congrArg question.
5. I would be happy to have more precise rules about iff naming. Currently #naming only says sometimes omitted along with the right hand side of the iff, and it would be good to provide clearer guidance on "sometimes". (And until/unless this is clarified, point 3 above applies!)
6. I would prefer to avoid entirely the duplication of X_iff and X_eq lemmas by where possible replacing the = versions with iff versions, and would be happy to review PRs effecting this.

[Mario Carneiro]

I agree that (6) would be the best solution for this particular issue, there is no need for simp to have eq lemmas here in the first place