The document layer round trip

theorem at_filterMap_comm (g : String × Json → Option (String × Json))
    (hg : ∀ kv w, g kv = some w → w.1 = kv.1) (k : String) :
    ∀ kvs : List (String × Json), at_ k (kvs.filterMap g) = (at_ k kvs).filterMap g

Restricting to a key commutes with a map that keeps keys.

theorem sortKeys_cons_filter {kvs : List (String × Json)} (hl : keysSorted kvs = true)
    {k : String} {v : Json} (hk : look k kvs = some v) :
    sortKeys ((k, v) :: kvs.filter (fun kv => kv.1 != k)) = kvs

Putting back an entry that was filtered out of a canonical object restores it.

theorem declFields_back (caps : Caps) (K : Kind) :
    ∀ f ∈ declFields caps K, ∀ n v d, f.2 n v = some d → canonVal v = true →
      backDecl K d = some (n, v) ∧ declField K d.kind = some f.1

Every declaration a field’s picker produces belongs to that field, and stands for its entry.

theorem compBase_blocks_at (caps : Caps) (K : Kind) (name : String) {kvs : List (String × Json)}
    (hl : keysSorted kvs = true) (k : String) :
    at_ k (compBase caps K name kvs).blocks = match look k kvs with

The blocks of a component, key by key.

theorem declKv_compOf (caps : Caps) (root : List (String × Json)) (rt : List (String × List String)) (K : Kind) (name : String)
    {kvs : List (String × Json)} (hv : canonVal (.obj kvs) = true) (f : String × (String → Json → Option Decl))
    (hf : f ∈ declFields caps K)
    (hsep : ∀ g ∈ declFields caps K, ∀ d ∈ (splitOpt g.2 (look g.1 kvs)).1,
      (declField K d.kind == some f.1) = (g.1 == f.1)) :
    declKv K (compOf caps root rt K name kvs) f.1 = some (at_ f.1 kvs)

A declaration field is rebuilt from the declarations and the residue block.

theorem filter_flatMap_field (P : String → List MC) (hP : ∀ g, ∀ m ∈ P g, m.field = g) :
    ∀ L : List String, L.Nodup → ∀ f ∈ L, (L.flatMap P).filter (fun m => m.field == f) = P f

The entries of the parts for field f, among the parts of distinct fields.

theorem at_filterMap_field (Q : String → Option (String × Json))
    (hQ : ∀ g kv, Q g = some kv → kv.1 = g) :
    ∀ L : List String, L.Nodup → ∀ f ∈ L, at_ f (L.filterMap Q) = (Q f).toList

The blocks of the parts for field f, among the parts of distinct fields.

theorem mathKv_compOf (caps : Caps) (root : List (String × Json)) (rt : List (String × List String)) (K : Kind) (name : String)
    {kvs : List (String × Json)} (hl : keysSorted kvs = true) (f : String) (hf : f ∈ mathFields) :
    mathKv (compOf caps root rt K name kvs) f = some (at_ f kvs)

A math field is rebuilt from its entries or its block.

theorem templatesOf_mathOf {caps : Caps} {S : Sym} {v : Json} {ms : List MC}
    (h : mathOf caps S "expression_templates" v = some ms) :
    templatesOf (some v) = ms.filterMap Mx.head

The headers of the native template entries are the symbol-table entries of the expression_templates value.

theorem compTs_compOf (caps : Caps) (root : List (String × Json)) (rt : List (String × List String))
    (K : Kind) (name : String) (kvs : List (String × Json)) :
    compTs (compOf caps root rt K name kvs) = templatesOf (look "expression_templates" kvs)

The finished section’s templates are those its entries were decided under.

theorem symWith_compOf (caps : Caps) (root : List (String × Json)) (rt : List (String × List String))
    (K : Kind) (name : String) (kvs : List (String × Json)) :
    symWith root rt (compOf caps root rt K name kvs) (compTs (compOf caps root rt K name kvs)) =
      compSym root rt K caps name kvs

The table of a finished section is the one its entries were decided under.

theorem at_flatMap_at (k : String) (kvs : List (String × Json)) :
    ∀ L : List String, L.Nodup → at_ k (L.flatMap (fun f => at_ f kvs)) = if k ∈ L then at_ k kvs else []

Restricting a concatenation of restrictions to distinct keys.

theorem ofComp_compOf (caps : Caps) (root : List (String × Json)) (rt : List (String × List String)) (K : Kind) (name : String)
    {kvs : List (String × Json)} (hv : canonVal (.obj kvs) = true) :
    ofComp (compOf caps root rt K name kvs) = some (.obj kvs)

A component is rebuilt exactly from its section.

theorem meta_rebuild (caps : Caps) {mkvs : List (String × Json)} (hl : keysSorted mkvs = true) :
    sortKeys (mkvs.filter (fun kv => !(kv.1 == "description" &&
        (descOf caps (look "description" mkvs)).isSome)) ++
      optKv "description" ((descOf caps (look "description" mkvs)).map Json.str)) = mkvs

The metadata entries are rebuilt from the front matter and the description.

theorem compField_join (caps : Caps) {kvs : List (String × Json)}
    (hv : canonVal (.obj kvs) = true) (root : List (String × Json)) (rt : List (String × List String))
    (K : Kind) (f : String) :
    joinField backComp ((splitOpt (pickComp caps) (look f kvs)).1.map
        (fun p => compOf caps root rt K p.1 p.2)) (splitOpt (pickComp caps) (look f kvs)).2 =
      some (look f kvs)

A component field (models, reaction_systems) is rebuilt from its directives and its residue block.

theorem ofDoc_toDoc (caps : Caps) (d : Json) (hd : canonDoc d = true) :
    ofDoc (toDoc caps d) = some d

The document layer round trip. For every container (caps), a document in canonical form is rebuilt exactly from its skeleton.