pw_filter is maximal

Stream: Is there code for X?

[Yaël Dillies]

@Mario Carneiro, is this true?

import data.list.pairwise

protected lemma sublist.pw_filter [is_trans α R] :
  ∀ {l₁ l₂ : list α}, l₁ <+ l₂ → pairwise R l₁ → l₁ <+ pw_filter R l₂

or maybe with is_prefix or is_suffix instead? Or using list.chain?

[Mario Carneiro]

No, it's not maximal in that sense. For example if the relation is R _ _ := false (so only singletons qualify). then [b] <+ [a, b] and pairwise R [b] but pw_filter R [a, b] = [a] and [b] <+ [a] is false

[Mario Carneiro]

However, you could say

protected lemma sublist.pw_filter [is_trans α R] : ∀ {l₁ l₂ : list α},
  l₁ <+ l₂ → pairwise R l₁ → pw_filter R l₂ <+ l₁ → pw_filter R l₂ = l₁

[Yaël Dillies]

Should I then use list.chain instead?

[Mario Carneiro]

I'm not sure what you mean. That theorem isn't true even with chain. It's a maximal sublist, not a maximum sublist (which may not even exist)