feat(Data): Results about RelatesInSteps with bounds on the reachable set by crei · Pull Request #779 · leanprover/cslib

crei · 2026-08-06T16:36:16Z

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 · 2026-08-06T17:32:00Z

+i.e. `r (f i) (f (i + 1))` holds for every `i < n`. The values of `f` beyond index `n` are
+irrelevant.
+-/
+def IsPath (r : α → α → Prop) (f : ℕ → α) (n : ℕ) : Prop := ∀ i < n, r (f i) (f (i + 1))


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?

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.

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)

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 · 2026-08-06T20:19:00Z

+theorem IsPath.exists_eq_of_ncard_le {f : ℕ → α} {n : ℕ}
+    (hf : IsPath r f n)
+    (hfin : Set.Finite (ReflTransGen r (f 0)))
+    (hn : Set.ncard (ReflTransGen r (f 0)) ≤ n) :


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

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 · 2026-08-12T20:37:20Z

+a length guarantee. -/
+lemma RelatesInSteps.exists_isChain {a b : α} {n : ℕ} (h : RelatesInSteps r a b n) :
+    ∃ chain : List α,
+      chain.IsChain r ∧ ∃ h_len : chain.length = n + 1, chain[0] = a ∧ chain[n] = b := by


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

ctchou · 2026-08-12T20:59:30Z

+/-- Any two elements along an `r`-chain are related in as many steps as their distance in the
+chain. -/
+lemma RelatesInSteps.of_isChain {chain : List α}
+    (hc : chain.IsChain r)
+    (p k : ℕ)
+    (hpk : p + k < chain.length) :
+    RelatesInSteps r chain[p] chain[p + k] k := by
+  induction k with
+  | zero => exact .refl _
+  | succ k ih =>
+    refine .tail _ (chain[p + k]) _ k (ih (by lia)) ?_
+    apply List.IsChain.getElem hc
+
+/-- A chain that visits the same element at two different positions can be shortened by splicing
+out the loop in between, i.e. the first and last elements are also related to each other
+by fewer steps. -/
+lemma RelatesInSteps.of_isChain_eq {chain : List α} {i j : ℕ}
+    (hc : chain.IsChain r)
+    (hij : i < j)
+    (hjn : j < chain.length)
+    (heq : chain[i] = chain[j]) :
+    RelatesInSteps r (chain.head (by grind)) (chain.getLast (by grind))
+      (i + (chain.length - 1 - j)) := by
+  rw [List.head_eq_getElem, List.getLast_eq_getElem]
+  have h₁ := RelatesInSteps.of_isChain hc 0 i (by omega)
+  have h₂ := RelatesInSteps.of_isChain hc j (chain.length - 1 - j) (by omega)
+  grind [RelatesInSteps.trans]
+
+/-- If a chain has duplicates, there is a shorter version with the same start and end point.
+This is a less explicit version of `RelatesInSteps.of_isChain_eq`. -/
+lemma RelatesInSteps.of_isChain_neg_nodup {chain : List α}
+    (hc : chain.IsChain r)
+    (hne : chain ≠ [])
+    (hdup : ¬ chain.Nodup) :
+    ∃ n < chain.length - 1, RelatesInSteps r (chain.head hne) (chain.getLast hne) n := by
+  rw [List.nodup_iff_getElem?_ne_getElem?] at hdup
+  push Not at hdup
+  obtain ⟨i, j, hij, hjn, heq⟩ := hdup
+  exact ⟨_, by omega, RelatesInSteps.of_isChain_eq hc hij hjn (by grind)⟩


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 · 2026-08-12T21:11:23Z

+Note that this cardinality is an `ℕ∞`, and if it is infinite, no bound on the number of steps
+is stated. -/
+theorem ReflTransGen.relatesInSteps_lt_encard {b : α} (h : ReflTransGen r a b) :
+    ∃ n, RelatesInSteps r a b n ∧ (n : ℕ∞) < {x | ReflTransGen r a x}.encard := by


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.

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.

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?

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)

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 · 2026-08-19T17:18:52Z

+  head_eq : chain.head ne_nil = a
+  getLast_eq : chain.getLast ne_nil = b


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 · 2026-08-19T17:25:41Z

+Note that applying this method iteratively does not necessarily lead to the shortest `r`-chain
+from `a` to `b`, since we always keep the initial and final segment. -/


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

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.

Thanks for the explanation. But I'm not sure you need this second sentence here. The purpose of the doc-string is to explain the contents of the theorem, not how its application may or may imply something. The first sentence alone suffices.

ctchou · 2026-08-19T17:52:43Z

+  classical
+  -- Let us use the shortest chain from `a` to `b`.
+  have hex : ∃ n, RelatesInSteps r a b n := h.relatesInSteps
+  refine ⟨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
+    simp only [Set.subset_def, Set.mem_ofPred_eq]
+    intro y hy
+    obtain ⟨i, hi, rfl⟩ := List.getElem_of_mem hy
+    have := RelatesInSteps.of_isChain hc.isChain 0 i (by omega)
+    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
+  push Not at hcard
+  -- Then there is at least one duplicate element.
+  have h_dup : ¬chain.Nodup := by
+    intro h_nodup
+    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
+  have := List.length_pos_iff.mpr hc'.ne_nil
+  exact Nat.find_min hex (m := chain'.length - 1) (by omega) (RelatesInSteps.of_isChainFromTo hc')


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 · 2026-08-19T18:03:33Z

+    have := hc.isChain.getElem (i := i - 1) (by omega)
+    grind


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 · 2026-08-20T09:39:19Z

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.

ctchou

Except for the two points I raised below, I am satisfied with this PR.

ctchou · 2026-08-20T22:07:07Z

+Note that applying this method iteratively does not necessarily lead to the shortest `r`-chain
+from `a` to `b`, since we always keep the initial and final segment. -/


Thanks for the explanation. But I'm not sure you need this second sentence here. The purpose of the doc-string is to explain the contents of the theorem, not how its application may or may imply something. The first sentence alone suffices.

ctchou · 2026-08-20T22:26:45Z

+  rw [nodup_iff_getElem?_ne_getElem?] at h_dup
+  push Not at h_dup
+  obtain ⟨i, j, h_ij, h_lt, h_eq⟩ := h_dup
+  use chain.take i ++ chain.drop j
+  constructor
+  · apply IsChainFromTo.mk ((hc.isChain.take _).append (hc.isChain.drop _) ?_)
+      (by simp; omega) (by grind) (by grind)
+    intro x hx y hy
+    rw [List.head?_drop] at hy
+    have := hc.isChain.getElem (i := i - 1)
+    grind
+  · grind


A little golfing:

simp only [nodup_iff_getElem?_ne_getElem?, not_forall, not_not] at h_dup obtain ⟨i, j, h_ij, h_lt, h_eq⟩ := h_dup use chain.take i ++ chain.drop j split_ands · apply IsChainFromTo.mk .. · apply (hc.isChain.take _).append (hc.isChain.drop _) grind [List.head?_drop, hc.isChain.getElem (i := i - 1)] · grind [append_eq_nil_iff, drop_eq_nil_iff] · grind · grind · grind

thomaskwaring

i think the results here are very nice, but i would like a little more api to go with the definition List.IsChainFromTo — i suggested the evident cons lemma, but there is also one for append and induction principles from the left (head) and right

thomaskwaring · 2026-08-20T22:49:25Z

+  head : chain.head ne_nil = a
+  last : chain.getLast ne_nil = b


Suggested change

head : chain.head ne_nil = a

last : chain.getLast ne_nil = b

head_eq : chain.head ne_nil = a

getLast_eq : chain.getLast ne_nil = b

attribute [grind →] List.IsChainFromTo.head_eq List.IsChainFromTo.getLast_eq

and then you can delete the duplicate lemmas

thomaskwaring · 2026-08-20T23:08:16Z

+    rw [List.head?_drop] at hy
+    have := hc.isChain.getElem (i := i - 1)
+    grind
+  · grind


i think this lemma would also be nice

Suggested change

· grind

· grind

lemma List.IsChainFromTo.exists_noDup (hc : chain.IsChainFromTo r a b) :

∃ chain' : List α, chain'.IsChainFromTo r a b ∧ chain'.Nodup := by

induction hn : chain.length using Nat.strong_induction_on generalizing chain with

| h n ih =>

by_cases h_dup : chain.Nodup

· use chain, hc, h_dup

· obtain ⟨chain', hc', hlen⟩ := hc.exists_length_lt_of_not_nodup h_dup

exact ih chain'.length (hn ▸ hlen) hc' rfl

thomaskwaring · 2026-08-20T23:10:34Z


+/-- If `b` is reachable from `a` via `r`, then they relate to each other for some number
+of steps.
+See `ReflTransGen.relatesInSteps_lt_encard` for a bound on the number of steps. -/


imo the second sentence is unnecessary

thomaskwaring · 2026-08-20T23:25:31Z

+@[simp, grind ←]
+lemma List.IsChainFromTo.singleton {a : α} : List.IsChainFromTo r [a] a a :=
+  ⟨List.IsChain.singleton a, by simp, rfl, rfl⟩
+


i think some further api lemmas for IsChainFromTo would be good — at very least this one can help with the proof of RelatesInSteps.exists_isChainFromTo

lemma List.IsChainFromTo.cons (h : r a b) (hc : chain.IsChainFromTo r b c) : (a :: chain).IsChainFromTo r a c where isChain := hc.isChain.cons_of_ne_nil hc.ne_nil (hc.head_eq.symm ▸ h) ne_nil := cons_ne_nil a chain head_eq := head_cons getLast_eq := hc.getLast_eq ▸ chain.getLast_cons hc.ne_nil

i think some induction principles (in the style of, say, RelatesInSteps.head_induction_on) would also be helpful, but if this pr is blocking something else maybe that can wait (though they oughtn't be too hard)

thomaskwaring · 2026-08-20T23:26:32Z

+lemma RelatesInSteps.exists_isChainFromTo {a b : α} {n : ℕ} (h : RelatesInSteps r a b n) :
+    ∃ chain : List α, chain.IsChainFromTo r a b ∧ chain.length = n + 1 := by
+  induction h with
+  | refl => exact ⟨[a], by simp, rfl⟩
+  | tail t' t'' m _ hstep ih =>
+    obtain ⟨l, hchain, hlen⟩ := ih
+    use l ++ [t'']
+    constructor
+    · apply List.IsChainFromTo.mk (hchain.isChain.append (by simp) (by grind))
+        (by simp) (by grind) (by simp)
+    · simp [hlen]


potentially simpler, using the lemma i suggested above

Suggested change

lemma RelatesInSteps.exists_isChainFromTo {a b : α} {n : ℕ} (h : RelatesInSteps r a b n) :

∃ chain : List α, chain.IsChainFromTo r a b ∧ chain.length = n + 1 := by

induction h with

| refl => exact ⟨[a], by simp, rfl⟩

| tail t' t'' m _ hstep ih =>

obtain ⟨l, hchain, hlen⟩ := ih

use l ++ [t'']

constructor

· apply List.IsChainFromTo.mk (hchain.isChain.append (by simp) (by grind))

(by simp) (by grind) (by simp)

· simp [hlen]

lemma RelatesInSteps.exists_isChainFromTo {a b : α} {n : ℕ} (h : RelatesInSteps r a b n) :

∃ chain : List α, chain.IsChainFromTo r a b ∧ chain.length = n + 1 := by

induction h using RelatesInSteps.head_induction_on with

| hrefl => exact ⟨[b], List.IsChainFromTo.singleton, rfl⟩

| @hhead a c n h' h ih =>

obtain ⟨l, hchain, hlen⟩ := ih

use a :: l, hchain.cons h'

simpa

thomaskwaring · 2026-08-20T23:32:58Z

+  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


this could be extracted as a lemma — with signature something like
chain.IsChainFromTo r a b → x ∈ chain → ReflTransGen r a x, plus also the one with conclusion ReflTransGen r x b

thomaskwaring · 2026-08-20T23:44:44Z

+is related to `a` in fewer steps than there are elements reachable from `a`.
+Note that this cardinality is an `ℕ∞`, and if it is infinite, no bound on the number of steps
+is stated. -/
+theorem ReflTransGen.relatesInSteps_lt_encard {b : α} (h : ReflTransGen r a b) :


possibly this whole proof could be simplified using List.IsChainFromTo.exists_noDup suggested above, something like:

... := by obtain ⟨_, hn⟩ := h.relatesInSteps obtain ⟨chain, hc, _⟩ := hn.exists_isChainFromTo replace ⟨chain, hc, h⟩ := hc.exists_noDup use chain.length - 1, RelatesInSteps.of_isChainFromTo hc suffices hcard : chain.length ≤ {x | ReflTransGen r a x}.encard by by_contra! hcard' grind [ENat.natCast_le_natCast, hcard.trans hcard'] classical rw [←List.toFinset_card_of_nodup h, ←Set.encard_coe_eq_coe_finsetCard, List.coe_toFinset] apply Set.encard_le_encard intro y hy obtain ⟨i, hi, rfl⟩ := List.getElem_of_mem hy have := RelatesInSteps.of_isChain hc.isChain 0 i grind [RelatesInSteps.reflTransGen]

which feels a little conceptually clearer to me (especially with hsub extracted as a lemma), but that could be a matter of taste

thomaskwaring · 2026-08-20T23:47:53Z

+
+/-- Any two elements along an `r`-chain are related in as many steps as their distance in the
+chain. -/
+lemma RelatesInSteps.of_isChain {chain : List α}


maybe (including more useful dot notation):

Suggested change

lemma RelatesInSteps.of_isChain {chain : List α}

lemma _root_.List.IsChain.relatesInSteps_getElem {chain : List α}

thomaskwaring · 2026-08-20T23:49:37Z

+
+/-- If there is an `r`-chain from `a` to `b`, then `a` and `b` are related to each other with
+a number of steps equal to the length of the chain minus one. -/
+lemma RelatesInSteps.of_isChainFromTo {chain : List α} (hc : chain.IsChainFromTo r a b) :


this proof might be easier with the induction principle(s) i mentioned, but maybe that's just my taste
also the same naming idea as above:

Suggested change

lemma RelatesInSteps.of_isChainFromTo {chain : List α} (hc : chain.IsChainFromTo r a b) :

lemma _root_.IsChainFromTo.relatesInSteps {chain : List α} (hc : chain.IsChainFromTo r a b) :

thomaskwaring · 2026-08-20T23:50:51Z

+  last : chain.getLast ne_nil = b
+
+/-- Create a `List.IsChainFromTo` from a non-empty `List.IsChain`. -/
+theorem List.IsChainFromTo.of_isChain_ne_nil


Suggested change

theorem List.IsChainFromTo.of_isChain_ne_nil

theorem List.IsChain.isChainFromTo_of_ne_nil

gives usable dot notation

thomaskwaring · 2026-08-21T11:42:28Z

i've proven some lemmas, feel free to add them to this pr or we can also do a followup

lemma List.IsChainFromTo.of_cons_cons {x y : α} (hc : (x :: y :: chain).IsChainFromTo r a b) :
    (y :: chain).IsChainFromTo r y b :=
  ⟨hc.isChain.of_cons, cons_ne_nil _ _, head_cons, by grind⟩

lemma List.IsChainFromTo.append_tail (hc : chain.IsChainFromTo r a b)
    (hc' : chain'.IsChainFromTo r b c) : (chain ++ chain'.tail).IsChainFromTo r a c where
  isChain := by
    have hb : chain.dropLast ++ [b] = chain :=
      hc.getLast_eq ▸ chain.dropLast_append_getLast hc.ne_nil
    have hb' : [b] ++ chain'.tail = chain' := by simp [←hc'.head_eq]
    rw [←hb] at hc ⊢
    exact hc.isChain.append_overlap (l₃ := chain'.tail) (hb'.symm ▸ hc'.isChain) (cons_ne_nil b [])
  ne_nil := append_ne_nil_of_left_ne_nil hc.ne_nil _
  head_eq := head_append_left hc.ne_nil |>.trans hc.head_eq
  getLast_eq := by grind

lemma List.IsChainFromTo.append_dropLast (hc : chain.IsChainFromTo r a b)
    (hc' : chain'.IsChainFromTo r b c) : (chain.dropLast ++ chain').IsChainFromTo r a c := by
  convert hc.append_tail hc' using 1
  nth_rw 1 [←chain'.cons_head_tail hc'.ne_nil, hc'.head_eq, append_cons, ←hc.getLast_eq,
    dropLast_concat_getLast hc.ne_nil]

lemma List.IsChainFromTo.take (hc : chain.IsChainFromTo r a b) {i : ℕ} (hi : i < chain.length) :
    (chain.take (i + 1)).IsChainFromTo r a chain[i] := by
  have : chain.take (i + 1) ≠ [] := by grind [ne_nil_iff_length_pos, length_take]
  exact ⟨hc.isChain.take _, this, by grind, by grind [chain.getLast_take this]⟩

lemma List.IsChainFromTo.drop (hc : chain.IsChainFromTo r a b) {i : ℕ} (hi : i < chain.length) :
    (chain.drop i).IsChainFromTo r chain[i] b := by
  have : chain.drop i ≠ [] := ne_nil_iff_length_pos.mpr <| chain.lt_length_drop hi
  refine ⟨hc.isChain.drop _, this, chain.head_drop this, hc.getLast_eq ▸ chain.getLast_drop this⟩

lemma List.IsChainFromTo.head_induction_on
    {motive : ∀ {chain : List α} {a b : α}, chain.IsChainFromTo r a b → Prop}
    (h_refl : ∀ {a : α}, motive (IsChainFromTo.singleton (a := a)))
    (h_head : ∀ {a b c : α} {chain : List α} (hab : r a b) (hc : chain.IsChainFromTo r b c),
      motive hc → motive (hc.cons hab))
    {chain : List α} {a b : α} (hc : chain.IsChainFromTo r a b) : motive hc := by
  induction htail : chain.tail generalizing chain a with
  | nil =>
    obtain rfl : chain = [a] := by grind
    grind
  | cons a' tail ih =>
    obtain rfl : chain = a :: a' :: tail := by grind
    obtain ⟨hrel, hchain⟩ := isChain_cons_cons.mp hc.isChain
    have : (a' :: tail).IsChainFromTo r a' b := hc.of_cons_cons
    exact h_head hrel this (ih this rfl)

crei requested review from chenson2018 and fmontesi as code owners August 6, 2026 16:36

Results about reachability with repeated visits.

cce51a6

crei force-pushed the relates_in_steps_bounded branch from 9a46a2d to cce51a6 Compare August 6, 2026 16:36

fmontesi reviewed Aug 6, 2026

View reviewed changes

thomaskwaring reviewed Aug 6, 2026

View reviewed changes

ctchou reviewed Aug 8, 2026

View reviewed changes

crei added 5 commits August 12, 2026 17:05

Use isChain.

c462faa

Merge remote-tracking branch 'origin/main' into relates_in_steps_bounded

dea453a

Extract a lemma and clean up.

877f6d5

Undo some golfing.

ba0c2b5

Undo some more golfing.

cd5c63f

ctchou requested changes Aug 12, 2026

View reviewed changes

crei added 4 commits August 17, 2026 15:28

Extract results related to List.isChain into their own file.

c4c92c1

Merge remote-tracking branch 'origin/main' into relates_in_steps_bounded

9ec5246

Minor tweaks.

af70d3b

Remove simp.

f03aca6

crei requested a review from ctchou August 18, 2026 14:36

crei mentioned this pull request Aug 19, 2026

feat(MultiTapeTM): Nondeterministic multi-tape Turing machines #802

Closed

Merge remote-tracking branch 'origin/main' into relates_in_steps_bounded

a54f681

ctchou requested changes Aug 19, 2026

View reviewed changes

crei added 2 commits August 20, 2026 10:50

Move file.

f85d8ed

Review comments.

bd393f3

ctchou requested changes Aug 20, 2026

View reviewed changes

thomaskwaring requested changes Aug 20, 2026

View reviewed changes

		head_eq : chain.head ne_nil = a
		getLast_eq : chain.getLast ne_nil = b

		Note that applying this method iteratively does not necessarily lead to the shortest `r`-chain
		from `a` to `b`, since we always keep the initial and final segment. -/

-  · grind
+  · grind
+lemma List.IsChainFromTo.exists_noDup (hc : chain.IsChainFromTo r a b) :
+    ∃ chain' : List α, chain'.IsChainFromTo r a b ∧ chain'.Nodup := by
+  induction hn : chain.length using Nat.strong_induction_on generalizing chain with
+  | h n ih =>
+    by_cases h_dup : chain.Nodup
+    · use chain, hc, h_dup
+    · obtain ⟨chain', hc', hlen⟩ := hc.exists_length_lt_of_not_nodup h_dup
+      exact ih chain'.length (hn ▸ hlen) hc' rfl

	lemma RelatesInSteps.of_isChain {chain : List α}
	lemma _root_.List.IsChain.relatesInSteps_getElem {chain : List α}

	lemma RelatesInSteps.of_isChainFromTo {chain : List α} (hc : chain.IsChainFromTo r a b) :
	lemma _root_.IsChainFromTo.relatesInSteps {chain : List α} (hc : chain.IsChainFromTo r a b) :

	theorem List.IsChainFromTo.of_isChain_ne_nil
	theorem List.IsChain.isChainFromTo_of_ne_nil

Uh oh!

Conversation

crei commented Aug 6, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

thomaskwaring Aug 6, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

ctchou left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

ctchou Aug 12, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

ctchou Aug 13, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

ctchou left a comment

Choose a reason for hiding this comment

Uh oh!

crei commented Aug 20, 2026

Uh oh!

ctchou left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

thomaskwaring left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

crei commented Aug 6, 2026 •

edited

Loading

thomaskwaring Aug 6, 2026 •

edited

Loading

ctchou Aug 12, 2026 •

edited

Loading

ctchou Aug 13, 2026 •

edited

Loading

thomaskwaring Aug 20, 2026 •

edited

Loading

thomaskwaring commented Aug 21, 2026 •

edited

Loading