# Pattern matching from Prop to Type in Lean

I'm a beginner in the world of proof assistants, and have been taking a look at Lean4 lately.

I wanted to write a function like

def List.index : (x : α) → {xs : List α // x ∈ xs} → Nat
| x, ⟨_ :: xs, ok⟩ =>
match ok with
| List.Mem.tail _ t => 1 + List.index x ⟨xs, t⟩


But when I do it, I receive the following error:

tactic 'cases' failed, nested error:
tactic 'induction' failed, recursor 'List.Mem.casesOn' can only eliminate into Prop
α : Type ?u.87469
x : α
xs : List α
ok✝¹ : x ∈ head✝ :: xs
motive : (head : α) → x ∈ head :: xs → Sort ?u.87826
h_1 : Unit → motive x (_ : Mem x (x :: xs))
h_2 : (x_1 : α) → (t : Mem x xs) → motive x_1 (_ : Mem x (x_1 :: xs))
a✝ : List α
ok✝ : Mem x a✝
⊢ head✝ :: xs = a✝ → HEq ok✝¹ ok✝ → motive head✝ ok✝¹ after processing
_, _
the dependent pattern matcher can solve the following kinds of equations
- <var> = <term> and <term> = <var>
- <term> = <term> where the terms are definitionally equal
- <constructor> = <constructor>, examples: List.cons x xs = List.cons y ys, and List.cons x xs = List.nil


If I write my own instance of Mem, with it being a Type, it works perfectly:

inductive MyMem (a : α) : List α → Type
| head (as : List α) : MyMem a (a::as)
| tail (b : α) {as : List α} : MyMem a as → MyMem a (b::as)

def List.index' : (x : α) → (xs : List α) → (ok : MyMem x xs) → Nat
| x, _ :: xs, ok =>
match ok with
| MyMem.tail _ t => 1 + List.index' x xs t


But, as soon as I set it as a Prop, the same error comes up. Am I doing something wrong? I'm a bit confused about this.

There are situations in which every morphism $$A \to B$$ is constant:

1. In topological spaces, if $$A$$ is a space with the trivial topology and $$B$$ is a $$T_0$$-space then a continuous map $$A \to B$$ is constant.
2. In partial orders, if $$A$$ is a linear order and $$B$$ is the discrete partial order then every monotone map $$A \to B$$ is constant.
3. Somewhat more exotically, but significant for type theory, in a realizability topos every morphism $$\nabla A \to B$$ with $$B$$ a modest assembly is constant.

In type theory, or some other formalism, we might wish to capture situations like these with a suitable formalism. One way of doing this is to simply declare that, under certain circumstances, a map $$f : A \to B$$ may not “look” at its argument (by using match or some such), thereby ensuring that it is constant.

In Lean we have such a situation. If $$A : \mathsf{Prop}$$ and $$B : \mathsf{Type}$$, then when defining a map $$A \to B$$ it is prohibited to match on the argument.

Why would anyone want this? If we think of $$A : \mathsf{Prop}$$ as a logical statement then $$a : A$$ is like a proof, or evidence, that $$A$$ holds. We may postulate that, even though there are many proofs of $$A$$, they are all to be considered “equal” or “indistinguishable”, at least for the purposes of mapping from $$A$$ to $$B : \mathsf{Type}$$.

For example, let $$\mathsf{bounded}(h) \mathbin{:=} \exists M : \mathbb{R} .\, \forall x : [0,1] .\, h(x) \leq M$$ be the statement “$$h$$ is bounded on $$[0,1]$$“ and consider the type $$A = \Sigma (h : [0,1] \to \mathbb{R}) \,. \mathsf{bounded}(h)$$ of bounded real-valued maps on $$[0,1]$$. The map $$f : A \to \mathbb{R}$$ defined by $$f(h, (M, \_)) \mathbin{:=} M$$ should not be considered well-defined, because it depends on the existential witness $$M$$, of which there are many. (If one wanted to have such an $$f$$, one can always define $$\mathsf{bounded}(h)$$ with $$\Sigma$$ in place of $$\exists$$.)

It still makes sense to allow matching on a proof when the codomain is a proposition. Continuing the example, the type $$\Pi (f : [0,1] \to \mathbb{R}) .\, \mathsf{bounded}(f) \to \mathsf{bounded}(\lambda x.f(x) + 42)$$ is inhabited by the proof “given a bound $$M$$ of $$f$$, $$M + 42$$ is a bound for $$\lambda x.f(x) + 42$$“. This proof “looks at $$M$$” because its output depends on $$M$$.

• I think it might be useful to mention, one reason why we don't want to look at and depend on Prop arguments of functions is erasure — we'd like to erase all our proofs at compile time and don't carry them around at run time (for reasons of efficiency). Jun 8, 2023 at 14:04
• Yes, that is another good reason. Jun 8, 2023 at 20:56

Short answer (probably the same as on Zulip, I didn't check): With proof irrelevance it doesn't make sense to match on an inductive Prop. This is what this error signifies:

tactic 'induction' failed, recursor 'List.Mem.casesOn' can only eliminate into Prop

There is, of course, one important exception where the motive is also a Prop. However, in the example for the question the motive is Nat.

This was already solved in the Lean4 Zulip chat.

• It might be good if you write a brief summary of the link. StackExchange contents are meant to be mostly self-contained. (I can answer the question myself later if you can't find time.)
– Trebor
May 4, 2023 at 18:54