List.mem

Stream: mathlib4

[Kevin Buzzard]

namespace List

def mem : α → List α → Prop
| a, [] => False
| a, h :: t => a = h ∨ mem a t

end List

would work for me, but I'm not sure it's Lean 4 style. Judging by Lean 4 definition of List.length

def List.lengthAux {α : Type u} : List α → Nat → Nat
  | nil,       n => n
  | cons a as, n => lengthAux as (Nat.succ n)

def List.length {α : Type u} (as : List α) : Nat :=
  lengthAux as 0

they are taking tail recursion seriously. What is a fast implementation of List.mem? Where does one look to answer such a question? Of course if you go for speed you still have to prove List.length_cons right?
they are taking

[Daniel Fabian]

@Kevin Buzzard, since lean is implemented in lean, the core functions really want to be as fast as possible. Arrays are also used quite a lot. If you care mostly about proving things, you can probably be a bit less careful and focus on making proofs easier.

The core of lean functions were written with performance at mind, because it's quite important for the compiler itself. And given the size of some of the functions, and thus expressions, it does matter.

On the other hand, how much do you plan to rely on evaluation to prove things? Do you plan to prove things mostly by rfl, i.e. computation or not? It is my understanding, that in mathlib3, at least, computation doesn't really play much of a role. In fact, quite a lot of definitions are noncomputable, correct?

[Kevin Buzzard]

Yes, we do not rely too much on definitional equality "higher up the food chain", however for things like List it's a different story with lots of cheeky rfl abuse in mathlib3.

[Kevin Buzzard]

I've since found List.elem but it assumes BEq (lawless decidable equality)

[Mario Carneiro]

List.mem has been defined in Data.List.Basic, as well as List.length' and List.append' which use the "naive" implementations with better defeq rather than the tail recursive versions in the core library. (I'm still not sure how much we should make use of those functions over the ones in the core library for proving activities.)

[François G. Dorais]

Using implementedBy would be a convenient compromise:

def lengthImplAux : List α → Nat → Nat
  | List.nil, n => n
  | List.cons a as, n => lengthImplAux as n.succ

def lengthImpl (as : List α) : Nat := lengthImplAux as 0

@[implementedBy lengthImpl]
def length : List α  → Nat
| [] => 0
| _::t => length t + 1

example (x : α) (xs : List α) : length (x::xs) = length xs + 1 := rfl -- works
example (x : α) (xs : List α) : lengthImpl (x::xs) = lengthImpl xs + 1 := rfl -- fails

However, as far as actual code generated, length and lengthImpl are the same: they both generate the more efficient tail recursive code.

Admittedly, every instance of implementedBy is a "trust me" statement, which doesn't look good in the core library! But, as a counterpoint, complicated code without any proof that it satisfies the expected equations is not trustworthy either.

[Mario Carneiro]

I agree that length' should use implementedBy length in mathlib, and if we can get it upstreamed length' should become length and length should become lengthImpl

[Mario Carneiro]

I don't think we should be stingy with implementedBy in the library since it is able to resolve the tradeoff between ease of proving and performance

[Mario Carneiro]

When we get the ability to do custom attributes, we can add a variant on implementedBy that requires a proof of equality, so that we can also avoid growing the compiler TCB