Composing explicit workspace certificates

space proves a ComputableInSpace goal by the existing budget-preserving fun_prop rules. space [f, g] unfolds the indicated program definitions. Local routine certificates are reused; unproved size inequalities and iteration invariants are not guessed. An input-length side condition must be reflexive or supplied in the context. When the search fails, the fun_prop error ends with a note naming these inputs.

This tactic does not assert logarithmic space in the original input: the goal specifies the encoding and budget. In particular, a Savitch callback is linear-space in the stored state, while a separate invariant bounds that state's length by a quadratic logarithm.

During the search, space does not unfold a primitive encoding, a definition whose body is an embedding ⟨fun a => …, _⟩ into List Bool such as encPair, encList or encFinEnum. Definitions that merely name an encoding, such as encTuple := encPair … or encLab := encFinEnum Label, still unfold. Two different primitive encodings are therefore never unified by unfolding both: without this, matching encPair ?e₁ ?e₂ against encFinEnum (A × B) evaluates the enumeration of A × B until maximum recursion depth, and nested pair encodings fail exponentially slowly. Nor does it unfold decide, which would evaluate the decision procedure of a condition that a rule does not match. Side conditions are proved with the usual unfolding.

Conditions built from ∧, ∨ and ≤, and equalities through the canonical finite encoding (budget_decideAnd, budget_decideOr, budget_natLe, budget_decideEq_encFinite), are tried only when a first search without them fails: registered globally, each would be tried, and fail, on every decidable condition. A certificate that needs them pays for the failed first search, which on a long condition chain can cost several times a hand-written proof.

Main definitions

• space: compose certificates within the goal's explicit workspace budget.

def spaceDischarge : Lean.ParserDescr

The side-condition discharger of space: a hypothesis or a reflexive bound, proved with the usual unfolding. Internal to space.

def spaceTac : Lean.ParserDescr

Compose explicit space certificates, optionally unfolding the named program definitions.