Pattern matching from `Prop` to `Type` in Lean

Question

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.head _ => 0
      | 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 α
head✝ : α
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.head _ => 0
      | 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.

Answer 1

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$.

Answer 2

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.

Answer 3

This was already solved in the Lean4 Zulip chat.