Maximal suffix/prefix of list satisfying the property exists

Stream: Is there code for X?

[Jihoon Hyun]

I had to use the following theorem in my project, and this theorem looks quite useful. Is there a code for this theorem?

protected theorem List.exists_maximal_suffix {α : Type _} {l : List α} {p : List α → Prop}
  (hp_empty : p []) (hp_suffix : ∀ l, p l → (∀ l', l' <:+ l → p l')) :
    ∃ l', l' <:+ l ∧ p l' ∧ (∀ l'', l'' <:+ l → p l'' → l''.length ≤ l'.length) := by
  induction' l with h l ih <;> simp [hp_empty]
  have ⟨l', hl'₁, hl'₂, hl'₃⟩ := ih
  by_cases h₁ : l' = l
  . by_cases h₂ : p (h :: l)
    . exists h :: l
      simp only [List.suffix_rfl, h₂, true_and]
      exact fun _ h _ => List.isSuffix.length_le h
    . exists l
      rw [h₁] at hl'₂
      simp only [suffix_cons, hl'₂, true_and]
      intro _ h₃ h₄
      rw [List.suffix_cons_iff] at h₃
      apply h₃.elim <;> intro h₃
      . rw [h₃] at h₄
        contradiction
      . exact List.isSuffix.length_le h₃
  . exists l'
    simp only [hl'₂, true_and]
    constructor
    . rw [List.suffix_cons_iff]; exact Or.inr hl'₁
    . intro _ h₂ h₃
      rw [List.suffix_cons_iff] at h₂
      apply h₂.elim <;> intro h₂
      . exfalso
        exact h₁ (List.isSuffix.eq_of_length hl'₁ (Nat.le_antisymm (List.isSuffix.length_le hl'₁)
          (hl'₃ _ List.suffix_rfl (hp_suffix _ (h₂ ▸ h₃) _ (List.suffix_cons _ _)))))
      . exact hl'₃ _ h₂ h₃

[Yakov Pechersky]

Isn't the witness to this just l.reverse.take_while p.reverse?

[Jihoon Hyun]

Yes, it seems like there is a function List.rtakeWhile for the reversed takeWhile, and there are bunch of lemmas such as rtakeWhile_suffix..

[Jihoon Hyun]

How do you find such definitions and lemmas which you want? I spend several minutes searching for desired definitions or lemmas, and after asking here it always turns out there exists one.

[Yakov Pechersky]

I knew about take while. And since you're talking about the retention of suffixes that satisfy predicates, it was a matter of composition. Although now I realize that my predicate was on your elements, yours is on the list itself. So my witness needs to be rejiggered to mention sublists or suffixes or something.