From cce51a62435c697dc35338a6576274cc15a68f7d Mon Sep 17 00:00:00 2001 From: crei Date: Thu, 6 Aug 2026 18:18:18 +0200 Subject: [PATCH] Results about reachability with repeated visits. --- .../Turing/SingleTape/Deterministic.lean | 2 +- Cslib/Foundations/Data/RelatesInSteps.lean | 126 +++++++++++++++++- 2 files changed, 120 insertions(+), 8 deletions(-) diff --git a/Cslib/Computability/Machines/Turing/SingleTape/Deterministic.lean b/Cslib/Computability/Machines/Turing/SingleTape/Deterministic.lean index 29f379d5a..77ce68176 100644 --- a/Cslib/Computability/Machines/Turing/SingleTape/Deterministic.lean +++ b/Cslib/Computability/Machines/Turing/SingleTape/Deterministic.lean @@ -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 diff --git a/Cslib/Foundations/Data/RelatesInSteps.lean b/Cslib/Foundations/Data/RelatesInSteps.lean index 052e52c98..33288889a 100644 --- a/Cslib/Foundations/Data/RelatesInSteps.lean +++ b/Cslib/Foundations/Data/RelatesInSteps.lean @@ -7,6 +7,7 @@ Authors: Bolton Bailey module public import Cslib.Init +public import Mathlib.Data.Set.Card public import Mathlib.Logic.Relation /-! # Relations Across Steps @@ -14,6 +15,13 @@ public import Mathlib.Logic.Relation 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 @@ -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)) + +/-- 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) : + ∃ 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. @@ -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 @@ -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