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}

[ctchou]

Sorry, I just saw this PR. I agree with @thomaskwaring that List.IsChain probably can do everything that IsPath can and has the advantage of having the enormous set of results about List in mathlib at its disposal.

Another potential problem with IsPath is that only the first n elements of the infinite sequence f matter. So when you need to exhibit an f, you need to supply a dummy value for all elements in f beyond the first n elements. This is not exactly elegant and may require you to add an assumption like [Inhabited α] in some situations.

[ctchou]

Since you don't refer to h_len below, you can replace it by _.

[ctchou]

It seems to me that the comments on these theorems do not accurately describe the contents of the theorems, because the word "chain" in these comments really refers to RelatesInSteps, rather than List.IsChain. One can imagine perfectly reasonable theorems fitting these comments that use List.IsChain instead.

[ctchou]

Personally I think the last part of the statement would have been clearer if you explicitly require the set being finite for the cardinality comparison. But that's just me and I don't insist on it.

More seriously, it seems to me that the real mathematical content of this theorem is that there is a shortest path from a to b in which there is no duplication of elements. I think you should try to phrase and prove that theorem in terms of List.IsChain and then derive this theorem as a corollary.

[crei]

I think both versions (with finiteness and Finset.card / just .encard) have their advantages and disadvantages. I like the current version better because it can be used both for finite and infinite sets and is "sharp" in both versions.

About the "IsChain-only" theorem: I guess I wanted to limit myself to results that directly relate to RelatesInSteps, but you are right, this is the cleaner approach, I'll try.

[crei]

I was wondering if it makes sense to introduce a structure here:

/-- A "chain from to" is a list of elements where adjacent elements relate to each other
(cf. `List.IsChain`) and start and end with specific elements. -/
structure _root_.List.IsChainFromTo {α : Type*}
    (r : α → α → Prop) (chain : List α) (a b : α) : Prop where
  h_chain : chain.IsChain r
  h_from : chain.head? = some a
  h_to : chain.getLast? = some b

/-- If there is an `r`-chain from `a` to `b` with duplicates, then there is a shorter `r`-chain
from `a` to `b`. -/
lemma _root_.List.IsChainFromTo.exists_length_lt_of_not_nodup {chain : List α}
    (hc : chain.IsChainFromTo r a b) (h_dup : ¬ chain.Nodup) :
    ∃ chain' : List α, chain'.IsChainFromTo r a b ∧ chain'.length < chain.length := by

Additionally, this is now much more general and should probably move to mathlib (I'm a bit surprised that it is not there yet, but maybe I didn't find it) - should I just create a new file for that? Plus, this is probably relevant for the emerging graph theory section as well?

[chenson2018]

Our usual procedure for Mathlib upstreaming is to leave them in the same file as any other proof, sometimes leaving a comment or in a section if it's several proofs. (If a comment is prefaced with TODO an issue will automatically open with that as its title)

[ctchou]

Yes, I think List.IsChainFromTo is a good idea. I like putting the new definitions and theorems about List in a new file under Cslib/Foundations/Data/List/. The file can be removed after the mathlib upstreaming happens. Personally I find this approach more modular.

[ctchou]

I would call these two fields head and getLast (or even last). Then the following two theorems can use the consistent naming convention List.IsChainFromTo.{head,getLast}_eq.

[ctchou]

I don't understand this sentence. It seems to contradict chain'.length < chain.length in the theorem statement.

[chriseth]

Iterating the method is a greedy search that cuts duplicates. Each iteration reduces the length and it will terminate at some point. But the length of that chain is not the minimum over all chains from a to b.

[ctchou]

I golfed your proof a little bit:

  classical
  -- Let us use the shortest chain from `a` to `b`.
  have hex : ∃ n, RelatesInSteps r a b n := h.relatesInSteps
  use Nat.find hex, Nat.find_spec hex
  obtain ⟨chain, hc, hlen⟩ := (Nat.find_spec hex).exists_isChainFromTo
  -- All elements in the chain are reachable from `a`.
  have hsub : {x | x ∈ chain} ⊆ {x | ReflTransGen r a x} := by
    intro y hy
    obtain ⟨i, hi, rfl⟩ := List.getElem_of_mem hy
    have := RelatesInSteps.of_isChain hc.isChain 0 i
    grind [RelatesInSteps.reflTransGen]
  -- Now assume, for the sake of contradiction, that the minimal chain has at least as many
  -- elements as there are reachable elements.
  by_contra! hcard
  -- Then there is at least one duplicate element.
  have h_dup : ¬chain.Nodup := by
    have hle := (Set.encard_le_encard hsub).trans hcard
    rw [← List.coe_toFinset, Set.encard_coe_eq_coe_finsetCard] at hle
    grind [List.toFinset_card_of_nodup, Nat.cast_le]
  -- But then we can shorten the chain which contradicts the fact that it is minimal.
  obtain ⟨chain', hc', hlt⟩ := hc.exists_length_lt_of_not_nodup h_dup
  grind [Nat.find_min hex (m := chain'.length - 1), RelatesInSteps.of_isChainFromTo hc']

[ctchou]

The (by omega) is unnecessary. The grind takes care of it.

[ctchou]

Please replace the refine you use to destruct a List.IsChainFromTo goal with:

apply List.IsChainFromTo.mk ..

This is a better style than the refine with nested by proofs.

[crei]

I discussed with @barni120400 about what to use for computation paths in nondeterministic machines. And of course what we will use there influences how the result here will be applied. In #820 he is using RelSeries, which is similar to IsChain (and compatible) and using that would probably not need an IsChainFromTo structure. So maybe we could think about switching over to that.