Relations Across Steps

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

The lemma RelatesInSteps.exists_isChainFromTo allows to obtain a chain (List.IsChainFromTo) of related elements that witness the reachability, and List.IsChainFromTo.relatesInSteps is the converse direction. Relation.relatesInSteps_iff_exists_isChainFromTo combines both.

Another result is Relation.ReflTransGen.relatesInSteps_lt_encard, which states that any element reachable from a is reachable in fewer steps than there are elements reachable from a.

inductive Relation.RelatesInSteps {α : Type u_1} (r : α → α → Prop) : α → α → ℕ → Prop

A relation r relates two elements of α in n steps if there is a chain of n pairs (t_i, t_{i+1}) such that r t_i t_{i+1} for each i, starting from the first element and ending at the second.

• refl {α : Type u_1} {r : α → α → Prop} (a : α) : RelatesInSteps r a a 0
• tail {α : Type u_1} {r : α → α → Prop} (t t' t'' : α) (n : ℕ) (h₁ : RelatesInSteps r t t' n) (h₂ : r t' t'') : RelatesInSteps r t t'' (n + 1)

theorem Relation.RelatesInSteps.reflTransGen {α : Type u_1} {r : α → α → Prop} {a b : α} {n : ℕ} (h : RelatesInSteps r a b n) : ReflTransGen r a b

theorem Relation.ReflTransGen.relatesInSteps {α : Type u_1} {r : α → α → Prop} {a b : α} (h : ReflTransGen r a b) : ∃ (n : ℕ), RelatesInSteps r a b n

If b is reachable from a via r, then they relate to each other for some number of steps.

theorem Relation.RelatesInSteps.single {α : Type u_1} {r : α → α → Prop} {a b : α} (h : r a b) : RelatesInSteps r a b 1

theorem Relation.RelatesInSteps.head {α : Type u_1} {r : α → α → Prop} (t t' t'' : α) (n : ℕ) (h₁ : r t t') (h₂ : RelatesInSteps r t' t'' n) : RelatesInSteps r t t'' (n + 1)

theorem Relation.RelatesInSteps.head_induction_on {α : Type u_1} {r : α → α → Prop} {b : α} {motive : (a : α) → (n : ℕ) → RelatesInSteps r a b n → Prop} {a : α} {n : ℕ} (h : RelatesInSteps r a b n) (hrefl : motive b 0 ⋯) (hhead : ∀ {a c : α} {n : ℕ} (h' : r a c) (h : RelatesInSteps r c b n), motive c n h → motive a (n + 1) ⋯) : motive a n h

theorem Relation.RelatesInSteps.zero {α : Type u_1} {r : α → α → Prop} {a b : α} (h : RelatesInSteps r a b 0) : a = b

@[simp]

theorem Relation.RelatesInSteps.zero_iff {α : Type u_1} {r : α → α → Prop} {a b : α} : RelatesInSteps r a b 0 ↔ a = b

theorem Relation.RelatesInSteps.trans {α : Type u_1} {r : α → α → Prop} {a b c : α} {n m : ℕ} (h₁ : RelatesInSteps r a b n) (h₂ : RelatesInSteps r b c m) : RelatesInSteps r a c (n + m)

theorem Relation.RelatesInSteps.succ {α : Type u_1} {r : α → α → Prop} {a b : α} {n : ℕ} (h : RelatesInSteps r a b (n + 1)) : ∃ (t' : α), RelatesInSteps r a t' n ∧ r t' b

theorem Relation.RelatesInSteps.succ_iff {α : Type u_1} {r : α → α → Prop} {a b : α} {n : ℕ} : RelatesInSteps r a b (n + 1) ↔ ∃ (t' : α), RelatesInSteps r a t' n ∧ r t' b

theorem Relation.RelatesInSteps.succ' {α : Type u_1} {r : α → α → Prop} {a b : α} {n : ℕ} (h : RelatesInSteps r a b (n + 1)) : ∃ (t' : α), r a t' ∧ RelatesInSteps r t' b n

theorem Relation.RelatesInSteps.succ'_iff {α : Type u_1} {r : α → α → Prop} {a b : α} {n : ℕ} : RelatesInSteps r a b (n + 1) ↔ ∃ (t' : α), r a t' ∧ RelatesInSteps r t' b n

theorem Relation.RelatesInSteps.apply_le_apply_add {α : Type u_1} {r : α → α → Prop} {a b : α} {m : ℕ} (hevals : RelatesInSteps r a b m) (h : α → ℕ) (h_step : ∀ (a b : α), r a b → h b ≤ h a + 1) : h b ≤ h a + m

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 number of steps.

theorem Relation.RelatesInSteps.map {α : Type u_2} {α' : Type u_3} {r : α → α → Prop} {r' : α' → α' → Prop} (g : α → α') (hg : ∀ (a b : α), r a b → r' (g a) (g b)) {a b : α} {n : ℕ} (h : RelatesInSteps r a b n) : RelatesInSteps r' (g a) (g b) n

If g is a homomorphism from r to r' (i.e., it preserves the reduction relation), then RelatesInSteps is preserved under g.

Translating between RelatesInSteps and chains (List.IsChainFromTo)

theorem Relation.RelatesInSteps.exists_isChainFromTo {α : Type u_1} {r : α → α → Prop} {a b : α} {n : ℕ} (h : RelatesInSteps r a b n) : ∃ (chain : List α), List.IsChainFromTo r chain a b ∧ chain.length = n + 1

If b is related to a via r in n steps, then there is an r-chain of n + 1 elements starting at a and ending at b. This is similar to List.exists_isChain_ne_nil_of_relationReflTransGen, but also provides a length guarantee.

theorem List.IsChain.relatesInSteps_getElem {α : Type u_1} {r : α → α → Prop} {chain : List α} (hc : IsChain r chain) (i k : ℕ) (hik : i + k < chain.length) : Relation.RelatesInSteps r chain[i] chain[i + k] k

Any two elements along an r-chain are related in as many steps as their distance in the chain.

theorem List.IsChainFromTo.relatesInSteps {α : Type u_1} {r : α → α → Prop} {a b : α} {chain : List α} {n : ℕ} (hc : IsChainFromTo r chain a b) (hlen : chain.length = n + 1) : Relation.RelatesInSteps r a b n

If there is an r-chain of n + 1 elements from a to b, then a and b are related to each other in n steps.

theorem Relation.relatesInSteps_iff_exists_isChainFromTo {α : Type u_1} {r : α → α → Prop} {a b : α} {n : ℕ} : RelatesInSteps r a b n ↔ ∃ (chain : List α), List.IsChainFromTo r chain a b ∧ chain.length = n + 1

a and b are related in n steps exactly when there is an r-chain of n + 1 elements from a to b.

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

def Relation.RelatesWithinSteps {α : Type u_1} (r : α → α → Prop) (a b : α) (n : ℕ) : Prop

RelatesWithinSteps is a variant of RelatesInSteps that allows for a loose bound. It states that a relates to b in at most n steps.

Equations

• Relation.RelatesWithinSteps r a b n = ∃ m ≤ n, Relation.RelatesInSteps r a b m

theorem Relation.RelatesWithinSteps.of_relatesInSteps {α : Type u_1} {r : α → α → Prop} {a b : α} {n : ℕ} (h : RelatesInSteps r a b n) : RelatesWithinSteps r a b n

RelatesInSteps implies RelatesWithinSteps with the same bound.

theorem Relation.RelatesWithinSteps.refl {α : Type u_1} {r : α → α → Prop} (a : α) : RelatesWithinSteps r a a 0

theorem Relation.RelatesWithinSteps.single {α : Type u_1} {r : α → α → Prop} {a b : α} (h : r a b) : RelatesWithinSteps r a b 1

theorem Relation.RelatesWithinSteps.zero {α : Type u_1} {r : α → α → Prop} {a b : α} (h : RelatesWithinSteps r a b 0) : a = b

@[simp]

theorem Relation.RelatesWithinSteps.zero_iff {α : Type u_1} {r : α → α → Prop} {a b : α} : RelatesWithinSteps r a b 0 ↔ a = b

theorem Relation.RelatesWithinSteps.trans {α : Type u_1} {r : α → α → Prop} {a b c : α} {n₁ n₂ : ℕ} (h₁ : RelatesWithinSteps r a b n₁) (h₂ : RelatesWithinSteps r b c n₂) : RelatesWithinSteps r a c (n₁ + n₂)

Transitivity of RelatesWithinSteps in the sum of the step bounds.

theorem Relation.RelatesWithinSteps.mono {α : Type u_1} {r : α → α → Prop} {a b : α} : Monotone fun (x : ℕ) => RelatesWithinSteps r a b x

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.

theorem Relation.RelatesWithinSteps.apply_le_apply_add {α : Type u_1} {r : α → α → Prop} {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

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.

theorem Relation.RelatesWithinSteps.map {α : Type u_2} {α' : Type u_3} {r : α → α → Prop} {r' : α' → α' → Prop} (g : α → α') (hg : ∀ (a b : α), r a b → r' (g a) (g b)) {a b : α} {n : ℕ} (h : RelatesWithinSteps r a b n) : RelatesWithinSteps r' (g a) (g b) n

If g is a homomorphism from r to r' (i.e., it preserves the reduction relation), then RelatesWithinSteps is preserved under g.

Reachability under a bound on the number of reachable elements

theorem Relation.ReflTransGen.relatesInSteps_lt_encard {α : Type u_1} {r : α → α → Prop} {a b : α} (h : ReflTransGen r a b) : ∃ (n : ℕ), RelatesInSteps r a b n ∧ ↑n < {x : α | ReflTransGen r a x}.encard

A more precise version of ReflTransGen.relatesInSteps: if b is reachable from a, then it 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.