Exhaustive limits of nested finite histories

@[simp]

theorem GenLimit.FiniteWitness.prefix_toFinset {α : Type u_1} [DecidableEq α] (stream : Generic.Stream α) (t : ℕ) : (textPrefix stream t).toFinset = Generic.sample stream t

def GenLimit.FiniteWitness.listOutput {α : Type u_1} (G : Generic.Generator α) (xs : List α) : α

Evaluate an ordered-history generator on a finite list of observations.

Equations

• GenLimit.FiniteWitness.listOutput G xs = G xs.length xs.get

@[simp]

theorem GenLimit.FiniteWitness.listOutput_prefix {α : Type u_1} (G : Generic.Generator α) (stream : Generic.Stream α) (t : ℕ) : listOutput G (textPrefix stream t) = Generic.output G stream t

def GenLimit.FiniteWitness.EventuallyValid {α : Type u_1} (F : List α → α) (L : Generic.Language α) : Prop

Eventual target validity of a list-input function; freshness is separate.

Equations

• GenLimit.FiniteWitness.EventuallyValid F L = ∀ (stream : GenLimit.Generic.Stream α), GenLimit.Generic.Presents stream L → ∃ (t₀ : ℕ), ∀ (t : ℕ), t₀ ≤ t → F (GenLimit.textPrefix stream t) ∈ L

def GenLimit.FiniteWitness.Fresh {α : Type u_1} (F : List α → α) : Prop

A list-input function always returns an element absent from its input.

Equations

• GenLimit.FiniteWitness.Fresh F = ∀ (xs : List α), F xs ∉ xs

noncomputable def GenLimit.FiniteWitness.freshRepair {α : Type u_1} [Infinite α] (G : Generic.Generator α) (xs : List α) : α

Replace a previously observed output by a fresh element of the infinite universe.

Equations

• GenLimit.FiniteWitness.freshRepair G xs = if GenLimit.FiniteWitness.listOutput G xs ∈ xs then ⋯.choose else GenLimit.FiniteWitness.listOutput G xs

theorem GenLimit.FiniteWitness.freshRepair_fresh {α : Type u_1} [Infinite α] (G : Generic.Generator α) : Fresh (freshRepair G)

theorem GenLimit.FiniteWitness.freshRepair_eventuallyValid {α : Type u_1} [Infinite α] {G : Generic.Generator α} {H : Generic.LanguageClass α} (hG : Generic.IsLimitGenerator G H) {L : Generic.Language α} (hL : L ∈ H) : EventuallyValid (freshRepair G) L

theorem GenLimit.FiniteWitness.history_prefix_mono {α : Type u_1} {v : ℕ → List α} (hp : ∀ (n : ℕ), v n <+: v (n + 1)) {n m : ℕ} (hnm : n ≤ m) : v n <+: v m

def GenLimit.FiniteWitness.chainStream {α : Type u_1} (v : ℕ → List α) (hlen : ∀ (n : ℕ), n ≤ (v n).length) : Generic.Stream α

The stream determined by a nested sequence whose lengths tend to infinity.

Equations

• GenLimit.FiniteWitness.chainStream v hlen k = (v (k + 1)).get ⟨k, ⋯⟩

theorem GenLimit.FiniteWitness.chainStream_eq_get {α : Type u_1} {v : ℕ → List α} (hp : ∀ (n : ℕ), v n <+: v (n + 1)) (hlen : ∀ (n : ℕ), n ≤ (v n).length) (n k : ℕ) (hk : k < (v n).length) : chainStream v hlen k = (v n).get ⟨k, hk⟩

theorem GenLimit.FiniteWitness.prefix_chainStream {α : Type u_1} {v : ℕ → List α} (hp : ∀ (n : ℕ), v n <+: v (n + 1)) (hlen : ∀ (n : ℕ), n ≤ (v n).length) (n : ℕ) : textPrefix (chainStream v hlen) (v n).length = v n

theorem GenLimit.FiniteWitness.chainStream_presents {α : Type u_1} {v : ℕ → List α} {L : Generic.Language α} (hp : ∀ (n : ℕ), v n <+: v (n + 1)) (hlen : ∀ (n : ℕ), n ≤ (v n).length) (hlegal : ∀ (n : ℕ), ∀ x ∈ v n, x ∈ L) (hexhaust : ∀ x ∈ L, ∃ (n : ℕ), x ∈ v n) : Generic.Presents (chainStream v hlen) L

theorem GenLimit.FiniteWitness.no_exhaustive_bad_chain {α : Type u_1} {F : List α → α} {L : Generic.Language α} (hvalid : EventuallyValid F L) (v : ℕ → List α) (hp : ∀ (n : ℕ), v n <+: v (n + 1)) (hlen : ∀ (n : ℕ), n ≤ (v n).length) (hlegal : ∀ (n : ℕ), ∀ x ∈ v n, x ∈ L) (hexhaust : ∀ x ∈ L, ∃ (n : ℕ), x ∈ v n) (hbad : ∀ (n : ℕ), F (v (n + 1)) ∉ L) : False

An exhaustive chain cannot have bad outputs at every positive stage.