Proving termination for mutually inductive proofs

Stream: new members

[Harry Goldstein]

Hey folks. Not sure if this is the right place to ask, but I'm having a hard time proving termination for this mutually inductive proof I'm working on.

I'm trying to show that a bidirectional type checking algorithm agrees with a relational notion of well-typedness for a simply-typed lambda calculus. The details aren't super important, the main thing is that the proof is supposed to have the same inductive structure (and therefore termination argument) as the mutually-defined type-checking algorithm, but for some reason Lean can figure out termination for one and not the other.

If anyone could help me I'd really appreciate it.

STLC.lean

[Timo Carlin-Burns]

(deleted)

[Joachim Breitner]

(deleted)

[Timo Carlin-Burns]

we both tried to post the same link.. It seems like there's something broken with linking to https://live.lean-lang.org when the code has parentheses

[Joachim Breitner]

This could be a bug I recently fixed, https://github.com/leanprover/lean4/pull/3204.

Hmm, or not.

[Joachim Breitner]

So, with set_option showInferredTerminationBy true I found out that your functions are proved terminating using

termination_by
  checkType x1 x2 x3 => (sizeOf x2, 1)
  inferType x1 x2 => (sizeOf x2, 0)

and it’s good practice to copy that after the mutual … end to be explicitly (an check that it matches your expectations).

I can now write

termination_by
  checkType_sound x1 x2 x3 => (sizeOf x2, 1)
  inferType_sound x1 x2 _ => (sizeOf x2, 0)

below the proofs and tell Lean how I’d expect the termination argument to go. This gives better error messages, namely

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
Γ✝: Context
e₁e₂: Expr
τ✝: Ty
x✝: ∀ (y : (_ : Context) ×' (_ : Expr) ×' Ty ⊕' (_ : Context) ×' (_ : Expr) ×' Ty),
  (invImage
          (fun a =>
            PSum.casesOn a (fun val => PSigma.casesOn val fun x1 snd => PSigma.casesOn snd fun x2 snd => (sizeOf x2, 1))
              fun val => PSigma.casesOn val fun x1 snd => PSigma.casesOn snd fun x2 snd => (sizeOf x2, 0))
          Prod.instWellFoundedRelationProd).1
      y (PSum.inr { fst := Γ✝, snd := { fst := e₁ ⋅ e₂, snd := τ✝ } }) →
    PSum.casesOn y (fun _x => checkType _x.1 _x.2.1 _x.2.2 = true → _x.1 ⊢ _x.2.1 : _x.2.2) fun _x =>
      inferType _x.1 _x.2.1 = some _x.2.2 → _x.1 ⊢ _x.2.1 : _x.2.2
h: inferType Γ✝ (e₁ ⋅ e₂) = some τ✝
τ₁: Ty
τ₂✝: inferType Γ✝ e₁ = some τ₁
hτ✝: (match τ₁ with
  | τa ==> τb => if h : checkType Γ✝ e₂ τa = true then some τb else none
  | x => none) =
  some τ✝
τaτb: Ty
τ₂: inferType Γ✝ e₁ = some (τa ==> τb)
hτ: (match τa ==> τb with
  | τa ==> τb => if h : checkType Γ✝ e₂ τa = true then some τb else none
  | x => none) =
  some τ✝
hτ₁: checkType Γ✝ e₂ τa = true
hτ₂: τb = τ✝
Γ: Context
e: Expr
τ: Ty
a✝: inferType Γ e = some τ
⊢ sizeOf e < 1 + sizeOf e₁ + sizeOf e₂

Now the e is unconnected to e1 and e2, so probably not provable, probably because somewhere the connection got lost.

[Joachim Breitner]

(It’s a bug (probably due to me) that this error message isn’t anchored at the relevant recursive call.)

[Joachim Breitner]

Ah, and if I replace

simp [inferType_sound, *]

with

apply inferType_sound; assumption

it works! So it might be that lean bug after all.

[Joachim Breitner]

(Background: Simp produces proof terms where the recursive call not fully saturated, and then the termination checker, without the mentioned fix, doesn’t see who the argument relates to your parameters.)

[Joachim Breitner]

BTW, I am currently working on improving things around well-founded recursion, e.g. generating induction principles from function definitions. Prototype at https://github.com/nomeata/lean-wf-induct. I am looking for alpha-testers and early adoptors, so if you expect to do more proofs about stuff defined by well-founded recursion and are interested to play guinea pig, that’d be great.

(Your definition should actually just be structurally recursive, but Lean doesn’t support that. It’s on the roadmap.)

[Joachim Breitner]

Oh, and welcome to the lean Zulip, @Harry Goldstein :-)

[Harry Goldstein]

Thank you! :-)

Oh wow, what a simple fix! Thank you so much. I had a feeling it might be doing something weird under the hood when I called simp, but I naïvely thought it couldn't be doing something weird enough to break the termination checker. But OK, this is good to know. I'm not sure I'll be doing a lot of this kind of thing moving forward, but if I decide to do more I'll definitely check out the prototype. For now I'm just noodling around to get my bearings.

[Joachim Breitner]

It’s a rather silly reason why this breaks.

When resolving identifiers, lean inserts a little meta-data note around the recursive call which remembers the original source position, so that later when we do the termination proof (and all surface syntax is gone) we can report the error location. But if the recursive call is not syntactically saturated (as in simp [foo]), this marker keeps the arguments “separate” from the recursive call, and to the termination checker it looks like a higher-order use. Kinda silly that a little hack to produce nicer termination errors causes more termination errors.

A while ago I fixed that by floating these markers out of applications. But due to my limited understanding of some of lean’s utility functions, that fix only worked for unary applications. I noticed that only recently, and the fix for that isn't released yet.

Not sure if anyone wanted to know these hairy details :-D