Understanding noConfusion

Data.List.getLast is defined as follows:

def getLast : ∀ (as : List α), as ≠ [] → α
| [],       h => absurd rfl h
| [a],      _ => a
| _::b::as, _ => getLast (b::as) (fun h => List.noConfusion h)


I do not understand this definition, in particular the details around the recursive call.

1. Why is the last argument a lambda, when the signature seems to suggest a proof?
2. What is List.noConfusion, where is it defined, and how does it relate to the "No Confusion" rule in general?
3. Here's the type of List.noConfusion:
List.noConfusion.{u_1, u} {α : Type u} {P : Sort u_1} {v1 v2 : List α} (h12 : v1 = v2) : List.noConfusionType P v1 v2


How should I interpreter this? What is noConfusionType?

• If it's any help, I wrote a blog post about the Lean 3 version of no_confusion here xenaproject.wordpress.com/2018/03/24/… . I believe that List.noConfusion is generated automatically by Lean 4 when you make List. Commented Oct 3, 2023 at 17:08
• As to where List.noConfusion is defined see this answer: proofassistants.stackexchange.com/a/1664/122. However it is slightly different in Lean 4. Namely these automatic theorems are hidden until they are used by some automation in Lean, like simp or what you are seeing. Commented Oct 3, 2023 at 20:36
• Small correction: It is just List.getLast. No Data. Commented Oct 3, 2023 at 20:46

The "no confusion" in type theory is a characterizing property of constructors, say, if two terms of an inductive type are generated from different constructors, they should be unequal.

Why is the last argument a lambda, when the signature seems to suggest a proof?

They are the same. a ≠ b is usually defined as a = b → False, which you usually prove via introducing a lambda.

where is it (no confusion) defined

Seems like it's defined internally (correct me if I'm wrong).

The noConfusionType should be similar to something you generate in Haskell from deriving Eq, which is a two-arg pattern matching function that returns the unit type when v1 and v2 are of the same constructor and the empty type otherwise.

• "no confusion" is different from "injective"! The three pillars of inductive types are "no confusion", "injective" and "occurs check" (and reflexivity), in the paper Eliminating Dependent Pattern Matching.
– Trebor
Commented Oct 3, 2023 at 16:28
• I love how computer scientists start counting at 0 ;-) Commented Oct 3, 2023 at 17:18
• Edited to address the mistake 😵
– ice1000
Commented Oct 3, 2023 at 18:48