let ← is not a definition

Or the deceptive appearance of the do notation.

Proof is cheap. Show me the proof.

Does this function terminate?

def f (xs : List Nat) : Except String Nat := do
  let tail ← do
    match xs with
    | [] => Except.error "empty"
    | _ :: tail => Except.ok tail
  f tail

Before you answer, I should note that this pattern do come up in real problems. This specific one is a distilled version of a mutually recursive parser, where the recursive f tail calls into other parser functions.

Now, to answer the original question: it does terminate. The proof is as follows: the only case where tail gets bound is when the list xs is not empty. In this case, the bound tail is the tail of xs and thus its length is smaller than xs.

Good. Next question: how do you write down this proof in Lean? The surprising answer is that you can’t, at least not in this form. Let’s give it a try and see where it breaks down.

def f (xs : List Nat) : Except String Nat := do
  let tail ← do
    match xs with
    | [] => Except.error "empty"
    | _ :: tail => Except.ok tail
  have : tail.length < xs.length := by sorry
  f tail
termination_by f xs => xs.length

The proof state clearly shows that something went wrong.

xs tail : List ℕ
⊢ List.length tail < List.length xs

As we can see, the only constraint on tail is that its type must be List Nat. There’s nothing to link it with xs. Inside the nested do block, we could use match h : xs with to extract a hypothesis, but this can not “escape” to the tail variable bound by the let ←.

As a side note, I did try to construct a proof of tail.length < xs.length and pass it through via Except.ok, but pattern matching on the proof always fails with an unresolved metavariable error. Maybe there’s some way to do this in Lean, but I didn’t have any luck finding it.

My first guess is that it’s a limitation of the do notation: the constraint is lost for variables bound by let ←. Then I tried to directly use the bind function. Still no success.

def f' (xs : List Nat) : Except String Nat :=
  let tail_except :=
    match xs with
    | [] => Except.error "empty"
    | _ :: tail => Except.ok tail
  tail_except >>= fun tail =>
    have : tail.length < xs.length := by sorry
    f' tail
termination_by f' xs => xs.length

The proof state:

xs : List ℕ
tail_except : Except String (List ℕ) := match xs with
| [] => Except.error "empty"
| head :: tail => Except.ok tail
tail : List ℕ
⊢ List.length tail < List.length xs

Although we have tail_except as what we need, there’s still nothing to link tail_except with tail.

This works, but why?

I further transformed the example to the most direct form and this time it works.

def f'' (xs : List Nat) : Except String Nat :=
  let tail_except :=
    match xs with
    | [] => Except.error "empty"
    | _ :: tail => Except.ok tail
  match h : tail_except with
  | .error e => .error e
  | .ok tail =>
    have : tail.length < xs.length := by
      cases xs
      case nil =>
        dsimp at h
        contradiction
      case cons hd tl =>
        dsimp at h
        simp at h
        rw [h]
        simp
        exact Nat.lt_succ_self tail.length
    f'' tail
termination_by f'' xs => xs.length

The crucial point is that by using the pattern matching instead of the monad bind, we get this hypothesis: h : tail_except = Except.ok tail.

But why doesn’t the monad bind work, while direct pattern matching works?

Bound by bind, I’m thus free

I’m sure that some of you are already screaming the answer at your screen. It’s pretty clear in the second example, let me add a pair of parentheses to make it even clearer: tail_except >>= (fun tail => f' tail). It is thus fair that tail_except and tail should have no relations: the former is the first argument to bind; the latter is an argument of the second argument to bind. Since bind can’t establish any relationship between its two arguments in general, it’s indeed understandable that none is available for the proof.

This should be pretty obvious in hindsight, but why did I think it’s possible to do so initially. On reflection, I realized that my mistake is to think of let ← as let :=. Despite their similarities, the former is desugared to bind and thus gives no constraints, while the latter generates a definition equivalence premise—you can rewrite the variable to its definition at any time. The do notation is designed to exploit this similarities between chain bindings and normal chain definitions, but it seems that today, the ambivalence finally caught up and bit me in the tail.

So I guess the lesson here is that let ← is not a definition, although it looks like one. A real lesson, though, is that although Frege points out that well-designed symbols can replace (some part of) thinking without sacrificing rigorousness, sometimes a false resemblance may also lead you astray.