Termination via well founded relation on subtype?

Stream: lean4

[James Gallicchio]

Two newbie questions about how to get this definition to compile:

def mwe [Stream ρ τ] (res : α) : {l : ρ // isFinite l} → α
  | ⟨l,h⟩ =>
    match next? l with
    | none => res
    | some (_,xs) =>
      have h_next : hasNext l xs := sorry
      mwe res ⟨xs, by sorry⟩
  termination_by _ l => l

I know there's a lot going on here, but I've essentially defined a subtype for streams which are finite, and now am trying to recurse through the stream.

1) I have an instance of WellFoundedRelation {l // isFinite l} but I'm not really sure how to use it to prove termination here

2) I'm not sure how to maintain information from the match; in particular, I need that next? l = some (_,xs) to prove the first sorry. I've tried the generalizing := true flag that I saw elsewhere, but that did not seem to do anything here

[Chris B]

The syntax for 2 is match h:next? l with, with no whitespace after the h:.

[Chris B]

I'll see about adding it to the docs, it looks like that's still not in there.

[Chris B]

For 1, you can try adding

  termination_by _ l => l
  decreasing_by
    trace_state

and observing the proof goal.

[James Gallicchio]

Chris B said:

The syntax for 2 is match h:next? l with, with no whitespace after the h:.

Ahh, I was trying h : with whitespace, that is a bit unfortunate whitespace sensitivity

[Chris B]

You're not alone. I'll mention the whitespace thing in the documentation.

[James Gallicchio]

As for the termination, it comes up as a type error?

type mismatch
  l
has type
  { l // isFinite l } : Type (max 0 u_1)
but is expected to have type
  ?β : Sort ?u.12065

[Chris B]

Is the whole thing posted anywhere?

[James Gallicchio]

hm, lemme try to cut this file down

[James Gallicchio]

https://gist.github.com/JamesGallicchio/9e5d08bce7ce4f9f563d1a9edc765d5b this should compile on most recent nightly (it does need a bug fix from a few days ago)

[Chris B]

There seems to be some issue with type parameter visibility in termination blocks; this makes this issue more clear:

set_option pp.all true in
def mwe [Stream ρ τ] (acc : α) : {l : ρ // isFinite l} → α
  | ⟨l,h⟩ =>
    match h:next? l with
    | none => acc
    | some (x,xs) =>
      have h_next : hasNext l xs := by exists x; simp [hasNext, h]
      mwe acc ⟨xs, by sorry⟩
  termination_by'
    invImage (fun ⟨ρ, τ, α, _, _, subty⟩ => subty) (hasNextWF)

/-
subty : @Subtype.{u_1 + 1} ρ fun (l : ρ) => @Stream.isFinite.{u_1, u_2} ρ τ x✝¹ l
type mismatch
  subty
has type
  @Subtype.{u_1 + 1} ρ fun (l : ρ) => @Stream.isFinite.{u_1, u_2} ρ τ x✝ l : Type (max 0 u_1)
but is expected to have type
  @Subtype.{?u.8671 + 1} ?m.8672 fun (s : ?m.8672) =>
    @Stream.isFinite.{?u.8671, ?u.8670} ?m.8672 ?m.8673 ?m.8674 s : Type ?u.8671
-/

And I can't give hasNextWF the type arguments explicitly.

[James Gallicchio]

Oh boy. I do see what you mean, since it feels like those should unify fine

[Leonardo de Moura]

Created an issue on GitHub for this. We will try to fix it this week. https://github.com/leanprover/lean4/issues/1017

[Leonardo de Moura]

This issue has been fixed.