list.nth_le

Stream: new members

[Cerek Hillen (he) (W2'20)]

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

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

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]

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

[Kevin Buzzard]

so this is a bit of a dirty hack

[Kevin Buzzard]

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

[Cerek Hillen (he) (W2'20)]

hahaha oh no that is definitely a dirty hack

[Kevin Buzzard]

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]

maybe nat.lt_of_succ_le?

[Kevin Buzzard]

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

[Cerek Hillen (he) (W2'20)]

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]

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)