Inductive type with Lists

Stream: new members

[Philipp]

Every time I encounter an inductive type that contains a list of itself, the termination checker becomes an enemy:

inductive Bar
  | B
  | Bs (b: List Bar)

def Bar.countBs : Bar → Nat
| B => 1
| Bs bs => bs.foldl (λbs b => b.countBs + bs) 0

This for example doesn't work, and the only (especially beginner-friendly) solution (https://proofassistants.stackexchange.com/a/2288) is to define my own foldl.

Is there a way to force the termination checker to unfold List.foldl or something similar?

[Henrik Böving]

You have two options here, one is to mark the def as partial which will turn off the termination checker but prevent you from proving things about your function. If you only want to program I would suggest doing that. The alternative approach is to use docs#List.attach:

import Batteries.Data.List.Init.Attach

inductive Bar
  | B
  | Bs (b: List Bar)

def Bar.countBs : Bar → Nat
| B => 1
| Bs bs => bs.attach.foldl (fun bs ⟨b, _⟩ => b.countBs + bs) 0

This allows the termination checker to see that indeed b is a member of bs and thus derive a proof that your recursive call must be decreasing.

[Philipp]

Thanks! I used partial previously but if I understood correctly, that was what prevented me to use examples to show the correctness of the function for a few test cases.