Exercise 3.26 (Scott 1981, PRG-19, §3) — the conditional operator cond

Scott asks: for every domain D there is an approximable mapping

cond : T × D × D → D

(the conditional operator) satisfying

• cond(true, x, y) = x,
• cond(false, x, y) = y,
• cond(⊥, x, y) = ⊥.

Here T is the truth domain of Example 1.2 (Example12.neighborhoodSystem), whose neighbourhoods are {Δ, {0}, {1}} with true = ↑{0} (Example23.trueElt), false = ↑{1} (falseElt) and ⊥ = {Δ} (botElt). The product T × D × D is the tagged product of Exercise 3.14, modelled here as prod T (prod V V) over the token type T.Token ⊕ (α ⊕ α); a neighbourhood is 0C ∪ 10X ∪ 110Y, recovered from W by the projections C = inl⁻¹ W, X = inl⁻¹ inr⁻¹ W, Y = inr⁻¹ inr⁻¹ W.

Scott's hint gives the relation directly:

0C ∪ 10X ∪ 110Y  cond  Z   iff   0 ∈ C and X ⊆ Z,  or
                                  1 ∈ C and Y ⊆ Z,  or
                                  0, 1 ∈ C and Δ ⊆ Z.

Since T = {Δ, {0}, {1}}, the three guards on C are mutually exclusive and exhaustive: 0 ∈ C (alone) means C = {0}, 1 ∈ C (alone) means C = {1}, and 0, 1 ∈ C means C = Δ. We therefore phrase the relation with explicit equalities C = {0} / {1} / Δ (condGuard), which is mathematically identical to Scott's membership form but makes the case analysis transparent and the three identities clean.

Everything is choice-free in spirit; the only classical input is inherited from T (Example 1.2) and from the project's ext_of_toElementMap/Element.ext machinery, as elsewhere in §3.

@[reducible, inline]

abbrev Domain.Neighborhood.Exercise326.TD : NeighborhoodSystem Example12.Token

The truth domain T of Example 1.2 (neighbourhoods {Δ, {0}, {1}}).

Equations

• Domain.Neighborhood.Exercise326.TD = Domain.Neighborhood.Example12.neighborhoodSystem

Token-level facts about T's three neighbourhoods {0}, {1}, Δ.

theorem Domain.Neighborhood.Exercise326.zero_ne_one : Example12.zero ≠ Example12.one

theorem Domain.Neighborhood.Exercise326.zero_ne_master : Example12.zero ≠ Example12.master

theorem Domain.Neighborhood.Exercise326.one_ne_master : Example12.one ≠ Example12.master

theorem Domain.Neighborhood.Exercise326.Tmem_eq_zero {C : Set Example12.Token} (hC : Example12.mem C) (h : C ⊆ Example12.zero) : C = Example12.zero

A T-neighbourhood contained in {0} is {0} (the other two, Δ and {1}, are not).

theorem Domain.Neighborhood.Exercise326.Tmem_eq_one {C : Set Example12.Token} (hC : Example12.mem C) (h : C ⊆ Example12.one) : C = Example12.one

A T-neighbourhood contained in {1} is {1}.

The conditional relation.

def Domain.Neighborhood.Exercise326.condGuard {α : Type u_1} (V : NeighborhoodSystem α) (W : Set (Example12.Token ⊕ α ⊕ α)) (Z : Set α) : Prop

Scott's guard for cond, phrased with explicit equalities on the truth component C = inl⁻¹ W. With X = inl⁻¹ inr⁻¹ W and Y = inr⁻¹ inr⁻¹ W:

• C = {0} (true): X ⊆ Z;
• C = {1} (false): Y ⊆ Z;
• C = Δ (⊥): Δ_D ⊆ Z.

Equations

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

theorem Domain.Neighborhood.Exercise326.condGuard_zero {α : Type u_1} (V : NeighborhoodSystem α) {W : Set (Example12.Token ⊕ α ⊕ α)} {Z : Set α} (hg : condGuard V W Z) (hC : Sum.inl ⁻¹' W = Example12.zero) : Sum.inl ⁻¹' Sum.inr ⁻¹' W ⊆ Z

theorem Domain.Neighborhood.Exercise326.condGuard_one {α : Type u_1} (V : NeighborhoodSystem α) {W : Set (Example12.Token ⊕ α ⊕ α)} {Z : Set α} (hg : condGuard V W Z) (hC : Sum.inl ⁻¹' W = Example12.one) : Sum.inr ⁻¹' Sum.inr ⁻¹' W ⊆ Z

theorem Domain.Neighborhood.Exercise326.condGuard_master {α : Type u_1} (V : NeighborhoodSystem α) {W : Set (Example12.Token ⊕ α ⊕ α)} {Z : Set α} (hg : condGuard V W Z) (hC : Sum.inl ⁻¹' W = Example12.master) : V.master ⊆ Z

theorem Domain.Neighborhood.Exercise326.cond_components {α : Type u_1} (V : NeighborhoodSystem α) {W : Set (Example12.Token ⊕ α ⊕ α)} (hW : (prod TD (prod V V)).mem W) : Example12.mem (Sum.inl ⁻¹' W) ∧ V.mem (Sum.inl ⁻¹' Sum.inr ⁻¹' W) ∧ V.mem (Sum.inr ⁻¹' Sum.inr ⁻¹' W)

The three components C, X, Y of an input neighbourhood are themselves neighbourhoods.

def Domain.Neighborhood.Exercise326.cond {α : Type u_1} (V : NeighborhoodSystem α) : ApproximableMap (prod TD (prod V V)) V

Exercise 3.26 (Scott 1981, PRG-19). The conditional operator cond : T × D × D → D.

Equations

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

@[simp]

theorem Domain.Neighborhood.Exercise326.cond_rel {α : Type u_1} (V : NeighborhoodSystem α) {W : Set (Example12.Token ⊕ α ⊕ α)} {Z : Set α} : (cond V).rel W Z ↔ (prod TD (prod V V)).mem W ∧ V.mem Z ∧ condGuard V W Z

Elementwise characterization, and the three defining identities.

theorem Domain.Neighborhood.Exercise326.cond_toElementMap_mem {α : Type u_1} (V : NeighborhoodSystem α) (t : TD.Element) (x y : V.Element) {Z : Set α} : ((cond V).toElementMap (pair t (pair x y))).mem Z ↔ t.mem Example12.zero ∧ x.mem Z ∨ t.mem Example12.one ∧ y.mem Z ∨ Z = V.master

The elementwise action of cond, computed at a paired argument ⟨t, ⟨x, y⟩⟩: a neighbourhood Z lies in cond(t, x, y) iff t selects true ({0} ∈ t) and Z ∈ x, or t selects false ({1} ∈ t) and Z ∈ y, or Z = Δ_D (the always-present master). The three defining identities are immediate corollaries.

theorem Domain.Neighborhood.Exercise326.cond_true {α : Type u_1} (V : NeighborhoodSystem α) (x y : V.Element) : (cond V).toElementMap (pair Example23.trueElt (pair x y)) = x

Exercise 3.26(i) (Scott 1981, PRG-19). cond(true, x, y) = x.

theorem Domain.Neighborhood.Exercise326.cond_false {α : Type u_1} (V : NeighborhoodSystem α) (x y : V.Element) : (cond V).toElementMap (pair Example23.falseElt (pair x y)) = y

Exercise 3.26(ii) (Scott 1981, PRG-19). cond(false, x, y) = y.

theorem Domain.Neighborhood.Exercise326.cond_bot {α : Type u_1} (V : NeighborhoodSystem α) (x y : V.Element) : (cond V).toElementMap (pair Example23.botElt (pair x y)) = V.bot

Exercise 3.26(iii) (Scott 1981, PRG-19). cond(⊥, x, y) = ⊥.