Zulip Chat Archive

Stream: new members

Topic: How to get element of list?


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

view this post on Zulip Alex J. Best (Dec 08 2020 at 01:17):

This is in core as docs#list.nth_le

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Reid Barton (Dec 08 2020 at 15:02):

or in this case, using the equation compiler


Last updated: May 14 2021 at 22:15 UTC