RFC: `lift` tactic postprocessing

Stream: mathlib4

[Jakub Nowak]

What do you think about adding customizable postprocessing step to lift tactic (via [lift_postprocess] attribute and/or custom procs)?

For example, by appropriately tagging Int.ofNat_add_ofNat, Int.cast_ofNat_Int, and Int.ofNat_inj we could have the following rewrites done automatically:

import Mathlib

example (a b : ℤ) : a + b = 42 := by
  lift a to ℕ using sorry
  lift b to ℕ using sorry
  guard_target = Nat.cast a + Nat.cast b = (42 : ℤ)
  -- This should be done automatically by `lift` tactic.
  rw [Int.ofNat_add_ofNat a b]
  rw [← Int.cast_ofNat_Int]
  rw [Int.ofNat_inj]
  guard_target = a + b = (42 : ℕ)

[Jakub Nowak]

Note that we can't really use simp for that, as usually the simp-normal form is with coercions pushed downwards, while for lift_postprocess we want to push coercions upwards with the hope of eventually eliminating them.

[Ruben Van de Velde]

Is this different to what norm_cast does?

[Jakub Nowak]

Oh, I didn't know about norm_cast. I think that's what I wanted.
Can we make this tactic more discoverable? By e.g. mentioning it in lift description or adding it to hint?

[Jakub Nowak]

Maybe we can make lift call norm_cast automatically by default?

[Floris van Doorn]

You might be interested in the tactic cheatsheet on the learn page of the community website

[Floris van Doorn]

I don't think that it is a good idea to make lift call norm_cast by default. But of course, nothing is preventing you from defining a macro my_lift that does lift and then calls norm_cast.

[Eric Wieser]

I'm not sure automatically combining tactics is a good idea, since then it just makes it harder to reason about what each tactic does

[Snir Broshi]

I think that's a strange view considering many existing tactics do this, e.g. rw = rewrite+rfl, obtain = have+rintro, norm_num calls simp only I think, etc
Do you feel the same way about these or do they differ in some sense from lift calling norm_cast?

[Eric Wieser]

I see your point about rw; though note in that case we also have the uncombined version still; similarly for norm_num and norm_num1. obtain can't be expanded using rintro + have as far as I known.

[Kevin Buzzard]

rintro := intro + rcases, obtain := have + rcases

[Jireh Loreaux]

The suggestion for lift + norm_cast is a bit different, because it's basically asking for lift to become lift <;> norm_cast at *, which would affect the entire context.

[Snir Broshi]

Oh sorry I meant rcases

[Jireh Loreaux]

That global effect is the biggest reason I wouldn't want it to be combined.

[Jakub Nowak]

Jireh Loreaux said:

That global effect is the biggest reason I wouldn't want it to be combined.

I was thinking about it too. Maybe we could implement a smarter version of norm_cast that goes upwards from the given starting subexpression/subexpressions (i.e. where the lift was applied) and only applies cast normalization on these (without going downwards into subexpressions)?

[Jakub Nowak]

I've made PR that adds norm_cast to documentation of lift: #33987

[Yury G. Kudryashov]

Does it make sense to add lift +normalize option?

[Yury G. Kudryashov]

I don't know; for me, lift; norm_cast at * is good enough.

[Jakub Nowak]

Yury G. Kudryashov said:

Does it make sense to add lift +normalize option?

If it's just the same as lift ..; norm_cast at * then I guess not, and certainly it shouldn't be the default.