unfold loops indefinitely

Stream: lean4

[pandaman]

Hi. I have encountered a situation where unfold tactic loops indefinitely (until a timeout is reached), and it depends on the use of match inside a proof in the definition.
Here is the example:

def PositionalNotation {base: Nat} {h: base > 1} := List (Fin base)
def toPositionalNotation {base: Nat} {h: base > 1} (n: Nat): @PositionalNotation base h :=
  if isLt: n < base then
    []
  else
    let rem := n % base;
    let quot := n / base;
    let h': base > 0 := by {
      sorry;
    };
    let n_gt_0: n > 0 := by {
      -- replacing the following "match" with "sorry" fixes the infinite loop.
      match Nat.lt_or_ge n base with
      | Or.inl _ => sorry;
      | Or.inr _ => sorry;
    };
    Fin.mk rem (Nat.mod_lt n h') :: @toPositionalNotation base h quot
termination_by _ n => n
decreasing_by {
  sorry;
}

theorem three_gt_one: 3 > 1 := by decide;
theorem ex1: @toPositionalNotation 3 three_gt_one 5 = [] := by {
  -- this "unfold" loops indefinitely:
  -- (deterministic) timeout at 'whnf', maximum number of heartbeats (50000) has been reached (use 'set_option maxHeartbeats <num>' to set the limit)
  unfold toPositionalNotation;
}

The unfold at last loops until the timeout, but if we replace match in n_gt_0 with sorry, the unfold unfolds the definition as expected.
I'm using Lean (version 4.0.0-nightly-2022-02-22, commit c932d9d33cea, Release) on Windows 10 with Lean4 VSCode extension.

[Mario Carneiro]

I think this is working as intended

[Mario Carneiro]

unfold unfolds all instances of the chosen constant, which means it usually diverges when applied to recursive functions. I'm not sure what the best ways to do this in lean 4 are, lean 3 would use rw [foo] or simp only [foo] {single_pass := tt} to limit the unfolding. Perhaps unfold has a config option for this

[pandaman]

But without match, it unfolds only one step. At least, the behavior looks inconsistent.

[Mario Carneiro]

This seems to be a bug. I wrote some diagnosis at leanprover/lean4#1026