3
$\begingroup$

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.

$\endgroup$

3 Answers 3

5
$\begingroup$

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

$\endgroup$
2
  • 1
    $\begingroup$ 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). $\endgroup$ Jun 8, 2023 at 14:04
  • 1
    $\begingroup$ Yes, that is another good reason. $\endgroup$ Jun 8, 2023 at 20:56
1
$\begingroup$

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.

$\endgroup$
0
$\begingroup$

This was already solved in the Lean4 Zulip chat.

$\endgroup$
1
  • 8
    $\begingroup$ 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.) $\endgroup$
    – Trebor
    May 4, 2023 at 18:54

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.