Zulip Chat Archive

Stream: Is there code for X?

Topic: nth_le with different le

view this post on Zulip Chase Norman (Dec 26 2020 at 20:37):

Is there a way to prove that list.nth_le l i a = list.nth_le l i b for distinct le proofs a and b? I'm failing to accomplish a simp_rw because of this distinction. Alternatively, is there a way to prove the inhabited type-class in tactic mode using a witness element? My trouble arises from not being able to express l.head' in terms of list.nth_le l 0 _.

view this post on Zulip Bhavik Mehta (Dec 26 2020 at 20:39):

I think rfl should work for the first question

view this post on Zulip Mario Carneiro (Dec 26 2020 at 20:50):

for the second:

import data.list.basic

namespace list
variables {α : Type*}
lemma nth_zero (l : list α) : l.nth 0 = l.head' := by cases l; refl
end list

example {α} (l : list α) (h) : l.head' = some (l.nth_le 0 h) :=
by rw [ list.nth_zero, list.nth_le_nth]

Last updated: May 07 2021 at 21:10 UTC