How to get element of list?

Stream: new members

[Rui Liu]

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,
    contradiction,
    have h1 := list.length_cons hd tl,
    rw h1 at h,
    by_cases h2: i < tl.length,
    exact htl h2,
end

[Alex J. Best]

This is in core as docs#list.nth_le

[Alex J. Best]

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]

@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]

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

[Reid Barton]

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]

or in this case, using the equation compiler