Helper function termination

Stream: lean4

[Leni Aniva]

I have this function which determines if a list is a sublist of another:

def mystery (src dst : List Nat) : MetaM Unit := do
  let m := src.length
  let n := dst.length

  let rec iter (iDst iSrc iOffset : Nat := 0)
    (map : Std.HashMap Nat Nat := .emptyWithCapacity src.length)
    : MetaM (Option (Std.HashMap Nat Nat)) := do
    if h_iSrc' : iSrc ≥ m then
      return map
    else if h_iDst' : iDst > n - m then
      -- Alignment failed
      return .none
    else if h_iOffset' : iSrc + iDst + iOffset ≥ n then
      -- Restart
      iter (iDst + 1) 0 0
    else
    let flag := src[iSrc] = dst[iSrc + iDst]

    if flag then
      -- We can advance one step forward
      iter iDst (iSrc + 1) iOffset map
    else
      -- Pairing is impossible
      iter iDst iSrc (iOffset + 1) map
  termination_by n - iDst
  let map? ← iter
  return ()

but when I tried to prove termination of iter (the decreasing measure is obviously wrong but just here for the sake of examples), Lean says:

unknown identifier 'n'

How can I prove termination of the function then? I noticed that if n shows up in the parameter list then there is no error.

[Kenny Lau]

why do you need meta?

[Leni Aniva]

Kenny Lau said:

why do you need meta?

this was extracted from another algorithm that requires MetaM

[Kenny Lau]

i might be wrong, but the standard practice seems to be either to use partial with meta, or to not use meta

[Kenny Lau]

sure, but meta can also call regular functions

[Leni Aniva]

Kenny Lau said:

i might be wrong, but the standard practice seems to be either to use partial with meta, or to not use meta

In Lean.Meta.Tactic.Apply, there is a similar case of MetaM with a termination proof, so I thought this would be possible to prove as well.

[Josh Clune]

Not a proper diagnosis of what's going on with this example, but I just wanted to comment that the error yielded by the example is surprisingly brittle.

In the original code, as Leni noted, Lean gives an unknown identifier 'n' error message. However, if any of the following variants are made, the error goes away and is replaced by the much more reasonable error that Lean is failing to prove termination:

• Replacing the line let flag := src[iSrc] = dst[iSrc + iDst] with let flag := src[iSrc] = dst[iSrc + iDst]! (just using getElem! instead of getElem).
• Replacing the line termination_by n - iDst with termination_by dst.length - iDst.
• Replacing the line let n := dst.length with have n := dst.length; have hn : n = dst.length := sorry.

No clue what to make of any of this beyond the fact that this behavior strikes me as decidedly strange, and I'd be interested if someone were able to explain what was causing this discrepancy.

[Leni Aniva]

Josh Clune said:

Not a proper diagnosis of what's going on with this example, but I just wanted to comment that the error yielded by the example is surprisingly brittle.

In the original code, as Leni noted, Lean gives an unknown identifier 'n' error message. However, if any of the following variants are made, the error goes away and is replaced by the much more reasonable error that Lean is failing to prove termination:

• Replacing the line let flag := src[iSrc] = dst[iSrc + iDst] with let flag := src[iSrc] = dst[iSrc + iDst]! (just using getElem! instead of getElem).
• Replacing the line termination_by n - iDst with termination_by dst.length - iDst.
• Replacing the line let n := dst.length with have n := dst.length; have hn : n = dst.length := sorry.

No clue what to make of any of this beyond the fact that this behavior strikes me as decidedly strange, and I'd be interested if someone were able to explain what was causing this discrepancy.

My initial hypothesis is that only arguments and variables introduced by have can show up in the termination_by, but then looking at Lean.Meta.Tactic.Apply, we have

    let rangeNumArgs ← if hasMVarHead then
      pure [numArgs : numArgs+1]
    else
      let targetTypeNumArgs ← getExpectedNumArgs targetType
      pure [numArgs - targetTypeNumArgs : numArgs+1]
    /-
    Auxiliary function for trying to add `n` underscores where `n ∈ [i: rangeNumArgs.stop)`
    See comment above
    -/
    let rec go (i : Nat) : MetaM (Array Expr × Array BinderInfo) := do
      if i < rangeNumArgs.stop then
        let s ← saveState
        let (newMVars, binderInfos, eType) ← forallMetaTelescopeReducing eType i
        if (← isDefEqApply cfg.approx eType targetType) then
          return (newMVars, binderInfos)
        else
          s.restore
          go (i+1)
      else

        let conclusionType? ← if rangeNumArgs.start = 0 then
          pure none
        else
          let (_, _, r) ← forallMetaTelescopeReducing eType (some rangeNumArgs.start)
          pure (some r)
        throwApplyError mvarId eType conclusionType? targetType term?
      termination_by rangeNumArgs.stop - i

[Leni Aniva]

I found out that if I explicitly provide the in-bound hypothesis src[iSrc]'hz where hz is derived from h_iSrc, then the error goes away as well. It seems like by not providing this hypothesis, there is some kind of variable elision going on

Nevermind it does not