Example 1.B (Scott 1981, PRG-19, §1) — binary sequences

Scott's recurring binary example, generalizing the finite binary tree of Example 1.4 to infinite sequences. Take Δ = Σ* with Σ = {0,1} (the finite binary strings, Λ = the empty string), and for σ ∈ Σ* let σΣ* be the set of all extensions of σ. The neighbourhoods are

B = {σΣ* ∣ σ ∈ Σ*},

a neighbourhood being "all extensions of a fixed prefix σ". We encode Σ* = List Bool, the empty sequence Λ = [], concatenation στ = σ ++ τ, and the initial-segment relation σ prefix τ by mathlib's list-prefix order σ <+: τ. The cone σΣ* is cone σ = {w ∣ σ <+: w}.

Deliverables (all of the Example-1.B paragraph, lines 281–315 of the source):

• Example 1.B / Exercise (B is a system). B : NeighborhoodSystem Str, built from the prefix trichotomy via ofNestedOrDisjoint — any two cones are nested or disjoint.
• σ⊥ (the finite elements). sigmaBot σ = ↑(cone σ), the principal filter of σΣ*; its minimal neighbourhood is σΔ = cone σ.
• Factoid σ₀⊥ ⊆ σ₁⊥ iff σ₀ initial segment of σ₁. sigmaBot_le_iff.
• Exercise (σx ∈ |B|). sigmaElt σ x, and sigmaElt σ ⊥ = σ⊥ (sigmaElt_bot) justifying the σ⊥ notation.
• Factoid x = ⋃ₙ σₙ⊥. mem_iff_exists_sigmaBot: every x ∈ |B| is the union of the finite elements σ⊥ with σΣ* ∈ x — the concrete "limit of finite approximations" in |B|. (The countable chain form, with σₙ prefix σₙ₊₁ enumerated, needs choice and is left to the prose.)

Everything is constructive (#print axioms ⊆ {propext, Quot.sound}): list-prefix is decidable, so the trichotomy is choice-free.

@[reducible, inline]

abbrev Domain.Neighborhood.ExampleB.Str : Type

The token type Σ* = List Bool (finite binary strings); Λ = [].

Equations

• Domain.Neighborhood.ExampleB.Str = List Bool

def Domain.Neighborhood.ExampleB.cone (σ : Str) : Set Str

The neighbourhood σΣ*: all extensions of σ (sequences with σ as an initial segment).

Equations

• Domain.Neighborhood.ExampleB.cone σ = {w : Domain.Neighborhood.ExampleB.Str | σ <+: w}

@[simp]

theorem Domain.Neighborhood.ExampleB.mem_cone {σ w : Str} : w ∈ cone σ ↔ σ <+: w

theorem Domain.Neighborhood.ExampleB.cone_nil : cone [] = Set.univ

ΛΣ* = Σ*: the cone of the empty string is everything (Scott's Δ).

theorem Domain.Neighborhood.ExampleB.cone_subset_cone {σ τ : Str} : cone σ ⊆ cone τ ↔ τ <+: σ

Cones reverse the prefix order. σΣ* ⊆ τΣ* iff τ is an initial segment of σ: a longer prefix carves out a smaller cone. (→ tests at σ ∈ σΣ*; ← is transitivity of <+:.)

theorem Domain.Neighborhood.ExampleB.cone_injective {σ τ : Str} (h : cone σ = cone τ) : σ = τ

Cones are one-one in the prefix. cone σ = cone τ ⟹ σ = τ: from the two inclusions we get τ <+: σ and σ <+: τ, and a prefix-antisymmetry (equal lengths) finishes. Used by the approximable maps B → T / B → B (Examples 2.3, 2.4) to read off the unique generating prefix of a cone.

theorem Domain.Neighborhood.ExampleB.cone_trichotomy (σ τ : Str) : cone σ ⊆ cone τ ∨ cone τ ⊆ cone σ ∨ cone σ ∩ cone τ = ∅

Prefix trichotomy for cones. Any two cones are nested-or-disjoint: either one contains the other, or they are disjoint (incomparable prefixes have no common extension). Choice-free: the prefix relation on List Bool is decidable.

def Domain.Neighborhood.ExampleB.memB (X : Set Str) : Prop

Membership in Scott's binary neighbourhood system B: X ∈ B iff X = σΣ* for some σ.

Equations

• Domain.Neighborhood.ExampleB.memB X = ∃ (σ : Domain.Neighborhood.ExampleB.Str), X = Domain.Neighborhood.ExampleB.cone σ

theorem Domain.Neighborhood.ExampleB.nestedOrDisjoint : NestedOrDisjoint memB

Exercise ("B is a neighbourhood system"). The family B = {σΣ* ∣ σ ∈ Σ*} is pairwise nested-or-disjoint, by cone_trichotomy.

def Domain.Neighborhood.ExampleB.B : NeighborhoodSystem Str

Example 1.B (Scott 1981, PRG-19). The binary neighbourhood system B on Δ = Σ*.

Equations

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

@[simp]

theorem Domain.Neighborhood.ExampleB.B_mem {X : Set Str} : B.mem X ↔ memB X

@[simp]

theorem Domain.Neighborhood.ExampleB.B_master : B.master = Set.univ

theorem Domain.Neighborhood.ExampleB.memB_cone (σ : Str) : B.mem (cone σ)

Every cone is a neighbourhood of B.

Prepending a prefix: σX = {στ ∣ τ ∈ X}.

def Domain.Neighborhood.ExampleB.prepend (σ : Str) (X : Set Str) : Set Str

Scott's σX = {στ ∣ τ ∈ X} (prepend the prefix σ to every member of X).

Equations

• Domain.Neighborhood.ExampleB.prepend σ X = {w : Domain.Neighborhood.ExampleB.Str | ∃ (τ : Domain.Neighborhood.ExampleB.Str), τ ∈ X ∧ w = σ ++ τ}

@[simp]

theorem Domain.Neighborhood.ExampleB.mem_prepend {σ : Str} {X : Set Str} {w : Str} : w ∈ prepend σ X ↔ ∃ (τ : Str), τ ∈ X ∧ w = σ ++ τ

theorem Domain.Neighborhood.ExampleB.prepend_cone (σ ρ : Str) : prepend σ (cone ρ) = cone (σ ++ ρ)

σ(τΣ*) = (στ)Σ*. Prepending σ to a cone yields the cone of the concatenation — this is why σx lands back in B and why σ⊥ is again a finite element.

theorem Domain.Neighborhood.ExampleB.prepend_univ (σ : Str) : prepend σ Set.univ = cone σ

σΣ* = σ·Σ*: prepending σ to the whole space recovers the cone of σ.

theorem Domain.Neighborhood.ExampleB.memB_prepend (σ : Str) {X : Set Str} (hX : B.mem X) : B.mem (prepend σ X)

Prepending preserves membership in B (σ applied to a cone is a cone).

The finite elements σ⊥ and the initial-segment factoid.

def Domain.Neighborhood.ExampleB.sigmaBot (σ : Str) : B.Element

σ⊥, a finite element of |B|. The principal filter ↑(σΣ*) of the cone of σ; its minimal neighbourhood is σΔ = σΣ* (Scott). These are exactly the finite elements of |B|.

Equations

• Domain.Neighborhood.ExampleB.sigmaBot σ = Domain.Neighborhood.ExampleB.B.principal ⋯

theorem Domain.Neighborhood.ExampleB.sigmaBot_le_iff (σ₀ σ₁ : Str) : sigmaBot σ₀ ≤ sigmaBot σ₁ ↔ σ₀ <+: σ₁

Factoid (Scott 1981, PRG-19). "σ₀⊥ ⊆ σ₁⊥ if and only if σ₀ is an initial segment of the sequence σ₁." The approximation order on finite elements is exactly the prefix order: σ₀⊥ ⊑ σ₁⊥ ↔ σ₀ <+: σ₁. (Via principal_le_iff — reversal — composed with cone_subset_cone — reversal again — which cancel to give the prefix order directly.)

The operation σx (Scott's left-multiplication on elements).

def Domain.Neighborhood.ExampleB.sigmaElt (σ : Str) (x : B.Element) : B.Element

Exercise (σx ∈ |B|). For x ∈ |B| and σ ∈ Σ*, Scott's σx = {Y ∣ σX ⊆ Y for some X ∈ x} is again an element of |B|.

The filter laws: master uses X = Δ ∈ x (σΔ ⊆ Δ trivially); inter takes X₁ ∩ X₂ ∈ x and the consistency witness σ(X₁∩X₂), which is a cone (hence in B, by memB_prepend) contained in both Y₁ and Y₂; up reuses the same X.

Equations

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

theorem Domain.Neighborhood.ExampleB.sigmaElt_bot (σ : Str) : sigmaElt σ B.bot = sigmaBot σ

σ⊥ really is σ applied to ⊥. sigmaElt σ ⊥ = sigmaBot σ, justifying the σ⊥ notation: applying σ to the least element produces the finite element ↑(σΣ*).

Every element is a union of its finite approximations σ⊥.

theorem Domain.Neighborhood.ExampleB.mem_iff_exists_sigmaBot (x : B.Element) {Z : Set Str} : x.mem Z ↔ ∃ (σ : Str), x.mem (cone σ) ∧ (sigmaBot σ).mem Z

Factoid (Scott 1981, PRG-19). "x = ⋃ₙ σₙ⊥": every x ∈ |B| is the union of the finite elements σ⊥ whose generating cone σΣ* lies in x. In membership form, a neighbourhood Z belongs to x iff Z lies in some σ⊥ = ↑(σΣ*) with σΣ* ∈ x.

This is the concrete "an element is uniquely determined by its finite approximations" in |B| (Basic.eq_iUnion_principal specialized to B, where every neighbourhood is a cone). The further arrangement of the σ into a single increasing chain σ₀ prefix σ₁ prefix … requires choice/enumeration and is left to Scott's prose.