Documentation

LeanPool.DomainTheory.Neighborhood.Exercise123

Exercise 1.23 (Scott 1981, PRG-19, §1) — the greedy total element of a countable #

system

Scott: suppose 𝒟 = {X₀, X₁, …} is countable and the consistency of finite sequences of neighbourhoods is decidable. Then the greedy sequence

Y₀     = X₀
Y_{n+1} = X_{n+1}  if X_{n+1} is consistent with Y₀, …, Yₙ;
        = Yₙ       otherwise.

is well defined, and {Y₀, Y₁, …} is a total element of |𝒟|. (Hint: first show that Y₀, …, Y_{n-1} is consistent for every n.)

This file formalizes the greedy construction over an enumeration enum : ℕ → Set α of 𝒟, encoding "consistency of the prefix + candidate is decidable" as [DecidablePred V.mem] (by Theorem 1.1c, a prefix is consistent iff its running intersection is a neighbourhood). We carry the state (Yₙ, ⋂_{i≤n} Yᵢ); the running intersection acc n is exactly interUpTo Y (n+1) and is always a neighbourhood, which is the hint Y_prefix_consistent.

greedyElement — the filter {X ∈ 𝒟 ∣ ⋂_{i<n} Yᵢ ⊆ X for some n} generated by ⟨Yₙ⟩;
greedyElement_isTotal — under surjectivity of enum, greedyElement is maximal: any W in a larger filter z is some enum k; if greedy skipped it then W was inconsistent with the prefix, contradicting z's closure under intersection.

The construction is [propext, Quot.sound] given the supplied DecidablePred.

theorem Domain.Neighborhood.NeighborhoodSystem.interUpTo_antitone {α : Type u_1} (V : NeighborhoodSystem α) (X : ℕ → Set α) {j k : ℕ} (h : j ≤ k) :

V.interUpTo X k ⊆ V.interUpTo X j

The finite intersection is antitone in its length: a longer prefix is contained in a shorter one.

def Domain.Neighborhood.Exercise123.state {α : Type u_1} (V : NeighborhoodSystem α) (enum : ℕ → Set α) [DecidablePred V.mem] :

ℕ → Set α × Set α

Greedy state: state n = (Yₙ, ⋂_{i≤n} Yᵢ). The running intersection in the second component lets the consistency test V.mem (acc ∩ enum (n+1)) be self-contained (Theorem 1.1c: the prefix Y₀,…,Yₙ,enum (n+1) is consistent iff this intersection is a neighbourhood).

Equations

One or more equations did not get rendered due to their size.
Domain.Neighborhood.Exercise123.state V enum 0 = (enum 0, V.master ∩ enum 0)

Instances For

def Domain.Neighborhood.Exercise123.Y {α : Type u_1} (V : NeighborhoodSystem α) (enum : ℕ → Set α) [DecidablePred V.mem] (n : ℕ) :

Set α

The greedy sequence Yₙ = (state n).1.

Equations

Domain.Neighborhood.Exercise123.Y V enum n = (Domain.Neighborhood.Exercise123.state V enum n).1

Instances For

def Domain.Neighborhood.Exercise123.acc {α : Type u_1} (V : NeighborhoodSystem α) (enum : ℕ → Set α) [DecidablePred V.mem] (n : ℕ) :

Set α

The running intersection acc n = ⋂_{i≤n} Yᵢ = (state n).2.

Equations

Domain.Neighborhood.Exercise123.acc V enum n = (Domain.Neighborhood.Exercise123.state V enum n).2

Instances For

@[reducible, inline]

abbrev Domain.Neighborhood.Exercise123.cond {α : Type u_1} (V : NeighborhoodSystem α) (enum : ℕ → Set α) [DecidablePred V.mem] (n : ℕ) :

The consistency test at stage n+1: is enum (n+1) consistent with the prefix Y₀,…,Yₙ? An abbrev so the [DecidablePred V.mem] instance is found through it.

Equations

Domain.Neighborhood.Exercise123.cond V enum n = V.mem (Domain.Neighborhood.Exercise123.acc V enum n ∩ enum (n + 1))

Instances For

@[simp]

theorem Domain.Neighborhood.Exercise123.Y_zero {α : Type u_1} (V : NeighborhoodSystem α) (enum : ℕ → Set α) [DecidablePred V.mem] :

Y V enum 0 = enum 0

@[simp]

theorem Domain.Neighborhood.Exercise123.acc_zero {α : Type u_1} (V : NeighborhoodSystem α) (enum : ℕ → Set α) [DecidablePred V.mem] :

acc V enum 0 = V.master ∩ enum 0

theorem Domain.Neighborhood.Exercise123.state_succ {α : Type u_1} (V : NeighborhoodSystem α) (enum : ℕ → Set α) [DecidablePred V.mem] (n : ℕ) :

state V enum (n + 1) = if cond V enum n then (enum (n + 1), acc V enum n ∩ enum (n + 1)) else state V enum n

The defining equation of state at a successor, written with the named cond/acc.

theorem Domain.Neighborhood.Exercise123.Y_succ_pos {α : Type u_1} (V : NeighborhoodSystem α) (enum : ℕ → Set α) [DecidablePred V.mem] {n : ℕ} (h : cond V enum n) :

Y V enum (n + 1) = enum (n + 1)

theorem Domain.Neighborhood.Exercise123.Y_succ_neg {α : Type u_1} (V : NeighborhoodSystem α) (enum : ℕ → Set α) [DecidablePred V.mem] {n : ℕ} (h : ¬cond V enum n) :

Y V enum (n + 1) = Y V enum n

theorem Domain.Neighborhood.Exercise123.acc_succ_pos {α : Type u_1} (V : NeighborhoodSystem α) (enum : ℕ → Set α) [DecidablePred V.mem] {n : ℕ} (h : cond V enum n) :

acc V enum (n + 1) = acc V enum n ∩ enum (n + 1)

theorem Domain.Neighborhood.Exercise123.acc_succ_neg {α : Type u_1} (V : NeighborhoodSystem α) (enum : ℕ → Set α) [DecidablePred V.mem] {n : ℕ} (h : ¬cond V enum n) :

acc V enum (n + 1) = acc V enum n

theorem Domain.Neighborhood.Exercise123.acc_eq_interUpTo {α : Type u_1} (V : NeighborhoodSystem α) (enum : ℕ → Set α) [DecidablePred V.mem] (n : ℕ) :

acc V enum n = V.interUpTo (Y V enum) (n + 1)

acc n = ⋂_{i<n+1} Yᵢ: the carried intersection is exactly the prefix intersection.

theorem Domain.Neighborhood.Exercise123.Y_mem {α : Type u_1} (V : NeighborhoodSystem α) (enum : ℕ → Set α) [DecidablePred V.mem] (henum : ∀ (n : ℕ), V.mem (enum n)) (n : ℕ) :

V.mem (Y V enum n)

Each Yₙ is a neighbourhood.

theorem Domain.Neighborhood.Exercise123.acc_mem {α : Type u_1} (V : NeighborhoodSystem α) (enum : ℕ → Set α) [DecidablePred V.mem] (henum : ∀ (n : ℕ), V.mem (enum n)) (n : ℕ) :

V.mem (acc V enum n)

The running intersection acc n is always a neighbourhood — the greedy choice guarantees it. This is the content of Scott's hint (consistency of the prefix).

theorem Domain.Neighborhood.Exercise123.mem_interUpTo_Y {α : Type u_1} (V : NeighborhoodSystem α) (enum : ℕ → Set α) [DecidablePred V.mem] (henum : ∀ (n : ℕ), V.mem (enum n)) (n : ℕ) :

V.mem (V.interUpTo (Y V enum) n)

⋂_{i<n} Yᵢ is always a neighbourhood.

theorem Domain.Neighborhood.Exercise123.Y_prefix_consistent {α : Type u_1} (V : NeighborhoodSystem α) (enum : ℕ → Set α) [DecidablePred V.mem] (henum : ∀ (n : ℕ), V.mem (enum n)) (n : ℕ) :

V.Consistent (Y V enum) n

Exercise 1.23 — the hint. For every n, the prefix Y₀, …, Y_{n-1} is consistent in 𝒟: its finite intersection is a neighbourhood, so it is its own common lower bound.

def Domain.Neighborhood.Exercise123.greedyElement {α : Type u_1} (V : NeighborhoodSystem α) (enum : ℕ → Set α) [DecidablePred V.mem] (henum : ∀ (n : ℕ), V.mem (enum n)) :

Exercise 1.23 — the greedy element. The filter generated by all Yₙ: {X ∈ 𝒟 ∣ ⋂_{i<n} Yᵢ ⊆ X for some n}. The prefix intersections ⋂_{i<n} Yᵢ are a descending chain of neighbourhoods, so this is a genuine filter.

Equations

One or more equations did not get rendered due to their size.

Instances For

theorem Domain.Neighborhood.Exercise123.greedyElement_mem_Y {α : Type u_1} (V : NeighborhoodSystem α) (enum : ℕ → Set α) [DecidablePred V.mem] (henum : ∀ (n : ℕ), V.mem (enum n)) (n : ℕ) :

(greedyElement V enum henum).mem (Y V enum n)

Every Yₙ belongs to the greedy element.

theorem Domain.Neighborhood.Exercise123.greedyElement_mem_acc {α : Type u_1} (V : NeighborhoodSystem α) (enum : ℕ → Set α) [DecidablePred V.mem] (henum : ∀ (n : ℕ), V.mem (enum n)) (n : ℕ) :

(greedyElement V enum henum).mem (acc V enum n)

The running intersection acc n belongs to the greedy element.

theorem Domain.Neighborhood.Exercise123.greedyElement_isTotal {α : Type u_1} (V : NeighborhoodSystem α) (enum : ℕ → Set α) [DecidablePred V.mem] (henum : ∀ (n : ℕ), V.mem (enum n)) (hsurj : ∀ {X : Set α}, V.mem X → ∃ (n : ℕ ), enum n = X) :

V.IsTotal (greedyElement V enum henum)

Exercise 1.23 — {Yₙ} is a total element. Maximality: if z extends the greedy element and W ∈ z, write W = enum k (surjectivity). For k = 0, W = Y₀ is already in the greedy element. For k = m+1: either the greedy step accepted enum k (then W = Y_k is in the element), or it rejected it — but then acc m ∩ enum k ∉ 𝒟, contradicting that both acc m (in the greedy element, hence in z) and W lie in the filter z.

theorem Domain.Neighborhood.Exercise123.filters_sequence_determined {α : Type u_1} (V : NeighborhoodSystem α) (enum : ℕ → Set α) (henum : ∀ (n : ℕ), V.mem (enum n)) (hsurj : ∀ {X : Set α}, V.mem X → ∃ (n : ℕ ), enum n = X) (x : V.Element) :

∃ (s : ℕ → Set α), (∀ (n : ℕ), V.mem (s n)) ∧ ∀ (Z : Set α), x.mem Z ↔ V.mem Z ∧ ∃ (n : ℕ ), s n ⊆ Z

Exercise 1.23 — "all filters can be determined by sequences". In a countable system, every filter x is the limit family of a sequence of neighbourhoods: take sₙ = enum n whenever enum n ∈ x and sₙ = Δ otherwise. Every member of x is some enum k (surjectivity), so it is caught by s; conversely each sₙ ∈ x, so anything above some sₙ is in x. (Classical: it selects the sequence by deciding membership in x.)