English
In a Nodup list l, for every index i with i < length(l), the next element after l[i] is the element at index (i+1) modulo length(l).
Русский
В списке без повторов l для каждого индекса i с i < length(l) следующий после l[i] элемент равен элементу с индексом (i+1) по модулю length(l).
LaTeX
$$$l.next\ (l[i])\ (get\_mem\ _\ _) = l[(i+1) \% l.length].$$$
Lean4
theorem next_getElem (l : List α) (h : Nodup l) (i : Nat) (hi : i < l.length) :
next l l[i] (get_mem _ _) = (l[(i + 1) % l.length]'(Nat.mod_lt _ (i.zero_le.trans_lt hi))) :=
match l, h, i, hi with
| [], _, i, hi => by simp at hi
| [_], _, _, _ => by simp
| x :: y :: l, _h, 0, h0 => by
have h₁ : (x :: y :: l)[0] = x := by simp
rw [next_cons_cons_eq' _ _ _ _ _ h₁]
simp
| x :: y :: l, hn, i + 1, hi =>
by
have hx' : (x :: y :: l)[i + 1] ≠ x := by
intro H
suffices (i + 1 : ℕ) = 0 by simpa
rw [nodup_iff_injective_get] at hn
refine Fin.val_eq_of_eq (@hn ⟨i + 1, hi⟩ ⟨0, by simp⟩ ?_)
simpa using H
have hi' : i ≤ l.length := Nat.le_of_lt_succ (Nat.succ_lt_succ_iff.1 hi)
rcases hi'.eq_or_lt with (hi' | hi')
· subst hi'
rw [next_getLast_cons]
· simp
· rw [getElem_cons_succ]; exact get_mem _ _
· exact hx'
· simp [getLast_eq_getElem]
· exact hn.of_cons
· rw [next_ne_head_ne_getLast _ _ _ _ _ hx']
· simp only [getElem_cons_succ]
rw [next_getElem (y :: l), ← getElem_cons_succ (a := x)]
· congr
dsimp
rw [Nat.mod_eq_of_lt (Nat.succ_lt_succ_iff.2 hi'),
Nat.mod_eq_of_lt (Nat.succ_lt_succ_iff.2 (Nat.succ_lt_succ_iff.2 hi'))]
· simp [Nat.mod_eq_of_lt (Nat.succ_lt_succ_iff.2 hi'), hi']
· exact hn.of_cons
· rw [getLast_eq_getElem]
intro h
have := nodup_iff_injective_get.1 hn h
simp at this; simp [this] at hi'
· rw [getElem_cons_succ]; exact get_mem _ _
