# Why is this not definitionally held?

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)


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)
List.rec (Bool.rec (fun x => head :: tail) (fun x => head :: x ⟨tail, ⟨[], false⟩⟩ ⋯) x₁.2.2)
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.)