Nightly broke well-founded proof

Stream: lean4

[James Gallicchio]

Just updated my toolchain to latest nightly, but going from leanprover/lean4:nightly-2022-02-18 to the next day breaks some of my proofs

https://github.com/JamesGallicchio/LeanColls/blob/main/LeanColls/LazyList.lean#L65

^ this goal was closed before by simp, but now leaves some expression in terms of WellFounded.fix

[James Gallicchio]

(And doing the thing I normally do, of tossing a bunch more expressions to simp, gets stuck on Acc.rec. I'm sure how any of the WellFounded machinery works in lean 4 :/)

[James Gallicchio]

Based on the timing this must be caused by the fix for https://github.com/leanprover/lean4/issues/1017

[James Gallicchio]

Just bumping this -- on nightly-2022-03-01 I'm still getting stuck trying to get an expression through Acc.rec

I never had to prove stuff in Lean 3 about functions that use well-founded recursion instead of structural recursion, so I'm not sure if this is something I can fix, or if my old solution should still be working and something broke in nightly

[Mario Carneiro]

@James Gallicchio Could you extract a #mwe? This looks like something that needs to be addressed in core (we can probably find a workaround but this is exposing implementation details that don't look deliberate)

[James Gallicchio]

This is as small as I can make it:

inductive LazyList (α : Type u)
| nil : LazyList α
| cons (hd : α) (tl : LazyList α) : LazyList α
| delayed (t : Thunk (LazyList α)) : LazyList α

namespace LazyList
variable {α : Type u} {β : Type v} {δ : Type w}

-- Height measures number of nodes (including delayeds)
noncomputable def height (ll : LazyList α) : Nat :=
  @LazyList.rec (motive_1 := fun _ => Nat) (motive_2 := fun _ => Nat)
    α 0 (fun _ _ ih => ih + 1) (fun _ ih => ih + 1) (fun _ ih => ih ()) ll

@[simp] theorem height_nil : (@LazyList.nil α).height = 0 := rfl
@[simp] theorem height_cons : (@LazyList.cons α a l).height = l.height + 1 := rfl
@[simp] theorem height_delayed (as) :
  (@LazyList.delayed α as).height = as.get.height + 1 := by
  have : as = ⟨fun x => as.get⟩ := by
    cases as with | _ fn => apply congrArg; funext (); rfl
  rw [this]; rfl

/-
Length of a list is number of actual elements
in the list, ignoring delays
-/
def length : LazyList α → Nat
| nil        => 0
| cons _ as  => length as + 1
| delayed as => length as.get
termination_by _ as => as.height

@[simp] theorem length_nil : (@nil α).length = 0 := by simp [length]
@[simp] theorem length_cons : (@cons α a as).length = as.length + 1 := by simp [length]
@[simp] theorem length_delayed (as)
  : (@delayed α as).length = as.get.length
  := by
  have : as = ⟨fun x => as.get⟩ := by
    cases as with | _ fn => apply congrArg; funext (); rfl
  rw [this]; rfl

@[simp] def toList : LazyList α → List α
| nil        => []
| cons a as  => a :: toList as
| delayed as => toList as.get
termination_by _ as => as.height

@[simp] theorem length_toList : (l : LazyList α) → l.toList.length = l.length
  := @rec α
    (λ l => l.toList.length = l.length)
    (λ t => t.get.toList.length = t.get.length)
    (by simp [toList])
    (by
      intros hd tl tl_ih
      simp [tl_ih, toList, Thunk.get]
      )
    (by
      intros t t_ih
      assumption
      )
    (by
      intros fn fn_ih
      have := fn_ih ()
      simp [Thunk.get] at this |-
      assumption
      )

I could mess around a bit more to try making it smaller but

[Leonardo de Moura]

I will take a look at why simp is exposing the internal encoding. In the meantime, you can avoid the problem by deleting the unnecessary length theorems, Lean can create them automatically for us.

inductive LazyList (α : Type u)
| nil : LazyList α
| cons (hd : α) (tl : LazyList α) : LazyList α
| delayed (t : Thunk (LazyList α)) : LazyList α

namespace LazyList
variable {α : Type u} {β : Type v} {δ : Type w}

instance : Inhabited (LazyList α) :=
⟨nil⟩

@[inline] protected def pure : α → LazyList α
| a => cons a nil

-- Height measures number of nodes (including delayeds)
noncomputable def height (ll : LazyList α) : Nat :=
  @LazyList.rec (motive_1 := fun _ => Nat) (motive_2 := fun _ => Nat)
    α 0 (fun _ _ ih => ih + 1) (fun _ ih => ih + 1) (fun _ ih => ih ()) ll

@[simp] theorem height_nil : (@LazyList.nil α).height = 0 := rfl
@[simp] theorem height_cons : (@LazyList.cons α a l).height = l.height + 1 := rfl
@[simp] theorem height_delayed (as) : (@LazyList.delayed α as).height = as.get.height + 1 := by
  have : as = ⟨fun x => as.get⟩ := by
    cases as with | _ fn => apply congrArg; funext (); rfl
  rw [this]; rfl

/-
Length of a list is number of actual elements
in the list, ignoring delays
-/
def length : LazyList α → Nat
| nil        => 0
| cons _ as  => length as + 1
| delayed as => length as.get
termination_by _ as => as.height

def toList : LazyList α → List α
  | nil        => []
  | cons a as  => a :: toList as
  | delayed as => toList as.get
termination_by _ as => as.height

attribute [simp] toList length

theorem length_toList (l : LazyList α) : l.toList.length = l.length := by
  match l with
  | nil => rfl
  | cons a as => simp [length_toList as]
  | delayed as => simp [length_toList as.get]
termination_by _ as => as.height

def force : LazyList α → Option (α × LazyList α)
  | delayed as => force as.get
  | nil        => none
  | cons a as  => some (a,as)
termination_by _ as => as.height

theorem toList_force_none (l : LazyList α) : force l = none ↔ l.toList = List.nil := by
  match l with
  | nil => simp [force]
  | delayed as => simp [force, toList_force_none as.get]
  | cons a as => simp [force, toList_force_none as]
termination_by _ as => as.height

[James Gallicchio]

Oh, huh, so adding the simp attribute after declaration has different behavior than adding it directly to the declaration?

[Leonardo de Moura]

I pushed a fix for this issue. I also added a nontrivial SizeOf instance for types like Thunk. The heigh auxiliary function is not needed anymore. We can write the example above as:

inductive LazyList (α : Type u)
  | nil : LazyList α
  | cons (hd : α) (tl : LazyList α) : LazyList α
  | delayed (t : Thunk (LazyList α)) : LazyList α
  deriving Inhabited

namespace LazyList

@[inline] protected def pure (a : α) : LazyList α :=
  cons a nil

/-
Length of a list is number of actual elements
in the list, ignoring delays
-/
@[simp] def length : LazyList α → Nat
  | nil        => 0
  | cons _ as  => length as + 1
  | delayed as => length as.get
termination_by _ as => as

@[simp] def toList : LazyList α → List α
  | nil        => []
  | cons a as  => a :: toList as
  | delayed as => toList as.get
termination_by _ as => as

theorem length_toList (l : LazyList α) : l.toList.length = l.length := by
  match l with
  | nil => rfl
  | cons a as => simp [length_toList as]
  | delayed as => simp [length_toList as.get]
termination_by _ as => as

def force : LazyList α → Option (α × LazyList α)
  | delayed as => force as.get
  | nil        => none
  | cons a as  => some (a,as)
termination_by _ as => as

theorem toList_force_none (l : LazyList α) : force l = none ↔ l.toList = List.nil := by
  match l with
  | nil => simp [force]
  | delayed as => simp [force, toList_force_none as.get]
  | cons a as => simp [force, toList_force_none as]
termination_by _ as => as

end LazyList

[James Gallicchio]

Ah, amazing! Thank you :)

[Leonardo de Moura]

The trivial termination_by _ as => as annotations in the example above are not needed anymore.
The simplified version is here: https://github.com/leanprover/lean4/blob/master/tests/lean/run/lazylistThunk.lean