BedrockClosing a code slot under its seven constructors
Read this chapter directly, or use the reading guide and dependency map to choose another route.
Reading guide · Dependency mapInside L, every formula is coded as an element of the carrier, and every formula has a key: the ordered pair of its arity numeral first and its code second. A slot at a bound collects the keys of a formula together with the keys of all its subformulas, so the slot is a tree of keys, and the bound is only an interface parameter of the lemmas about it. This chapter proves that the slot is closed: whenever the key of a compound formula lies in the slot, the keys of its immediate subformulas lie there as well, and this for the seven constructors that carry subformulas.
The abstract closure principles become concrete here: the keys generated by a formula's syntax tree satisfy closedAt. This is the exact closure premise needed to define a graph recursively over those keys.
Seven of the language's constructors carry subformulas; the other three do not, and for them there is nothing to close. Each of the seven clauses is four moves: invert a member of the slot back to the formula whose key it is, compute that formula's constructor from the clause's tag, put the parts' keys back into the compound's own slot, and carry them up to the slot of the whole.
Three mathematical objects organize the chapter. The key keyʟ χ of a formula χ of arity j is the ordered pair of the numeral j and the code of χ, where the code itself is the coding module's encoding LCode.⌜ χ ⌝. The slot slot B φ is a set of such keys, namely the keys of φ and of its whole subformula tree. And closedAt is the statement that a slot is closed under the seven constructors, conjunction, disjunction, implication, the two quantifiers, and the two bounded quantifiers.
{-# OPTIONS --cubical --safe --guardedness #-} open import Base.Prelude open import Base.Classical using ( LEM ) module L.Coding.SlotClosure {ℓ : Level} (lem : LEM (ℓ-suc ℓ)) where
Formulas are those of the object language, and their satisfaction is read in the constructible structure: the satisfaction symbol below always means satisfaction there. The ambient hierarchy supplies the underlying elements of which keys and slots are made.
open import FOL.ZFStructure using ( module hPropStructure ) open import FOL.Syntax using ( Term; Formula; _∧̇_; _∨̇_; _⇒̇_; ∃̇_; ∀̇_; ∀̇∈; ∃̇∈ ) import FOL.Absoluteness open import V.Hierarchy {ℓ} using ( 𝒮ᵥ )
Ordered pairs code the keys, with recoverable components, so a key can be taken apart into its arity component and its code component. The constructible structure carries the codes; the coding module defines the encoding ⌜_⌝ of formulas and the pair operation on codes; and the closure module states the seven closure clauses and their introduction forms, shape by shape.
open import V.Coding {ℓ} using ( pr; pr-inj ) open import L.Constructible {ℓ} using ( 𝒮ʟ; isL; isL-trans ) open import L.Coding.Model {ℓ} using ( module LCode; prʟ; prʟ-fst ) open import L.Coding.Closure {ℓ} using ( closedAt; binSameClosed-in; unSameClosed-in; unSuccClosed-in; binSuccClosed-in; binShapeAt; unShapeAt; bothSameAt; oneSameAt; oneSuccAt; succSndAt )
The satisfaction table chapter is the source of the three central objects. It defines the key keyʟ of a formula, the shape lemma keyʟ-shape that decomposes a formula by its constructor tag, the slot slot attached to a formula at a bound, the inversion slot-inv that returns a slot member to the formula it is a key of, and the parts lemmas Parts on the key tree.
open import L.Axioms.Numerals {ℓ} using ( numeralL; numeralL-fst ) open import L.Coding.SatisfactionTable {ℓ} lem using ( keyʟ; keyʟ-shape; slot; satTable; slot-inv; module Parts )
A slot member can be inverted only under propositional truncation, so every clause eliminates that truncation into a proposition. The binary same-arity case has a conjunction of two membership propositions; each unary or bounded case has one membership proposition.
import Cubical.HITs.PropositionalTruncation as PT open import Cubical.Foundations.HLevels using ( isProp× ) open import Cubical.HITs.CumulativeHierarchy.Base using ( V; _∈_ ) open import Cubical.HITs.CumulativeHierarchy.Constructions using ( module InfinitySet )
Arity is recorded by numerals, and the constructors that raise the arity record the successor of a numeral; both come from the ambient infinity set.
open InfinitySet using ( #_; sucV )
The carrier of the constructible structure is the type on which every code, key, and slot of the chapter lives.
open hPropStructure 𝒮ʟ
Here S ^ n denotes a length-n environment vector. The relation renamed to _⊨_ is satisfaction in the restricted constructible structure, evaluated under such an environment.
module AbsL = FOL.Absoluteness.Single 𝒮ᵥ isL isL-trans open AbsL using ( _^_ ) renaming ( _⊨ᵐ_ to _⊨_ )
Putting a part's key back
The key tree is governed by the parts lemmas. Parts.self says that a formula's own key lies in its own slot, and Parts.left, Parts.right, and Parts.only say that the slot of a compound contains the keys from the slots of its immediate parts: this is subtree inclusion along the constructor tree, supplied by the parts lemmas and the inversion, never by an ordering of the bound. The bound B travels through them only as an interface parameter. What a closure clause needs, therefore, is to recognize the pair it reads as a part's key; the two lemmas below do exactly that.
module _ (B : S) where private Sl : ∀ {n} → Formula S n → S Sl = slot B
The key computation, stated for a formula χ of arity j: any pair whose first component is the arity numeral # j and whose second component is the code component of ⌜ χ ⌝ equals the key fst (keyʟ χ). Note the three quantities are distinct: ⌜ χ ⌝ is the code of the formula, its first component is what enters the key, and the key is the ordered pair with the numeral in front.
key≡ : ∀ {j} (χ : Formula S j) (ar p : V ℓ) → # j ≡ ar → p ≡ fst LCode.⌜ χ ⌝ → pr ar p ≡ fst (keyʟ χ)
Both hypotheses are needed, the arity equation and the code-component equation, and the proof is a short chain through the two computation laws: the first component of the numeral of j is # j, and the first component of the coded pair is the pair of first components.
key≡ {j} χ ar p qa qp = cong₂ pr (sym qa) qp ∙ cong (λ w → pr w (fst LCode.⌜ χ ⌝)) (sym (numeralL-fst j)) ∙ sym (prʟ-fst (numeralL j) LCode.⌜ χ ⌝)
The raised form states the same for a formula χ of arity suc j: the key's first component is then the successor of the arity numeral, which is exactly what a clause reads when the constructor raises the arity.
keyS≡ : ∀ {j} (χ : Formula S (suc j)) (ar p : V ℓ) → # j ≡ ar → p ≡ fst LCode.⌜ χ ⌝ → pr (sucV ar) p ≡ fst (keyʟ χ)
The chain is the same, with the successor pushed through the arity equation: the numeral of suc j has first component suc (# j), and the clause's raised reading matches it.
keyS≡ {j} χ ar p qa qp = cong₂ pr (cong sucV (sym qa)) qp ∙ cong (λ w → pr w (fst LCode.⌜ χ ⌝)) (sym (numeralL-fst (suc j))) ∙ sym (prʟ-fst (numeralL (suc j)) LCode.⌜ χ ⌝)
The seven clauses
The clauses are organized by the shape of the closure each constructor demands. Four bodies are proved, one per shape: a binary constructor keeping the arity, a unary constructor keeping it, a unary constructor raising it, and a binary constructor pairing a term with a raised-arity formula. What changes between two clauses of the same body is the constructor's tag and which parts it hands back, and both are arguments. Each clause runs in four moves: invert the slot member into a formula, read off its constructor by the tag, put the parts' keys back into that formula's own slot, and carry them up to the slot of the whole.
module _ {n : ℕ} (φ : Formula S n) {k : ℕ} (γ : S ^ k) where private δ : S ^ (suc (suc (suc k))) δ = B ∷ satTable B φ ∷ Sl φ ∷ γ
The recursion whose closure is being proved is indexed by the slot of the fixed formula φ, and its environment carries three named entries: the bound, the satisfaction table at φ, and that slot. The remaining slots of the environment are left to the instance.
Ci : Fin (suc (suc (suc k)))
Ci = suc (suc zero)
The position Ci is the index of the slot inside this environment, and every clause reads the slot at exactly this position.
binSame : (k' : ℕ) (op : ∀ {m} → Formula S m → Formula S m → Formula S m)
→ (∀ {m} (ψ : Formula S m) → LCode.Match k' ψ
→ Σ[ a' ∈ Formula S m ] (Σ[ b' ∈ Formula S m ] (ψ ≡ op a' b')))
→ (∀ {m} (a' b' : Formula S m)
→ LCode.payOf (op a' b') ≡ prʟ LCode.⌜ a' ⌝ LCode.⌜ b' ⌝)
The first body covers a binary constructor that keeps the arity, the shape of conjunction, disjunction, and implication. Its hypotheses describe the tag k': a formula matches the tag exactly when it is op a' b' for two formulas of the same arity, and the payload of such a compound is the ordered pair of the two parts' codes.
→ (∀ {m} (a' b' : Formula S m) (z : V ℓ) → ⟨ z ∈ fst (Sl a') ⟩ → ⟨ z ∈ fst (Sl (op a' b')) ⟩) → (∀ {m} (a' b' : Formula S m) (z : V ℓ) → ⟨ z ∈ fst (Sl b') ⟩ → ⟨ z ∈ fst (Sl (op a' b')) ⟩) → ⟨ δ ⊨ binShapeAt Ci k' (bothSameAt Ci) ⟩
The two closure directions are the subtree inclusions from the parts lemmas, for the left and the right part respectively, and the conclusion is the clause itself: the slot is closed under the tag k' in the shape that returns both parts' keys.
binSame k' op get payOp inL inR = binSameClosed-in Ci k' δ (λ c ar a b c∈ sh → PT.rec (isProp× (snd (pr (fst ar) (fst a) ∈ fst (Sl φ))) (snd (pr (fst ar) (fst b) ∈ fst (Sl φ)))) (λ { (m , ψ , (q , incl)) →
The first move inverts a member c of the slot. It is, merely, the key of some formula ψ of arity m, and the inversion returns that key's membership in the slot of φ. The goal is a conjunction of two memberships, a proposition by isProp×, which is what licenses eliminating the truncation.
let r = keyʟ-shape ψ k' (fst ar) (pr (fst a) (fst b)) (sym q ∙ sh) g = get ψ (r .fst) a' = g .fst b' = g .snd .fst eψ = g .snd .snd
The second move computes the constructor. The shape lemma matches ψ against the tag k', returning the arity equation and the payload equation along with the match, and the decomposition hypothesis then writes ψ as op a' b' for two immediate subformulas.
pay = sym (prʟ-fst LCode.⌜ a' ⌝ LCode.⌜ b' ⌝) ∙ cong fst (sym (payOp a' b')) ∙ cong (λ w → fst (LCode.payOf w)) (sym eψ) ∙ r .snd .snd
The third move is the shared computation on the payload. The member c is a key-shaped pair whose payload component records the two parts' code components, and the chain proves that those recorded components are, componentwise, the codes ⌜ a' ⌝ and ⌜ b' ⌝: the payload of ψ is the pair of the two parts' codes by the constructor's own payload law, and the shape lemma's payload equation connects it to the pair read from c. Do not conflate the three quantities at play: the code ⌜ ψ ⌝ of the whole formula, the payload component inside it, and the final key, which carries the arity in its first slot.
inψ : (χ : Formula S m) → ⟨ fst (keyʟ χ) ∈ fst (Sl ψ) ⟩ → ⟨ fst (keyʟ χ) ∈ fst (Sl φ) ⟩ inψ χ h = incl (fst (keyʟ χ)) h in subst (λ w → ⟨ w ∈ fst (Sl φ) ⟩) (sym (key≡ a' (fst ar) (fst a) (r .snd .fst) (sym (pr-inj pay .fst))))
The fourth move carries keys back. A helper first lifts a key from the slot of any formula of arity m to the slot of φ, using the inclusion returned by the inversion. The arity equation from the shape lemma and the first component equality supplied by injectivity of the coding feed key≡, which rewrites the membership of the pair the clause reads into the membership of the key of a'.
(inψ a' (subst (λ w → ⟨ fst (keyʟ a') ∈ fst (Sl w) ⟩) (sym eψ) (inL a' b' _ (Parts.self B keyʟ a')))) , subst (λ w → ⟨ w ∈ fst (Sl φ) ⟩) (sym (key≡ b' (fst ar) (fst b) (r .snd .fst) (sym (pr-inj pay .snd))))
The right component repeats the assembly with the right closure direction and the second component equality supplied by the injectivity, rewriting to the membership of the pair with b'. The two halves close the clause.
(inψ b' (subst (λ w → ⟨ fst (keyʟ b') ∈ fst (Sl w) ⟩) (sym eψ) (inR a' b' _ (Parts.self B keyʟ b')))) }) (slot-inv B φ (fst c) c∈))
The elimination is fed by the inversion, which is where the inclusion came from. With both components assembled, the clause is proved.
andC : ⟨ δ ⊨ binShapeAt Ci 2 (bothSameAt Ci) ⟩
andC = binSame 2 _∧̇_ (λ _ m → m) (λ _ _ → refl)
(λ a' b' → Parts.left B keyʟ (a' ∧̇ b') a' b')
(λ a' b' → Parts.right B keyʟ (a' ∧̇ b') a' b')
Conjunction is the first instance: the slot of a' ∧̇ b' contains the slots' keys of both conjuncts.
orC : ⟨ δ ⊨ binShapeAt Ci 3 (bothSameAt Ci) ⟩
orC = binSame 3 _∨̇_ (λ _ m → m) (λ _ _ → refl)
(λ a' b' → Parts.left B keyʟ (a' ∨̇ b') a' b')
(λ a' b' → Parts.right B keyʟ (a' ∨̇ b') a' b')
Disjunction is the second instance with the same shape, its own tag and its own parts lemmas.
impC : ⟨ δ ⊨ binShapeAt Ci 4 (bothSameAt Ci) ⟩
impC = binSame 4 _⇒̇_ (λ _ m → m) (λ _ _ → refl)
(λ a' b' → Parts.left B keyʟ (a' ⇒̇ b') a' b')
(λ a' b' → Parts.right B keyʟ (a' ⇒̇ b') a' b')
Implication is the third: the slot of a' ⇒̇ b' contains the slots' keys of the antecedent and of the consequent, and the clause is proved by the same four moves.
unSame : (k' : ℕ) (op : ∀ {m} → Formula S m → Formula S m)
→ (∀ {m} (ψ : Formula S m) → LCode.Match k' ψ
→ Σ[ a' ∈ Formula S m ] (ψ ≡ op a'))
→ (∀ {m} (a' : Formula S m) → LCode.payOf (op a') ≡ LCode.⌜ a' ⌝)
The helper unSame proves the analogous closure principle for a hypothetical unary operation that preserves arity. None of the ten constructors in this language has that shape, so closedAt does not use this helper.
→ (∀ {m} (a' : Formula S m) (z : V ℓ) → ⟨ z ∈ fst (Sl a') ⟩ → ⟨ z ∈ fst (Sl (op a')) ⟩) → ⟨ δ ⊨ unShapeAt Ci k' (oneSameAt Ci) ⟩
The closure direction and the conclusion are the one-component shape: only the single subformula's key is demanded back.
unSame k' op get payOp inA = unSameClosed-in Ci k' δ (λ c ar a c∈ sh → PT.rec (snd (pr (fst ar) (fst a) ∈ fst (Sl φ))) (λ { (m , ψ , (q , incl)) → let r = keyʟ-shape ψ k' (fst ar) (fst a) (sym q ∙ sh) g = get ψ (r .fst)
The proof runs the same four moves with one component. The inversion produces ψ with its inclusion into the slot of φ, the shape lemma decomposes it by the tag, and the reading now involves only the arity and the single code.
a' = g .fst eψ = g .snd pay = cong fst (sym (payOp a')) ∙ cong (λ w → fst (LCode.payOf w)) (sym eψ) ∙ r .snd .snd in subst (λ w → ⟨ w ∈ fst (Sl φ) ⟩)
The shared computation is shorter here: the payload of op a' is the code of a' alone, so the chain identifies the code component recorded in the member c with the code component of a', with no pair to split.
(sym (key≡ a' (fst ar) (fst a) (r .snd .fst) (sym pay))) (incl (fst (keyʟ a')) (subst (λ w → ⟨ fst (keyʟ a') ∈ fst (Sl w) ⟩) (sym eψ) (inA a' _ (Parts.self B keyʟ a')))) }) (slot-inv B φ (fst c) c∈))
The fourth move assembles the case at once: the key of a' lies in its own slot, inA moves it into the slot of op a', incl lifts it to the slot of φ, and key≡ rewrites the membership the clause reads, the arity equation included.
unSucc : (k' : ℕ) (op : ∀ {m} → Formula S (suc m) → Formula S m)
→ (∀ {m} (ψ : Formula S m) → LCode.Match k' ψ
→ Σ[ a' ∈ Formula S (suc m) ] (ψ ≡ op a'))
→ (∀ {m} (a' : Formula S (suc m)) → LCode.payOf (op a') ≡ LCode.⌜ a' ⌝)
→ (∀ {m} (a' : Formula S (suc m)) (z : V ℓ)
The third body covers a unary constructor that raises the arity, the shape of the two quantifiers. The hypotheses are the raised counterparts: the tag matches exactly the formulas op a' built from a formula of the raised arity, the payload is that formula's code alone, and one closure direction passes its key into the compound's slot.
→ ⟨ z ∈ fst (Sl a') ⟩ → ⟨ z ∈ fst (Sl (op a')) ⟩) → ⟨ δ ⊨ unShapeAt Ci k' (oneSuccAt Ci) ⟩
The reading and the conclusion use the raised form: the clause reads the pair whose first component is the successor of the arity numeral, and demands the subformula's key back in the one-component shape.
unSucc k' op get payOp inA = unSuccClosed-in Ci k' δ (λ c ar a c∈ sh → PT.rec (snd (pr (sucV (fst ar)) (fst a) ∈ fst (Sl φ))) (λ { (m , ψ , (q , incl)) → let r = keyʟ-shape ψ k' (fst ar) (fst a) (sym q ∙ sh) g = get ψ (r .fst)
The first two moves are as before: invert the member into a formula, and decompose it by the tag into the single subformula of raised arity.
a' = g .fst eψ = g .snd pay = cong fst (sym (payOp a')) ∙ cong (λ w → fst (LCode.payOf w)) (sym eψ) ∙ r .snd .snd in subst (λ w → ⟨ w ∈ fst (Sl φ) ⟩)
The payload computation identifies the recorded code component with the subformula's code. Separately, the shape equation gives # m ≡ fst ar; the successor is introduced only when keyS≡ applies sucV to that equality.
(sym (keyS≡ a' (fst ar) (fst a) (r .snd .fst) (sym pay))) (incl (fst (keyʟ a')) (subst (λ w → ⟨ fst (keyʟ a') ∈ fst (Sl w) ⟩) (sym eψ) (inA a' _ (Parts.self B keyʟ a')))) }) (slot-inv B φ (fst c) c∈))
The rewriting goes through keyS≡: it applies sucV to # m ≡ fst ar, combines the result with the code-component equality, and thereby identifies the pair read by the clause with the key of a'.
binSucc : (k' : ℕ)
→ (op : ∀ {m} → Term S m → Formula S (suc m) → Formula S m)
→ (∀ {m} (ψ : Formula S m) → LCode.Match k' ψ
→ Σ[ t ∈ Term S m ] (Σ[ a' ∈ Formula S (suc m) ] (ψ ≡ op t a')))
→ (∀ {m} (t : Term S m) (a' : Formula S (suc m))
The fourth body covers the bounded quantifiers, whose constructors pair a term with a formula of raised arity. The payload of such a compound codes the term and the subformula in order, and only the subformula is itself a formula, so only its key is demanded back.
→ LCode.payOf (op t a') ≡ prʟ LCode.⌜ t ⌝ᵗ LCode.⌜ a' ⌝) → (∀ {m} (t : Term S m) (a' : Formula S (suc m)) (z : V ℓ) → ⟨ z ∈ fst (Sl a') ⟩ → ⟨ z ∈ fst (Sl (op t a')) ⟩) → ⟨ δ ⊨ binShapeAt Ci k' (succSndAt Ci) ⟩
The conclusion is the second-component shape: the clause reads the pair with the raised arity in front and the formula's code component behind, and asks for the subformula's key back.
binSucc k' op get payOp inA = binSuccClosed-in Ci k' δ (λ c ar a b c∈ sh → PT.rec (snd (pr (sucV (fst ar)) (fst b) ∈ fst (Sl φ))) (λ { (m , ψ , (q , incl)) → let r = keyʟ-shape ψ k' (fst ar) (pr (fst a) (fst b)) (sym q ∙ sh) g = get ψ (r .fst)
The member c is a key-shaped pair whose payload carries two components: the code component of the term t in front, and the code component of the subformula a' behind. The clause reads the raised arity together with the second component.
t = g .fst a' = g .snd .fst eψ = g .snd .snd pay = sym (prʟ-fst LCode.⌜ t ⌝ᵗ LCode.⌜ a' ⌝) ∙ cong fst (sym (payOp t a'))
The shared computation identifies the payload recorded in the member, componentwise, with the coded pair of ⌜ t ⌝ᵗ and ⌜ a' ⌝. The second component equality, supplied by the injectivity of the coding, is what the rewriting consumes; the term rides in the first component and drops out.
∙ cong (λ w → fst (LCode.payOf w)) (sym eψ) ∙ r .snd .snd in subst (λ w → ⟨ w ∈ fst (Sl φ) ⟩) (sym (keyS≡ a' (fst ar) (fst b) (r .snd .fst) (sym (pr-inj pay .snd)))) (incl (fst (keyʟ a'))
The rewriting by keyS≡ uses the arity equation and the second component equality, landing at the membership of the pair the clause reads. The fourth move then carries the key of a' up to the slot of φ through its own slot and the closure direction, and the inversion supplies the inclusion.
(subst (λ w → ⟨ fst (keyʟ a') ∈ fst (Sl w) ⟩) (sym eψ) (inA t a' _ (Parts.self B keyʟ a')))) }) (slot-inv B φ (fst c) c∈))
The two quantifiers instantiate the third body. Each supplies its tag, its decomposition, the payload equation, which is definitional, and the single closure direction: the slot of ∃̇ a' contains the slot's key of a', and likewise for the universal.
exC : ⟨ δ ⊨ unShapeAt Ci 6 (oneSuccAt Ci) ⟩
exC = unSucc 6 ∃̇_ (λ _ m → m) (λ _ → refl)
(λ a' → Parts.only B keyʟ (∃̇ a') a')
The universal quantifier is the second instance of the same body, with tag seven and its own parts lemma.
allC : ⟨ δ ⊨ unShapeAt Ci 7 (oneSuccAt Ci) ⟩
allC = unSucc 7 ∀̇_ (λ _ m → m) (λ _ → refl)
(λ a' → Parts.only B keyʟ (∀̇ a') a')
The two bounded quantifiers instantiate the fourth body with tags eight and nine: the slot of ∀̇∈ t a' contains the slot's key of a', and likewise for the existential bounded quantifier.
allInC : ⟨ δ ⊨ binShapeAt Ci 8 (succSndAt Ci) ⟩
allInC = binSucc 8 ∀̇∈ (λ _ m → m) (λ _ _ → refl)
(λ t a' → Parts.only B keyʟ (∀̇∈ t a') a')
The existential bounded quantifier is the last of the seven clauses.
exInC : ⟨ δ ⊨ binShapeAt Ci 9 (succSndAt Ci) ⟩
exInC = binSucc 9 ∃̇∈ (λ _ m → m) (λ _ _ → refl)
(λ t a' → Parts.only B keyʟ (∃̇∈ t a') a')
The seven clauses assemble into the closure statement closedAt: the slot of φ at the bound is closed under every constructor that carries subformulas. This discharges the hypothesis a recursion on codes states about its index set, and it is why such a recursion can appeal, at each compound code, to the values recorded at the keys of the immediate subformulas. The chapter's three objects have all played their parts: the key identified the pairs the clauses read, the slot tree supplied the closure directions, and closedAt gathered the results.
slotClosed : ⟨ δ ⊨ closedAt Ci ⟩
slotClosed = andC , (orC , (impC
, (exC , (allC , (allInC , exInC)))))