feat: List.forall_get_iff_forall_mem

[Qiu233]

theorem forall_mem_iff_forall_index [DecidableEq α] {p : α → Prop} {l : List α} :
  (∀ x ∈ l, p x) ↔ (∀ i : Fin (l.length), p (l.get i))

is trivial but sometimes useful.

[Qiu233]

awaiting-review

[digama0]

I usually obtain the headline theorem using simp [List.mem_iff_get]. The other stuff is more API surface that should probably be considered in its own PR.

[Qiu233]

I usually obtain the headline theorem using simp [List.mem_iff_get]. The other stuff is more API surface that should probably be considered in its own PR.

Sorry I didn't find this theorem. Now other stuff has been removed.

[semorrison]

Suggested change

	theorem forall_mem_iff_forall_index {p : α → Prop} {l : List α} :
	(∀ x ∈ l, p x) ↔ (∀ i : Fin (l.length), p (l.get i)) :=
	⟨fun h i => h _ (get_mem l i.1 i.2),
	fun h _ hx => by have ⟨_, hi⟩ := mem_iff_get.mp hx; simp only [← hi, h]⟩
	theorem forall_mem_iff_forall_index {p : α → Prop} {l : List α} :
	(∀ x ∈ l, p x) ↔ (∀ i : Fin (l.length), p (l.get i)) := by
	simp [List.mem_iff_get]

[semorrison]

What is the use case of this theorem?

[Qiu233]

What is the use case of this theorem?

Sometimes some propositions of List are expressed in indexed form, especially when translating algorithm proof from CS books.

I struggled with it for hours and it's until this issue then I know the existence of List.mem_iff_get which derives this theorem. Without it there may be someone else facing the same trouble again.

[semorrison]

Sorry about the slow reply here. Let's reverse the iff, rename to forall_get_iff_forall_mem, and maybe even mark this as @[simp].

[Qiu233]

Done.

[digama0]

I think it shouldn't be @[simp]; this will not fire reliably anyway (only the RTL direction looks like it would match), and whether it is better to use indexing or membership in a given context is very dependent on other factors.