English
For two sequences a and b with a motive relating their lengths, there is a step that decomposes and preserves the relation, yielding b.length' ≤ a.length'.
Русский
Для двух последовательностей a и b существует мотив, обеспечивающий сравнение их длины; разложение сохраняет отношение и в итоге получается b.length' ≤ a.length'.
LaTeX
$$$\\text{motive } a b \\land (\\forall a' b', \\; \\text{motive } a' b' \\Rightarrow \\text{лечь}) \\Rightarrow b.$length' \\le a.$length'$$
Lean4
/-- Coinductive principle for proving `b.length' ≤ a.length'` for two sequences `a` and `b`. -/
theorem at_least_as_long_as_coind {a : Seq α} {b : Seq β} (motive : Seq α → Seq β → Prop) (base : motive a b)
(step :
∀ a b, motive a b → (∀ b_hd b_tl, (b = .cons b_hd b_tl) → ∃ a_hd a_tl, a = .cons a_hd a_tl ∧ motive a_tl b_tl)) :
b.length' ≤ a.length' :=
by
have (n) (hb : b.drop n ≠ .nil) : motive (a.drop n) (b.drop n) := by
induction n with
| zero => simpa
| succ m ih =>
simp only [drop] at hb ⊢
generalize b.drop m = tb at *
cases tb with
| nil => simp at hb
| cons tb_hd tb_tl =>
simp only [ne_eq, cons_ne_nil, not_false_eq_true, forall_const] at ih
obtain ⟨a_hd, a_tl, ha, h_tail⟩ := step (a.drop m) (.cons tb_hd tb_tl) ih _ _ rfl
simpa [ha]
by_cases ha : a.Terminates; swap
· simp [length'_of_not_terminates ha]
simp [length'_of_terminates ha, length'_le_iff]
by_contra! hb
have hb_cons : b.drop (a.length ha) ≠ .nil := by
intro hb'
simp only [← length'_eq_zero_iff_nil, drop_length', tsub_eq_zero_iff_le, length'_le_iff] at hb'
contradiction
specialize this (a.length ha) hb_cons
generalize b.drop (a.length ha) = b' at *
cases b' with
| nil => contradiction
| cons b_hd b_tl =>
obtain ⟨a_hd, a_tl, ha', _⟩ := step _ _ this _ _ rfl
apply_fun length' at ha'
simp only [drop_length', length'_of_terminates ha, tsub_self, length'_cons] at ha'
generalize a_tl.length' = u at ha'
enat_to_nat
omega
