Exercise 4.19 (Scott 1981, PRG-19, Lecture IV) — verifying Example 4.4

Example 4.4 leaves many assertions to the reader. This module discharges the two explicitly requested ones:

• "Peano's Axioms" for {0,1}*. The structured set ⟨Σ*, Λ, 0·, 1·⟩ (here Σ* = List Bool, Λ = [], and the two successors b ↦ b :: ·) satisfies the natural two-successor analogue of Definition 4.5: Λ is not a successor (peano_nil_ne_cons), each successor is injective (peano_cons_injective), the two successor ranges are disjoint (peano_cons_disjoint), and the induction principle holds (peano_induction). So Σ* is the free monoid on two generators — the binary-tree analogue of ⟨ℕ, 0, ⁺⟩.

• one : C → T is definable from the rest of the structure by a fixed-point equation. We first build the three tests empty, zero, one : C → T as honest approximable maps (Scott: "it is an exercise to show these are approximable"), via a uniform head-test combinator liftC. We then show

  one(x) = cond(empty(x), false, cond(zero(x), false, true))

  on every generator of |C| (one_def_strElem, one_def_strBot), exhibiting one as the solution of a fixed-point/recursion equation in the remaining structure ⟨C, Λ, 0, 1, empty, zero, cond⟩ (the right-hand side does not mention one, so this is the trivial fixed point — Scott's point that the tests are not independent).

The liftC combinator (a map C → V determined by its values on the partial elements σ⊥ and the total elements σ, subject to two monotonicity conditions) is reusable; with it one likewise gets Scott's tail : C → C (tail(bx) = x, tail(Λ) = ⊥), here noted but not needed for one.

The liftC data is choice-free; the truth-domain tests inherit Classical.choice structurally from T (Example 1.2), exactly as Example23.parityMap and Example43.zeroMap do.

"Peano's Axioms" for {0,1}* = List Bool.

theorem Domain.Neighborhood.Exercise419.peano_nil_ne_cons (b : Bool) (σ : ExampleB.Str) : [] ≠ b :: σ

Exercise 4.19 — Peano (i) for {0,1}*. Λ is not a successor: [] ≠ b :: σ.

theorem Domain.Neighborhood.Exercise419.peano_cons_injective {b : Bool} {σ τ : ExampleB.Str} (h : b :: σ = b :: τ) : σ = τ

Exercise 4.19 — Peano (ii) for {0,1}*. Each successor b ::· is injective.

theorem Domain.Neighborhood.Exercise419.peano_cons_disjoint (σ τ : ExampleB.Str) : false :: σ ≠ true :: τ

Exercise 4.19 — Peano (ii′) for {0,1}*. The two successor ranges are disjoint: 0σ ≠ 1τ.

theorem Domain.Neighborhood.Exercise419.peano_induction (P : ExampleB.Str → Prop) (hnil : P []) (hcons : ∀ (b : Bool) (σ : ExampleB.Str), P σ → P (b :: σ)) (σ : ExampleB.Str) : P σ

Exercise 4.19 — Peano (iii) for {0,1}*. Induction: a predicate holding at Λ and closed under both successors holds everywhere. (This is List.rec; it is the two-successor analogue of Definition 4.5(iii) and the recursion engine behind tail/empty/zero/one.)

Disjointness facts for C's neighbourhoods (cones vs singletons).

theorem Domain.Neighborhood.Exercise419.not_cone_subset_singleton (τ σ : ExampleB.Str) : ¬ExampleB.cone τ ⊆ {σ}

A cone is never contained in a singleton (it has at least two elements).

theorem Domain.Neighborhood.Exercise419.cone_ne_singleton (τ σ : ExampleB.Str) : ExampleB.cone τ ≠ {σ}

A cone is never equal to a singleton.

The head-test value functions.

def Domain.Neighborhood.Exercise419.headValC {β : Type u_1} (V : NeighborhoodSystem β) (z a0 a1 : V.Element) : ExampleB.Str → V.Element

The codomain value chosen by inspecting the head of a sequence: [] ↦ z, 0σ ↦ a₀, 1σ ↦ a₁. With z = ⊥ this is the value at the partial element σ⊥; with z = vΛ the value at the total element σ.

Equations

• Domain.Neighborhood.Exercise419.headValC V z a0 a1 [] = z
• Domain.Neighborhood.Exercise419.headValC V z a0 a1 (false :: tail) = a0
• Domain.Neighborhood.Exercise419.headValC V z a0 a1 (true :: tail) = a1

@[simp]

theorem Domain.Neighborhood.Exercise419.headValC_nil {β : Type u_1} (V : NeighborhoodSystem β) (z a0 a1 : V.Element) : headValC V z a0 a1 [] = z

@[simp]

theorem Domain.Neighborhood.Exercise419.headValC_false {β : Type u_1} (V : NeighborhoodSystem β) (z a0 a1 : V.Element) (σ : ExampleB.Str) : headValC V z a0 a1 (false :: σ) = a0

@[simp]

theorem Domain.Neighborhood.Exercise419.headValC_true {β : Type u_1} (V : NeighborhoodSystem β) (z a0 a1 : V.Element) (σ : ExampleB.Str) : headValC V z a0 a1 (true :: σ) = a1

theorem Domain.Neighborhood.Exercise419.headValC_bot_le {β : Type u_1} (V : NeighborhoodSystem β) (z' a0 a1 : V.Element) {σ τ : ExampleB.Str} (h : σ <+: τ) : headValC V V.bot a0 a1 σ ≤ headValC V z' a0 a1 τ

Monotonicity of the head value: along a prefix σ <+: τ, the partial value (z = ⊥) at σ is below any head value at τ with the same head constants. Covers both required conditions (cone→cone with z' = ⊥, cone→singleton with z' = vΛ).

The combinator liftC: an approximable map out of C.

def Domain.Neighborhood.Exercise419.liftC {β : Type u_1} (V : NeighborhoodSystem β) (coneVal singVal : ExampleB.Str → V.Element) (hcone : ∀ {σ τ : ExampleB.Str}, σ <+: τ → coneVal σ ≤ coneVal τ) (hsing : ∀ {σ τ : ExampleB.Str}, σ <+: τ → coneVal σ ≤ singVal τ) : ApproximableMap Example44.C V

A map C → V determined by its value coneVal σ on each partial element σ⊥ and singVal σ on each total element σ, provided (a) the partial values are monotone along prefixes and (b) a partial value sits below the total value of any extending prefix. The relation says: a cone σΣ* relates to the neighbourhoods of coneVal σ, and a singleton {σ} to those of singVal σ.

Equations

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

theorem Domain.Neighborhood.Exercise419.liftC_strBot {β : Type u_1} (V : NeighborhoodSystem β) (coneVal singVal : ExampleB.Str → V.Element) (hcone : ∀ {σ τ : ExampleB.Str}, σ <+: τ → coneVal σ ≤ coneVal τ) (hsing : ∀ {σ τ : ExampleB.Str}, σ <+: τ → coneVal σ ≤ singVal τ) (σ : ExampleB.Str) : (liftC V coneVal singVal ⋯ ⋯).toElementMap (Example44.strBot σ) = coneVal σ

liftC on a partial element: f(σ⊥) = coneVal σ.

theorem Domain.Neighborhood.Exercise419.liftC_strElem {β : Type u_1} (V : NeighborhoodSystem β) (coneVal singVal : ExampleB.Str → V.Element) (hcone : ∀ {σ τ : ExampleB.Str}, σ <+: τ → coneVal σ ≤ coneVal τ) (hsing : ∀ {σ τ : ExampleB.Str}, σ <+: τ → coneVal σ ≤ singVal τ) (σ : ExampleB.Str) : (liftC V coneVal singVal ⋯ ⋯).toElementMap (Example44.strElem σ) = singVal σ

liftC on a total element: f(σ) = singVal σ.

The three tests empty, zero, one : C → T.

@[reducible, inline]

abbrev Domain.Neighborhood.Exercise419.T : NeighborhoodSystem Example12.Token

The truth domain T of Example 1.2.

Equations

• Domain.Neighborhood.Exercise419.T = Domain.Neighborhood.Example23.T

def Domain.Neighborhood.Exercise419.emptyMap : ApproximableMap Example44.C T

Example 4.4 — empty. empty(Λ) = true, empty(0x) = empty(1x) = false, strict.

Equations

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

def Domain.Neighborhood.Exercise419.zeroMap : ApproximableMap Example44.C T

Example 4.4 — zero. zero(Λ) = false, zero(0x) = true, zero(1x) = false, strict.

Equations

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

def Domain.Neighborhood.Exercise419.oneMap : ApproximableMap Example44.C T

Example 4.4 — one. one(Λ) = false, one(0x) = false, one(1x) = true, strict.

Equations

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

Value equations on total elements σ and partial elements σ⊥.

@[simp]

theorem Domain.Neighborhood.Exercise419.emptyMap_strElem (σ : ExampleB.Str) : emptyMap.toElementMap (Example44.strElem σ) = headValC T Example23.trueElt Example23.falseElt Example23.falseElt σ

@[simp]

theorem Domain.Neighborhood.Exercise419.emptyMap_strBot (σ : ExampleB.Str) : emptyMap.toElementMap (Example44.strBot σ) = headValC T T.bot Example23.falseElt Example23.falseElt σ

@[simp]

theorem Domain.Neighborhood.Exercise419.zeroMap_strElem (σ : ExampleB.Str) : zeroMap.toElementMap (Example44.strElem σ) = headValC T Example23.falseElt Example23.trueElt Example23.falseElt σ

@[simp]

theorem Domain.Neighborhood.Exercise419.zeroMap_strBot (σ : ExampleB.Str) : zeroMap.toElementMap (Example44.strBot σ) = headValC T T.bot Example23.trueElt Example23.falseElt σ

@[simp]

theorem Domain.Neighborhood.Exercise419.oneMap_strElem (σ : ExampleB.Str) : oneMap.toElementMap (Example44.strElem σ) = headValC T Example23.falseElt Example23.falseElt Example23.trueElt σ

@[simp]

theorem Domain.Neighborhood.Exercise419.oneMap_strBot (σ : ExampleB.Str) : oneMap.toElementMap (Example44.strBot σ) = headValC T T.bot Example23.falseElt Example23.trueElt σ

one is defined from empty, zero and cond by a fixed-point

equation.

theorem Domain.Neighborhood.Exercise419.condT_bot (x y : T.Element) : (Exercise326.cond T).toElementMap (pair T.bot (pair x y)) = T.bot

cond(⊥, x, y) = ⊥ in T, phrased with T.bot (which the head-test empty(⊥) produces) rather than the syntactically distinct Example23.botElt of Exercise326.cond_bot.

def Domain.Neighborhood.Exercise419.oneDef (x : Example44.C.Element) : T.Element

The defining right-hand side: cond(empty(x), false, cond(zero(x), false, true)). It uses only empty, zero and the conditional cond (Exercise 3.26) — not one.

Equations

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

theorem Domain.Neighborhood.Exercise419.one_def_strElem (σ : ExampleB.Str) : oneMap.toElementMap (Example44.strElem σ) = oneDef (Example44.strElem σ)

Exercise 4.19 (Scott 1981, PRG-19). one is definable from empty, zero, cond: the equation one(x) = cond(empty(x), false, cond(zero(x), false, true)) holds on every total element σ.

theorem Domain.Neighborhood.Exercise419.one_def_strBot (σ : ExampleB.Str) : oneMap.toElementMap (Example44.strBot σ) = oneDef (Example44.strBot σ)

Exercise 4.19 (Scott 1981, PRG-19). The same defining equation holds on every partial element σ⊥ — including ⊥ = []⊥ where empty(⊥) = ⊥ forces cond(⊥, …) = ⊥.