Lax53.StructuralRepresentations
Certified structural representations for ranked-tree model checking
concepts/Lax53/StructuralRepresentations.lean · lax-53
No public endorsements yet.
Loading review…
Sign in with ORCIDConcept map
Evidence
This concept declares 4 statements. Each proof establishes one of them relative to its assumptions.
1st statement formula_structural proven
2nd statement sentence_lawful proven
3rd statement tree_lawful proven
4th statement tree_structural proven
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 vocabulary. Intrinsic formulas and ranked trees have datatype-specific first-class certificates covering every constructor and primitive field. Each invocation emits the encoder, its proposition, and its witness. For example, `#print formulaStructure.Laws` displays the full generated formula contract. Field resolution is closed and never consults instances.
These presentations contain no compiled automaton, semantic annotation, or other advice. Their distinguished word-memory realization is the generic construction. Any evaluator-specific representation engineering belongs only to the proof package and is charged there.
Lean source view on GitHub
| 1 | import Lax58.CertifiedDerivationElab |
| 2 | import Lax58.WordArena |
| 3 | import Lax53.ValueTranslations |
| 4 | |
| 5 | /-! |
| 6 | --- |
| 7 | title: Certified structural representations for ranked-tree model checking |
| 8 | type: definition and theorem |
| 9 | --- |
| 10 | |
| 11 | The finite automaton values used by the uniform evaluator have explicit |
| 12 | structural presentations. Product and list codes are built transitively from |
| 13 | the fixed `lax-58` vocabulary. Intrinsic formulas and ranked trees have |
| 14 | datatype-specific first-class certificates covering every constructor and |
| 15 | primitive field. Each `derive_certified_encoding` invocation emits the encoder, |
| 16 | its `.Laws` proposition, and its `.certified` witness. For example, |
| 17 | `#print formulaStructure.Laws` displays the full generated formula contract. |
| 18 | Field resolution is closed and never consults `FieldEncoding` instances. |
| 19 | |
| 20 | These presentations contain no compiled automaton, semantic annotation, or |
| 21 | other advice. Their distinguished word-memory realization is the generic |
| 22 | `Lax58.WordArena.encode` construction. Any evaluator-specific representation |
| 23 | engineering belongs only to the proof package and is charged there. |
| 24 | -/ |
| 25 | |
| 26 | namespace Lax53.StructuralRepresentations |
| 27 | |
| 28 | open FirstOrder |
| 29 | open FirstOrder.Language |
| 30 | open Lax52.MSOSyntax |
| 31 | open Lax53.RankedTree |
| 32 | open Lax53.TreeStructure |
| 33 | open Lax53.ValueTranslations |
| 34 | open Lax58.StructuralPresentation |
| 35 | open Lax58.StructuralPresentation.Presentation |
| 36 | open Lax58.StructuralCombinators |
| 37 | open Lax58.CertifiedDerivation |
| 38 | |
| 39 | universe u |
| 40 | |
| 41 | /-- Structural presentation of the complete finite automaton value. Its |
| 42 | components are derived automatically from the `Nat`, product, and ordered-list |
| 43 | structure of `EncodedAutomaton`. -/ |
| 44 | def automatonPresentation : Presentation EncodedAutomaton := |
| 45 | derivedPresentation |
| 46 | |
| 47 | /-- Structural representation of a term in the ranked-tree signature. That |
| 48 | signature has no function symbols, so every term is intrinsically a variable; |
| 49 | the impossible function case carries no represented data. -/ |
| 50 | derive_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 |
| 55 | signature. Subtype proofs in child indices are erased; their natural value is |
| 56 | the complete computational content of the field. -/ |
| 57 | derive_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 |
| 62 | Lax-52 formula syntax. Recursive occurrences are represented recursively and |
| 63 | finite term families are enumerated in their intrinsic order. This is not a |
| 64 | second formula datatype and performs no elaboration or semantic preprocessing. -/ |
| 65 | derive_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. -/ |
| 70 | noncomputable def sentencePresentation (alphabet : RankedAlphabetCode) : |
| 71 | Presentation (Lax52.MSOSyntax.Sentence |
| 72 | (treeSignature alphabet.toRankedAlphabet)) := |
| 73 | Lax58.StructuralPresentation.presentationOf (formulaStructure alphabet) |
| 74 | |
| 75 | /-- Constructor-structural map for a ranked tree over an encoded alphabet. -/ |
| 76 | derive_certified_encoding treeStructure (alphabet : RankedAlphabetCode) |
| 77 | indexed : Tree alphabet.toRankedAlphabet |
| 78 | |
| 79 | /-- Named structural presentation of ranked trees. -/ |
| 80 | noncomputable def treePresentation (alphabet : RankedAlphabetCode) : |
| 81 | Presentation (Tree alphabet.toRankedAlphabet) := |
| 82 | Lax58.StructuralPresentation.presentationOf (treeStructure alphabet) |
| 83 | |
| 84 | /-- The complete generated formula laws use only certified fields, including |
| 85 | the generated term and relation encodings. -/ |
| 86 | axiom formula_structural (alphabet : RankedAlphabetCode) : |
| 87 | ∀ {n m : Nat}, formulaStructure.Laws alphabet (n := n) (m := m) |
| 88 | |
| 89 | /-- The tree encoder agrees pointwise with the complete constructor fold |
| 90 | generated from the dependent ranked-tree datatype. -/ |
| 91 | axiom tree_structural (alphabet : RankedAlphabetCode) : |
| 92 | treeStructure.Laws alphabet |
| 93 | |
| 94 | /-- The recursive tree presentation is a genuine round-tripping |
| 95 | presentation. Advice-freedom is stated separately by `tree_structural`. -/ |
| 96 | axiom tree_lawful (alphabet : RankedAlphabetCode) : |
| 97 | (StructuralRepresentations.treePresentation alphabet).Lawful |
| 98 | |
| 99 | /-- The constructor-derived sentence representation is a genuine |
| 100 | round-tripping presentation. -/ |
| 101 | axiom sentence_lawful (alphabet : RankedAlphabetCode) : |
| 102 | (StructuralRepresentations.sentencePresentation alphabet).Lawful |
| 103 | |
| 104 | end Lax53.StructuralRepresentations |
| 105 |
From Mathlib
none
Community review
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above; your ORCID profile must share a public name.
0 comments