# 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. Oct 3 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. Oct 3 at 20:36
• Small correction: It is just List.getLast. No Data. Oct 3 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
Oct 3 at 16:28
• I love how computer scientists start counting at 0 ;-) Oct 3 at 17:18
• Edited to address the mistake 😵 Oct 3 at 18:48