Extrinsic finiteness proofs for iterators

Stream: lean4

[Paul Reichert]

The iterator API would be much nicer if one could use it.toList without already knowing that it is finite, while still being able to later provide the finiteness proof and then prove things about this usage. This comes up whenever instance inference isn't able to automatically prove finiteness, has it happens when using filter on an infinite iterator.

While we learned that extrinsic partial termination is a delicate issue, it just occurred to me that I only need total extrinsic termination for the iterators.

And total extrinsic termination seems like a much smaller problem if we believe that rewriting during WF preprocessing is sound. I'm considering using the following easy fixpoint combinator:

variable {α} {C : α → Sort _}

partial def partialFix [∀ x, Nonempty (C x)] (F : (x : α) → ((y : α) → C y) → C x) (x : α) : C x :=
  F x (partialFix F)

def TerminatesTotally (F : (x : α) → ((y : α) → C y) → C x) : Prop :=
  ∃ (r : α → α → Prop) (F' : (x : α) → ((y : α) → r y x → C y) → C x), WellFounded r ∧ ∀ x G, F x G = F' x (fun x _ => G x)

/-
SAFE assuming that the code generated by iteration over `F` is compatible
with the kernel semantics of iteration over `F' : (x : α) → ((y : α) → r y x → C y) → C x`
for all `F'` as in `TerminatesTotally`.
-/
@[implemented_by partialFix]
def extrinsicFix [∀ x, Nonempty (C x)] (F : (x : α) → ((y : α) → C y) → C x) (x : α) : C x :=
  open scoped Classical in
  if h : TerminatesTotally F then
    let F' := h.choose_spec.choose
    let h := h.choose_spec.choose_spec
    h.1.fix F' x
  else
    partialFix F x

def extrinsicFix_eq [∀ x, Nonempty (C x)] {F : (x : α) → ((y : α) → C y) → C x}
    (h : TerminatesTotally F) {x : α} :
    extrinsicFix F x = F x (extrinsicFix F) := by
  simp only [extrinsicFix, dif_pos h]
  rw [WellFounded.fix_eq, show (extrinsicFix F) = (fun y => extrinsicFix F y) by rfl]
  simp only [extrinsicFix, dif_pos h, h.choose_spec.choose_spec.2]

I see two downsides:

• usage of implemented_by
• need to require Nonempty, but there's no way around this.

The present use of implemented_by seems safe to me because the underlying assumption is the same as for WF preprocessing.

Are there soundness risks I have overlooked? Would you like to have it.toList using extrinsicFix, or do you prefer having nontermination explicitly mentioned as in it.allowNontermination.toList as it is right now?