Lax Lean Archive

While this submission is a draft, it cannot be used by other submissions.

The Personnel example

Lax392996.PersonnelExample · concepts/Lax392996/PersonnelExample.lean · lax-392996

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

    Example

    The running example of the paper: the relation Personnel\mathit{Personnel} of arity 4 with seven tuples, giving an id, a name, a position and a city (1, Juma, Director, Nairobi; 2, Paul, Janitor, Nairobi; 3, David, Analyst, Paris; 4, Ellen, Field agent, Beijing; 5, Aaheli, Double agent, Paris; 6, Nancy, HR, Paris; 7, Jing, Analyst, Beijing), the database II holding it, and the query asking for the cities where at least two persons work, qcity=ε(Π#4(Personnel⋈#4=#8∧#1<#5Personnel))q_{\mathrm{city}} = \varepsilon(\Pi_{\#4}(\mathit{Personnel} \bowtie_{\#4 = \#8 \wedge \#1 < \#5} \mathit{Personnel})), the join being a selection over a cross product. Values are strings, ordered as strings; the claim is Example 2, [ ⁣[qcity] ⁣]I={ ⁣∣(Nairobi),(Paris),(Beijing)∣ ⁣}[\![q_{\mathrm{city}}]\!]_I = \{\!|(\mathrm{Nairobi}), (\mathrm{Paris}), (\mathrm{Beijing})|\!\}.

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

    Each proof establishes this claim relative to its assumptions.

    In the paper

    • page 3 of this submission's paper

    Lean source view on GitHub

    1import Mathlib.Data.Fin.VecNotation
    2import Mathlib.Data.String.Basic
    3import Mathlib.Data.Multiset.Basic
    4import Lax392996.Databases
    5import Lax392996.RelationalAlgebra
    6import Lax392996.MultisetSemantics
    7
    8/-!
    9---
    10title: The Personnel example
    11type: example
    12---
    13The running example of the paper: the relation Personnel\mathit{Personnel} of
    14arity 4 with seven tuples, giving an id, a name, a position and a city
    15(1, Juma, Director, Nairobi; 2, Paul, Janitor, Nairobi; 3, David, Analyst,
    16Paris; 4, Ellen, Field agent, Beijing; 5, Aaheli, Double agent, Paris;
    176, Nancy, HR, Paris; 7, Jing, Analyst, Beijing), the database II holding
    18it, and the query asking for the cities where at least two persons work,
    19qcity=ε(Π#4(Personnel⋈#4=#8∧#1<#5Personnel))q_{\mathrm{city}} = \varepsilon(\Pi_{\#4}(\mathit{Personnel} \bowtie_{\#4 = \#8 \wedge \#1 < \#5} \mathit{Personnel}))
    20, the join being
    21a selection over a cross product. Values are strings, ordered as strings;
    22the claim is Example 2, [ ⁣[qcity] ⁣]I={ ⁣∣(Nairobi),(Paris),(Beijing)∣ ⁣}[\![q_{\mathrm{city}}]\!]_I = \{\!|(\mathrm{Nairobi}), (\mathrm{Paris}), (\mathrm{Beijing})|\!\}
    23.
    24-/
    25
    26namespace Lax392996.PersonnelExample
    27
    28open Lax392996.Databases Lax392996.RelationalAlgebra Lax392996.MultisetSemantics
    29
    30/-- Strings as values, ordered as strings; the arithmetic of terms, which
    31the example does not use, is trivial on them. -/
    32instance instValueTypeString : ValueType String where
    33 zero := ""
    34 add _ _ := ""
    35 sub _ _ := ""
    36 mul _ _ := ""
    37 add_comm _ _ := rfl
    38 add_assoc _ _ _ := rfl
    39
    40/-- The relation `Personnel` of the paper's Table 1: id, name, position, city. -/
    41def personnel : Relation String 4 := Multiset.ofList [
    42 !["1", "Juma", "Director", "Nairobi"],
    43 !["2", "Paul", "Janitor", "Nairobi"],
    44 !["3", "David", "Analyst", "Paris"],
    45 !["4", "Ellen", "Field agent", "Beijing"],
    46 !["5", "Aaheli", "Double agent", "Paris"],
    47 !["6", "Nancy", "HR", "Paris"],
    48 !["7", "Jing", "Analyst", "Beijing"]]
    49
    50/-- The database `I`, with its one relation. -/
    51def instanceI : Database String := [("Personnel", ⟨4, personnel⟩)]
    52
    53/-- The query `q_city`: the cities where at least two persons work, as
    54duplicate elimination of a projection of a selection over the cross
    55product of `Personnel` with itself. Attributes are numbered from 0 here,
    56from 1 in the paper. -/
    57def qcity : Query String 1 :=
    58 Query.Dedup (Query.Proj ![Term.index 3]
    59 (Query.Sel (Selection.And (Selection.BT (BoolTerm.EQ (Term.index 3) (Term.index 7)))
    60 (Selection.BT (BoolTerm.LT (Term.index 0) (Term.index 4))))
    61 (@Query.Prod _ 4 4 8 rfl (Query.Rel 4 "Personnel") (Query.Rel 4 "Personnel"))))
    62
    63/-- Example 2: the answer of `q_city` on `I`. -/
    64axiom qcity_answer :
    65 Query.evaluate qcity instanceI = Multiset.ofList [!["Nairobi"], !["Paris"], !["Beijing"]]
    66
    67end Lax392996.PersonnelExample
    68
    Show Proof
    Builds on
    Used by
    From Mathlib

    Discussion

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

    Loading discussion…