Lax Lean Archive

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

The Personnel example, annotated

Lax392996.ProvenanceExample · concepts/Lax392996/ProvenanceExample.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 B[X]\mathcal{B}[X]-instance I^\hat I of the paper's Example 9, for X={t1,…,t7}X = \{t_1, \dots, t_7\}: the tuple with id ii of Personnel\mathit{Personnel} annotated by the variable tit_i. The annotated answer ⟨ ⁣⟨qcity⟩ ⁣⟩I^\langle\!\langle q_{\mathrm{city}} \rangle\!\rangle_{\hat I} has the three cities as data parts, and their annotations are the Boolean functions t1∧t2t_1 \wedge t_2 for Nairobi, (t3∧t5)∨(t5∧t6)∨(t3∧t6)(t_3 \wedge t_5) \vee (t_5 \wedge t_6) \vee (t_3 \wedge t_6) for Paris and t4∧t7t_4 \wedge t_7 for Beijing, the claims being stated pointwise on the valuations of XX. Variables are numbered from 0 here, from 1 in the paper.

    Concept map
    10 concepts; 1 descendant hidden
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A
    Evidence

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

    1 beijing_annotation proven

    2 data_answer proven

    3 nairobi_annotation proven

    4 paris_annotation proven

    In the paper

    • page 4 of this submission's paper

    Lean source view on GitHub

    1import Mathlib.Data.Fin.VecNotation
    2import Mathlib.Data.Prod.Lex
    3import Lax392996.SemiringsWithMonus
    4import Lax392996.BooleanFunctions
    5import Lax392996.Databases
    6import Lax392996.AnnotatedDatabases
    7import Lax392996.RelationalAlgebra
    8import Lax392996.AnnotatedSemantics
    9import Lax392996.ProbabilisticDatabases
    10import Lax392996.PersonnelExample
    11
    12/-!
    13---
    14title: The Personnel example, annotated
    15type: example
    16---
    17The B[X]\mathcal{B}[X]-instance I^\hat I of the paper's Example 9, for
    18X={t1,…,t7}X = \{t_1, \dots, t_7\}: the tuple with id ii of Personnel\mathit{Personnel}
    19annotated by the variable tit_i. The annotated answer
    20⟨ ⁣⟨qcity⟩ ⁣⟩I^\langle\!\langle q_{\mathrm{city}} \rangle\!\rangle_{\hat I} has the three
    21cities as data parts, and their annotations are the Boolean functions
    22t1∧t2t_1 \wedge t_2 for Nairobi, (t3∧t5)∨(t5∧t6)∨(t3∧t6)(t_3 \wedge t_5) \vee (t_5 \wedge t_6) \vee (t_3 \wedge t_6)
    23 for Paris and t4∧t7t_4 \wedge t_7 for Beijing, the claims
    24being stated pointwise on the valuations of XX. Variables are numbered
    25from 0 here, from 1 in the paper.
    26-/
    27
    28namespace Lax392996.ProvenanceExample
    29
    30open Lax392996.SemiringsWithMonus Lax392996.BooleanFunctions Lax392996.Databases
    31open Lax392996.AnnotatedDatabases Lax392996.RelationalAlgebra Lax392996.AnnotatedSemantics
    32open Lax392996.ProbabilisticDatabases Lax392996.PersonnelExample
    33
    34/-- The variable `t_i`, as the Boolean function reading it off a valuation. -/
    35def t (i : Fin 7) : BoolFunc (Fin 7) := fun ν => ν i
    36
    37/-- `Personnel` annotated: the tuple with id `i` carries `t_i`. -/
    38def personnelB : AnnotatedRelation String (BoolFunc (Fin 7)) 4 := Multiset.ofList [
    39 toLex (!["1", "Juma", "Director", "Nairobi"], t 0),
    40 toLex (!["2", "Paul", "Janitor", "Nairobi"], t 1),
    41 toLex (!["3", "David", "Analyst", "Paris"], t 2),
    42 toLex (!["4", "Ellen", "Field agent", "Beijing"], t 3),
    43 toLex (!["5", "Aaheli", "Double agent", "Paris"], t 4),
    44 toLex (!["6", "Nancy", "HR", "Paris"], t 5),
    45 toLex (!["7", "Jing", "Analyst", "Beijing"], t 6)]
    46
    47/-- The `B[X]`-instance `Î`. -/
    48def instanceB : AnnotatedDatabase String (BoolFunc (Fin 7)) := [("Personnel", ⟨4, personnelB⟩)]
    49
    50/-- Example 9, the data: the annotated answer has the three cities as data parts. -/
    51axiom data_answer : ∀ hq : qcity.source,
    52 Multiset.map Prod.fst (Query.evaluateAnnotated qcity hq instanceB)
    53 = Multiset.ofList [!["Nairobi"], !["Paris"], !["Beijing"]]
    54
    55/-- Example 9, Nairobi: annotated by `t_1 ∧ t_2`. -/
    56axiom nairobi_annotation : ∀ (hq : qcity.source) (ν : Fin 7 → Bool),
    57 tupleAnnotation (Query.evaluateAnnotated qcity hq instanceB) !["Nairobi"] ν = (ν 0 && ν 1)
    58
    59/-- Example 9, Paris: annotated by `(t_3 ∧ t_5) ∨ (t_5 ∧ t_6) ∨ (t_3 ∧ t_6)`. -/
    60axiom paris_annotation : ∀ (hq : qcity.source) (ν : Fin 7 → Bool),
    61 tupleAnnotation (Query.evaluateAnnotated qcity hq instanceB) !["Paris"] ν
    62 = ((ν 2 && ν 4) || (ν 4 && ν 5) || (ν 2 && ν 5))
    63
    64/-- Example 9, Beijing: annotated by `t_4 ∧ t_7`. -/
    65axiom beijing_annotation : ∀ (hq : qcity.source) (ν : Fin 7 → Bool),
    66 tupleAnnotation (Query.evaluateAnnotated qcity hq instanceB) !["Beijing"] ν = (ν 3 && ν 6)
    67
    68end Lax392996.ProvenanceExample
    69
    Show ProofShow ProofShow ProofShow 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…