Lax Lean Archive

Draft — mutable and not usable as a dependency; its citation marks the draft state.

Lax58.StructuralCombinators

Certified structural presentation combinators

concepts/Lax58/StructuralCombinators.lean · lax-58

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.

    Concept map

    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

    Evidence

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

    1st statement lawful proven

    2nd statement Raw.constructor_eq_iff proven

    3rd statement sizeLaws proven

    Definition and theorem

    A small fixed vocabulary builds structural presentations from natural-number fields, products, and ordered lists. These are exactly the generic forms used by the current downstream ranked-tree development. Its laws show that the resulting representations round-trip and have exact constructor-derived sizes.

    The named constructor helper localizes the numerical realization of symbolic constructor names. Application-specific structurality is certified separately by equations describing each datatype constructor in terms of these fixed operations, without exposing numeric tags or binary-pair nesting.

    Lean source view on GitHub

    1import Mathlib.Data.Nat.Pairing
    2import Lax58.StructuralPresentation
    3
    4/-!
    5---
    6title: Certified structural presentation combinators
    7type: definition and theorem
    8---
    9
    10A small fixed vocabulary builds structural presentations from natural-number
    11fields, products, and ordered lists. These are exactly the generic forms used
    12by the current downstream ranked-tree development. Its laws show that the
    13resulting representations round-trip and have exact constructor-derived
    14sizes.
    15
    16The named constructor helper localizes the numerical realization of symbolic
    17constructor names. Application-specific structurality is certified separately
    18by equations describing each datatype constructor in terms of these fixed
    19operations, without exposing numeric tags or binary-pair nesting.
    20-/
    21
    22namespace Lax58.StructuralCombinators
    23
    24open Lax58.StructuralPresentation
    25open Lax58.StructuralPresentation.Presentation
    26
    27universe u v
    28
    29namespace Raw
    30
    31/-- An injective numerical realization of character lists, used only inside
    32the named-constructor combinator. -/
    33def constructorCharsCode : List Char → Nat
    34 | [] => 0
    35 | c :: cs => Nat.pair c.toNat (constructorCharsCode cs) + 1
    36
    37/-- The internal numerical realization of a symbolic constructor name. -/
    38def constructorNameCode (name : String) : Nat :=
    39 constructorCharsCode name.toList
    40
    41/-- Structural representation of an ordered list of already represented fields. -/
    42def fields : List StructuralPresentation.Raw → StructuralPresentation.Raw
    43 | [] => .nat 0
    44 | x :: xs => .pair x (fields xs)
    45
    46/-- A symbolically named constructor occurrence with ordered fields. -/
    47def constructor (name : String) (xs : List StructuralPresentation.Raw) :
    48 StructuralPresentation.Raw :=
    49 .pair (.nat (constructorNameCode name)) (fields xs)
    50
    51/-- Named constructors agree exactly when their names and ordered fields agree. -/
    52axiom constructor_eq_iff {name₁ name₂ : String}
    53 {xs₁ xs₂ : List StructuralPresentation.Raw} :
    54 constructor name₁ xs₁ = constructor name₂ xs₂ ↔ name₁ = name₂ ∧ xs₁ = xs₂
    55
    56end Raw
    57
    58/-- Structural presentation of natural numbers. -/
    59def nat : Presentation Nat where
    60 toRaw := .nat
    61 fromRaw
    62 | .nat n => some n
    63 | _ => none
    64
    65/-- Structural presentation of a product. -/
    66def prod {α : Type u} {β : Type v} (A : Presentation α) (B : Presentation β) :
    67 Presentation (α × β) where
    68 toRaw x := .pair (A.toRaw x.1) (B.toRaw x.2)
    69 fromRaw
    70 | .pair a b =>
    71 match A.fromRaw a with
    72 | none => none
    73 | some x =>
    74 match B.fromRaw b with
    75 | none => none
    76 | some y => some (x, y)
    77 | _ => none
    78
    79/-- Universal structural representation of a list. -/
    80def listToRaw {α : Type u} (P : Presentation α) : List α → StructuralPresentation.Raw
    81 | [] => .nat 0
    82 | x :: xs => .pair (P.toRaw x) (listToRaw P xs)
    83
    84/-- Partial inverse of `listToRaw`. -/
    85def listFromRaw {α : Type u} (P : Presentation α) : StructuralPresentation.Raw → Option (List α)
    86 | .nat 0 => some []
    87 | .pair x xs => do
    88 let x ← P.fromRaw x
    89 let xs ← listFromRaw P xs
    90 pure (x :: xs)
    91 | _ => none
    92
    93/-- Cons-list structural presentation. -/
    94def list {α : Type u} (P : Presentation α) : Presentation (List α) where
    95 toRaw := listToRaw P
    96 fromRaw := listFromRaw P
    97
    98/-- Round-trip laws for the fixed structural presentation vocabulary. -/
    99structure Lawful : Prop where
    100 nat : StructuralCombinators.nat.Lawful
    101 prod {α : Type u} {β : Type v} (A : Presentation α) (B : Presentation β) :
    102 A.Lawful → B.Lawful → (StructuralCombinators.prod A B).Lawful
    103 list {α : Type u} (P : Presentation α) : P.Lawful → (StructuralCombinators.list P).Lawful
    104
    105/-- Exact node-count equations for the fixed structural vocabulary. -/
    106structure SizeLaws : Prop where
    107 nat (n : Nat) : StructuralCombinators.nat.structuralSize n = 1
    108 prod {α : Type u} {β : Type v} (A : Presentation α) (B : Presentation β) (x : α) (y : β) :
    109 (StructuralCombinators.prod A B).structuralSize (x, y) =
    110 A.structuralSize x + B.structuralSize y + 1
    111 list {α : Type u} (P : Presentation α) (xs : List α) :
    112 (StructuralCombinators.list P).structuralSize xs =
    113 1 + xs.length + (xs.map P.structuralSize).sum
    114
    115axiom lawful : Lawful.{u, v}
    116
    117axiom sizeLaws : SizeLaws.{u, v}
    118
    119/-- Evidence that a presentation was obtained solely from the fixed primitive
    120and combinator vocabulary. Unlike an unconstrained presentation typeclass,
    121this witness cannot certify an advice-bearing encoder. -/
    122inductive Generated : {α : Type} → Presentation α → Prop
    123 | nat : Generated StructuralCombinators.nat
    124 | prod {α β : Type} {A : Presentation α} {B : Presentation β} :
    125 Generated A → Generated B → Generated (StructuralCombinators.prod A B)
    126 | list {α : Type} {P : Presentation α} :
    127 Generated P → Generated (StructuralCombinators.list P)
    128
    129/-- A type whose presentation can be synthesized from the fixed structural
    130vocabulary. The accompanying derivation, rather than mere typeclass
    131membership, is the no-advice certificate. -/
    132class Derivable (α : Type) where
    133 presentation : Presentation α
    134 generated : Generated presentation
    135
    136instance : Derivable Nat where
    137 presentation := nat
    138 generated := .nat
    139
    140instance {α β : Type} [A : Derivable α] [B : Derivable β] :
    141 Derivable (α × β) where
    142 presentation := prod A.presentation B.presentation
    143 generated := .prod A.generated B.generated
    144
    145instance {α : Type} [P : Derivable α] : Derivable (List α) where
    146 presentation := list P.presentation
    147 generated := .list P.generated
    148
    149/-- Presentation synthesized by recursively following the `Nat`, product,
    150and list structure of its type. -/
    151def derivedPresentation {α : Type} [P : Derivable α] : Presentation α :=
    152 P.presentation
    153
    154end Lax58.StructuralCombinators
    155
    Show ProofShow ProofShow Proof

    Builds on

    Used by

    From Mathlib

    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

    Loading discussion…