English
If l1 is a sublist of l2 and l1 is an R-chain, then the length of l1 is at most the length of the destutter of l2 with respect to R.
Русский
Если l1 является подпоследовательностью l2, и l1 образует R-цепочку, тогда длина l1 не превосходит длины destutter_R(l2).
LaTeX
$$$l_1 \\subseteq l_2 \\Rightarrow (l_1 \\text{ IsChain } R) \\Rightarrow |l_1| \\le |\\mathrm{destutter}_R(l_2)|$$$
Lean4
/-- `destutter` of relations like `≠`, whose negation is an equivalence relation,
gives a list of maximal length over any chain.
In other words, `l.destutter R` is an `R`-chain sublist of `l`, and is at least as long as any other
`R`-chain sublist. -/
theorem length_le_length_destutter [IsEquiv α Rᶜ] :
∀ {l₁ l₂ : List α}, l₁ <+ l₂ → l₁.IsChain R → l₁.length ≤ (l₂.destutter R).length
| [], [], _, _ => by
simp
-- `l₁ := l₁`, `l₂ := a :: l₂`
| l₁, _, .cons (l₂ := l₂) a hl, hl₁ =>
(hl₁.length_le_length_destutter hl).trans length_destutter_le_length_destutter_cons
| _, _, .cons₂ (l₁ := []) (l₂ := l₁) a hl, hl₁ => by
simp [Nat.one_le_iff_ne_zero]
-- `l₁ := a :: l₁`, `l₂ := a :: b :: l₂`
| _, _, .cons₂ a <| .cons (l₁ := l₁) (l₂ := l₂) b hl, hl₁ =>
by
by_cases hab : R a b
· simpa [destutter_cons_cons, hab] using hl₁.tail.length_le_length_destutter (hl.cons _)
·
simpa [destutter_cons_cons, hab] using
hl₁.length_le_length_destutter
(hl.cons₂ _)
-- `l₁ := a :: b :: l₁`, `l₂ := a :: b :: l₂`
| _, _, .cons₂ a <| .cons₂ (l₁ := l₁) (l₂ := l₂) b hl, hl₁ => by
simpa [destutter_cons_cons, rel_of_isChain_cons_cons hl₁] using hl₁.tail.length_le_length_destutter (hl.cons₂ _)
