Zulip Chat Archive

Stream: new members

Topic: list.nth_le


Cerek Hillen (he) (W2'20) (Jan 30 2020 at 17:23):

hey y'all, looking at the implementation of list.nth_le, and i was confused about how the definition works

Cerek Hillen (he) (W2'20) (Jan 30 2020 at 17:23):

ref: https://github.com/leanprover/lean/blob/master/library/init/data/list/basic.lean#L90-L93

@[simp] def nth_le : Π (l : list α) (n), n < l.length → α
| []       n     h := absurd h (not_lt_zero n)
| (a :: l) 0     h := a
| (a :: l) (n+1) h := nth_le l n (le_of_succ_le_succ h)

Cerek Hillen (he) (W2'20) (Jan 30 2020 at 17:24):

in particular, how can it use le_of_succ_le_succ on h when h is defining a strict inequality? i'm trying to replicate similar behavior but Lean is complaining about the differences in equality

Kevin Buzzard (Jan 30 2020 at 17:24):

On nat, a < b is defined to mean a + 1 <= b

Kevin Buzzard (Jan 30 2020 at 17:24):

so this is a bit of a dirty hack

Kevin Buzzard (Jan 30 2020 at 17:25):

example (a b : ℕ) : a < b ↔ a + 1 ≤ b := iff.rfl

Cerek Hillen (he) (W2'20) (Jan 30 2020 at 17:25):

hahaha oh no that is definitely a dirty hack

Kevin Buzzard (Jan 30 2020 at 17:26):

For more readability they should also apply a + 1 <= b -> a < b but this theorem might not even be in the library because it's true by definition :-/

Kevin Buzzard (Jan 30 2020 at 17:26):

maybe nat.lt_of_succ_le?

Kevin Buzzard (Jan 30 2020 at 17:27):

lemma lt_of_succ_le {a b : ℕ} (h : succ a ≤ b) : a < b := h -- from core.

Cerek Hillen (he) (W2'20) (Jan 30 2020 at 17:33):

i'll just provide a more explicit proof--i'm rewriting some code for the purposes of a presentation on why SWEs should like dependent typing so it's better if it's more explicit

Mathieu Guay-Paquet (Feb 01 2020 at 21:40):

Note that the core library already has a lemma called nat.lt_of_succ_lt_succ (see this link, where it's just defined as a synonym for le_of_succ_le_succ, but with the right type annotation)


Last updated: Dec 20 2023 at 11:08 UTC