Can not unfold definition

Stream: lean4

[Yanning Chen (LightQuantum)]

namespace List

-- List.map, but carrying the proof that the element is in the list
@[specialize]
def mapMem (as : List α) (f : (a : α) → a ∈ as → β) : List β := match as with
  | [] => []
  | a :: as' => f a (.head _) :: as'.mapMem (f · <| ·.tail _)

end List

namespace Std.Range

def toList (r : Range) : List Nat := if r.step = 0 then
   []
  else if r.start < r.stop then
    r.start :: toList { r with start := r.start + r.step }
  else
    []

theorem toList_append (h₁ : l ≤ m) (h₂ : m ≤ n) : [l:m].toList ++ [m:n].toList = [l:n].toList := by sorry

theorem toList_upper (In: i ∈ [0:n].toList): i < n := by sorry

def constructGetN {as : List Nat} : (a : Nat) → a ∈ [0:as.length].toList → Nat :=
  fun i H => as[i]' (toList_upper H)

theorem baseCase : ([0:0].toList.mapMem (@constructGetN [])) = [] := by
  unfold toList   -- failed

I expect this unfold to success, but lean4 says

tactic 'unfold' failed to unfold 'Std.Range.toList' at
  { start := 0, stop := 0, step := 1 }.toList.mapMem constructGetN = []

With pp.all,

tactic 'unfold' failed to unfold 'Std.Range.toList' at
  @Eq.{1} (List.{0} Nat)
    (@List.mapMem.{0, 0} Nat Nat
      (Std.Range.toList
        (Std.Range.mk (@OfNat.ofNat.{0} Nat 0 (instOfNatNat 0)) (@OfNat.ofNat.{0} Nat 0 (instOfNatNat 0))
          (@OfNat.ofNat.{0} Nat 1 (instOfNatNat 1))))
      (@Std.Range.constructGetN (@List.nil.{0} Nat)))
    (@List.nil.{0} Nat)

I don't see any reason why this fails. Could anyone help me with this? Thanks!

My lean4 version is
Lean (version 4.14.0, arm64-apple-darwin23.6.0, commit 410fab728470, Release)

Also, lean playground

[Yanning Chen (LightQuantum)]

And here's the proof of toList_append and toList_upper. The problem still exists if you replace the sorrys with the actual proof.

theorem toList_append (h₁ : l ≤ m) (h₂ : m ≤ n) : [l:m].toList ++ [m:n].toList = [l:n].toList := by
  rw [toList, if_neg Nat.one_ne_zero]
  split
  · case isTrue h =>
    apply Eq.symm
    rw [toList, if_neg Nat.one_ne_zero]
    apply Eq.symm
    simp only at *
    rw [if_pos (Nat.lt_of_lt_of_le h h₂), List.cons_append, toList_append (Nat.succ_le_of_lt h) h₂]
  · case isFalse h =>
    simp only at *
    have : l = m := match Nat.lt_trichotomy l m with
      | .inl lltm => h lltm |>.elim
      | .inr (.inl leqm) => leqm
      | .inr (.inr mltn) => Nat.not_lt_of_le h₁ mltn |>.elim
    rw [this, List.nil_append]
termination_by m - l
decreasing_by
  all_goals simp_wf
  apply Nat.sub_succ_lt_self
  assumption

theorem toList_upper (In: i ∈ [0:n].toList): i < n := by
  induction n
  . case zero =>
    simp_all [toList]
  . case succ n l =>
    rw [<- toList_append (m := n)] at In <;> simp_all
    cases In
    . simp_all [Nat.lt_add_right]
    . case inr In =>
      simp [toList] at In
      simp_all

[Matt Diamond]

(deleted)

[Jovan Gerbscheid]

I looked into it, and this is a bug. If a constant has an "unfold" theorem (generally this is for recursive functions) then unfold will try rewriting with that theorem using simp. But simp doesn't apply simp in dependent arguments (I mean arguments for which rewriting them in a non-defeq way can cause problems) In this case List.mapMem is the function where a later argument depends on the List argument.

[Jovan Gerbscheid]

This also fails, as a result of the rewriting theorem being in applied form, so a loose toList won't get unfolded:

namespace List

-- List.map, but carrying the proof that the element is in the list
@[specialize]
def mapMem (as : List α) (f : (a : α) → a ∈ as → β) : List β := match as with
  | [] => []
  | a :: as' => f a (.head _) :: as'.mapMem (f · <| ·.tail _)

end List

namespace Std.Range

def toList (r : Range) : List Nat := if r.step = 0 then
   []
  else if r.start < r.stop then
    r.start :: toList { r with start := r.start + r.step }
  else
    []

theorem baseCase : toList = toList := by
  unfold toList   -- failed

[Jovan Gerbscheid]

Actually, this isn't a bug in unfold. It is a result of toList being defined through well-founded recursion. And that means that replacing it by its definition doesn't hold definitionally. So it isn't safe for unfold to replace the definition in the dependent position.

[Jovan Gerbscheid]

We have

List.mapMem {α : Type u_1} {β : Type u_2} (as : List α) (f : (a : α) → a ∈ as → β) : List

where f depends on as. simp is smart enought that if the f argument type were to be a proposition, it can simply insert a coercion. However, I'd argue that here, since as appears in a proposition argument of f, Lean should still be able to insert the coercion: if the argument is f, it can be replaced by fun a ha => f a (cast ha). But such an inserted lambda would look a bit strange.

[Kim Morrison]

@Yanning Chen (LightQuantum), just making sure you are aware of List.pmap which provides the functionality you're implementing here.

[Yanning Chen (LightQuantum)]

Kim Morrison said:

Yanning Chen (LightQuantum), just making sure you are aware of List.pmap which provides the functionality you're implementing here.

I had no idea I could do that! Thank you!

[Yanning Chen (LightQuantum)]

Jovan Gerbscheid said:

Actually, this isn't a bug in unfold. It is a result of toList being defined through well-founded recursion. And that means that replacing it by its definition doesn't hold definitionally. So it isn't safe for unfold to replace the definition in the dependent position.

Thank you for your detailed explanation! I completely missed there's a non-trivial termination proof hidden in its definition.

Jovan Gerbscheid said:

We have

List.mapMem {α : Type u_1} {β : Type u_2} (as : List α) (f : (a : α) → a ∈ as → β) : List

where f depends on as. simp is smart enought that if the f argument type were to be a proposition, it can simply insert a coercion. However, I'd argue that here, since as appears in a proposition argument of f, Lean should still be able to insert the coercion: if the argument is f, it can be replaced by fun a ha => f a (cast ha). But such an inserted lambda would look a bit strange.

Could you please elaborate on how this cast works? I thought you could cast the entire function (not just its argument) to argue that this unfold is judgmentally equal, (morally) akin to replacing f with (cast unfold_lemma.mpr <f unfolded>).

[Jovan Gerbscheid]

Yes, You can use a cast to cast the type of the funtion itself. But it's generally nicer to avoid casts between types when possible.