brecOn application type mismatch during termination check?

Stream: lean4

[Don Unagi]

I'm trying to understand why this code:

inductive A : Type
  | a1 : A
  | a2 : A → A → A

mutual

  inductive C : List A → Type
    | c1 : C as
    | c2 : C [] → C [a]
    | c3 : C [A.a2 y x] → C [A.a2 x y]

  inductive B : Type
    | b : B

end

def f : C as → Unit
  | C.c1 => ()
  | C.c2 x => f x
  | C.c3 x => f x

produces this error:

fail to show termination for
  f
with errors
argument #2 was not used for structural recursion
  application type mismatch
    @C.brecOn (fun {as} x => Unit) as
  argument
    as
  has type
    List A : Type
  but is expected to have type
    B → Type : Type 1

[Don Unagi]

This looks obviously structurally recursive to me, and seemingly unrelated changes like removing the definition of B make the error go away, so I'm confused about what's happening

[Joachim Breitner]

Lean does not support structural recursion over mutual data types (yet). It seems that even an “unused” type definition in the mutual block makes it a mutual data type.

[Don Unagi]

It's curious that many other seemingly unrelated changes (for instance removing the c2 constructor, or changing its type from c2 : C [] → C [a] to c2 : C [a] → C [], or a half dozen other random things I tried) also make the error go away

[Don Unagi]

I guess "not supported" could mean "works unpredictably" but I wonder if there's a heuristic for when it does and doesn't work?

[Mario Carneiro]

it will use well founded induction on sizeOf, so if there is something else which is decreasing then it may do the proof over that instead

[Mario Carneiro]

Note that your original example works when written as

def f : C as → Unit
  | C.c1 => ()
  | C.c2 x => f x
  | C.c3 x => f x
termination_by x => sizeOf x

It appears that lean is trying to do induction on as instead of x, resulting in the unprovable goal sizeOf [A.a2 y x] < sizeOf [A.a2 x y]

[Mario Carneiro]

this seems like a bug in GuessLex @Joachim Breitner

[Joachim Breitner]

If that's the case, a bug report is very much appreciated

[Joachim Breitner]

Had a look. This also works:

def f : C as → Unit
  | C.c1 => ()
  | C.c2 x => f x
  | C.c3 x => f x
-- termination_by x2 => (sizeOf as, sizeOf x2)
decreasing_by all_goals simp_wf; omega

Here is what happens: GuessLex looks at how as and x2 decrease in each call, and finds out that (as, x2) is a suitable termination measure. In the third case, as decreases non-strictly (≤) and x2 decreases strictly (<). Because GuessLex looks at how each of these behave separately, this looks promising, and it sets

termination_by x2 => (sizeOf as, sizeOf x2)

But then the default decreasing_tactic is not able to make use sense of this, because

    repeat (first | apply Prod.Lex.right | apply Prod.Lex.left)

can only handle (<, ?) and (=, <), (with = being defeq), but not (≤, <). When I wrote GuessLex I was hoping to improve the decreasing_tactic behavior along it, but revamping that did not happen yet.

Incidentially, omega has some (incomplete) support for Prod.Lex, that’s why simp_wf; omega works.

Probably GuessLex should not even look for ≤, at least not until the default termination tactic can handle that, as unfortunate as that is.

[Joachim Breitner]

Noted as https://github.com/leanprover/lean4/issues/3906.