feat(Data): Results about RelatesInSteps with bounds on the reachable set

[crei]

If the number of elements reachable from an element a along a relation r is at most k, then any of those elements can be reached in at most k - 1 steps.

This is a generalization of a result in #767, which was specific for Turing machine configurations (that PR still needs to be adapted).

This PR adds that result and introduces the notion of "Path": A function ℕ → α where successive values are related, up to a path length (it could be debated to use Fin n instead of ℕ).

I believe that going back and forth from relation to path is useful in the future for various computation models.

Note that Mathlib has a notion similar to "Path" called RelSeries. I did not re-use it because it is defined on top of sets of pairs instead of relations.

AI disclosure: LLMs were used in creating this PR but everything was carefully edited and reviewed.

[fmontesi]

Why is this not just a list of elements? This reminds me a lot of Execution in LTS and its omega-counterpart. What you have here looks like the omega-sequence infinite execution concept, but you use only a finite part of it.

@ctchou, what do you think?

[fmontesi]

In general I'm otherwise very positive about this. We should just make sure that the API experience between Relation and LTS for these things is similar enough to be familiar to people using both.

[thomaskwaring]

for a list this is exactly List.IsChain — i would advocate not duplicating that definition (EDIT: by which i mean using that definition instead of IsPath — unless there is some reason the indexing over Nat is necessary)

[thomaskwaring]

on this point, here's the equivalent RelatesInSteps.exists_isPath phrased using List.IsChain — to my mind the proof is simpler

theorem RelatesInSteps.exists_isChain {a b : α} {n : ℕ} (h : RelatesInSteps r a b n) :
    ∃ (l : List α), (a :: l).IsChain r ∧ b ∈ (a :: l).getLast? ∧ l.length = n := by
  induction h using RelatesInSteps.head_induction_on with
  | hrefl => use (discharger := simp) []
  | @hhead a c n h h' ih =>
    obtain ⟨l, hchain, hb, hlen⟩ := ih
    use c :: l
    grind

for other results, note the existing api connected to Relation.ReflTransGen, and List.isChain_ofFn, which is more-or-less the Fin n version of your IsPath

[thomaskwaring]

i think using Set.ncard on the predicate ReflTransGen r (f 0) should be considered defeq abuse — the preferred spelling would be Set.ncard {x | ReflTransGen r (f 0) x}. also, the assumptions hfin and hn can be collapsed to Set.encard {...} ≤ n

[crei]

I wonder if it makes sense to give this a name:

abbrev ReachableFrom (r : α → α → Prop) (a : α) := {x | ReflTransGen r a x}