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.

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

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 : ℕ} : 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.

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.of_le {α : Type u_1} {r : α → α → Prop} {a b : α} {n₁ n₂ : ℕ} (h : RelatesWithinSteps r a b n₁) (hn : n₁ ≤ n₂) : RelatesWithinSteps r a b n₂

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.