apply motive failure

Stream: lean4

[James Gallicchio]

mwe:

theorem natAbs_elim {motive : Nat → Prop} (i : Int)
  (hpos : ∀ (n : Nat), i = n → motive n)
  (hneg : ∀ (n : Nat), i = -↑n → motive n)
  : motive (Int.natAbs i)
  := by sorry

example (x : Int) (y : Nat) : x.natAbs < y := by
  apply natAbs_elim x
  sorry

Is there an easy way to get apply to find the correct motive here? I'm a bit disappointed that it doesn't just work, but ofc I have low expectations for an undecidable problem

[Mario Carneiro]

The way it's supposed to "just work" is to put @[elab_as_elim] on the theorem, but it doesn't work:

unexpected eliminator resulting type
  motive i.natAbs

[Mario Carneiro]

(I believe this is a regression relative to lean 3)

[James Gallicchio]

do you know if there's a gh issue for it? otherwise i'll go digging

[Mario Carneiro]

I don't think so

[James Gallicchio]

https://github.com/leanprover/lean4/issues/4086

[James Gallicchio]

Temporary workaround:

@[elab_as_elim]
theorem natAbs_elim {motive : Nat → Prop} {i : Int} (x : Nat)
  (hi : Int.natAbs i = x)
  (hpos : ∀ (n : Nat), i = n → motive n)
  (hneg : ∀ (n : Nat), i = -↑n → motive n)
  : motive x := by
  sorry

example (x : Int) (y : Nat) : x.natAbs < y := by
  generalize hn : x.natAbs = n
  refine natAbs_elim n hn ?_ ?_
  sorry

which I can wrap into a tactic easily enough. Maybe this is not an unreasonable request for elab_as_elim to support!

[James Gallicchio]

macro "elim_int_natabs" : tactic => do
  `(tactic| (
    generalize h : Int.natAbs _ = n at *
    refine Int.natAbs_elim n h ?_ ?_ <;> cases h
  ) )

example (x : Int) (y : Nat) : x.natAbs < y := by
  elim_int_natabs
  sorry

daily love for lean macros