The drawn instance draws the intended code

The correctness of the drawing: the instance built by DescriptiveComplexity.codeProgInterp is well formed (DescriptiveComplexity.codeWF_codeProg) and its root draws

comp cP (pair (numeral card) (nest of the tables))

(DescriptiveComplexity.decodesTo_rootPt).

Everything is a walk of the input order, taken with the increasing enumeration DescriptiveComplexity.ordEnum of the universe: the numeral chain and each level of each table block are proved by the same downward induction, from the tail of the chain – the shared zero element – back to its head.

The subtree of the fixed code cP is the one place the induction is on a code rather than on the order: DescriptiveComplexity.decodesTo_subPos says that a drawing whose marks and children follow DescriptiveComplexity.subAt, DescriptiveComplexity.sub1 and DescriptiveComplexity.sub2 draws every subterm at its position, by structural induction on the code.

Drawing a fixed code

structure DescriptiveComplexity.Draws {N : Type} [FirstOrder.Language.code.Structure N] (c : Nat.Partrec.Code) (F : SubPos c → N) : Prop

A drawing of the syntax tree of a code: every position carries the mark of its subterm's constructor, and the child relations follow the positions of the children.

• mark (p : SubPos c) : Mark (tagOf (subAt c p)) (F p)

  Every position carries the mark of its subterm's constructor.

• arg1 (p q : SubPos c) : sub1 c p = some q → CArg1 (F p) (F q)

  The first-child relation follows the first child of a position.

• arg2 (p q : SubPos c) : sub2 c p = some q → CArg2 (F p) (F q)

  The second-child relation follows the second child of a position.

theorem DescriptiveComplexity.Draws.embed {N : Type} [FirstOrder.Language.code.Structure N] {c c' : Nat.Partrec.Code} {F : SubPos c → N} (h : Draws c F) (e : SubPos c' → SubPos c) (hsub : ∀ (q : SubPos c'), subAt c (e q) = subAt c' q) (h1e : ∀ (q : SubPos c'), sub1 c (e q) = Option.map e (sub1 c' q)) (h2e : ∀ (q : SubPos c'), sub2 c (e q) = Option.map e (sub2 c' q)) : Draws c' (F ∘ e)

A drawing restricts to a drawing of a subterm, along an embedding of positions that respects subterms and children.

theorem DescriptiveComplexity.decodesTo_subPos {N : Type} [FirstOrder.Language.code.Structure N] (c : Nat.Partrec.Code) (F : SubPos c → N) : Draws c F → ∀ (p : SubPos c), DecodesTo (F p) (subAt c p)

A drawing of a code draws every subterm at its position. The hypotheses are exactly what the defining formulas of the interpretation give for the tags of cP; the induction is on the code.

The increasing enumeration of a finite linear order

noncomputable def DescriptiveComplexity.ordEnum (A : Type) [LinearOrder A] [Finite A] : Fin (Nat.card A) ≃o A

The increasing enumeration of a finite linear order. Every chain of the drawing walks the order along it.

Equations

• DescriptiveComplexity.ordEnum A = monoEquivOfFin A ⋯

Uniqueness of the elements the guards pin down

The elements of the drawing

noncomputable def DescriptiveComplexity.botOrd (A : Type) [LinearOrder A] [Finite A] [Nonempty A] : A

The least element of the input order.

Equations

• DescriptiveComplexity.botOrd A = (DescriptiveComplexity.ordEnum A) ⟨0, ⋯⟩

noncomputable def DescriptiveComplexity.botTup {L : FirstOrder.Language} (V : L.FinVocab) (A : Type) [LinearOrder A] [Finite A] [Nonempty A] : Fin (dimOf V) → A

The canonically padded tuple every unindexed element of the drawing carries.

Equations

• DescriptiveComplexity.botTup V A x✝ = DescriptiveComplexity.botOrd A

theorem DescriptiveComplexity.canon_botTup {L : FirstOrder.Language} {V : L.FinVocab} {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (m : ℕ) : Canon m (botTup V A)

The two shared leaves

The chains of the blocks

theorem DescriptiveComplexity.canon_setCo {L : FirstOrder.Language} {V : L.FinVocab} {A : Type} [LinearOrder A] {m j : ℕ} (hj : j < m) (a : A) {u : Fin (dimOf V) → A} (h : Canon m u) : Canon m (setCo V j a u)

theorem DescriptiveComplexity.setCo_at {L : FirstOrder.Language} {V : L.FinVocab} {A : Type} (l : Fin (dimOf V)) (a : A) (t : Fin (dimOf V) → A) : setCo V (↑l) a t l = a

theorem DescriptiveComplexity.setCo_at_fz {L : FirstOrder.Language} {V : L.FinVocab} {A : Type} (a : A) (t : Fin (dimOf V) → A) : setCo V 0 a t (CodeProgRed.fz V) = a

theorem DescriptiveComplexity.setCo_bot_at {L : FirstOrder.Language} {V : L.FinVocab} {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (l : Fin (dimOf V)) {u : Fin (dimOf V) → A} (h : IsBot (u l)) : setCo V (↑l) (botOrd A) u = u

theorem DescriptiveComplexity.okOn_chainN {L : FirstOrder.Language} {V : L.FinVocab} {cP : Nat.Partrec.Code} {A : Type} [LinearOrder A] (i : Fin V.numSyms) (l : Fin (dimOf V)) (u : Fin (dimOf V) → A) : OkOn (ProgTag.chainN i l) u ↔ Canon (↑l + 1) u

The chain of the blocks of the symbols

The numeral chain

The whole instance

theorem DescriptiveComplexity.decodesTo_rootPt {L : FirstOrder.Language} {V : L.FinVocab} {A : Type} [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (cP : Nat.Partrec.Code) : DecodesTo (progPt ProgTag.root (botTup V A)) (cP.comp ((numCode (Nat.card A)).pair (codeNestFrom (blockCode V (Nat.card A) (⇑(ordEnum A)) (botTup V A)) 0)))

The root of the drawn instance draws the intended program: the fixed procedure cP, composed with the pair of the numeral of the universe size and the nest of the tables.

The drawing is well formed

theorem DescriptiveComplexity.progPt_congr {L : FirstOrder.Language} {V : L.FinVocab} {cP : Nat.Partrec.Code} {A : Type} {t t' : ProgTag V cP} {u u' : Fin (dimOf V) → A} (h : t = t') (h2 : u = u') : progPt t u = progPt t' u'

theorem DescriptiveComplexity.canon0_ext {L : FirstOrder.Language} {V : L.FinVocab} {A : Type} [LinearOrder A] {u u' : Fin (dimOf V) → A} (h : Canon 0 u) (h' : Canon 0 u') : u = u'

theorem DescriptiveComplexity.canon_one_bot {L : FirstOrder.Language} {V : L.FinVocab} {A : Type} [LinearOrder A] {u : Fin (dimOf V) → A} (h1 : Canon 1 u) (h0 : IsBot (u (CodeProgRed.fz V))) : Canon 0 u

theorem DescriptiveComplexity.okOn_numN {L : FirstOrder.Language} {V : L.FinVocab} {cP : Nat.Partrec.Code} {A : Type} [LinearOrder A] (u : Fin (dimOf V) → A) : OkOn ProgTag.numN u ↔ Canon 1 u

theorem DescriptiveComplexity.codeWF_codeProg {L : FirstOrder.Language} (V : L.FinVocab) (cP : Nat.Partrec.Code) (A : Type) [L.Structure A] [LinearOrder A] : CodeWF ((codeProgInterp V cP).Map A)

The drawn instance is well formed: at most one constructor mark per element and functional child relations, which is what makes what an element draws unique.