Exercise 5.16 (Scott 1981, PRG-19, Lecture V) — neg, merge and d on C

Returning to Example 4.4 (the domain C of finite or infinite binary sequences), this module gives fixed-point/recursive definitions of three maps and verifies their characterizing equations:

• tail : C → C (tail(bx) = x, tail(Λ) = ⊥) — Scott's predecessor analogue, the item left to the reader in Example 4.4, built here with the head-test combinator Exercise419.liftC.
• neg : C → C with neg(0x) = 1·neg(x), neg(1x) = 0·neg(x) — bit-complement. We solve the recursion in closed form via liftC (neg(σ) = (flip σ), flip = List.map not), prove the recursion equations neg_cons_false/neg_cons_true (so it is the solution), and prove Scott's involution law neg(neg x) = x for all x ∈ |C| (negMap_negMap) — using that an approximable map is determined by its values on the finite elements σ⊥, σ (Exercise 2.8, eq_of_toElementMap_principal), so it suffices to check the two-fold complement on those, where it is flip ∘ flip = id.
• d : C → C (d(Λ) = Λ, d(0x) = 00·d(x), d(1x) = 11·d(x)) — the bit-doubling map of Example 4.4, again via liftC (d(σ) = double σ).
• merge : C × C → C with merge(εx, δy) = ε·δ·merge(x, y) — bit-interleaving. Built directly as an approximable map out of prod C C from an explicit interleave value function mergeVal. The boundary that Scott flags (merge(Λ, y) etc.) is resolved by the unique monotone convention (merge(Λ, y) = Λ, merge(εx, y) = ε⊥ once y runs out), the only choice compatible with approximability. We prove the recursion equation and merge(x, x) = d(x) (mergeMap_diag).

All data (tail, negMap, dMap, mergeMap) is choice-free (#print axioms ⊆ {propext, Quot.sound}); equalities of maps go through eq_of_toElementMap_principal (classical, exactly like the project's ext_of_toElementMap).

The Thue–Morse properties of t = 0·merge(neg t, tail t) (its digit-sum-mod-2 description and overlap-freeness) are real combinatorics-on-words and are left as a separate follow-up.

List helpers: bit-complement flip and bit-doubling double.

@[reducible, inline]

abbrev Domain.Neighborhood.Exercise516.flip (σ : ExampleB.Str) : ExampleB.Str

Complement every bit of a finite string.

Equations

• Domain.Neighborhood.Exercise516.flip σ = List.map not σ

@[simp]

theorem Domain.Neighborhood.Exercise516.flip_nil : flip [] = []

@[simp]

theorem Domain.Neighborhood.Exercise516.flip_cons (b : Bool) (σ : ExampleB.Str) : flip (b :: σ) = (!b) :: flip σ

theorem Domain.Neighborhood.Exercise516.flip_flip (σ : ExampleB.Str) : flip (flip σ) = σ

flip is an involution.

theorem Domain.Neighborhood.Exercise516.flip_prefix {σ τ : ExampleB.Str} (h : σ <+: τ) : flip σ <+: flip τ

flip preserves the prefix order.

def Domain.Neighborhood.Exercise516.double : ExampleB.Str → ExampleB.Str

Double every bit of a finite string: double (b :: σ) = b :: b :: double σ.

Equations

• Domain.Neighborhood.Exercise516.double [] = []
• Domain.Neighborhood.Exercise516.double (b :: σ) = b :: b :: Domain.Neighborhood.Exercise516.double σ

@[simp]

theorem Domain.Neighborhood.Exercise516.double_nil : double [] = []

@[simp]

theorem Domain.Neighborhood.Exercise516.double_cons (b : Bool) (σ : ExampleB.Str) : double (b :: σ) = b :: b :: double σ

theorem Domain.Neighborhood.Exercise516.double_append (σ τ : ExampleB.Str) : double (σ ++ τ) = double σ ++ double τ

double distributes over append.

theorem Domain.Neighborhood.Exercise516.double_prefix {σ τ : ExampleB.Str} (h : σ <+: τ) : double σ <+: double τ

double preserves the prefix order.

The approximation order on the finite elements σ⊥ and σ.

theorem Domain.Neighborhood.Exercise516.strBot_le_strBot_iff {σ τ : ExampleB.Str} : Example44.strBot σ ≤ Example44.strBot τ ↔ σ <+: τ

theorem Domain.Neighborhood.Exercise516.strBot_le_strElem_iff {σ τ : ExampleB.Str} : Example44.strBot σ ≤ Example44.strElem τ ↔ σ <+: τ

theorem Domain.Neighborhood.Exercise516.strElem_le_strElem_iff {σ τ : ExampleB.Str} : Example44.strElem σ ≤ Example44.strElem τ ↔ σ = τ

theorem Domain.Neighborhood.Exercise516.not_strElem_le_strBot {σ τ : ExampleB.Str} : ¬Example44.strElem σ ≤ Example44.strBot τ

theorem Domain.Neighborhood.Exercise516.tail_prefix {σ τ : ExampleB.Str} (h : σ <+: τ) : List.tail σ <+: List.tail τ

A prefix relation descends to tails.

Determination by finite elements: an equality criterion for maps C → V.

theorem Domain.Neighborhood.Exercise516.map_ext_C {β : Type u_1} {V : NeighborhoodSystem β} {f g : ApproximableMap Example44.C V} (hbot : ∀ (σ : ExampleB.Str), f.toElementMap (Example44.strBot σ) = g.toElementMap (Example44.strBot σ)) (helem : ∀ (σ : ExampleB.Str), f.toElementMap (Example44.strElem σ) = g.toElementMap (Example44.strElem σ)) : f = g

Two approximable maps out of C agree as soon as they agree on every finite element σ⊥ and σ (Exercise 2.8). This is the workhorse for the map equalities below.

tail : C → C — Scott's predecessor analogue (Example 4.4).

def Domain.Neighborhood.Exercise516.tailSing : ExampleB.Str → Example44.C.Element

The value of tail on a total element σ: tail(Λ) = ⊥, tail(bσ') = σ'.

Equations

• Domain.Neighborhood.Exercise516.tailSing [] = Domain.Neighborhood.Example44.strBot []
• Domain.Neighborhood.Exercise516.tailSing (b :: σ) = Domain.Neighborhood.Example44.strElem σ

theorem Domain.Neighborhood.Exercise516.tail_hcone {σ τ : ExampleB.Str} (h : σ <+: τ) : Example44.strBot (List.tail σ) ≤ Example44.strBot (List.tail τ)

theorem Domain.Neighborhood.Exercise516.tail_hsing {σ τ : ExampleB.Str} (h : σ <+: τ) : Example44.strBot (List.tail σ) ≤ tailSing τ

def Domain.Neighborhood.Exercise516.tailMap : ApproximableMap Example44.C Example44.C

Exercise 5.16 / Example 4.4 — tail : C → C. Built with the head-test combinator liftC: on σ⊥ it returns (tail σ)⊥, on σ the total tail σ (with tail Λ = ⊥).

Equations

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

@[simp]

theorem Domain.Neighborhood.Exercise516.tailMap_strBot (σ : ExampleB.Str) : tailMap.toElementMap (Example44.strBot σ) = Example44.strBot (List.tail σ)

@[simp]

theorem Domain.Neighborhood.Exercise516.tailMap_strElem (σ : ExampleB.Str) : tailMap.toElementMap (Example44.strElem σ) = tailSing σ

theorem Domain.Neighborhood.Exercise516.tailMap_consMap_strBot (b : Bool) (σ : ExampleB.Str) : tailMap.toElementMap ((Example44.consMap b).toElementMap (Example44.strBot σ)) = Example44.strBot σ

tail(b(σ⊥)) = σ⊥.

theorem Domain.Neighborhood.Exercise516.tailMap_consMap_strElem (b : Bool) (σ : ExampleB.Str) : tailMap.toElementMap ((Example44.consMap b).toElementMap (Example44.strElem σ)) = Example44.strElem σ

tail(b(σ)) = σ.

neg : C → C — bit complement, neg(0x)=1·neg(x), neg(1x)=0·neg(x).

theorem Domain.Neighborhood.Exercise516.neg_hcone {σ τ : ExampleB.Str} (h : σ <+: τ) : Example44.strBot (flip σ) ≤ Example44.strBot (flip τ)

theorem Domain.Neighborhood.Exercise516.neg_hsing {σ τ : ExampleB.Str} (h : σ <+: τ) : Example44.strBot (flip σ) ≤ Example44.strElem (flip τ)

def Domain.Neighborhood.Exercise516.negMap : ApproximableMap Example44.C Example44.C

Exercise 5.16 — neg : C → C. The closed-form solution of Scott's recursion, built with liftC: neg(σ⊥) = (flip σ)⊥ and neg(σ) = flip σ.

Equations

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

@[simp]

theorem Domain.Neighborhood.Exercise516.negMap_strBot (σ : ExampleB.Str) : negMap.toElementMap (Example44.strBot σ) = Example44.strBot (flip σ)

@[simp]

theorem Domain.Neighborhood.Exercise516.negMap_strElem (σ : ExampleB.Str) : negMap.toElementMap (Example44.strElem σ) = Example44.strElem (flip σ)

theorem Domain.Neighborhood.Exercise516.neg_cons_false : negMap.comp (Example44.consMap false) = (Example44.consMap true).comp negMap

Exercise 5.16 — the recursion for neg, case 0. neg(0·x) = 1·neg(x) as a map identity.

theorem Domain.Neighborhood.Exercise516.neg_cons_true : negMap.comp (Example44.consMap true) = (Example44.consMap false).comp negMap

Exercise 5.16 — the recursion for neg, case 1. neg(1·x) = 0·neg(x) as a map identity.

theorem Domain.Neighborhood.Exercise516.negMap_comp_negMap : negMap.comp negMap = ApproximableMap.idMap Example44.C

Exercise 5.16 (Scott 1981, PRG-19). neg ∘ neg = id as approximable maps: it suffices to check on the finite elements σ⊥, σ, where it is flip ∘ flip = id.

theorem Domain.Neighborhood.Exercise516.negMap_negMap (x : Example44.C.Element) : negMap.toElementMap (negMap.toElementMap x) = x

Exercise 5.16 (Scott 1981, PRG-19). neg(neg(x)) = x for all x ∈ |C|.

d : C → C — bit-doubling, d(Λ)=Λ, d(0x)=00·d(x), d(1x)=11·d(x).

theorem Domain.Neighborhood.Exercise516.d_hcone {σ τ : ExampleB.Str} (h : σ <+: τ) : Example44.strBot (double σ) ≤ Example44.strBot (double τ)

theorem Domain.Neighborhood.Exercise516.d_hsing {σ τ : ExampleB.Str} (h : σ <+: τ) : Example44.strBot (double σ) ≤ Example44.strElem (double τ)

def Domain.Neighborhood.Exercise516.dMap : ApproximableMap Example44.C Example44.C

Exercise 5.16 / Example 4.4 — d : C → C. The doubling map, closed form via liftC: d(σ⊥) = (double σ)⊥, d(σ) = double σ.

Equations

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

@[simp]

theorem Domain.Neighborhood.Exercise516.dMap_strBot (σ : ExampleB.Str) : dMap.toElementMap (Example44.strBot σ) = Example44.strBot (double σ)

@[simp]

theorem Domain.Neighborhood.Exercise516.dMap_strElem (σ : ExampleB.Str) : dMap.toElementMap (Example44.strElem σ) = Example44.strElem (double σ)

merge : C × C → C — bit interleaving.

The principal elements of C are tagged strings (b, σ): b = true is the total σ, b = false the partial σ⊥. We encode the corresponding neighbourhood (shape) and element (shapeElem), the partial order between them (SLe), and the interleaving value function mergeVal.

def Domain.Neighborhood.Exercise516.shape : Bool → ExampleB.Str → Set ExampleB.Str

The neighbourhood of the tagged string (b, σ): {σ} if total, cone σ if partial.

Equations

• Domain.Neighborhood.Exercise516.shape true x✝ = {x✝}
• Domain.Neighborhood.Exercise516.shape false x✝ = Domain.Neighborhood.ExampleB.cone x✝

theorem Domain.Neighborhood.Exercise516.memC_shape (b : Bool) (σ : ExampleB.Str) : Example44.memC (shape b σ)

def Domain.Neighborhood.Exercise516.shapeElem (b : Bool) (σ : ExampleB.Str) : Example44.C.Element

The element of the tagged string (b, σ): total σ if b, partial σ⊥ otherwise.

Equations

• Domain.Neighborhood.Exercise516.shapeElem b σ = Domain.Neighborhood.Example44.C.principal ⋯

@[simp]

theorem Domain.Neighborhood.Exercise516.shapeElem_true (σ : ExampleB.Str) : shapeElem true σ = Example44.strElem σ

@[simp]

theorem Domain.Neighborhood.Exercise516.shapeElem_false (σ : ExampleB.Str) : shapeElem false σ = Example44.strBot σ

theorem Domain.Neighborhood.Exercise516.shape_injective {b b' : Bool} {σ σ' : ExampleB.Str} : shape b σ = shape b' σ' → b = b' ∧ σ = σ'

def Domain.Neighborhood.Exercise516.SLe : Bool → ExampleB.Str → Bool → ExampleB.Str → Prop

The approximation order between tagged strings: (b, σ) ⊑ (b', σ'). A total string is maximal (only ⊑ itself); a partial string σ⊥ is ⊑ anything extending σ.

Equations

• Domain.Neighborhood.Exercise516.SLe true x✝² x✝¹ x✝ = (x✝¹ = true ∧ x✝² = x✝)
• Domain.Neighborhood.Exercise516.SLe false x✝² x✝¹ x✝ = (x✝² <+: x✝)

theorem Domain.Neighborhood.Exercise516.shapeElem_le_iff {b b' : Bool} {σ σ' : ExampleB.Str} : shapeElem b σ ≤ shapeElem b' σ' ↔ SLe b σ b' σ'

SLe characterizes the element order on shapeElem.

def Domain.Neighborhood.Exercise516.mergeVal : ExampleB.Str → Bool → ExampleB.Str → Bool → ExampleB.Str × Bool

The interleave value function: mergeVal σ b₀ τ b₁ returns the interleaving of the tagged strings (b₀, σ) and (b₁, τ) as a tagged string. Boundary convention (the only monotone one): merge(Λ, y) = Λ, merge(⊥, y) = ⊥, and merge(εx, y) = ε⊥ once y runs out.

Equations

• Domain.Neighborhood.Exercise516.mergeVal [] x✝² x✝¹ x✝ = ([], x✝²)
• Domain.Neighborhood.Exercise516.mergeVal (a :: tail) x✝¹ [] x✝ = ([a], false)
• Domain.Neighborhood.Exercise516.mergeVal (a :: σ) x✝¹ (b :: τ) x✝ = (a :: b :: (Domain.Neighborhood.Exercise516.mergeVal σ x✝¹ τ x✝).1, (Domain.Neighborhood.Exercise516.mergeVal σ x✝¹ τ x✝).2)

@[simp]

theorem Domain.Neighborhood.Exercise516.mergeVal_nil (b₀ : Bool) (τ : ExampleB.Str) (b₁ : Bool) : mergeVal [] b₀ τ b₁ = ([], b₀)

@[simp]

theorem Domain.Neighborhood.Exercise516.mergeVal_cons_nil (a : Bool) (σ : ExampleB.Str) (b₀ b₁ : Bool) : mergeVal (a :: σ) b₀ [] b₁ = ([a], false)

@[simp]

theorem Domain.Neighborhood.Exercise516.mergeVal_cons_cons (a : Bool) (σ : ExampleB.Str) (b₀ b : Bool) (τ : ExampleB.Str) (b₁ : Bool) : mergeVal (a :: σ) b₀ (b :: τ) b₁ = (a :: b :: (mergeVal σ b₀ τ b₁).1, (mergeVal σ b₀ τ b₁).2)

def Domain.Neighborhood.Exercise516.mergeElem (σ : ExampleB.Str) (b₀ : Bool) (τ : ExampleB.Str) (b₁ : Bool) : Example44.C.Element

The element produced by interleaving (b₀, σ) and (b₁, τ).

Equations

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

The monotonicity of mergeVal (the crux of approximability).

theorem Domain.Neighborhood.Exercise516.SLe_cons2 {p p' : Bool} {ρ ρ' : ExampleB.Str} (c d : Bool) (h : SLe p ρ p' ρ') : SLe p (c :: d :: ρ) p' (c :: d :: ρ')

Two equal head bits prepended preserve SLe.

theorem Domain.Neighborhood.Exercise516.SLe_cons_inv {b₀ b₀' a : Bool} {σ₀ σ' : ExampleB.Str} (h : SLe b₀ (a :: σ₀) b₀' σ') : ∃ (σ₀' : List Bool), σ' = a :: σ₀' ∧ SLe b₀ σ₀ b₀' σ₀'

Invert SLe on a cons in the first string: the second string starts with the same head.

theorem Domain.Neighborhood.Exercise516.mergeVal_SLe (σ : ExampleB.Str) (b₀ : Bool) (σ' : ExampleB.Str) (b₀' : Bool) (τ : ExampleB.Str) (b₁ : Bool) (τ' : ExampleB.Str) (b₁' : Bool) : SLe b₀ σ b₀' σ' → SLe b₁ τ b₁' τ' → SLe (mergeVal σ b₀ τ b₁).2 (mergeVal σ b₀ τ b₁).1 (mergeVal σ' b₀' τ' b₁').2 (mergeVal σ' b₀' τ' b₁').1

The monotonicity of interleaving. If (b₀, σ) ⊑ (b₀', σ') and (b₁, τ) ⊑ (b₁', τ') then the interleavings are ⊑-ordered. The crux that makes merge approximable.

theorem Domain.Neighborhood.Exercise516.mergeElem_mono {σ σ' τ τ' : ExampleB.Str} {b₀ b₀' b₁ b₁' : Bool} (h0 : shapeElem b₀ σ ≤ shapeElem b₀' σ') (h1 : shapeElem b₁ τ ≤ shapeElem b₁' τ') : mergeElem σ b₀ τ b₁ ≤ mergeElem σ' b₀' τ' b₁'

The element-order form of mergeVal_SLe.

theorem Domain.Neighborhood.Exercise516.mergeVal_diag (s : Bool) (σ : ExampleB.Str) : mergeVal σ s σ s = (double σ, s)

The diagonal value: interleaving (s, σ) with itself doubles.

theorem Domain.Neighborhood.Exercise516.mergeElem_diag (s : Bool) (σ : ExampleB.Str) : mergeElem σ s σ s = shapeElem s (double σ)

On the diagonal merge(⟨(s, σ), (s, σ)⟩) doubles σ.

A refinement lemma packaging both the representation and the order.

theorem Domain.Neighborhood.Exercise516.shape_refine {b : Bool} {σ : ExampleB.Str} {P : Set ExampleB.Str} (hP : Example44.memC P) (hsub : P ⊆ shape b σ) : ∃ (b' : Bool) (σ' : ExampleB.Str), P = shape b' σ' ∧ shapeElem b σ ≤ shapeElem b' σ'

The map merge.

def Domain.Neighborhood.Exercise516.mergeMap : ApproximableMap (prod Example44.C Example44.C) Example44.C

Exercise 5.16 (Scott 1981, PRG-19). The interleaving map merge : C × C → C with merge(εx, δy) = ε·δ·merge(x, y). Built directly as an approximable map: an input neighbourhood shape b₀ σ ∪ shape b₁ τ relates to the neighbourhoods of mergeElem σ b₀ τ b₁.

Equations

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

@[simp]

theorem Domain.Neighborhood.Exercise516.consMap_shapeElem (b c : Bool) (σ : ExampleB.Str) : (Example44.consMap b).toElementMap (shapeElem c σ) = shapeElem c (b :: σ)

consMap b shifts a tagged string: b·(c, σ) = (c, b :: σ).

theorem Domain.Neighborhood.Exercise516.mergeMap_pair (b₀ : Bool) (σ : ExampleB.Str) (b₁ : Bool) (τ : ExampleB.Str) : mergeMap.toElementMap (pair (shapeElem b₀ σ) (shapeElem b₁ τ)) = mergeElem σ b₀ τ b₁

The value of merge on a pair of finite elements. merge(⟨(b₀, σ), (b₁, τ)⟩) = mergeElem σ b₀ τ b₁. The analogue of liftC_strBot/liftC_strElem for the product.

Extensionality for maps C × C → C via finite element pairs.

theorem Domain.Neighborhood.Exercise516.memC_eq_shape {X : Set ExampleB.Str} (hX : Example44.memC X) : ∃ (b : Bool) (σ : ExampleB.Str), X = shape b σ

theorem Domain.Neighborhood.Exercise516.prod_principal_pair (b₀ : Bool) (σ : ExampleB.Str) (b₁ : Bool) (τ : ExampleB.Str) : (prod Example44.C Example44.C).principal ⋯ = pair (shapeElem b₀ σ) (shapeElem b₁ τ)

theorem Domain.Neighborhood.Exercise516.prodMap_ext {f g : ApproximableMap (prod Example44.C Example44.C) Example44.C} (h : ∀ (b₀ : Bool) (σ : ExampleB.Str) (b₁ : Bool) (τ : ExampleB.Str), f.toElementMap (pair (shapeElem b₀ σ) (shapeElem b₁ τ)) = g.toElementMap (pair (shapeElem b₀ σ) (shapeElem b₁ τ))) : f = g

Two maps C × C → C agree as soon as they agree on every pair of finite elements.

The recursion equation and merge(x, x) = d(x).

theorem Domain.Neighborhood.Exercise516.mergeMap_cons (ε δ : Bool) (x y : Example44.C.Element) : mergeMap.toElementMap (pair ((Example44.consMap ε).toElementMap x) ((Example44.consMap δ).toElementMap y)) = (Example44.consMap ε).toElementMap ((Example44.consMap δ).toElementMap (mergeMap.toElementMap (pair x y)))

Exercise 5.16 (Scott 1981, PRG-19). The defining recursion of merge: merge(εx, δy) = ε·δ·merge(x, y) for all x, y ∈ |C| and bits ε, δ.

theorem Domain.Neighborhood.Exercise516.mergeMap_diag (x : Example44.C.Element) : mergeMap.toElementMap (pair x x) = dMap.toElementMap x

Exercise 5.16 (Scott 1981, PRG-19). merge(x, x) = d(x) for all x ∈ |C| (the doubling map of Example 4.4).