Quantifying over words through a prefix

A predicate that looks only at the first n entries of a word of length m ≥ n holds for some (every) such word exactly when it holds for some (every) word of length n: a short word is the prefix of its padding (List.exists_length_eq_take_iff, List.forall_length_eq_take_iff). Complexity-class arguments use this to pad certificate blocks to longer, uniform or easily computed lengths and let the verifier cut them back.

Main results

• List.exists_length_eq_take_iff, List.forall_length_eq_take_iff: quantifying over words of length m through their length-n prefix quantifies over words of length n.

theorem List.exists_length_eq_take_iff {α : Type u_1} [Nonempty α] {n m : ℕ} {P : List α → Prop} (h : n ≤ m) : (∃ (w : List α), w.length = m ∧ P (take n w)) ↔ ∃ (w : List α), w.length = n ∧ P w

Some word of length m ≥ n has a length-n prefix satisfying P exactly when some word of length n satisfies P.

theorem List.forall_length_eq_take_iff {α : Type u_1} [Nonempty α] {n m : ℕ} {P : List α → Prop} (h : n ≤ m) : (∀ (w : List α), w.length = m → P (take n w)) ↔ ∀ (w : List α), w.length = n → P w

Every word of length m ≥ n has a length-n prefix satisfying P exactly when every word of length n satisfies P.