fail to show termination

Stream: new members

[Xiyu Zhai]

Hi, everyone. In the following code, the compiler fails to show termination for X.n2, but X.n1 is fine.

Probably because X.n2 involves a map.

inductive X
  | None
  | Single (x : X)
  | Many (xs : List X)

def X.n1 : X -> Nat
  | None => 0
  | Single x => x.n1
  | Many xs => xs.length

def X.n2 : X -> Nat
  | None => 0
  | Single x => x.n2
  | Many xs => match (xs.map X.n2).maximum? with
    | some v => v
    | none => 0

Is this a feature or is this to be improved in the future?
If this will be okay in the future, how to circumstance it for now?
Thanks a lot.

[Xiyu Zhai]

The following also doesn't work for X.n2

inductive X
  | None
  | Single (x : X)
  | Many (xs : List X)

def X.n1 : X -> Nat
  | None => 0
  | Single x => x.n1
  | Many xs => xs.length

def X.n2 : X -> Nat
  | None => 0
  | Single x => x.n2
  | Many xs => match xs with
    | [] => 0
    | x::xs => match (xs.map X.n2).maximum? with
      | some v => max x.n2 v
      | none => x.n2

[Arthur Adjedj]

Would this work for you ?

def X.n2 : X -> Nat
  | None => 0
  | Single x => x.n2
  | Many [] => 0
  | Many (x::xs) => max x.n2 (Many xs).n2

[Kyle Miller]

Xiyu Zhai said:

Is this a feature or is this to be improved in the future?

To get it to work you need to help Lean out with a termination_by clause. This is incomplete, but here's one way to try to set it up that I think is possible to complete:

inductive X
  | None
  | Single (x : X)
  | Many (xs : List X)

def X.n1 : X -> Nat
  | None => 0
  | Single x => x.n1
  | Many xs => xs.length

def List.attach {α : Type _} : (xs : List α) → List {x // x ∈ xs}
| [] => []
| x::xs => ⟨x, by constructor⟩ :: xs.attach.map (λ y => ⟨y.val, by { constructor; exact y.2 }⟩)

def X.n2 : X -> Nat
  | None => 0
  | Single x => x.n2
  | Many xs =>
    have : ∀ (x : {x // x ∈ xs}), sizeOf x.val < 1 + sizeOf xs := by
      intro x
      sorry
    match (xs.attach.map (λ x => have := this x; X.n2 x.val)).maximum? with
    | some v => v
    | none => 0
termination_by X.n2 x => x

[Kyle Miller]

The definition by @Arthur Adjedj is much simpler.

[Xiyu Zhai]

Arthur Adjedj said:

Would this work for you ?

def X.n2 : X -> Nat
  | None => 0
  | Single x => x.n2
  | Many [] => 0
  | Many (x::xs) => max x.n2 (Many xs).n2

Thanks a lot! This works amazingly.

[Xiyu Zhai]

Kyle Miller said:

Xiyu Zhai said:

Is this a feature or is this to be improved in the future?

To get it to work you need to help Lean out with a termination_by clause. This is incomplete, but here's one way to try to set it up that I think is possible to complete:

inductive X
  | None
  | Single (x : X)
  | Many (xs : List X)

def X.n1 : X -> Nat
  | None => 0
  | Single x => x.n1
  | Many xs => xs.length

def List.attach {α : Type _} : (xs : List α) → List {x // x ∈ xs}
| [] => []
| x::xs => ⟨x, by constructor⟩ :: xs.attach.map (λ y => ⟨y.val, by { constructor; exact y.2 }⟩)

def X.n2 : X -> Nat
  | None => 0
  | Single x => x.n2
  | Many xs =>
    have : ∀ (x : {x // x ∈ xs}), sizeOf x.val < 1 + sizeOf xs := by
      intro x
      sorry
    match (xs.attach.map (λ x => have := this x; X.n2 x.val)).maximum? with
    | some v => v
    | none => 0
termination_by X.n2 x => x

Thanks a lot! I really need to learn a lot about well-defined recursion.