Documentation

Provenance.HavingJoinCompositional

Compositional correctness of the JOIN rewriting for HAVING COUNT(*) #

Provenance.HavingQueryCorrectness proves the join-based rewriting of a HAVING COUNT(*) op (C+1) correct extensionally: per group key, the sum of the annotations of the join query's rows is the fused predicate provenance. This file upgrades that to an intensional, multiset-level equality, the form needed to substitute the rewriting for the fused operator inside an arbitrary surrounding query.

The one obstruction to multiset-level equality is the failing groups: the fused operator emits a 𝟘-annotated row for a group that fails the comparison, while the join query emits no row at all. The rewriting is therefore padded: joinCountQueryPadded adds to the join query the self-difference keysQuery q βˆ– keysQuery q – one 𝟘-annotated row per group key – and duplicate-eliminates the union, which merges everything into exactly one row per group key carrying the summed annotation. The result (joinCountQueryPadded_correct) is equal as a multiset of annotated tuples to the key projection of the fused HAVING output (proj_fused_eq_keyed), so the substitution is transparent to every surrounding operator – including annotation-sensitive ones like Diff and further HAVINGs, which are not congruences for the naive β€œequal up to 𝟘-rows” relation (a 𝟘-annotated row still changes the deterministic aggregate values of an enclosing group).

source
@[instance_reducible]
instance instMembershipAnnotatedTupleAnnotatedRelation {T K : Type} {n : β„•} :
Membership (AnnotatedTuple T K n) (AnnotatedRelation T K n)

AnnotatedRelation is an opaque def over Multiset, so instance search does not see the multiset membership through it; register it.

Equations
Dependency graph

The padded join query #

source
def keyIdx :
Tuple (Fin 3) 1

The canonical key selector of the (key, value, identifier) base schema.

Equations
Instances For
    Dependency graph
    source
    def keyTerm :
    Tuple (Term β„• 3) 1

    The key column, as a projection term.

    Equations
    Instances For
      Dependency graph
      source
      def keyOf {K : Type} (p : AnnotatedTuple β„• K 3) :
      Tuple β„• 1

      The group key of an annotated base row.

      Equations
      Instances For
        Dependency graph
        source
        def keysQuery (q : Query β„• 3) :
        Query β„• 1

        One row per distinct group key, annotated by the βŠ•-sum of the group's annotations.

        Equations
        Instances For
          Dependency graph
          source
          def zeroPadQuery (q : Query β„• 3) :
          Query β„• 1

          One 𝟘-annotated row per distinct group key: the self-difference of the key query (Ξ± βŠ– Ξ± = 𝟘).

          Equations
          Instances For
            Dependency graph
            source
            def keyPadded (Q : Query β„• 3 β†’ Query β„• 1) (q : Query β„• 3) :
            Query β„• 1

            Key padding of a one-column rewriting Q of a HAVING site over the base query q: Q, padded with a 𝟘-annotated row per group key of q and duplicate-eliminated into one row per group key.

            Equations
            Instances For
              Dependency graph
              source
              def joinCountQueryPadded (q : Query β„• 3) (op : CompOp) (C : β„•) :
              Query β„• 1

              The padded join-based rewriting of HAVING COUNT(*) op (C + 1): the join query, padded with a 𝟘-annotated row per group key and duplicate-eliminated into one row per group key.

              Equations
              Instances For
                Dependency graph
                source
                theorem keysQuery_source (q : Query β„• 3) (hq : q.source) :
                (keysQuery q).source
                Dependency graph
                source
                theorem zeroPadQuery_source (q : Query β„• 3) (hq : q.source) :
                (zeroPadQuery q).source
                Dependency graph
                source
                theorem keyPadded_source (Q : Query β„• 3 β†’ Query β„• 1) (q : Query β„• 3) (hQ : (Q q).source) (hq : q.source) :
                (keyPadded Q q).source
                Dependency graph
                source
                theorem joinCountQueryPadded_source (q : Query β„• 3) (hq : q.source) (op : CompOp) (C : β„•) :
                (joinCountQueryPadded q op C).source
                Dependency graph

                Key bookkeeping #

                source
                theorem joinChain_key_mem {K : Type} [CommSemiringWithMonus K] [DecidableEq K] (q : Query β„• 3) (hq : q.source) (d : AnnotatedDatabase β„• K) (C : β„•) (x : AnnotatedTuple β„• K (3 * C + 3)) :
                x ∈ (joinChain q C).evaluateAnnotated β‹― d β†’ βˆƒ p ∈ q.evaluateAnnotated hq d, x.1 ⟨0, β‹―βŸ© = p.1 ⟨0, β‹―βŸ©

                Every row of the join chain carries the key of some base row in its key coordinate.

                Dependency graph
                source
                theorem keyed_fst {K : Type} [CommSemiringWithMonus K] [DecidableEq K] (q : Query β„• 3) (hq : q.source) (d : AnnotatedDatabase β„• K) :
                Multiset.map Prod.fst ((Ξ  keyTerm q).evaluateAnnotated hq d) = Multiset.map keyOf (q.evaluateAnnotated hq d)

                The key multiset of the base query, through the key projection.

                Dependency graph
                source
                theorem joinChainQuery_key_mem {K : Type} [CommSemiringWithMonus K] [DecidableEq K] (q : Query β„• 3) (hq : q.source) (d : AnnotatedDatabase β„• K) (C : β„•) (x : AnnotatedTuple β„• K 1) (hx : x ∈ (joinChainQuery q C).evaluateAnnotated β‹― d) :
                x.1 ∈ (Multiset.map keyOf (q.evaluateAnnotated hq d)).dedup

                Every row of the chain-projected key query carries a key of the base query.

                Dependency graph
                source
                theorem diff_row_mem {K : Type} [CommSemiringWithMonus K] [DecidableEq K] (q₁ qβ‚‚ : Query β„• 1) (h₁ : q₁.source) (hd : (q₁ - qβ‚‚).source) (d : AnnotatedDatabase β„• K) (y : AnnotatedTuple β„• K 1) (hy : y ∈ (q₁ - qβ‚‚).evaluateAnnotated hd d) :
                βˆƒ z ∈ q₁.evaluateAnnotated h₁ d, y.1 = z.1

                Rows of a difference keep the data parts of its left argument.

                Dependency graph
                source
                theorem joinCountQuery_key_mem {K : Type} [CommSemiringWithMonus K] [DecidableEq K] (q : Query β„• 3) (hq : q.source) (d : AnnotatedDatabase β„• K) (op : CompOp) (C : β„•) (x : AnnotatedTuple β„• K 1) (hx : x ∈ (q.joinCountQuery op C).evaluateAnnotated β‹― d) :
                x.1 ∈ (Multiset.map keyOf (q.evaluateAnnotated hq d)).dedup

                Every row of the join-based query, for any comparison operator, carries a key of the base query.

                Dependency graph

                Evaluation of the padding #

                source
                theorem keysQuery_eval {K : Type} [CommSemiringWithMonus K] [DecidableEq K] (q : Query β„• 3) (hq : q.source) (d : AnnotatedDatabase β„• K) :
                (keysQuery q).evaluateAnnotated β‹― d = Multiset.map (fun (u : Tuple β„• 1) => (u, (Multiset.map Prod.snd (Multiset.filter (fun (p : AnnotatedTuple β„• K 1) => p.1 = u) ((Ξ  keyTerm q).evaluateAnnotated hq d))).sum)) (Multiset.map keyOf (q.evaluateAnnotated hq d)).dedup

                The key query evaluates to one row per distinct key with the summed annotation.

                Dependency graph
                source
                theorem zeroPadQuery_eval {K : Type} [CommSemiringWithMonus K] [DecidableEq K] (q : Query β„• 3) (hq : q.source) (d : AnnotatedDatabase β„• K) :
                (zeroPadQuery q).evaluateAnnotated β‹― d = Multiset.map (fun (u : Tuple β„• 1) => (u, 0)) (Multiset.map keyOf (q.evaluateAnnotated hq d)).dedup

                The padding query evaluates to one 𝟘-annotated row per distinct key.

                Dependency graph

                Site correctness: the padded rewriting, row for row #

                source
                theorem keyPadded_correct_of {K : Type} [CommSemiringWithMonus K] [DecidableEq K] (Q : Query β„• 3 β†’ Query β„• 1) (q : Query β„• 3) (hQ : (Q q).source) (hq : q.source) (d : AnnotatedDatabase β„• K) (F : Tuple β„• 1 β†’ K) (hkeys : βˆ€ x ∈ (Q q).evaluateAnnotated hQ d, x.1 ∈ (Multiset.map keyOf (q.evaluateAnnotated hq d)).dedup) (hkey : βˆ€ (u : Tuple β„• 1), (Multiset.map Prod.snd (Multiset.filter (fun (p : Tuple β„• 1 Γ— K) => p.1 = u) ((Q q).evaluateAnnotated hQ d))).sum = F u) :
                (keyPadded Q q).evaluateAnnotated β‹― d = Multiset.map (fun (g : Tuple β„• 1) => (g, F g)) (Multiset.map keyOf (q.evaluateAnnotated hq d)).dedup

                The padding argument, for any one-column rewriting Q whose rows carry keys of the base query: whenever Q q gives every group key u the annotation F u as a per-key annotation sum, the padded query evaluates to exactly one row per group key g of q, annotated F g. Instances: joinCountQueryPadded_correct_of for the COUNT(*) join rewritings, and the existential and compositional rewritings of Provenance.HavingMonotone.

                Dependency graph
                source
                theorem joinCountQueryPadded_correct_of {K : Type} [CommSemiringWithMonus K] [DecidableEq K] [HasAltLinearOrder K] (q : Query β„• 3) (hq : q.source) (d : AnnotatedDatabase β„• K) (ts : Tuple (Term β„• 3) 1) (op : CompOp) (C : β„•) (hkey : βˆ€ (u : Tuple β„• 1), (Multiset.map Prod.snd (Multiset.filter (fun (p : Tuple β„• 1 Γ— K) => p.1 = u) ((q.joinCountQuery op C).evaluateAnnotated β‹― d))).sum = Having.havingProv (Having.havingGroup keyIdx (q.evaluateAnnotated hq d) u) (ts 0) SeqAggFunc.count op (C + 1)) :
                (joinCountQueryPadded q op C).evaluateAnnotated β‹― d = Multiset.map (fun (g : Tuple β„• 1) => (g, Having.havingProv (Having.havingGroup keyIdx (q.evaluateAnnotated hq d) g) (ts 0) SeqAggFunc.count op (C + 1))) (Multiset.map keyOf (q.evaluateAnnotated hq d)).dedup

                The padding argument for the COUNT(*) join rewritings: whenever Query.joinCountQuery q op C gives every group key the fused predicate provenance as a per-key annotation sum, the padded query evaluates to exactly one row per group key carrying it. Both joinCountQueryPadded_correct and joinCountQueryPadded_monotone_correct are instances.

                Dependency graph
                source
                theorem joinCountQueryPadded_correct {K : Type} [CommSemiringWithMonus K] [DecidableEq K] [HasAltLinearOrder K] (h_abs : absorptive K) (h_distrib : mul_sub_left_distributive K) (q : Query β„• 3) (hq : q.source) (d : AnnotatedDatabase β„• K) (hnodup : (Multiset.map Prod.fst (q.evaluateAnnotated hq d)).Nodup) (ts : Tuple (Term β„• 3) 1) (op : CompOp) (C : β„•) :
                (joinCountQueryPadded q op C).evaluateAnnotated β‹― d = Multiset.map (fun (g : Tuple β„• 1) => (g, Having.havingProv (Having.havingGroup keyIdx (q.evaluateAnnotated hq d) g) (ts 0) SeqAggFunc.count op (C + 1))) (Multiset.map keyOf (q.evaluateAnnotated hq d)).dedup

                Multiset-level correctness of the padded JOIN rewriting. In an absorptive commutative m-semiring whose βŠ— distributes over βŠ–, the padded join-based query evaluates to exactly – row for row, annotation for annotation – one row per group key of the base query, annotated with the fused COUNT(*) op (C + 1) predicate provenance. The sole hypothesis is the injective per-group occurrence identifiers (global row-distinctness of the base query's output).

                Dependency graph
                source
                theorem joinCountQueryPadded_monotone_correct {K : Type} [CommSemiringWithMonus K] [DecidableEq K] [HasAltLinearOrder K] (h_abs : absorptive K) (q : Query β„• 3) (hq : q.source) (d : AnnotatedDatabase β„• K) (hnodup : (Multiset.map Prod.fst (q.evaluateAnnotated hq d)).Nodup) (ts : Tuple (Term β„• 3) 1) (op : CompOp) (hop : op = CompOp.ge ∨ op = CompOp.gt) (C : β„•) :
                (joinCountQueryPadded q op C).evaluateAnnotated β‹― d = Multiset.map (fun (g : Tuple β„• 1) => (g, Having.havingProv (Having.havingGroup keyIdx (q.evaluateAnnotated hq d) g) (ts 0) SeqAggFunc.count op (C + 1))) (Multiset.map keyOf (q.evaluateAnnotated hq d)).dedup

                Padded rewriting of the monotone comparisons, without distributivity. For op ∈ {β‰₯, >}, joinCountQueryPadded_correct holds in every absorptive commutative m-semiring (Query.joinCount_monotone_correct).

                Dependency graph
                source
                theorem fused_key_proj_gen {K : Type} [CommSemiringWithMonus K] [DecidableEq K] [HasAltLinearOrder K] (qg : AggQuery β„• 3 (ColKind.allReg 3)) (q : Query β„• 3) (hq : q.source) (d : AnnotatedDatabase β„• K) (hin : qg.evaluateAnnotated d = q.evaluateAnnotated hq d) (ts' : Tuple (Term β„• 3) 1) (fs : Tuple (SeqAggFunc β„•) 1) (op : CompOp) (s : Term β„• 1) :
                Multiset.map (fun (p : AnnotatedTuple β„• K (1 + 1)) => (fun (x : Fin 1) => p.1 ⟨0, β‹―βŸ©, p.2)) ((AggQuery.havingSite keyIdx ts' fs op 0 s qg).evaluateAnnotated d) = Multiset.map (fun (g : Tuple β„• 1) => (g, Having.havingProv (Having.havingGroup keyIdx (q.evaluateAnnotated hq d) g) (ts' 0) (fs 0) op (s.eval g))) (Multiset.map keyOf (q.evaluateAnnotated hq d)).dedup

                The key-projected fused output. Projecting the output of a fused HAVING f(t) op s site to its group key yields one row per group key of the base query, annotated with the predicate provenance of its group: the shape the padded rewritings evaluate to (keyPadded_correct_of), so that a padded rewriting can be substituted for the key-projected fused operator inside any surrounding query.

                Dependency graph
                source
                theorem fused_key_proj {K : Type} [CommSemiringWithMonus K] [DecidableEq K] [HasAltLinearOrder K] (qg : AggQuery β„• 3 (ColKind.allReg 3)) (q : Query β„• 3) (hq : q.source) (d : AnnotatedDatabase β„• K) (hin : qg.evaluateAnnotated d = q.evaluateAnnotated hq d) (ts' : Tuple (Term β„• 3) 1) (op : CompOp) (C : β„•) :
                Multiset.map (fun (p : AnnotatedTuple β„• K (1 + 1)) => (fun (x : Fin 1) => p.1 ⟨0, β‹―βŸ©, p.2)) ((AggQuery.havingSite keyIdx ts' (fun (x : Fin 1) => SeqAggFunc.count) op 0 (Term.const (C + 1)) qg).evaluateAnnotated d) = Multiset.map (fun (g : Tuple β„• 1) => (g, Having.havingProv (Having.havingGroup keyIdx (q.evaluateAnnotated hq d) g) (ts' 0) SeqAggFunc.count op (C + 1))) (Multiset.map keyOf (q.evaluateAnnotated hq d)).dedup

                The COUNT(*) op (C + 1) instance of fused_key_proj_gen.

                Dependency graph
                source
                theorem countHaving_site_rewrite {K : Type} [CommSemiringWithMonus K] [DecidableEq K] [HasAltLinearOrder K] (h_abs : absorptive K) (h_distrib : mul_sub_left_distributive K) (q : Query β„• 3) (hq : q.source) (d : AnnotatedDatabase β„• K) (hnodup : (Multiset.map Prod.fst (q.evaluateAnnotated hq d)).Nodup) (ts' : Tuple (Term β„• 3) 1) (op : CompOp) (C : β„•) :
                Multiset.map (fun (p : AnnotatedTuple β„• K (1 + 1)) => (fun (x : Fin 1) => p.1 ⟨0, β‹―βŸ©, p.2)) ((AggQuery.havingSite keyIdx ts' (fun (x : Fin 1) => SeqAggFunc.count) op 0 (Term.const (C + 1)) (q.toAgg hq)).evaluateAnnotated d) = (joinCountQueryPadded q op C).evaluateAnnotated β‹― d

                Site substitution. The key-projected fused HAVING COUNT(*) op (C + 1) site over the embedded classical query and the padded join-based rewriting evaluate to the same multiset of annotated tuples: substituting one for the other inside any surrounding query preserves the annotated semantics verbatim.

                Dependency graph
                source
                theorem countHaving_site_rewrite_monotone {K : Type} [CommSemiringWithMonus K] [DecidableEq K] [HasAltLinearOrder K] (h_abs : absorptive K) (q : Query β„• 3) (hq : q.source) (d : AnnotatedDatabase β„• K) (hnodup : (Multiset.map Prod.fst (q.evaluateAnnotated hq d)).Nodup) (ts' : Tuple (Term β„• 3) 1) (op : CompOp) (hop : op = CompOp.ge ∨ op = CompOp.gt) (C : β„•) :
                Multiset.map (fun (p : AnnotatedTuple β„• K (1 + 1)) => (fun (x : Fin 1) => p.1 ⟨0, β‹―βŸ©, p.2)) ((AggQuery.havingSite keyIdx ts' (fun (x : Fin 1) => SeqAggFunc.count) op 0 (Term.const (C + 1)) (q.toAgg hq)).evaluateAnnotated d) = (joinCountQueryPadded q op C).evaluateAnnotated β‹― d

                Site substitution for the monotone comparisons, in every absorptive commutative m-semiring: countHaving_site_rewrite for op ∈ {β‰₯, >} with the distributivity hypothesis dropped.

                Dependency graph