Encodings of structures as the tuple of their fields

enc_structure eS : S where f₁ : e₁, …, fₙ : eₙ declares the encoding of a structure as the framed tuple of its fields, with everything a certificate needs to work with it:

• eSFields, the encoding of the tuple, and eS, the encoding of the structure;
• eS_apply, unfolding eS to eSFields of the tuple;
• eS_fields_deg, the linear map from a structure to the tuple of its fields;
• for each field f, the linear rules eS_f_deg and eS_f_inO, eS_f_budget retaining a caller's workspace budget, and eS_f_polyTime reading the field of a polynomial-time structure;
• the constructor rules eS_mk_deg on tuples, eS_mk_inO adding up the bounds of its arguments, eS_mk_budget constructing a record whose fields share a workspace budget, and eS_mk_polyTime.

Public rules are registered as scoped fun_prop rules, activated by the declaration's namespace. Private rules are registered with local fun_prop in the defining scope and are not exported to importers. The optional public or private prefix sets the visibility of the encoding, tuple abbreviation and every generated rule. Without a prefix all are public, even outside a public section; private enc_structure keeps them private.

An applied structure type is also accepted: with variable {n : ℕ}, write enc_structure eS : S n where .... The parameter remains implicit in the generated declarations.

The fields f₁, …, fₙ must be the fields of S (as getStructureFields lists them, so a parent structure is the single field toParent), each once and in declaration order, since that order fixes the encoded words. S must be a structure, not a class. The command checks this before declaring anything, and names the first unknown, repeated or misplaced field, or all missing ones.

def Turing.MultiTapeTM.encStructure : Lean.ParserDescr

enc_structure eS : S where f₁ : e₁, f₂ : e₂ declares the encoding eS of the structure S as the tuple of its fields encoded by e₁, e₂, with its rules. List every field of S once, in declaration order; the command reports an unknown, repeated or misplaced field, or all missing ones. An optional public or private prefix applies to every generated declaration; the default is public, independently of the surrounding section. Public fun_prop rules are scoped; private ones are registered locally and do not export. Applied structure parameters are accepted, as in enc_structure eS : S n where ….

def Turing.MultiTapeTM.elabEncStructure : Lean.Elab.Command.CommandElab

Elaborate enc_structure: the encoding, its unfolding lemma and its rules.