## Stream: new members

### Topic: How to get element of list?

#### Rui Liu (Dec 08 2020 at 01:16):

Any idea of how to prove: def list_at: Π {a: Type}, Π l: list a, Π i: ℕ, i < l.length → a?

Here's one of my WIP version, I don't know prove some property of natural number arithmetic... Basically how to split a case of i < tl.length + 1 into two cases of i < tl.length and i = tl.length?

def list_at: Π {a: Type}, Π l: list a, Π i: ℕ, i < l.length → a := begin
intros a l i h,
induction l with hd tl htl,
have nh := nat.not_lt_zero i,
have h1 := list.length_cons hd tl,
rw h1 at h,
by_cases h2: i < tl.length,
exact htl h2,
end


#### Alex J. Best (Dec 08 2020 at 01:17):

This is in core as docs#list.nth_le

#### Alex J. Best (Dec 08 2020 at 01:19):

If you look at src#list.nth_le you can see its defined using the equation compiler, which is normally easier for these inductive definitions. In fact its really not recommended to use tactic mode to make defs as tactics can introduce a lot of unwanted clutter in your definitions.

#### Rui Liu (Dec 08 2020 at 14:54):

@Alex J. Best Why is it not recommended to use tactic mode to make def? Is it purely because the resulting definition is more complicated? Or is there more reasons to it?

#### Eric Wieser (Dec 08 2020 at 15:01):

Because you're likely in for a bad time if you try and unfold the definition in a proof

#### Reid Barton (Dec 08 2020 at 15:01):

Assuming you intend to prove something about the def later, the form of the proof will depend on exactly what term makes up the definition anyways, and so life is easier if you just write down that term explicitly in the first place

#### Reid Barton (Dec 08 2020 at 15:02):

or in this case, using the equation compiler

Last updated: Dec 20 2023 at 11:08 UTC