Case split on prop

Stream: general

[Patrick Stevens]

Here's something that doesn't work:

import Batteries.Data.Nat.Basic
def position_of (elt : List.Mem 3 [4,3,6]) : Nat :=
  match elt with
  | .head _ => sorry
  | .tail _ => sorry

The head block does not type check - of course it can't! - and this prevents compilation. How can I access the fact that List.Mem knows where the 3 is?

The XY of this is that I want to convert this function so that it outputs data rather than a Prop: I want to know which k it found, along with a proof that the k has the property. (Changing the "exists" to a Sum fails because the equality proof is a Prop.) I think it should be possible to do this without any need to decide equality, because Mem already knows where the element is.

import Batteries.Data.Nat.Basic
import Batteries.Data.List.Basic
import Mathlib.Tactic.Use

def hits'
  {m : Nat} {B : Type}
  (f : Fin m → B)
  {r : B} {n i : Nat} {pr : n + i = m}
  (elt : List.Mem r (List.ofFn.go f n i pr))
  : ∃ k, f k = r
  := by
  match n with
  | 0 =>
    exfalso
    unfold List.ofFn.go at elt
    exact (List.mem_nil_iff r).mp elt
  | n + 1 =>
  rcases elt with _ | ⟨_, isMem⟩
  · use ⟨i, by omega⟩
  · exact @hits' m B f r n (i + 1) (by omega) isMem

[Henrik Böving]

List.Mem does not actually know where 3 is. Lean erases propositions at compile time so you cannot create any data (i.e. anything that is not a proposition) from a proposition. You can encode Membership in a way that lives in Type and explicitly tracks the index at which the element is but that is not possible with the built in List.Mem.

[Patrick Stevens]

Ah right - is the reason List.Mem was defined as a Prop simply runtime efficiency, or does Prop have any other benefits to outweigh the fact that it's harder to compute with?

[Henrik Böving]

Proof irrelvance also helps doing other proofs, e.g. when proving equality of subtypes etc. There is just, not much of a reason to define it not as Prop I think.

[Kyle Miller]

You can make a function that, using DecidableEq and a membership proof, gives you the first index.

[Kyle Miller]

This sort of fits the bill: docs#List.indexOf_lt_length

[Patrick Stevens]

The annoying part of that is I'm doing this so as to prove that Mathlib.ModelTheory.Syntax's Term has decidable equality; this is the recursive case, Term.func f (vars : Fin n -> Term), and I don't trivially have access to the proof of decidability yet

[Patrick Stevens]

Somewhere in my proof I have implicitly computed the index, I just need to thread it through a bunch of functions (and I was hoping it could be derived from the Mem instead)

[Kyle Miller]

Maybe you could use the type {n : Nat // lst.get? n = v} instead, or something like it?

[Patrick Stevens]

Thanks, that's working out well I think and is a very simple change!