Fail to show termination when using universe u

Stream: new members

[LizBonn]

I want to define the Nat.le relation on a general type α. As an mwe, I first define a type class C, declaring a succ : α → α function on type α. Then I define le exactly as Nat.le :

import Mathlib
set_option autoImplicit false

class C (α : Type*) where
  succ : α → α

inductive le {α : Type*} [C α] : α → α → Prop where
| refl {n : α} : le n n
| step {a b : α} (h : le a b) : le a (C.succ b)

After that, I want to prove the transitivity of le. However, if the underlying type α has type Type u, Lean fails to show termination of the proof. If the underlying type α has type Type* or other concrete types like Type, Lean doesn't complain.

namespace Hidden
theorem le_trans₁.{u} {α : Type u} [C α] {a b c : α} : le a b → le b c → le a c
  | h, .refl => h
  | h, .step h' => .step (le_trans₁ h h')

theorem le_trans₂ {α : Type} [C α] {a b c : α} : le a b → le b c → le a c
  | h, .refl => h
  | h, .step h' => .step (le_trans₂ h h')

theorem le_trans₃ {α : Type*} [C α] {a b c : α} : le a b → le b c → le a c
  | h, .refl => h
  | h, .step h' => .step (le_trans₃ h h')

Error message for le_trans₁:

fail to show termination for
  Hidden.le_trans₁
with errors
failed to infer structural recursion:
Not considering parameter α of Hidden.le_trans₁:
  it is unchanged in the recursive calls
Not considering parameter #2 of Hidden.le_trans₁:
  it is unchanged in the recursive calls
Not considering parameter a of Hidden.le_trans₁:
  it is unchanged in the recursive calls
Not considering parameter b of Hidden.le_trans₁:
  it is unchanged in the recursive calls
Not considering parameter c of Hidden.le_trans₁:
  its type is not an inductive
Cannot use parameter #6:
  application type mismatch
    @le α
  argument
    α
  has type
    Type u : Type (u + 1)
  but is expected to have type
    Type u_1 : Type (u_1 + 1)
Cannot use parameter #7:
  application type mismatch
    @le α
  argument
    α
  has type
    Type u : Type (u + 1)
  but is expected to have type
    Type u_1 : Type (u_1 + 1)


Could not find a decreasing measure.
The basic measures relate at each recursive call as follows:
(<, ≤, =: relation proved, ? all proofs failed, _: no proof attempted)

1) 15:26-40
Please use `termination_by` to specify a decreasing measure.

It is so weird to me. Could someone explain this?

Thanks in advance!

[Aaron Liu]

This is a bug in the recursion compiler

[Joachim Breitner]

This is structural recursion on inductive predicates? So maybe fixed en passant by @Robin Arnez’s #9995?

[Aaron Liu]

lean4#9995

[Robin Arnez]

It's not fixed. I'll look into it

[Robin Arnez]

Seems like an issue with docs#Lean.Meta.Match.getMkMatcherInputInContext. Shouldn't be too hard to fix

[Robin Arnez]

Yup, works now. I added a test based on your example