Potential elaboration bug with `elabAsElim`

Stream: lean4

[Scott Morrison]

Calling refine' as below with a lemma marked as elabAsElim doesn't seem to be behaving correctly (on leanprover/lean4:nightly-2022-09-15):

/-- `Perm l₁ l₂` or `l₁ ~ l₂` asserts that `l₁` and `l₂` are Permutations
  of each other. This is defined by induction using pairwise swaps. -/
inductive Perm {α} : List α → List α → Prop
| nil   : Perm [] []
| cons  : ∀ (x : α) {l₁ l₂ : List α}, Perm l₁ l₂ → Perm (x::l₁) (x::l₂)
| swap  : ∀ (x y : α) (l : List α), Perm (y::x::l) (x::y::l)
| trans : ∀ {l₁ l₂ l₃ : List α}, Perm l₁ l₂ → Perm l₂ l₃ → Perm l₁ l₃

infixl:50 " ~ " => Perm

protected theorem Perm.refl : ∀ (l : List α), l ~ l
| []      => Perm.nil
| (x::xs) => (Perm.refl xs).cons x

@[elabAsElim]
theorem perm_induction_on {P : List α → List α → Prop} {l₁ l₂ : List α} (p : l₁ ~ l₂) (h₁ : P [] [])
    (h₂ : ∀ x l₁ l₂, l₁ ~ l₂ → P l₁ l₂ → P (x :: l₁) (x :: l₂))
    (h₃ : ∀ x y l₁ l₂, l₁ ~ l₂ → P l₁ l₂ → P (y :: x :: l₁) (x :: y :: l₂))
    (h₄ : ∀ l₁ l₂ l₃, l₁ ~ l₂ → l₂ ~ l₃ → P l₁ l₂ → P l₂ l₃ → P l₁ l₃) : P l₁ l₂ :=
  have P_refl : ∀ l, P l l := fun l => List.recOn l h₁ fun x xs ih => h₂ x xs xs (Perm.refl xs) ih
  Perm.recOn p h₁ h₂ (fun x y l => h₃ x y l l (Perm.refl l) (P_refl l)) @h₄

theorem perm_inv_core {a : α} {l₁ l₂ r₁ r₂ : List α} : l₁ ++ a :: r₁ ~ l₂ ++ a :: r₂ → l₁ ++ r₁ ~ l₂ ++ r₂ := by
  generalize e₁ : l₁ ++ a :: r₁ = s₁
  generalize e₂ : l₂ ++ a :: r₂ = s₂
  intro p
  revert l₁ l₂ r₁ r₂ e₁ e₂
  refine' @(perm_induction_on p _ (fun x t₁ t₂ p IH => _) (fun x y t₁ t₂ p IH => _) (fun t₁ t₂ t₃ p₁ p₂ IH₁ IH₂ => _))
  intro l₁ l₂ r₁ r₂ e₁ e₂
  -- Hypotheses include
  -- `e₁: l₁ ++ a :: r₁ = s₁`
  -- `e₂: l₂ ++ a :: r₂ = s₂`
  -- but these should be
  -- `e₁: l₁ ++ a :: r₁ = nil`
  -- `e₂: l₂ ++ a :: r₂ = nil`
  all_goals sorry

[Scott Morrison]

This can be readily minimized to

inductive Q {α} : List α → Prop
| nil   : Q []

@[elabAsElim]
theorem Q_induction_on {P : List α → Prop} {l₁ : List α} (p : Q l₁) (h : P []) : P l₁ :=
  Q.recOn p h

example {a : α} {l r : List α} : Q (l ++ a :: r) → Q (l ++ r) := by
  generalize e : l ++ a :: r = s
  intro p
  revert l r e
  refine' @(Q_induction_on p _)
  intro l r e
  -- Hypotheses include
  -- `e: l ++ a :: r = s`
  -- but this should should be
  -- `e: l ++ a :: r = nil`
  sorry

[Leonardo de Moura]

@Scott Morrison I cannot reproduce the errors above, could you please get the latest nightly build and try again?

[Leonardo de Moura]

elabAsElim instructs Lean to use a different approach/heuristic to compute the implicit motive (P in your example). However, the motive does not take the major premise p as a parameter, and this information is necessary for the current implementation. The following variant works

inductive Q {α} : List α → Prop
| nil   : Q []

@[elabAsElim]
theorem Q_induction_on {P : (s : List α) → Q s → Prop} {l₁ : List α} (p : Q l₁) (h : P [] .nil) : P l₁ p :=
  Q.recOn p h

example {a : α} {l r : List α} : Q (l ++ a :: r) → Q (l ++ r) := by
  generalize e : l ++ a :: r = s
  intro p
  revert l r e
  refine' @(Q_induction_on p _)