recursive definitions fail if recursive calls appear in the types of matchers

Prerequisites

[x] 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

In the following code (sorry, tried to make it even smaller, but couldn't), a "failed to prove termination" error shows up in the definition of variable asdf, despite that the statement proving well-foundedness of the call is directly above in hereIAm.

The error disappears when the line containing aaLtA is commented out, or extracted to another function, which provides a workaround.

As probably a separate issue, when I try to inline asdf, Lean won't even notice the variable hereIAm (it won't be shown among other defined variables in the error description).

open Classical

def least (s: T → Prop) (nonempty: { t: T // s t }): T := sorry

structure WellOrder where
  T: Type
  lt: T → T → Prop
  wf: WellFounded lt

instance (w: WellOrder): WellFoundedRelation w.T where
  rel := w.lt
  wf := w.wf

namespace WellOrder
  @[reducible] def succ.lt (w: WellOrder): (a b: Option w.T) → Prop
    | none, _ => False
    | some _, none => True
    | some a, some b => w.lt a b

  def succ (w: WellOrder): WellOrder :=
    {
      T := Option w.T,
      lt := succ.lt w,
      wf := sorry
    }

  noncomputable def Morphism.initial.helper
    {wa wb: WellOrder}
    (aSucc: wa.succ.T)
    (fA: wa.T)
  :
    wb.T
  :=
    -- If I inline this, Lean won't even notice the variable
    -- `hereIAm` at all.
    let asdf (aa: { aa: wa.T // wa.succ.lt (some aa) aSucc }) :=
      let hereIAm: wa.succ.lt (some aa.val) aSucc := aa.property
      initial.helper (some aa)

    if hEq: some fA = aSucc then
      least
        (fun b =>
          ∀ aa: { aa: wa.T // wa.succ.lt (some aa) aSucc },
            (asdf aa) aa.val ≠ b)
        ⟨
          sorry,
          fun aa eq =>
            -- If the next line is commented out, or extracted
            -- to a separate function, the error disappears.
            let aaLtA: wa.lt aa fA := hEq.symm ▸ aa.property
            sorry
        ⟩
      else sorry
    termination_by initial.helper a fA => a
end WellOrder

Steps to Reproduce

Paste the above code to VS Code.

Expected behavior: Termination is proven.

Actual behavior: An error shows up.

Reproduces how often: Always.

Versions

Both Lean 4 stable and nightly Lean (version 4.0.0-nightly-2022-09-14, commit fccb60fb69be, Release), Lean (version 4.0.0, commit 7dbfaf9b7519, Release)

Ubuntu 22.04.1 LTS

In the following code (sorry, tried to make it even smaller, but couldn't), a "failed to prove termination" error shows up in the definition of variable asdf, despite that the statement proving well-foundedness of the call is directly above in hereIAm.

I see this goal:

failed to prove termination, possible solutions:
  - Use `have`-expressions to prove the remaining goals
  - Use `termination_by` to specify a different well-founded relation
  - Use `decreasing_by` to specify your own tactic for discharging this kind of goal
wawb: WellOrder
aSucc✝: wa.succ.T
fA✝: wa.T
a✝: (y : (_ : wa.succ.T) ×' wa.T) →
  (invImage (fun x => PSigma.casesOn x fun aSucc fA => aSucc) (instWellFoundedRelationT wa.succ)).1 y ⟨aSucc✝, fA✝⟩ →
    wb.T
asdf: { aa // wa.succ.lt (some aa) aSucc✝ } → wa.T → wb.T := fun aa =>
  let hereIAm := ⋯;
  fun fA => a✝ ⟨some aa.val, fA⟩ ⋯
hEq: some fA✝ = aSucc✝
aa✝: { aa // wa.succ.lt (some aa) aSucc✝ }
eq: asdf aa✝ aa✝.val = sorryAx wb.T
h✝¹: some fA✝ = aSucc✝
h✝: wa.succ.lt (some aa✝.val) aSucc✝
aSucc: wa.succ.T
aa: { aa // wa.succ.lt (some aa) aSucc }
hereIAm: wa.succ.lt (some aa.val) aSucc := aa.property
fA: wa.T
⊢ wa.succ.lt (some aa.val) aSucc✝

Note that the goal wants aSucc✝, which is shadowed by aSucc, and hereIAm is about aSucc not aSucc✝. I have not idea why the let below would introduce a new aSucc binding here.

Turning let asdf into have asdf also makes the issue go away. So it’s likely due to some beta-reduction somewhere.

I found a much smaller, and sorry-free code that may be related. Here, the issue is also termination checking, and it goes away if I comment out a piece of code that, I suppose, is capable of rewriting the context in a way similar to ▸.


def foo (_: True): Prop := True

def bar (n: Nat): True :=
  match n with
  | Nat.zero => trivial

  | Nat.succ nPred =>
    let asdf: foo (bar nPred) := trivial
    -- Commenting out the next line hides the issue.
    let ⟨⟩ := asdf
    trivial

The error:

failed to prove termination, possible solutions:
  - Use `have`-expressions to prove the remaining goals
  - Use `termination_by` to specify a different well-founded relation
  - Use `decreasing_by` to specify your own tactic for discharging this kind of goal
nPred: Nat
x✝: ∀ (y : Nat), (invImage (fun x => x) instWellFoundedRelationOfSizeOf).1 y nPred.succ → True
asdf: foo ⋯ := trivial
n: Nat
⊢ n < nPred + 1

Thanks for minimizing. Writing

def bar (n: Nat): True :=
  match n with
  | Nat.zero => trivial

  | Nat.succ nPred =>
    let asdf: foo (bar nPred) := trivial
    -- Commenting out the next line hides the issue.
    let ⟨⟩ := asdf
    trivial
decreasing_by done

I see two goals, namely

unsolved goals
nPred: Nat
x✝: ∀ (y : Nat), (invImage (fun x => x) instWellFoundedRelationOfSizeOf).1 y nPred.succ → True
⊢ (invImage (fun x => x) instWellFoundedRelationOfSizeOf).1 nPred nPred.succ

nPred: Nat
x✝: ∀ (y : Nat), (invImage (fun x => x) instWellFoundedRelationOfSizeOf).1 y nPred.succ → True
asdf: foo (x✝ nPred ?m.202) := trivial
n: Nat
⊢ (invImage (fun x => x) instWellFoundedRelationOfSizeOf).1 n nPred.succ

The first one seems to corresponds to the type of the let binding, and is fine (nPred is mentioned).

The second one comes from

match asdf with | True.intro => trivial

which, if we disable pp.match, reads like this

bar.match_1 bar nPred (fun (asdf : foo (bar nPred)) => True) asdf fun (_ : Unit) => trivial

with

bar.match_1 : ∀ (bar : Nat → True) (nPred : Nat) (motive : foo (bar nPred) → Prop) (asdf : foo (bar nPred)),
  (Unit → motive True.intro) → motive asdf

and after the translation we get

          bar.match_1
            (fun (n : Nat) =>
              x n
                (sorryAx
                  ((@invImage Nat Nat (fun (x : Nat) => x) (@instWellFoundedRelationOfSizeOf Nat instSizeOfNat)).1 n
                    nPred.succ)
                  true))
            nPred
            (fun
                (asdf :
                  foo
                    (x nPred
                      (sorryAx
                        ((@invImage Nat Nat (fun (x : Nat) => x) (@instWellFoundedRelationOfSizeOf Nat instSizeOfNat)).1
                          nPred nPred.succ)
                        true))) =>
              True)
            asdf fun (_ : Unit) => trivial)

where the sorryAx comes from the failing decreasing_by done.

So the problem is that the match construction yielding to bar.match_1 abstracts the free variables, including bar, it seems. This means we have an unsaturated call to bar, and there is no chance to proof that terminating.

If the matcher would abstract over bar_nPred together and have the type

bar.match_1 : ∀ (bar_nPred : True) (motive : foo bar_nPred → Prop) (asdf : foo bar_nPred),
  (Unit → motive True.intro) → motive asdf

then things would be well. Alternatively, we could try to unfold the matcher in this construction, although that is likely to blow up the proof term size.

The code to improve to abstract over each applications of free variables separately would be in Lean.Meta.Closure.mkValueTypeClosure.

A work-around is to let-bind the recursive call, on its own, yourself:

def bar (n: Nat): True :=
  match n with
  | Nat.zero => trivial
  | Nat.succ nPred =>
    let bar_nPred := bar nPred
    let asdf: foo bar_nPred := trivial
    let ⟨⟩ := asdf
    trivial

Given that the work-around exists, and it may be hard to fix, maybe not too pressing.

Just for reference, I found another small piece of code that might be worth looking into if someone ever decides to dedicate their time to this. This time, there isn't any recursion involved at all.

structure Asdf where
  T: Type
  t: T

def foo (asdf: Asdf) :=
  let ⟨T, _⟩ := asdf

  let a: asdf.T := asdf.t
  let b: T := asdf.t

  42

It seems that extracting a member of a structure with ⟨⟩ and a member access operator, though it naively ought to be the same, are quite different operations.

The error:

type mismatch
  asdf.t
has type
  asdf.T : Type
but is expected to have type
  T : Type

I think this is unrelated, and probably an instances of the issue described in https://github.com/leanprover/lean4/issues/5216

leanprover / lean4