Commit 2025-09-17 05:19 81dcdf5c

View on Github →

feat(Data/Seq): coinductive predicates for sequences (#28874)

  • Prove eq_of_bisim' and eq_of_bisim_strong coinductive principles for equality.
  • Develop API for a predicate ∀ x ∈ s, p x where s : Seq α, including coinductive principle all_coind.
  • Introduce the Pairwise predicate along with API and coinductive principles Pairwise.coind and Pairwise.coind_trans.
  • Introduce ENat-valued length of a sequence, length', along with minimal API.
  • Move theorems about length from Defs.lean to Basic.lean.
  • Prove a coinductive principle for a predicate a.length' ≤ b.length'.

All of these "coinductive principles" are stated in the form as similar as possible to inductive principles.

Estimated changes

added theorem Stream'.Seq.all_coind
added theorem Stream'.Seq.all_cons
added theorem Stream'.Seq.all_get
added theorem Stream'.Seq.all_of_get
added theorem Stream'.Seq.drop_zero
added theorem Stream'.Seq.length_nil
added theorem Stream'.Seq.set_all
added theorem Stream'.Seq.take_all
deleted theorem Stream'.Seq.length_le_iff
deleted theorem Stream'.Seq.length_nil
deleted theorem Stream'.Seq.lt_length_iff