Exercise 1.19 (Scott 1981, PRG-19, §1) — positive neighbourhood systems

Scott replaces condition (ii) of Definition 1.1 by the biconditional (ii′): whenever X, Y ∈ 𝒟, then X ∩ Y ≠ ∅ iff X ∩ Y ∈ 𝒟. The predicate IsPositive and the builder ofPositive (positive ⟹ neighbourhood system) live in Basic.lean.

This file supplies the two examples requested by the exercise:

• positiveExample — a genuinely positive system (all non-empty subsets of Δ, built with ofPositive), with positiveExample_isPositive;
• a non-positive neighbourhood system notPositiveSystem over Δ = {0,1,2} with 𝒟 = {Δ, {0,1}, {1,2}}. It satisfies Definition 1.1 (the only overlapping pair {0,1}, {1,2} has intersection {1}, which has no consistency witness in 𝒟, so (ii) never fires) yet fails (ii′): {0,1} ∩ {1,2} = {1} is non-empty but is not a neighbourhood (not_isPositive). This is a small stand-in for Hoare's ℕ × ℕ example (Scott notes "smaller examples are of course possible").

Everything is [propext, Quot.sound].

A positive system: all non-empty subsets of Fin 2.

def Domain.Neighborhood.Exercise119.positiveExample : NeighborhoodSystem (Fin 2)

All non-empty subsets of Fin 2 form a positive neighbourhood system: there X ∩ Y ∈ 𝒟 literally is (X ∩ Y).Nonempty, so (ii′) is Iff.rfl.

Equations

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

theorem Domain.Neighborhood.Exercise119.positiveExample_isPositive : positiveExample.IsPositive

A non-positive system over Δ = {0,1,2}.

@[reducible, inline]

abbrev Domain.Neighborhood.Exercise119.Tok : Type

Tokens Δ = {0, 1, 2}.

Equations

• Domain.Neighborhood.Exercise119.Tok = Fin 3

def Domain.Neighborhood.Exercise119.master : Set Tok

The master neighbourhood Δ.

Equations

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

def Domain.Neighborhood.Exercise119.a : Set Tok

The neighbourhood {0, 1}.

Equations

• Domain.Neighborhood.Exercise119.a = {0, 1}

def Domain.Neighborhood.Exercise119.b : Set Tok

The neighbourhood {1, 2}.

Equations

• Domain.Neighborhood.Exercise119.b = {1, 2}

def Domain.Neighborhood.Exercise119.memSet : Set (Set Tok)

𝒟 = {Δ, {0,1}, {1,2}}.

Equations

• Domain.Neighborhood.Exercise119.memSet = {Domain.Neighborhood.Exercise119.master, Domain.Neighborhood.Exercise119.a, Domain.Neighborhood.Exercise119.b}

def Domain.Neighborhood.Exercise119.mem (X : Set Tok) : Prop

Membership in 𝒟.

Equations

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

theorem Domain.Neighborhood.Exercise119.mem_iff (X : Set Tok) : mem X ↔ X = master ∨ X = a ∨ X = b

theorem Domain.Neighborhood.Exercise119.mem_master : mem master

theorem Domain.Neighborhood.Exercise119.mem_a : mem a

theorem Domain.Neighborhood.Exercise119.mem_b : mem b

theorem Domain.Neighborhood.Exercise119.a_inter_b : a ∩ b = {1}

{0,1} ∩ {1,2} = {1}.

theorem Domain.Neighborhood.Exercise119.one_not_mem : ¬mem {1}

{1} is not a neighbourhood (it is neither Δ, {0,1}, nor {1,2}).

theorem Domain.Neighborhood.Exercise119.not_mem_sub_one {Z : Set Tok} (hZ : mem Z) (hsub : Z ⊆ {1}) : False

No neighbourhood is contained in {1} (each contains a token other than 1). This is why the overlapping pair {0,1}, {1,2} never triggers condition (ii).

theorem Domain.Neighborhood.Exercise119.inter_eq (X Y : Set Tok) (hX : mem X) (hY : mem Y) : X ∩ Y = master ∨ X ∩ Y = a ∨ X ∩ Y = b ∨ X ∩ Y = {1}

Classification of binary intersections in 𝒟.

def Domain.Neighborhood.Exercise119.notPositiveSystem : NeighborhoodSystem Tok

Exercise 1.19 — the non-positive example is a neighbourhood system. The only intersection that is not already a neighbourhood is {0,1} ∩ {1,2} = {1}, and that case is impossible: a consistency witness Z ⊆ {1} with Z ∈ 𝒟 does not exist (not_mem_sub_one).

Equations

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

theorem Domain.Neighborhood.Exercise119.not_isPositive : ¬notPositiveSystem.IsPositive

Exercise 1.19 — the example is not positive. {0,1} and {1,2} are neighbourhoods whose intersection {1} is non-empty but is not a neighbourhood, contradicting (ii′).