Lax Lean Archive

Certified structural representations for ranked-tree model checking

Lax842588.StructuralRepresentations · concepts/Lax842588/StructuralRepresentations.lean · lax-842588

proven

Loading review…

Community review

Flags

Each flag is tied to a public ORCID identity and explains why this concept may be incorrect.

No flags have been submitted.

    Community review

    Flag this concept

    State precisely what appears incorrect. This explanation will be public under your ORCID name.

    No source line selected.

    Natural Language Statement

    Definition and theorem

    The finite automaton values used by the uniform evaluator have explicit structural presentations. Product and list codes are built transitively from the fixed lax−58lax-58 vocabulary. Intrinsic formulas and ranked trees have datatype-specific first-class certificates covering every constructor and primitive field. Each derivecertifiedencodingderive_certified_encoding invocation emits the encoder, its .Laws.Laws proposition, and its .certified.certified witness. For example, #print formulaStructure.Laws displays the full generated formula contract. Field resolution is closed and never consults FieldEncodingFieldEncoding instances.

    These presentations contain no compiled automaton, semantic annotation, or other advice. Their distinguished word-memory realization is the generic Lax560851.WordArena.encodeLax560851.WordArena.encode construction. Any evaluator-specific representation engineering belongs only to the proof package and is charged there.

    Concept map
    12 concepts; 3 descendants hidden
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A
    Evidence

    This concept declares 2 statements. Each proof establishes one of them relative to its assumptions.

    1 sentence_lawful proven

    2 tree_lawful proven

    Lean source view on GitHub

    1import Lax560851.CertifiedDerivationElab
    2import Lax560851.WordArena
    3import Lax842588.ValueTranslations
    4
    5/-!
    6---
    7title: Certified structural representations for ranked-tree model checking
    8type: definition and theorem
    9---
    10
    11The finite automaton values used by the uniform evaluator have explicit
    12structural presentations. Product and list codes are built transitively from
    13the fixed `lax-58` vocabulary. Intrinsic formulas and ranked trees have
    14datatype-specific first-class certificates covering every constructor and
    15primitive field. Each `derive_certified_encoding` invocation emits the encoder,
    16its `.Laws` proposition, and its `.certified` witness. For example,
    17`#print formulaStructure.Laws` displays the full generated formula contract.
    18Field resolution is closed and never consults `FieldEncoding` instances.
    19
    20These presentations contain no compiled automaton, semantic annotation, or
    21other advice. Their distinguished word-memory realization is the generic
    22`Lax560851.WordArena.encode` construction. Any evaluator-specific representation
    23engineering belongs only to the proof package and is charged there.
    24-/
    25
    26namespace Lax842588.StructuralRepresentations
    27
    28open FirstOrder
    29open FirstOrder.Language
    30open Lax146103.MSOSyntax
    31open Lax842588.RankedTree
    32open Lax842588.TreeStructure
    33open Lax842588.ValueTranslations
    34open Lax560851.StructuralPresentation
    35open Lax560851.StructuralPresentation.Presentation
    36open Lax560851.StructuralCombinators
    37open Lax560851.CertifiedDerivation
    38
    39universe u
    40
    41/-- Structural presentation of the complete finite automaton value. Its
    42components are derived automatically from the `Nat`, product, and ordered-list
    43structure of `EncodedAutomaton`. -/
    44def automatonPresentation : Presentation EncodedAutomaton :=
    45 derivedPresentation
    46
    47/-- Structural representation of a term in the ranked-tree signature. That
    48signature has no function symbols, so every term is intrinsically a variable;
    49the impossible function case carries no represented data. -/
    50derive_certified_encoding termStructure (alphabet : RankedAlphabetCode)
    51 indexed {n : Nat} :
    52 (treeSignature alphabet.toRankedAlphabet).Term (Fin n)
    53
    54/-- Structural representation of a relation symbol in the ranked-tree
    55signature. Subtype proofs in child indices are erased; their natural value is
    56the complete computational content of the field. -/
    57derive_certified_encoding relationStructure (alphabet : RankedAlphabetCode)
    58 indexed {arity : Nat} :
    59 (treeSignature alphabet.toRankedAlphabet).Relations arity
    60
    61/-- Constructor-derived structural representation of the existing intrinsic
    62Lax-52 formula syntax. Recursive occurrences are represented recursively and
    63finite term families are enumerated in their intrinsic order. This is not a
    64second formula datatype and performs no elaboration or semantic preprocessing. -/
    65derive_certified_encoding formulaStructure (alphabet : RankedAlphabetCode)
    66 indexed {n m : Nat} :
    67 Formula (treeSignature alphabet.toRankedAlphabet) n m
    68
    69/-- Named structural presentation of intrinsically scoped MSO sentences. -/
    70noncomputable def sentencePresentation (alphabet : RankedAlphabetCode) :
    71 Presentation (Lax146103.MSOSyntax.Sentence
    72 (treeSignature alphabet.toRankedAlphabet)) :=
    73 Lax560851.StructuralPresentation.presentationOf (formulaStructure alphabet)
    74
    75/-- Constructor-structural map for a ranked tree over an encoded alphabet. -/
    76derive_certified_encoding treeStructure (alphabet : RankedAlphabetCode)
    77 indexed : Tree alphabet.toRankedAlphabet
    78
    79/-- Named structural presentation of ranked trees. -/
    80noncomputable def treePresentation (alphabet : RankedAlphabetCode) :
    81 Presentation (Tree alphabet.toRankedAlphabet) :=
    82 Lax560851.StructuralPresentation.presentationOf (treeStructure alphabet)
    83
    84/-- The recursive tree presentation is a genuine round-tripping
    85presentation. Constructor-structurality is supplied by the generated
    86`treeStructure.certified.checked` certificate. -/
    87axiom tree_lawful (alphabet : RankedAlphabetCode) :
    88 (StructuralRepresentations.treePresentation alphabet).Lawful
    89
    90/-- The constructor-derived sentence representation is a genuine
    91round-tripping presentation. -/
    92axiom sentence_lawful (alphabet : RankedAlphabetCode) :
    93 (StructuralRepresentations.sentencePresentation alphabet).Lawful
    94
    95end Lax842588.StructuralRepresentations
    96
    Show ProofShow Proof
    Builds on
    Used by
    From Mathlib

    none

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…