Why is this not definitionally held?

Question

The following Lean4 code:

def alternate : (xs ys : List α) → List α
  | [], ys => ys
  | x::xs, ys => x :: alternate ys xs
  termination_by xs ys => xs.length + ys.length

theorem alternate_empty:
  (ys: List α) ->
  alternate [] ys = ys :=
  λ ys => Eq.refl ys

errs with the message:

type mismatch
  Eq.refl ys
has type
  ys = ys : Prop
but is expected to have type
  alternate [] ys = ys : Prop

From my understanding, it is almost just Nat.add and Nat.zero_add. The only possible reason I guess is that alternate has an extra termination proof while Nat.add doesn't. But I still don't get why it does not resolve to a sub-case now that xs is known to be [].

I have some experience with Agda, if this information helps.

❯ lean --version
Lean (version 4.10.0-rc2, arm64-apple-darwin23.5.0, commit 702c31b80712, Release)

Answer 1

My guess is that it is because the termination_by causes it not to be fully reduced when you leave a variable ys in there:

def alternate : (xs ys : List α) → List α
  | [], ys => ys
  | x::xs, ys => x :: alternate ys xs
  termination_by xs ys => xs.length + ys.length

#reduce fun (α : Type) (ys: List α) => (alternate [] ys)
/-
fun α ys =>
  Acc.rec (fun x₁ h ih => List.rec (fun x => x₁.2) (fun head tail tail_ih x => head :: x ⟨x₁.2, tail⟩ ⋯) x₁.1 ih) ⋯
-/

And it is not just because of your manual use of termination_by. Sometimes Lean is able to figure out the termination automatically for you, but the definition is still wrapped in Acc.rec, making reduction and judgmental equality more complicated.

def alternate' : (xs ys : List α) -> (left_first : Bool := true) → List α
  | [], ys, true => ys
  | xs, [], false => xs
  | x::xs, ys, true => x :: alternate' xs ys false
  | xs, y::ys, false => y :: alternate' xs ys true

#reduce fun (α : Type) (ys: List α) => (alternate' [] ys)
/-
fun α ys =>
  Acc.rec
    (fun x₁ h ih =>
      List.rec
        (List.rec (Bool.rec (fun x => []) (fun x => []) x₁.2.2)
          (fun head tail tail_ih => Bool.rec (fun x => head :: x ⟨[], ⟨tail, true⟩⟩ ⋯) (fun x => head :: tail) x₁.2.2)
          x₁.2.1)
        (fun head tail tail_ih =>
          List.rec (Bool.rec (fun x => head :: tail) (fun x => head :: x ⟨tail, ⟨[], false⟩⟩ ⋯) x₁.2.2)
            (fun head_1 tail_1 tail_ih =>
              Bool.rec (fun x => head_1 :: x ⟨head :: tail, ⟨tail_1, true⟩⟩ ⋯)
                (fun x => head :: x ⟨tail, ⟨head_1 :: tail_1, false⟩⟩ ⋯) x₁.2.2)
            x₁.2.1)
        x₁.1 ih)
    ⋯
-/

You can however still prove your goal with simp or unfold:

theorem alternate_empty (ys: List α) : alternate [] ys = ys := by
  simp [alternate]

theorem alternate_empty (ys: List α) : alternate [] ys = ys := by
  unfold alternate
  rfl

(I'm not sure of a convenient term proof off-hand, unfortunately.)