Puzzling failure of termination checker

Stream: lean4

[Graham Leach-Krouse]

Minor puzzle: the following MWE doesn't pass the termination checker

inductive Form : Type
  | atom : Nat → Form
  | impl : Form → Form → Form

infix:256 "⊃"  => Form.impl

inductive BTheorem : Form → Type
  | taut {p} : BTheorem (p ⊃ p)
  | mp {p q} (h₁ : BTheorem p) (h₂ : BTheorem (p ⊃ q)) : BTheorem q

def proofDepth (prf : BTheorem f) : Nat := by
  cases prf
  case taut => exact 0
  case mp thm₁ thm₂ =>
    have l₁ : Nat := proofDepth thm₁
    have l₂ : Nat := proofDepth thm₂
    exact l₁ + l₂

A workaround is to use induction rather than cases(thanks @Kevin Buzzard ), which has now solved the original more complicated problem. But at least in the context of the MWE, that gives code generator does not support BTheorem.rec yet.

There are other (more natural) ways of defining the proofDepth function that don't cause problems, but is there an easy way to see why this MWE doesn't work?

[Adam Topaz]

This works...

def proofDepth : BTheorem f → Nat
  | BTheorem.taut => 0
  | BTheorem.mp t1 t2 => proofDepth t1 + proofDepth t2

[Adam Topaz]

Just a guess, but the issue might be that you're trying to use tactics to make this definition.

[Henrik Böving]

So first things first as a general rule of thumb in 99.9% of cases you do never want to use tactics to generate running code, this is the case here as well. If you just write your code the proper way this works:

def proofDepth (prf : BTheorem f) : Nat :=
  match prf with
  | .taut => 0
  | .mp thm1 thm2 => proofDepth thm1 + proofDepth thm2

The reason you do not want to use tactics is that they are not mean to generate a certain term of some type but just any term of some type and you can kinda guide them in doing so but as you can see from your error this will not work out. (Also the reason you do not just want any term is that if you have running code you usually care about what it does and not just that it inhabits some type)

Tangent: The reason the induction variant does not end up working out is that executable code uses another primitive to perform recursion (namely brecOn and casesOn) while proofs via induction use the recursor (.rec) directly and generating code for recursors in a strict programming language is a little annoying so we don't do that and that is the reason it complains if you start doing it this way.

Now why this doesn't pass the termination checker if you use the cases variant is a question I don't know the answer to because I don't actually know what the structural recursion heuristic is doing under the hood

[Graham Leach-Krouse]

OK, got it. Yeah, defining this particular function is not the problem (it's trivial to do so) - this is a reduced version of a more complicated proof where tactics made sense.

[Graham Leach-Krouse]

Now why this doesn't pass the termination checker if you use the cases variant is a question I don't know the answer to because I don't actually know what the structural recursion heuristic is doing under the hood

OK, that's good to know. I'm glad it's not obvious, at least.

[Henrik Böving]

In principle the termination checker can cooperate with manual recursion + cases and I have done that myself in the past.

[Graham Leach-Krouse]

Yes, all other cases in the larger argument were fine. There's something about the return type of mp that causes trouble. Within the mp case, lean infers that thm₂ : BTheorem (p✝⊃f), where f is from the declaration proofDepth (prf : BTheorem f) : Nat. Either avoiding recursion on thm₂, or redefining mp so that the return type isn't exactly q seems to allow the termination checker figure out how to proceed.