Helper Lemmas about the Kleene Star #
Nothing here is specific about PDL, but we prove some useful results about the reflexive-transitive
closure ReflTransGen and the transitive closure TransGen.
theorem
ReflTransGen.cases_tail_eq_neq
{α : Type u_1}
{x z : α}
{r : α → α → Prop}
(h : Relation.ReflTransGen r x z)
:
A version of Relation.ReflTransGen.cases_tail also giving (in)equalities.
theorem
ReflTransGen.to_finitelyManySteps
{α : Type u_1}
{x z : α}
{r : α → α → Prop}
(h : Relation.ReflTransGen r x z)
:
ReflTransGen r a b implies ∃ x₀ ... xₙ, a = x₀ ∧ r x₀ x₁ ∧ ... ∧ xₙ = b.
Similar to List.exists_chain_of_relationReflTransGen.
theorem
ReflTransGen.from_finitelyManySteps
{α : Type u_1}
(r : α → α → Prop)
{n : ℕ}
(x z : α)
(ys : List.Vector α n.succ)
:
a = x₀ ∧ r x₀ x₁ ∧ ... ∧ xₙ = b implies ReflTransGen r a b.
Similar to List.relationReflTransGen_of_exists_chain in mathlib.
theorem
Relation.ReflTransGen_or_left
{α : Type u_1}
{r r' : α → α → Prop}
{a b : α}
:
ReflTransGen r a b → ReflTransGen (fun (x y : α) => r x y ∨ r' x y) a b
theorem
Relation.ReflTransGen_or_right
{α : Type u_1}
{r r' : α → α → Prop}
{a b : α}
:
ReflTransGen r a b → ReflTransGen (fun (x y : α) => r' x y ∨ r x y) a b
theorem
Relation.ReflTransGen_imp
{α : Type u_1}
{r r' : α → α → Prop}
{a b : α}
:
(∀ (x y : α), r x y → r' x y) → ReflTransGen r a b → ReflTransGen r' a b
theorem
Relation.TransGen_of_ReflTransGen
{α : Type}
{r : α → α → Prop}
{a b : α}
(h : ReflTransGen r a b)
(hne : a ≠ b)
:
TransGen r a b