Termination problem

Stream: new members

[sgcs]

I have the following mwe that has a termination problem:

inductive Foo where
  | foo

inductive Bar where
  | bar

inductive Baz : Foo → Bar → Foo → Type where
  | baz (f : Foo) : Baz f Bar.bar Foo.foo

inductive Ex : Foo → Type where
  | ex {f f_in f_out : Foo} (b : Bar) : Baz f b f_in → Ex f_in → Ex f_out

def thm {f : Foo} (e : Ex f) : Nat := by
  cases e with
  | ex b bz e =>
      let x := thm e

      cases b with
      | bar =>
          cases bz -- why does this cause the termination problem?
          sorry

The error is:

fail to show termination for
  thm
with errors
argument #2 was not used for structural recursion
  failed to eliminate recursive application
    thm e

structural recursion cannot be used

failed to prove termination, use `termination_by` to specify a well-founded relation

I'm confused why this is problematic, and it only happens when cases bz is present. Calling it recursively without that has no problems, but for some reason once bz is pattern matched on and the index of e becomes Foo.foo Lean suddenly has a problem with the recursive call. Would be helpful is someone could explain why this is happening and a way to work around it.

[Kyle Miller]

You shouldn't be using tactics for defining recursive definitions. Here's some match syntax for you:

def thm {f : Foo} (e : Ex f) : Nat :=
  match e with
  | .ex b bz e =>
      let x := thm e
      match b with
      | .bar =>
          match bz with
          | .baz _ =>
            sorry

[sgcs]

Thanks, that makes sense. Though I've mixed tactics before with no problems a lot, so it's interesting it fails here. Using cases has been more convenient ime because it doesn't require a lot of redundant matches on other variables to allow for pattern matching to succeed. Like I switched to match in the full code and now I have to match on 3 other things to let me complete the proof, is that expected usage of match?

[Kyle Miller]

Basically using recursion with cases isn't supported. You might be able to use induction, but you have to be sure to use the induction hypothesis and not thm itself.

Without a #mwe it's hard to know what's expected or not, at least for me.