termination_by fails when recursive argument is provided by apply

[semorrison]

Prerequisites

• Put an X between the brackets on this line if you have done all of the following:
  • Checked that your issue isn't already filed.
  • Reduced the issue to a self-contained, reproducible test case.

Description

termination_by is failing to correctly identify the recursive arguments when they are provided by apply.
This is an attempt at minimising an issue seen in mathlib porting (where the arguments were provided by simp or rw).

Steps to Reproduce

set_option trace.Elab.definition.wf true

theorem ex1 (P : List α → Prop) (P_nil : P []) (P_cons : ∀ h t, P t → P (h :: t)) (x : List α) : P x :=
  match x with
  | .nil => P_nil
  | .cons h t => by
    apply P_cons
    apply ex1 P P_nil P_cons
termination_by ex1 P P_nil P_cons x => x -- fails with `failed to prove termination, possible solutions:`

-- `trace.Elab.definition.wf` said:
--   [Elab.definition.wf] replaceRecApps:
--     match x with
--     | [] => P_nil
--     | h :: t => P_cons h t ((ex1 P P_nil P_cons) t) 
-- Note the extra parentheses!

theorem ex2 (P : List α → Prop) (P_nil : P []) (P_cons : ∀ h t, P t → P (h :: t)) (x : List α) : P x :=
  match x with
  | .nil => P_nil
  | .cons h t => by
    apply P_cons
    apply ex2 P P_nil P_cons t
termination_by ex2 P P_nil P_cons x => x -- succeeds

-- `trace.Elab.definition.wf` said:
--   [Elab.definition.wf] replaceRecApps:
--     match x with
--     | [] => P_nil
--     | h :: t => P_cons h t (ex2 P P_nil P_cons t) 

Expected behavior:

I would hope both example succeed.

Actual behavior:

The first example fails. Note that in the trace output from replaceRecArgs there we have ((ex1 P P_nil P_cons) t) rather than just (ex2 P P_nil P_cons t) as in the successful second example.

I suspect this may be caused by metadata nodes, but my attempts to change how they are handled in Lean.Elab.WF.replaceRecApps didn't get anywhere so far.

Reproduces how often: Consistently

Versions

Lean (version 4.0.0-nightly-2023-06-20, commit a44dd71, Release)

Additional Information

Curiously

section ex3

variable (P : List α → Prop) (P_nil : P []) (P_cons : ∀ h t, P t → P (h :: t))

theorem ex3 (x : List α) : P x :=
  match x with
  | .nil => P_nil
  | .cons h t => by
    apply P_cons
    apply ex3
termination_by ex3 P P_nil P_cons x => x -- Curiously this version works!

end ex3

works just fine, even though we are still generating the recursive argument via apply.

[leodemoura]

Fixed.