Skip to content

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

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
crei wants to merge 1 commit into
base: main
Choose a base branch
from
+120 −8
Open

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

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion Cslib/Computability/Machines/Turing/SingleTape/Deterministic.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -445,7 +445,7 @@ def TimeComputable.comp {f g : List Symbol → List Symbol}
(hg.timeBound (f a).length) hg_outputsFun
-- Therefore, the computer reduces a to g (f a) in the sum of those times.
have h_a_reducesTo_g_f_a := RelatesWithinSteps.trans h_a_reducesTo_f_a h_f_a_reducesTo_g_f_a
apply RelatesWithinSteps.of_le h_a_reducesTo_g_f_a
refine RelatesWithinSteps.mono ?_ h_a_reducesTo_g_f_a
refine Nat.add_le_add_left ?_ (hf.timeBound a.length)
· apply h_mono
-- Use the lemma about output length being bounded by input length + time
Expand Down
126 changes: 119 additions & 7 deletions Cslib/Foundations/Data/RelatesInSteps.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,13 +7,21 @@ Authors: Bolton Bailey
module

public import Cslib.Init
public import Mathlib.Data.Set.Card
public import Mathlib.Logic.Relation

/-! # Relations Across Steps

This file defines `Relation.RelatesInSteps` (and `Relation.RelatesWithinSteps`).
These are inductively defines propositions that communicate whether a relation forms a
chain of length `n` (or at most `n`) between two elements.

The theorem `RelatesInSteps.exists_isPath` allows to obtain a path along the relation of
transitively related elements and `IsPath.relatesInSteps` is the converse direction.

Another result is `Relation.reflTransGen_iff_relatesWithinSteps_of_finite`, which states that if
only `n` elements are reachable from `a`, then any element reachable from `a` is reachable in at
most `n - 1` steps.
-/

@[expose] public section
Expand Down Expand Up @@ -147,6 +155,81 @@ lemma RelatesInSteps.map {α α' : Type*}
| tail t' t'' m _ hstep ih =>
exact .tail (g _) (g t') (g t'') m ih (hg t' t'' hstep)

/-! ## Definition of and results about paths along a relation -/

/--
`IsPath r f n` means that the first `n` steps of the sequence `f : ℕ → α` form a path along `r`,
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))

@fmontesi fmontesi Aug 6, 2026

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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 fmontesi Aug 6, 2026

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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 thomaskwaring Aug 6, 2026 •
edited
Loading

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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 thomaskwaring Aug 7, 2026

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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


/-- A path of length `n` is in particular a path of any smaller length. -/
lemma IsPath.mono {f : ℕ → α} : Antitone (IsPath r f) := by
intro m n hle h_path i hi
exact h_path i (by omega)

/-- If `a` and `b` are related in `n` steps, then there is a path of length `n` from `a` to `b`. -/
theorem RelatesInSteps.exists_isPath {a b : α} {n : ℕ} (h : RelatesInSteps r a b n) :
∃ f : ℕ → α, f 0 = a ∧ f n = b ∧ IsPath r f n := by
induction h with
| refl => exact ⟨fun _ => a, rfl, rfl, by simp [IsPath]⟩
| tail t' t'' m _ hstep ih =>
obtain ⟨f, hf0, hfm, hfstep⟩ := ih
refine ⟨fun i => if i ≤ m then f i else t'', by simpa using hf0, by simp, fun i hi => ?_⟩
rcases Nat.lt_or_ge i m with h' | h'
· simpa [h'.le, h'] using hfstep i h'
· have : i = m := by lia
subst this
simpa [hfm] using hstep

/-- Any two positions along a path are related in as many steps as their distance. -/
theorem IsPath.relatesInSteps {f : ℕ → α} {n : ℕ} (hf : IsPath r f n) (p k : ℕ) (hpk : p + k ≤ n) :
RelatesInSteps r (f p) (f (p + k)) k := by
induction k with
| zero => exact .refl _
| succ k ih =>
refine .tail _ (f (p + k)) _ k (ih (by lia)) ?_
have := hf (p + k) (by lia)
rwa [← Nat.add_assoc]

/-- A path that visits the same element at two different positions can be shortened by splicing
out the loop in between. -/
theorem IsPath.relatesInSteps_of_eq {f : ℕ → α} {n i j : ℕ}
(hf : IsPath r f n)
(hij : i < j)
(hjn : j ≤ n)
(heq : f i = f j) :
RelatesInSteps r (f 0) (f n) (i + (n - j)) := by
have h₁ : RelatesInSteps r (f 0) (f j) i := by grind [hf.relatesInSteps 0 i (by lia)]
have h₂ : RelatesInSteps r (f j) (f n) (n - j) := by grind [hf.relatesInSteps j (n - j) (by lia)]
exact h₁.trans h₂

/-- Every element visited by a path is reachable from its starting point. -/
theorem IsPath.reflTransGen {f : ℕ → α} {n : ℕ} (hf : IsPath r f n) {i : ℕ} (hi : i ≤ n) :
ReflTransGen r (f 0) (f i) := by
have := (hf.relatesInSteps 0 i (by lia)).reflTransGen
rwa [Nat.zero_add] at this

/-- A path visiting more positions than there are elements reachable from its starting point must
visit some element twice. -/
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) :

@thomaskwaring thomaskwaring Aug 6, 2026

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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 crei Aug 6, 2026

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

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

∃ i j, i < j ∧ j ≤ n ∧ f i = f j := by
have hmaps : ∀ i ∈ Finset.range (n + 1), f i ∈ hfin.toFinset := fun i hi =>
hfin.mem_toFinset.mpr (hf.reflTransGen (by simpa [Nat.lt_succ_iff] using hi))
have hcard : hfin.toFinset.card < (Finset.range (n + 1)).card := by
grind [Set.ncard_eq_toFinset_card _ hfin]
obtain ⟨i, hi, j, hj, hij, hfij⟩ := Finset.exists_ne_map_eq_of_card_lt_of_maps_to hcard hmaps
simp only [Finset.mem_range, Nat.lt_succ_iff] at hi hj
rcases Nat.lt_or_ge i j with hlt | hge
· exact ⟨i, j, hlt, hj, hfij⟩
· exact ⟨j, i, by lia, hi, hfij.symm⟩

/-! ## RelatesWithinSteps - only requires an upper bound on the number of steps -/

/--
`RelatesWithinSteps` is a variant of `RelatesInSteps` that allows for a loose bound.
It states that `a` relates to `b` in *at most* `n` steps.
Expand Down Expand Up @@ -191,17 +274,18 @@ lemma RelatesWithinSteps.trans {a b c : α} {n₁ n₂ : ℕ}
· lia
· exact RelatesInSteps.trans hevals₁ hevals₂

lemma RelatesWithinSteps.of_le {a b : α} {n₁ n₂ : ℕ}
(h : RelatesWithinSteps r a b n₁) (hn : n₁ ≤ n₂) :
RelatesWithinSteps r a b n₂ := by
obtain ⟨m, hm, hevals⟩ := h
/-- If two elements `a` and `b` are related in at most `n₁` steps in the relation `r` and
`n₁ ≤ n₂`, then they are also related in at most `n₂` steps. -/
lemma RelatesWithinSteps.mono {a b : α} : Monotone (RelatesWithinSteps r a b ·) := by
intro n₁ n₂ hn ⟨m, hm, hevals⟩
exact ⟨m, Nat.le_trans hm hn, hevals⟩

/-- If `h : α → ℕ` increases by at most 1 on each step of `r`,
then the value of `h` at the output is at most `h` at the input plus the step bound. -/
lemma RelatesWithinSteps.apply_le_apply_add {a b : α} {m : ℕ} (hevals : RelatesWithinSteps r a b m)
(h : α → ℕ) (h_step : ∀ a b, r a b → h b ≤ h a + 1)
:
lemma RelatesWithinSteps.apply_le_apply_add {a b : α} {m : ℕ}
(hevals : RelatesWithinSteps r a b m)
(h : α → ℕ)
(h_step : ∀ a b, r a b → h b ≤ h a + 1) :
h b ≤ h a + m := by
obtain ⟨m, hm, hevals_m⟩ := hevals
have := RelatesInSteps.apply_le_apply_add hevals_m h h_step
Expand All @@ -218,4 +302,32 @@ lemma RelatesWithinSteps.map {α α' : Type*} {r : α → α → Prop} {r' : α'
obtain ⟨m, hm, hevals⟩ := h
exact ⟨m, hm, RelatesInSteps.map g hg hevals⟩

/-! ### Reachability under a bound on the number of reachable elements -/

/-- An `r`-chain from `a` to `b` visiting at least as many positions as there are elements
(transitively) related to `a` must visit some element twice, and can therefore be shortened. -/
theorem RelatesInSteps.exists_lt_of_ncard_le {b : α} {n : ℕ}
(hfin : Set.Finite (ReflTransGen r a))
(h : RelatesInSteps r a b n)
(hn : Set.ncard (ReflTransGen r a) ≤ n) :
∃ m < n, RelatesInSteps r a b m := by
obtain ⟨f, rfl, rfl, hpath⟩ := h.exists_isPath
obtain ⟨i, j, hij, hjn, heq⟩ := hpath.exists_eq_of_ncard_le hfin hn
exact ⟨i + (n - j), by lia, hpath.relatesInSteps_of_eq hij hjn heq⟩

/-- If only a finite number of elements are (transitively) related to `a`, then any such element
is related to `a` in at most `k - 1` steps, where `k` is the cardinality of that set. -/
theorem reflTransGen_iff_relatesWithinSteps_of_finite {b : α}
(hfin : Set.Finite (ReflTransGen r a)) :
ReflTransGen r a b ↔ RelatesWithinSteps r a b (Set.ncard (ReflTransGen r a) - 1) := by
classical
simp only [RelatesWithinSteps]
constructor
· intro h_reach
have hex : ∃ n, RelatesInSteps r a b n := ReflTransGen.relatesInSteps h_reach
-- A chain of minimal length cannot be shortened, so it is short enough.
have hmin : ∀ m < Nat.find hex, ¬ RelatesInSteps r a b m := fun m hm => Nat.find_min hex hm
grind [RelatesInSteps.exists_lt_of_ncard_le]
· grind [RelatesInSteps.reflTransGen]

end Relation
Loading