Constants by occurrence

Parameter abstraction needs a finite list of a formula's constants without assuming decidable equality on the constant domain. This chapter therefore counts and enumerates constant occurrences, preserving repetitions, and develops the index arithmetic that places their replacement variables after the existing free variables.

A formula's constants form an ordered list of occurrences. This chapter counts and enumerates them, supplies the index arithmetic used by abstraction, and handles the boundary case in which the list is empty.

Parameter abstraction rewrites a formula that mentions constants as a parameter-free formula of higher arity, together with the list of constants that the new variables will stand for. The construction needs that list to be finite, but it may not assume that equality on the constant domain is decidable, so it cannot merge or deduplicate entries. Two occurrences of the same constant therefore stay two separate positions, each later receiving its own replacement variable. The work divides into three steps: count the occurrences, enumerate them in order, and develop the index arithmetic that places the new variables after the existing free variables.

{-# OPTIONS --cubical --safe --guardedness #-}

module FOL.Manipulation.ConstantOccurrences where

open import Base.Prelude
open import FOL.Syntax using
  ( Term; con; var; Formula; _∈̇_; _≐_; _∧̇_; _∨̇_; _⇒̇_; ⊥̇; ∃̇_; ∀̇_; ∀̇∈; ∃̇∈ )

Concretely, a formula's constants are read off as an ordered list of occurrences: each time a constant appears, anywhere in a term or under any quantifier, it occupies the next position of the list. Counting and enumerating then go together. The count is a natural number recording how many occurrences there are; the enumeration is a vector of exactly that length, holding the constants in the order the formula mentions them. Because repetitions are preserved rather than resolved, no comparison between constants is ever performed. The chapter closes with the boundary case of an empty occurrence list, where the formula is shown to live over the empty constant alphabet.

open import FOL.Manipulation.ConstantMapping using ( mapTm; mapFo )
open import Cubical.Data.Nat using ( _+_; snotz )
open import Cubical.Data.Vec using ( _++_; map )
import Cubical.Data.Empty as Empty

Counting by occurrence

countTm and countFo count every constant occurrence, while constantsTm and constantsFo list those constants in the same order. Repeated occurrences of one constant therefore remain distinct positions.

The design point of the chapter is decided here, before any syntax moves. A formula's constants are counted by occurrence, not by value: a formula with k constant-occurrences yields a vector of length k, and two occurrences of the same constant are two entries of that vector, holding the same set twice.

A reader who expects the set of constants a formula mentions will look for the decidable equality that would let two occurrences of one constant be recognized as one, and will not find it. There is none to find: the constant domain is an arbitrary type, nothing obliges its equality to be decidable, and no decidable equality on the intended carrier is assumed. Counting by occurrence is what frees the whole chapter from that demand. The cost is an abstraction of higher arity than strictly necessary, in the form of variables that receive a value twice over, and nothing downstream can tell the difference: a vector of parameters is a vector of parameters.

The count is a structural recursion over the ten constructors, with a term's count as its input: a constant is one occurrence, a variable is none. Where a constructor has two parts, the counts add, left part first.

A small example fixes the convention. In ∀̇∈ (con a) ((con a) ∈̇ (var f0)), the bounded quantifier carries the term con a and the left side of the atom repeats con a, while the right side is a variable: there are two occurrences, both of the same constant, so the count must be two, read from left to right. Terms are counted first. A constant con c is one occurrence, a variable var i is none, and these are the only two term forms; nothing inspects the free-variable index. The two atomic relations then add the counts of their two terms, the left one written first, which is what makes the example's total come out in reading order. The enumeration will return [a, a], the same constant listed twice.

countTm : ∀ {ℓc} {K : Type ℓc} {n} → Term K n → ℕ
countTm (con c) = suc zero
countTm (var i) = zero

countFo : ∀ {ℓc} {K : Type ℓc} {n} → Formula K n → ℕ
countFo (t ∈̇ u)  = countTm t + countTm u

The propositional constructors divide by role rather than being read one by one. Those that combine branches, namely conjunction, disjunction and implication, add the counts of their two subformulas, again left first; falsum carries no terms and contributes zero. So the count of a whole formula is a sum over exactly those nodes that hold terms: at a binary node the two branch counts are added, and nowhere else does the number move.

countFo (t ≐ u)  = countTm t + countTm u
countFo (φ ∧̇ ψ)  = countFo φ + countFo ψ
countFo (φ ∨̇ ψ)  = countFo φ + countFo ψ
countFo (φ ⇒̇ ψ)  = countFo φ + countFo ψ
countFo ⊥̇        = zero

Quantifiers divide according to whether they carry a term. The unbounded ∃̇ and ∀̇ bind a variable and hold no constant, so they pass the body's count through unchanged; binding does not create occurrences. The bounded ∀̇∈ and ∃̇∈ do carry a term, as in the example above, so their count is countTm t added in front of the body's count. This keeps the left-to-right reading order that the enumeration will reproduce term for term.

countFo (∃̇ φ)    = countFo φ
countFo (∀̇ φ)    = countFo φ
countFo (∀̇∈ t φ) = countTm t + countFo φ
countFo (∃̇∈ t φ) = countTm t + countFo φ

Collecting is the same recursion written a second time, and it has to be a second recursion rather than one returning both: the length of the vector it returns is precisely what the first computes, so the count must already exist for the collection to be typeable at all. Every clause mirrors its counterpart above, with ++ where the count had +, so the constants come out in the order the formula mentions them, left to right.

The collection is bound to the count by one invariant: the recursion is dependent, and the result type Vec K (countTm t) demands that the returned vector's length be definitionally the term's own occurrence count, with the entries in left-to-right order. A constant yields the single-entry vector c ∷ [], a variable the empty vector; the formula case concatenates the two term vectors, left one first.

constantsTm : ∀ {ℓc} {K : Type ℓc} {n} (t : Term K n) → Vec K (countTm t)
constantsTm (con c) = c ∷ []
constantsTm (var i) = []

constantsFo : ∀ {ℓc} {K : Type ℓc} {n} (φ : Formula K n) → Vec K (countFo φ)
constantsFo (t ∈̇ u)  = constantsTm t ++ constantsTm u

The same invariant runs through the propositional constructors: each binary formula concatenates its two sublists at exactly the node where the count added its two summands, and falsum contributes the empty vector where the count contributed zero. Because concatenation replaces addition node for node, the length of the result computes to the count, with no separate bookkeeping.

constantsFo (t ≐ u)  = constantsTm t ++ constantsTm u
constantsFo (φ ∧̇ ψ)  = constantsFo φ ++ constantsFo ψ
constantsFo (φ ∨̇ ψ)  = constantsFo φ ++ constantsFo ψ
constantsFo (φ ⇒̇ ψ)  = constantsFo φ ++ constantsFo ψ
constantsFo ⊥̇        = []

The quantifier clauses close the recursion and settle the order: unbounded quantification passes the body's list through, while the bounded quantifiers prepend the term's list to the body's list, matching the reading order the count already used. For the example above the result is [a, a], of length the formula's count, and this vector is precisely the input that parameter abstraction will consume.

constantsFo (∃̇ φ)    = constantsFo φ
constantsFo (∀̇ φ)    = constantsFo φ
constantsFo (∀̇∈ t φ) = constantsTm t ++ constantsFo φ
constantsFo (∃̇∈ t φ) = constantsTm t ++ constantsFo φ

Placing the new parameter variables

Parameter abstraction extends an environment of arity n with k positions for constant occurrences. The original variables occupy the first n positions and the parameters the following k positions. The two index embeddings and their lookup laws show that both parts keep their values in the concatenated environment.

Two placements do the index arithmetic, and each is three lines. padRight b reads an index of the first a slots of a + b; padLeft a reads an index of the last b. They are one another's mirror, and the asymmetry in their arguments is the asymmetry of the recursion: padRight recurses on the index, padLeft on the number of slots it steps over.

A numeric example shows what the embeddings must do: with a = 2 and b = 3, an environment of five slots splits into the first two slots, holding the original variables, and the last three, holding the parameters. padRight embeds Fin a into Fin (a + b) by leaving the index where it is, since the first a slots of the concatenation are the original a: an index of the first half stays at the same position among five. The bound b is implicit and fixed throughout, so each recursive step just wraps the index in one more suc: zero stays zero, and suc i becomes suc (padRight b i).

padRight : ∀ {a} b → Fin a → Fin (a + b)
padRight b zero    = zero
padRight b (suc i) = suc (padRight b i)

padLeft : ∀ a {b} → Fin b → Fin (a + b)
padLeft zero    j = j

padLeft embeds Fin b into Fin (a + b) by shifting the index past the first a slots, so here the bound a is explicit and the recursion runs on it. In the example, padLeft 2 sends the parameter index 0 to position 2, the first slot after the original variables. When a is zero the concatenation is the second half and j already points correctly; each additional slot prepended adds one suc, placing the second half after the first.

padLeft (suc a) j = suc (padLeft a j)

Each placement comes with one law, and it is exactly the law an environment obeys: looking up a padded index in a concatenated vector is looking up the original index in the corresponding half. Alongside them stands a third law of the same shape, that lookup passes through map, and it is this law that lets the interpretation of the constants travel through the collected vector of occurrences. All three are proved by simultaneous structural recursion on the vector and the index, and each base or step case reduces to refl or to the induction hypothesis; no further equivalence machinery is involved.

The picture to keep in mind is an environment written as a concatenation p ++ q: p holds the values of the original free variables, q the values assigned to the constant occurrences. The two embeddings answer one and the same question, whether a lookup in the joined environment still finds the value it found before the join. For an original variable with index i : Fin a into the first half, the first law states lookup (padRight b i) (p ++ q) ≡ lookup i p: padRight b i names the same position inside the concatenation, so the entry read is unchanged.

lookup-padRight : ∀ {ℓa} {A : Type ℓa} {a b} (p : Vec A a) (q : Vec A b) (i : Fin a)
                → lookup (padRight b i) (p ++ q) ≡ lookup i p
lookup-padRight []      q ()
lookup-padRight (x ∷ p) q zero    = refl
lookup-padRight (x ∷ p) q (suc i) = lookup-padRight p q i

The second law covers a parameter with natural index j : Fin b into the second half: lookup (padLeft a j) (p ++ q) ≡ lookup j q, that is, the shifted index reads exactly the value lookup j q reads in q. Together the two laws say what an environment must say: each half of a concatenated environment keeps the value it had on its own. Both proofs descend through the vector and the index together, each step stripping one entry and one constructor until the base case is reached.

lookup-padLeft : ∀ {ℓa} {A : Type ℓa} a {b} (p : Vec A a) (q : Vec A b) (j : Fin b)
               → lookup (padLeft a j) (p ++ q) ≡ lookup j q
lookup-padLeft zero    []      q j = refl
lookup-padLeft (suc a) (x ∷ p) q j = lookup-padLeft a p q j

lookup-map : ∀ {ℓa ℓb} {A : Type ℓa} {B : Type ℓb} {n}

The third law concerns a relabelled vector: lookup j (map f v) ≡ f (lookup j v). Reading the mapped vector and then applying f is the same as applying f first. In parameter abstraction this is what lets the interpretation of the constants travel with the occurrences: if f assigns to each constant the value its replacement variable should carry, and v is the vector of occurrences collected from a formula, then looking up any position of map f v computes f of the constant at that position. The proof follows the same shape as the two placement laws, descending through the vector and the index together.

             (f : A → B) (v : Vec A n) (j : Fin n)
           → lookup j (map f v) ≡ f (lookup j v)
lookup-map f []      ()
lookup-map f (x ∷ v) zero    = refl
lookup-map f (x ∷ v) (suc j) = lookup-map f v j

Formulas with no constant occurrences

The counting and collecting machinery attaches a finite occurrence data to every formula. This section develops the boundary case of that interface: when the count is zero, no constant occurs anywhere in the formula, so every term it contains is a variable. Such a formula can be expressed over the empty constant alphabet ⊥*, that is, as a parameter-free formula of the same arity. The module ZeroOccurrences is parameterised by the original constant domain K and contains, first, the arithmetic that lets a proof of countFo φ ≡ 0 be split between the two sides of a sum, and then the two maps: erase, which removes the constant domain, and erase-inv, which shows that mapping back into K recovers the original formula exactly.

The boundary question of the occurrence interface is: what does a count of zero force about the syntax? The section answers it for an arbitrary constant type K, given a formula φ and a proof that its occurrence count is zero. Since nothing in the answer may depend on which type K is, and in particular nothing may use a decidable equality on K, the argument is developed once, uniformly for every such K at the level ℓ.

module ZeroOccurrences {ℓ : Level} (K : Type ℓ) where

The section formalises the boundary case. Its input is a formula φ together with a proof p : countFo φ ≡ 0; from p the construction first extracts, for each subterm and subformula, a proof that its own count is zero, and on that basis rebuilds the same syntax over the empty constant alphabet. The map eraseTm and erase go from K to ⊥*, and the maps eraseTm-inv and erase-inv show that relabelling along Empty.rec*, the eliminator that reads a constant out of the empty type, returns the original term or formula as a path. Together they say that over K, the formulas with no constant occurrences are exactly the images of parameter-free formulas, without any decidability assumption on K.

The first ingredient is arithmetical: a sum is zero only when both summands are. Since the count of a composite formula is always a sum of the counts of its parts, a proof of countFo φ ≡ 0 must split into zero-count proofs for the parts, and plus-zero-l and plus-zero-r perform exactly this split, extracting a ≡ 0 and b ≡ 0 from a + b ≡ 0. The split works because a nonzero left summand computes to a successor: suc a + b is suc (a + b), and the lemma snotz turns the equation of a successor with 0 into a contradiction, from which any conclusion follows. When the left summand is zero, zero + b computes to b, and the claims are immediate.

  plus-zero-l : {a b : ℕ} → a + b ≡  → a ≡ 
  plus-zero-l {zero} {b} p = refl
  plus-zero-l {suc a} {b} p = Empty.rec (snotz p)

  plus-zero-r : {a b : ℕ} → a + b ≡  → b ≡ 
  plus-zero-r {zero} {b} p = p

Count zero is a theorem about syntax: no constant constructor can occur. For terms this is outright. A term has count zero precisely when it is a variable, and eraseTm turns this into a map: from t together with p : countTm t ≡ 0 it produces a term over the empty alphabet ⊥* at the same arity n. The constant case is excluded because countTm (con a) computes to 1, making p a proof of suc _ ≡ 0; the contradiction supplies the required term. The variable case keeps the index, giving var i: free variables are untouched, the empty alphabet forbids only constants.

  plus-zero-r {suc a} {b} p = Empty.rec (snotz p)

  eraseTm : {n : ℕ} (t : Term K n) → countTm t ≡  → Term (⊥* {ℓ}) n
  eraseTm (con a) p = Empty.rec {A = Term (⊥* {ℓ}) _} (snotz p)
  eraseTm (var i) _ = var i

  erase : {n : ℕ} (φ : Formula K n) → countFo φ ≡  → Formula (⊥* {ℓ}) n

The same rebuild runs through the whole of erase, and the atoms show the pattern in its simplest form. For t ∈̇ u, the count is countTm t + countTm u, so plus-zero-l and plus-zero-r split p into zero-count proofs for t and u, and erase recurses on each side, rebuilding the relation over ⊥*. The equality atom ≐ behaves identically. Throughout, the arity n of free variables is never touched: erasing constants changes only the constant domain, not the free-variable structure.

  erase (t ∈̇ u) p = eraseTm t (plus-zero-l p) ∈̇ eraseTm u (plus-zero-r p)
  erase (t ≐ u) p = eraseTm t (plus-zero-l p) ≐ eraseTm u (plus-zero-r p)
  erase (φ ∧̇ ψ) p = erase φ (plus-zero-l p) ∧̇ erase ψ (plus-zero-r p)
  erase (φ ∨̇ ψ) p = erase φ (plus-zero-l p) ∨̇ erase ψ (plus-zero-r p)
  erase (φ ⇒̇ ψ) p = erase φ (plus-zero-l p) ⇒̇ erase ψ (plus-zero-r p)

One quantifier case shows how binding interacts with the count. For an unbounded quantifier such as ∃̇ φ, the count of the whole equals the count of the body, so the same p is carried into the recursive call and the result is ∃̇ applied to the erased body; falsum, with no parts and no occurrences, erases to itself. The bounded quantifiers ∀̇∈ and ∃̇∈ combine a term and a formula, and there the sum is split exactly as in the atomic cases, the term going through eraseTm and the body through a recursive erase. Every clause preserves the shape of the original formula, replacing only its constants.

  erase ⊥̇ _ = ⊥̇
  erase (∃̇ φ) p = ∃̇ erase φ p
  erase (∀̇ φ) p = ∀̇ erase φ p
  erase (∀̇∈ t φ) p = ∀̇∈ (eraseTm t (plus-zero-l p)) (erase φ (plus-zero-r p))
  erase (∃̇∈ t φ) p = ∃̇∈ (eraseTm t (plus-zero-l p)) (erase φ (plus-zero-r p))

The round trip is what makes the construction more than a translation: mapping back into K must return the original formula. The term-level statement eraseTm-inv comes first. If t has count zero, then relabelling eraseTm t p along Empty.rec* gives back t itself, as a path between terms over K. The relabelling function Empty.rec* : ⊥* → K is the eliminator of the empty type: asked to produce a constant of K, it demands an element of ⊥*, and since the erased term was built by eraseTm it contains no constant node, so the function is never actually applied. The induction then has only a contradictory case and a variable case, the latter closed by the computation rule of mapTm, which rebuilds var i from var i.

  eraseTm-inv : {n : ℕ} (t : Term K n) (p : countTm t ≡ )
              → mapTm Empty.rec* (eraseTm t p) ≡ t
  eraseTm-inv (con a) p = Empty.rec (snotz p)
  eraseTm-inv (var i) _ = refl

  erase-inv : {n : ℕ} (φ : Formula K n) (p : countFo φ ≡ )

At the formula level the inverse erase-inv is proved by structural induction over the syntax tree, combining the term-level inverse with itself recursively. The atoms display the base pattern with two subparts: since mapFo distributes the relabelling into the two erased terms, the goal is a path between two applications of the same constructor, and cong₂ lifts the pair of term-level paths eraseTm-inv t _ and eraseTm-inv u _ to that path. The zero-count proofs for the subterms come from plus-zero-l and plus-zero-r applied to p, exactly as in erase itself.

            → mapFo Empty.rec* (erase φ p) ≡ φ
  erase-inv (t ∈̇ u) p =
    cong₂ _∈̇_ (eraseTm-inv t (plus-zero-l p)) (eraseTm-inv u (plus-zero-r p))
  erase-inv (t ≐ u) p =
    cong₂ _≐_ (eraseTm-inv t (plus-zero-l p)) (eraseTm-inv u (plus-zero-r p))

Because erase preserves the shape of the formula at every node, the induction hypothesis available at each node already has exactly the form the inverse needs there. The three binary connectives repeat the two-subpart pattern: for ∧̇, ∨̇ and ⇒̇ the count of the whole splits between the two subformulas, and cong₂ lifts the pair of induction hypotheses to a path between the reconstructed connectives. The uniformity is structural rather than coincidental: the inverse law is a property of the syntax tree, checked one node at a time.

  erase-inv (φ ∧̇ ψ) p =
    cong₂ _∧̇_ (erase-inv φ (plus-zero-l p)) (erase-inv ψ (plus-zero-r p))
  erase-inv (φ ∨̇ ψ) p =
    cong₂ _∨̇_ (erase-inv φ (plus-zero-l p)) (erase-inv ψ (plus-zero-r p))
  erase-inv (φ ⇒̇ ψ) p =

Single-subpart nodes are correspondingly lighter. Falsum needs only refl, since both sides reduce to the constructor ⊥̇ itself. The two unbounded quantifiers use cong rather than cong₂, because they carry a single subformula: after the computation rule of mapFo unfolds, the goal is a path under ∃̇_, and cong ∃̇_ (erase-inv φ p) supplies exactly that, with the same p passed through unchanged.

    cong₂ _⇒̇_ (erase-inv φ (plus-zero-l p)) (erase-inv ψ (plus-zero-r p))
  erase-inv ⊥̇ _ = refl
  erase-inv (∃̇ φ) p = cong ∃̇_ (erase-inv φ p)
  erase-inv (∀̇ φ) p = cong ∀̇_ (erase-inv φ p)
  erase-inv (∀̇∈ t φ) p =

The bounded quantifiers close the induction, mixing a term and a formula just as the atoms did: cong₂ lifts the pair consisting of the term-level path eraseTm-inv t (plus-zero-l p) and the formula-level path erase-inv φ (plus-zero-r p). With this clause the theorem is complete. Every formula of count zero is the exact image, up to a path, of its erased parameter-free form, so the boundary case of the occurrence interface is fully accounted for: over K, the constant-free formulas are precisely the parameter-free ones, with no decidability assumption anywhere.

    cong₂ ∀̇∈ (eraseTm-inv t (plus-zero-l p)) (erase-inv φ (plus-zero-r p))
  erase-inv (∃̇∈ t φ) p =
    cong₂ ∃̇∈ (eraseTm-inv t (plus-zero-l p)) (erase-inv φ (plus-zero-r p))

Recap

Occurrences give a formula's constants a finite interface that never asks whether two symbols of the constant domain are equal. The count countFo indexes both the enumeration of the occurrences and, later, parameter abstraction, where each occurrence receives its own replacement variable; the placements and their lookup laws supply the resulting index arithmetic for concatenated environments. When the count is zero, ZeroOccurrences shows that the formula is the exact image of a parameter-free formula, so the empty constant domain can be adopted without losing any syntax.