Rename `norm_cast` to `pull_cast`?

Stream: mathlib4

[Jovan Gerbscheid]

I was looking at the tactic cheat sheet, and it says:

push/pull: move the given constant inwards/outwards
norm_cast: simplify the expression by moving casts outwards
push_cast: push casts inwards

This makes me wonder if norm_cast should be called pull_cast. I'm not saying that it should, but I'd be curious to hear what others think.

[Kenny Lau]

agreed

[Yury G. Kudryashov]

This is a Mathlib tactic, so I'm going to move this thread to #mathlib4 .

[Notification Bot]

This topic was moved here from #lean4 > Rename `norm_cast` to `pull_cast`? by Yury G. Kudryashov.

[Anne Baanen]

I am weakly in favour. Apart from the pain of renaming/deprecating everywhere, I can see the objection being that norm_cast defines a normal form (which also helps with knowing how to phrase declarations), while pull_cast would not.

[Anne Baanen]

That would not be a strong enough objection for me to block the change though.

[Jovan Gerbscheid]

norm_cast is a Lean core tactic, it was upstreamed in 2024: lean4#3322

[Yury G. Kudryashov]

Should I move it back?

[Floris van Doorn]

norm_cast also does some simplification , e.g. normalizing ↑n < ↑m to n < m. You can view that as "pulling the cast outside <, which just happens to make it go away", but I think the name norm_cast is also fine, given this "extra" normalization step.

[Floris van Doorn]

I'm not against the rename, but personally I don't think it's worth the effort, since I also like the current name.

[Ruben Van de Velde]

Yeah, I see the goal of norm_cast mostly as removing casts rather than pulling them

[Aaron Liu]

I think of removing casts and pulling casts as mostly the same thing

[Jovan Gerbscheid]

Note that the goal of push_neg is often just to remove a negation rather than pushing it.

[Ruben Van de Velde]

So should it be norm_neg?

[Jovan Gerbscheid]

Well, it is a macro for push ¬ _...

[Floris van Doorn]

it's funny to contrast the duality that pushing negations in allows you to cancel them and that pulling casts out allows you to cancel them.

[Jovan Gerbscheid]

If you push the cast in ↑(Fin.mk n ...) with push_cast it cancels the cast. So it isn't just norm_cast doing that.