Lax Lean Archive

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

Lax979537.OrderedStructures

Finite ordered relational structures and queries

concepts/Lax979537/OrderedStructures.lean · lax-979537

definition

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

    Definition

    A finite relational vocabulary is a finite list of arities. An ordered structure of size nn has universe {0,…,n−1}\{0,\ldots,n-1\}, its usual strict order, and an interpretation of each relation symbol. This is the canonical representative of a finite linearly ordered structure up to isomorphism. The order is available to formulas as a distinguished atomic predicate.

    A pointed structure additionally carries a kk-tuple of elements. A kk-ary query is a property of these pointed structures; k=0k=0 gives Boolean queries. Empty universes and nullary relation symbols are allowed. The vocabulary and query arity are fixed independently of the input structure.

    Lean source view on GitHub

    1import Mathlib.Data.Fin.Tuple.Basic
    2import Mathlib.Data.List.FinRange
    3
    4/-!
    5---
    6title: Finite ordered relational structures and queries
    7type: definition
    8---
    9A finite relational vocabulary is a finite list of arities. An ordered
    10structure of size nn has universe {0,…,n−1}\{0,\ldots,n-1\}, its usual strict
    11order, and an interpretation of each relation symbol. This is the canonical
    12representative of a finite linearly ordered structure up to isomorphism.
    13The order is available to formulas as a distinguished atomic predicate.
    14
    15A pointed structure additionally carries a kk-tuple of elements. A kk-ary
    16query is a property of these pointed structures; k=0k=0 gives Boolean queries.
    17Empty universes and nullary relation symbols are allowed. The vocabulary and
    18query arity are fixed independently of the input structure.
    19-/
    20
    21namespace Lax979537.OrderedStructures
    22
    23abbrev Vocabulary := List Nat
    24
    25/-- Relation symbols are numbered in the order of the vocabulary. -/
    26abbrev Symbol (σ : Vocabulary) := Fin σ.length
    27
    28structure OrderedStructure (σ : Vocabulary) where
    29 size : Nat
    30 relation : (r : Symbol σ) → (Fin (σ.get r) → Fin size) → Bool
    31
    32structure PointedStructure (σ : Vocabulary) (k : Nat) where
    33 structureValue : OrderedStructure σ
    34 tuple : Fin k → Fin structureValue.size
    35
    36abbrev Query (σ : Vocabulary) (k : Nat) := PointedStructure σ k → Prop
    37
    38end Lax979537.OrderedStructures
    39

    Builds on

    none

    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…