Example 1.3 (Scott 1981, PRG-19, §1)

Scott's second worked example: tokens Δ = {0, 1, 2} and neighbourhoods 𝒟 = {{0, 1, 2}, {1, 2}, {2}}.

We construct the neighbourhood system, prove it satisfies Definition 1.1, and classify its domain elements (Definition 1.6): there are exactly three filters in a linear chain ⊥ < {Δ,{1,2}} < {Δ,{1,2},{2}}, with token 2 the sole total element.

This is a concrete finite computation (fin_cases/simp); footprint [propext, Classical.choice, Quot.sound] — same as Example 1.2.

@[reducible, inline]

abbrev Domain.Neighborhood.Example13.Token : Type

Tokens for Example 1.3: Δ = {0, 1, 2}.

Equations

• Domain.Neighborhood.Example13.Token = Fin 3

def Domain.Neighborhood.Example13.master : Set Token

The master neighbourhood Δ = {0, 1, 2}.

Equations

• Domain.Neighborhood.Example13.master = Set.univ

def Domain.Neighborhood.Example13.twelve : Set Token

The neighbourhood {1, 2}.

Equations

• Domain.Neighborhood.Example13.twelve = {2, 1}

def Domain.Neighborhood.Example13.two : Set Token

The neighbourhood {2}.

Equations

• Domain.Neighborhood.Example13.two = {2}

def Domain.Neighborhood.Example13.memSet : Set (Set Token)

The three neighbourhoods of Example 1.3.

Equations

• Domain.Neighborhood.Example13.memSet = {Domain.Neighborhood.Example13.master, Domain.Neighborhood.Example13.twelve, Domain.Neighborhood.Example13.two}

def Domain.Neighborhood.Example13.mem (X : Set Token) : Prop

Membership in the neighbourhood system 𝒟 of Example 1.3.

Equations

• Domain.Neighborhood.Example13.mem X = (X ∈ Domain.Neighborhood.Example13.memSet)

theorem Domain.Neighborhood.Example13.mem_master : mem master

theorem Domain.Neighborhood.Example13.mem_twelve : mem twelve

theorem Domain.Neighborhood.Example13.mem_two : mem two

theorem Domain.Neighborhood.Example13.mem_iff (X : Set Token) : mem X ↔ X = master ∨ X = twelve ∨ X = two

A neighbourhood of Example 1.3 is exactly one of Δ, {1,2}, or {2}.

def Domain.Neighborhood.Example13.neighborhoodSystem : NeighborhoodSystem Token

Example 1.3. The neighbourhood system on Δ = {0, 1, 2}.

Equations

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

def Domain.Neighborhood.Example13.neighborhoodSystem.bot : neighborhoodSystem.Element

The bottom element ⊥ = {Δ}.

Equations

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

def Domain.Neighborhood.Example13.neighborhoodSystem.elemTwelve : neighborhoodSystem.Element

The intermediate partial element {Δ, {1,2}}.

Equations

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

def Domain.Neighborhood.Example13.neighborhoodSystem.elemTwo : neighborhoodSystem.Element

The total element {Δ, {1,2}, {2}}.

Equations

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

theorem Domain.Neighborhood.Example13.neighborhoodSystem.element_classification (x : neighborhoodSystem.Element) : x = bot ∨ x = elemTwelve ∨ x = elemTwo

Every element of Example 1.3 is one of the three filters in the linear chain.

theorem Domain.Neighborhood.Example13.neighborhoodSystem.bot_lt_elemTwelve : bot < elemTwelve

theorem Domain.Neighborhood.Example13.neighborhoodSystem.elemTwelve_lt_elemTwo : elemTwelve < elemTwo

theorem Domain.Neighborhood.Example13.neighborhoodSystem.elemTwo_maximal (x : neighborhoodSystem.Element) (h : elemTwo ≤ x) : x = elemTwo