Exercise 3.26, continued (Scott 1981, PRG-19, §3) — the sum-valued conditional

and which

This module completes Exercise 3.26 with the two follow-up operators Scott asks for:

• the sum-valued conditional condSum : T × D₀ × D₁ → D₀ + D₁, routing true → in₀, false → in₁, ⊥ → ⊥. It is obtained for free by composition: feeding the two inputs through the injections in₀, in₁ into the common domain S = D₀ + D₁ and then applying the conditional cond S : T × S × S → S of Exercise 3.26. The three identities follow from cond_true/false/bot.

• the discriminator which : D₀ + D₁ → T reading the tag (0X ↦ true, 1Y ↦ false, Λ ↦ ⊥), together with Scott's identity

  cond(which x, in₀(out₀ x), in₁(out₁ x)) = x for all x ∈ |D₀ + D₁|.

The discriminator is built directly as a neighbourhood relation; its three guards on the truth component are mutually exclusive because the three forms of a sum-neighbourhood (Λ-master, left copy, right copy) are mutually exclusive (Exercise 3.18, using non-emptiness).

The sum-valued conditional condSum.

def Domain.Neighborhood.Exercise326.condSumEmb {α : Type u_1} {β : Type u_2} (V₀ : NeighborhoodSystem α) (V₁ : NeighborhoodSystem β) (h₀ : ∀ (X : Set α), V₀.mem X → X.Nonempty) (h₁ : ∀ (Y : Set β), V₁.mem Y → Y.Nonempty) : ApproximableMap (prod TD (prod V₀ V₁)) (prod TD (prod (sum V₀ V₁ h₀ h₁) (sum V₀ V₁ h₀ h₁)))

The embedding T × D₀ × D₁ → T × S × S (S = D₀ + D₁) that injects the two value slots into the sum via in₀ and in₁, leaving the truth slot fixed.

Equations

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

def Domain.Neighborhood.Exercise326.condSum {α : Type u_1} {β : Type u_2} (V₀ : NeighborhoodSystem α) (V₁ : NeighborhoodSystem β) (h₀ : ∀ (X : Set α), V₀.mem X → X.Nonempty) (h₁ : ∀ (Y : Set β), V₁.mem Y → Y.Nonempty) : ApproximableMap (prod TD (prod V₀ V₁)) (sum V₀ V₁ h₀ h₁)

Exercise 3.26 (Scott 1981, PRG-19). The sum-valued conditional T × D₀ × D₁ → D₀ + D₁.

Equations

• Domain.Neighborhood.Exercise326.condSum V₀ V₁ h₀ h₁ = (Domain.Neighborhood.Exercise326.cond (Domain.Neighborhood.sum V₀ V₁ h₀ h₁)).comp (Domain.Neighborhood.Exercise326.condSumEmb V₀ V₁ h₀ h₁)

theorem Domain.Neighborhood.Exercise326.condSumEmb_toElementMap {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {h₀ : ∀ (X : Set α), V₀.mem X → X.Nonempty} {h₁ : ∀ (Y : Set β), V₁.mem Y → Y.Nonempty} (t : TD.Element) (x : V₀.Element) (y : V₁.Element) : (condSumEmb V₀ V₁ h₀ h₁).toElementMap (pair t (pair x y)) = pair t (pair (inMap₀.toElementMap x) (inMap₁.toElementMap y))

theorem Domain.Neighborhood.Exercise326.condSum_true {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {h₀ : ∀ (X : Set α), V₀.mem X → X.Nonempty} {h₁ : ∀ (Y : Set β), V₁.mem Y → Y.Nonempty} (x : V₀.Element) (y : V₁.Element) : (condSum V₀ V₁ h₀ h₁).toElementMap (pair Example23.trueElt (pair x y)) = inMap₀.toElementMap x

Exercise 3.26. condSum(true, x, y) = in₀(x).

theorem Domain.Neighborhood.Exercise326.condSum_false {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {h₀ : ∀ (X : Set α), V₀.mem X → X.Nonempty} {h₁ : ∀ (Y : Set β), V₁.mem Y → Y.Nonempty} (x : V₀.Element) (y : V₁.Element) : (condSum V₀ V₁ h₀ h₁).toElementMap (pair Example23.falseElt (pair x y)) = inMap₁.toElementMap y

Exercise 3.26. condSum(false, x, y) = in₁(y).

theorem Domain.Neighborhood.Exercise326.condSum_bot {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {h₀ : ∀ (X : Set α), V₀.mem X → X.Nonempty} {h₁ : ∀ (Y : Set β), V₁.mem Y → Y.Nonempty} (x : V₀.Element) (y : V₁.Element) : (condSum V₀ V₁ h₀ h₁).toElementMap (pair Example23.botElt (pair x y)) = (sum V₀ V₁ h₀ h₁).bot

Exercise 3.26. condSum(⊥, x, y) = ⊥.

The discriminator which : D₀ + D₁ → T.

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

A T-neighbourhood containing Δ is Δ.

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

A T-neighbourhood containing {0} is {0} or Δ.

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

A T-neighbourhood containing {1} is {1} or Δ.

theorem Domain.Neighborhood.Exercise326.inter_in_zeroset {C C' : Set Example12.Token} (hc : C = Example12.master ∨ C = Example12.zero) (hc' : C' = Example12.master ∨ C' = Example12.zero) : C ∩ C' = Example12.master ∨ C ∩ C' = Example12.zero

theorem Domain.Neighborhood.Exercise326.inter_in_oneset {C C' : Set Example12.Token} (hc : C = Example12.master ∨ C = Example12.one) (hc' : C' = Example12.master ∨ C' = Example12.one) : C ∩ C' = Example12.master ∨ C ∩ C' = Example12.one

def Domain.Neighborhood.Exercise326.whichGuard {α : Type u_1} {β : Type u_2} (V₀ : NeighborhoodSystem α) (V₁ : NeighborhoodSystem β) (W : Set (Option (α ⊕ β))) (C : Set Example12.Token) : Prop

Scott's guard for which: the truth output is true ({0}/Δ) on a left copy 0X, false ({1}/Δ) on a right copy 1Y, and ⊥ (Δ) on the basepoint master.

Equations

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

theorem Domain.Neighborhood.Exercise326.whichGuard_left {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {W : Set (Option (α ⊕ β))} {C : Set Example12.Token} {X : Set α} (hg : whichGuard V₀ V₁ W C) (hW : W = inj₀ X) (hX : X.Nonempty) : C = Example12.master ∨ C = Example12.zero

theorem Domain.Neighborhood.Exercise326.whichGuard_right {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {W : Set (Option (α ⊕ β))} {C : Set Example12.Token} {Y : Set β} (hg : whichGuard V₀ V₁ W C) (hW : W = inj₁ Y) (hY : Y.Nonempty) : C = Example12.master ∨ C = Example12.one

theorem Domain.Neighborhood.Exercise326.whichGuard_masterC {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {W : Set (Option (α ⊕ β))} {C : Set Example12.Token} (hg : whichGuard V₀ V₁ W C) (hW : W = sumMaster V₀ V₁) : C = Example12.master

def Domain.Neighborhood.Exercise326.whichMap {α : Type u_1} {β : Type u_2} (V₀ : NeighborhoodSystem α) (V₁ : NeighborhoodSystem β) (h₀ : ∀ (X : Set α), V₀.mem X → X.Nonempty) (h₁ : ∀ (Y : Set β), V₁.mem Y → Y.Nonempty) : ApproximableMap (sum V₀ V₁ h₀ h₁) TD

Exercise 3.26 (Scott 1981, PRG-19). The discriminator which : D₀ + D₁ → T.

Equations

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

Membership facts and the composite identity.

theorem Domain.Neighborhood.Exercise326.not_sum_mem_empty {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {h₀ : ∀ (X : Set α), V₀.mem X → X.Nonempty} {h₁ : ∀ (Y : Set β), V₁.mem Y → Y.Nonempty} : ¬(sum V₀ V₁ h₀ h₁).mem ∅

∅ is never a sum-neighbourhood (every neighbourhood is non-empty).

theorem Domain.Neighborhood.Exercise326.which_mem_zero {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {h₀ : ∀ (X : Set α), V₀.mem X → X.Nonempty} {h₁ : ∀ (Y : Set β), V₁.mem Y → Y.Nonempty} {x : (sum V₀ V₁ h₀ h₁).Element} : ((whichMap V₀ V₁ h₀ h₁).toElementMap x).mem Example12.zero ↔ ∃ (X : Set α), V₀.mem X ∧ x.mem (inj₀ X)

which(x) selects true ({0} ∈ which x) exactly when x reaches into the left copy.

theorem Domain.Neighborhood.Exercise326.which_mem_one {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {h₀ : ∀ (X : Set α), V₀.mem X → X.Nonempty} {h₁ : ∀ (Y : Set β), V₁.mem Y → Y.Nonempty} {x : (sum V₀ V₁ h₀ h₁).Element} : ((whichMap V₀ V₁ h₀ h₁).toElementMap x).mem Example12.one ↔ ∃ (Y : Set β), V₁.mem Y ∧ x.mem (inj₁ Y)

which(x) selects false ({1} ∈ which x) exactly when x reaches into the right copy.

theorem Domain.Neighborhood.Exercise326.inMap₀_outMap₀_eq_of_left {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {h₀ : ∀ (X : Set α), V₀.mem X → X.Nonempty} {h₁ : ∀ (Y : Set β), V₁.mem Y → Y.Nonempty} {x : (sum V₀ V₁ h₀ h₁).Element} (hL : ∃ (X : Set α), V₀.mem X ∧ x.mem (inj₀ X)) : inMap₀.toElementMap (outMap₀.toElementMap x) = x

On a "left" element (one reaching into the left copy), the round-trip in₀ ∘ out₀ is the identity.

theorem Domain.Neighborhood.Exercise326.inMap₁_outMap₁_eq_of_right {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {h₀ : ∀ (X : Set α), V₀.mem X → X.Nonempty} {h₁ : ∀ (Y : Set β), V₁.mem Y → Y.Nonempty} {x : (sum V₀ V₁ h₀ h₁).Element} (hR : ∃ (Y : Set β), V₁.mem Y ∧ x.mem (inj₁ Y)) : inMap₁.toElementMap (outMap₁.toElementMap x) = x

On a "right" element, the round-trip in₁ ∘ out₁ is the identity.

theorem Domain.Neighborhood.Exercise326.sum_element_trichotomy {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {h₀ : ∀ (X : Set α), V₀.mem X → X.Nonempty} {h₁ : ∀ (Y : Set β), V₁.mem Y → Y.Nonempty} (x : (sum V₀ V₁ h₀ h₁).Element) : (∃ (X : Set α), V₀.mem X ∧ x.mem (inj₀ X)) ∨ (∃ (Y : Set β), V₁.mem Y ∧ x.mem (inj₁ Y)) ∨ ∀ (W : Set (Option (α ⊕ β))), x.mem W → W = (sum V₀ V₁ h₀ h₁).master

Trichotomy for a sum-element: it reaches the left copy, or the right copy, or is ⊥.

theorem Domain.Neighborhood.Exercise326.cond_which {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {h₀ : ∀ (X : Set α), V₀.mem X → X.Nonempty} {h₁ : ∀ (Y : Set β), V₁.mem Y → Y.Nonempty} (x : (sum V₀ V₁ h₀ h₁).Element) : (cond (sum V₀ V₁ h₀ h₁)).toElementMap (pair ((whichMap V₀ V₁ h₀ h₁).toElementMap x) (pair (inMap₀.toElementMap (outMap₀.toElementMap x)) (inMap₁.toElementMap (outMap₁.toElementMap x)))) = x

Exercise 3.26 (Scott 1981, PRG-19). Scott's identity for the discriminator: cond(which x, in₀(out₀ x), in₁(out₁ x)) = x for every x ∈ |D₀ + D₁|.