Temporal reasoning over infinite sequences.

def Cslib.ωSequence.Step {α : Type u_1} (xs : ωSequence α) (p q : Set α) : Prop

Step p q means that whenever p holds at a position in xs, q holds at the next position in xs.

Equations

• xs.Step p q = ∀ (k : ℕ), xs k ∈ p → xs (k + 1) ∈ q

theorem Cslib.ωSequence.Step.mk {α : Type u_1} {p q : Set α} {xs : ωSequence α} (h : ∀ (k : ℕ), xs k ∈ p → xs (k + 1) ∈ q) : xs.Step p q

def Cslib.ωSequence.LeadsTo {α : Type u_1} (xs : ωSequence α) (p q : Set α) : Prop

"p leads to q" means that whenever p holds at a position in xs, q holds at the same or a later position in xs.

Equations

• xs.LeadsTo p q = ∀ (k : ℕ), xs k ∈ p → ∃ (k' : ℕ), k ≤ k' ∧ xs k' ∈ q

theorem Cslib.ωSequence.LeadsTo.mk {α : Type u_1} {p q : Set α} {xs : ωSequence α} (h : ∀ (k : ℕ), xs k ∈ p → ∃ (k' : ℕ), k ≤ k' ∧ xs k' ∈ q) : xs.LeadsTo p q

theorem Cslib.ωSequence.step_leadsTo {α : Type u_1} {xs : ωSequence α} {p q : Set α} (h : xs.Step p q) : xs.LeadsTo p q

Step implies LeadsTo.

theorem Cslib.ωSequence.leadsTo_trans {α : Type u_1} {xs : ωSequence α} {p q r : Set α} (h1 : xs.LeadsTo p q) (h2 : xs.LeadsTo q r) : xs.LeadsTo p r

LeadsTo is transitive.

theorem Cslib.ωSequence.leadsTo_cases_or {α : Type u_1} {xs : ωSequence α} {p q r s : Set α} (h1 : xs.LeadsTo (p ∩ q) r) (h2 : xs.LeadsTo (p ∩ qᶜ) s) : xs.LeadsTo p (r ∪ s)

If p ∩ q leads to r and p ∩ qᶜ leads to s, then p leads to r ∪ s.

theorem Cslib.ωSequence.until_frequently_not_leadsTo {α : Type u_1} {xs : ωSequence α} {p q : Set α} (h1 : xs.Step (p ∩ qᶜ) p) (h2 : ∃ᶠ (k : ℕ) in Filter.atTop, xs k ∉ p) : xs.LeadsTo p q

If p holds until q and p fails infinitely often, then p leads to q.

theorem Cslib.ωSequence.until_frequently_leadsTo_and {α : Type u_1} {xs : ωSequence α} {p q : Set α} (h1 : xs.Step (p ∩ qᶜ) p) (h2 : ∃ᶠ (k : ℕ) in Filter.atTop, xs k ∈ q) : xs.LeadsTo p (p ∩ q)

If p holds until q and q holds infinite often, then p leads to p ∩ q.

theorem Cslib.ωSequence.frequently_leadsTo_frequently {α : Type u_1} {xs : ωSequence α} {p q : Set α} (h1 : ∃ᶠ (k : ℕ) in Filter.atTop, xs k ∈ p) (h2 : xs.LeadsTo p q) : ∃ᶠ (k : ℕ) in Filter.atTop, xs k ∈ q

If p holds infinitely often and p leads to q, then q holds infinite often as well.

theorem Cslib.ωSequence.drop_frequently_iff_frequently {α : Type u_1} {xs : ωSequence α} {p : Set α} (n : ℕ) : (∃ᶠ (k : ℕ) in Filter.atTop, (drop n xs) k ∈ p) ↔ ∃ᶠ (k : ℕ) in Filter.atTop, xs k ∈ p