Nested values under a homomorphism, at every storey

A homomorphism f : K → K' relates an evaluation over K and one over K' row by row, and a second-level aggregation builds, from two related groups of rows, two nested values. Their worlds correspond (NestedValue.WCorr), and that is what every reading of a nested value asks of them: this module proves it at every storey (wcorr_of_rel).

The two values are related family by family (NestInner.Rel). An expression family is presented on each side by a listing, the target's a tie-block permutation of the source's pushed through f, through the same readings (ListingRel); such a pair moves positions along a bijection under which every selection reads the same rows (ListingRel.move, off TiePerm.exists_equiv). A node's occurrences are the two sides of one bag of pairs, annotations pushed through f and inner values related. Where two related families have one key on one side exactly when they have one on the other (KeysFaithful – which a coherent evaluation gives), both sides' worlds are the images of one bag of indices: a decision over the root's pairs, a set of positions of each expression family, and a decision over the pairs of each node, chosen once per node (Zof).

def TiePerm.liftEquiv {n m : ℕ} (π : Fin n ≃ Fin m) : Fin (n + 1) ≃ Fin (m + 1)

One position more at the front, kept at the front.

Equations

• TiePerm.liftEquiv π = (finSuccEquiv n).trans (π.optionCongr.trans (finSuccEquiv m).symm)

theorem TiePerm.exists_equiv {α γ : Type} {eqv : α → α → Prop} (rd : α → γ) (hrd : ∀ {a b : α}, eqv a b → rd a = rd b) {l₁ l₂ : List α} : TiePerm eqv l₁ l₂ → ∃ (π : Fin l₁.length ≃ Fin l₂.length), (∀ (i : Fin l₁.length), l₂.get (π i) = l₁.get i) ∧ ∀ (W : Finset (Fin l₁.length)), List.map rd (Having.seqOf l₂ (Finset.map π.toEmbedding W)) = List.map rd (Having.seqOf l₁ W)

A tie-block permutation moves the elements along a bijection of positions, and a selection carried along it reads the same rows, in the same order, as long as tied elements read alike.

A listing pair moves positions

theorem ListingRel.exists_move {T K K' : Type} [CommSemiringWithMonus K] [CommSemiringWithMonus K'] {f : K →+* K'} (D : ListingRel f T) : ∃ (mv : Fin D.L.length ≃ Fin D.L'.length), (∀ (i : Fin D.L.length), D.ann' (D.L'.get (mv i)) = f (D.ann (D.L.get i))) ∧ ∀ (W : Finset (Fin D.L.length)), List.map D.str' (Having.seqOf D.L' (Finset.map mv.toEmbedding W)) = List.map D.str (Having.seqOf D.L W)

noncomputable def ListingRel.move {T K K' : Type} [CommSemiringWithMonus K] [CommSemiringWithMonus K'] {f : K →+* K'} (D : ListingRel f T) : Fin D.L.length ≃ Fin D.L'.length

The positions a listing pair moves, chosen.

Equations

• D.move = Classical.choose ⋯

Two towers related under a homomorphism

def NestInner.Rel {T K K' : Type} [CommSemiringWithMonus K] [CommSemiringWithMonus K'] (f : K →+* K') (lp : LeafKey T K → ListingRel f T) (LG : AggExpr T K' → AggExpr T K → Prop) (NG : (j : ℕ) → NestNode T K' (NestInner T K' j) → NestNode T K (NestInner T K j) → Prop) (j : ℕ) : NestInner T K' j → NestInner T K j → Prop

How two inner values correspond under a homomorphism, storey by storey. At storey 0 the two expressions belong to one family, presented on each side by the listing the family is given (lp), through the same readings; above, two nodes with the same outer aggregate and convention, whose occurrences are the two sides of one bag of pairs – annotations pushed through f, inner values corresponding. LG and NG restrict which pairs are considered: the hypotheses of wcorr_of_rel are stated on them.

Equations

• One or more equations did not get rendered due to their size.
• NestInner.Rel f lp LG NG j.succ (Sum.inl x') (Sum.inl x_3) = NestInner.Rel f lp LG NG j x' x_3
• NestInner.Rel f lp LG NG n.succ (Sum.inl val) (Sum.inr val_1) = False
• NestInner.Rel f lp LG NG n.succ (Sum.inr val) (Sum.inl val_1) = False

def lkey {T K K' : Type} [CommSemiringWithMonus K] [CommSemiringWithMonus K'] {f : K →+* K'} (lp : LeafKey T K → ListingRel f T) (κ : LeafKey T K) : LeafKey T K'

The key a related expression family has on the target side.

Equations

• lkey lp κ = (κ.1, List.map (lp κ).ann' (lp κ).L')

The nodes, decided once

def PairsOf {T K K' : Type} [CommSemiringWithMonus K] [CommSemiringWithMonus K'] (f : K →+* K') (lp : LeafKey T K → ListingRel f T) (LG : AggExpr T K' → AggExpr T K → Prop) (NG : (j : ℕ) → NestNode T K' (NestInner T K' j) → NestNode T K (NestInner T K j) → Prop) (j : ℕ) (N' : NestNode T K' (NestInner T K' j)) (N : NestNode T K (NestInner T K j)) (Z : Multiset ((NestInner T K' j × K' × NestInner T K j) × K)) : Prop

The bag of pairs a related node pair is the two sides of.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Zof {T K K' : Type} [CommSemiringWithMonus K] [CommSemiringWithMonus K'] (f : K →+* K') (lp : LeafKey T K → ListingRel f T) (LG : AggExpr T K' → AggExpr T K → Prop) (NG : (j : ℕ) → NestNode T K' (NestInner T K' j) → NestNode T K (NestInner T K j) → Prop) (j : ℕ) (κ : NodeKey T K j) : Multiset ((NestInner T K' j × K' × NestInner T K j) × K)

The bag of pairs chosen for a node, by key: one for all the copies of the node.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def nkeyAt {T K K' : Type} [CommSemiringWithMonus K] [CommSemiringWithMonus K'] (f : K →+* K') (lp : LeafKey T K → ListingRel f T) (LG : AggExpr T K' → AggExpr T K → Prop) (NG : (j : ℕ) → NestNode T K' (NestInner T K' j) → NestNode T K (NestInner T K j) → Prop) (j : ℕ) (κ : NodeKey T K j) : NodeKey T K' j

The key a related node has on the target side, at its storey.

Equations

• nkeyAt f lp LG NG j κ = (κ.1, Multiset.map (fun (z : (NestInner T K' j × K' × NestInner T K j) × K) => (z.1.1, z.1.2.1)) (Zof f lp LG NG j κ))

noncomputable def nkey {T K K' : Type} [CommSemiringWithMonus K] [CommSemiringWithMonus K'] (f : K →+* K') (lp : LeafKey T K → ListingRel f T) (LG : AggExpr T K' → AggExpr T K → Prop) (NG : (j : ℕ) → NestNode T K' (NestInner T K' j) → NestNode T K (NestInner T K j) → Prop) (e : (j : ℕ) × NodeKey T K j) : (j : ℕ) × NodeKey T K' j

The key a related node has on the target side.

Equations

• nkey f lp LG NG e = ⟨e.fst, nkeyAt f lp LG NG e.fst e.snd⟩

Enumerations carried along

def finsOf {n : ℕ} (S : Finset ℕ) : Finset (Fin n)

The positions of a family of length n a set of numbers names.

Equations

• finsOf S = {i : Fin n | ↑i ∈ S}

noncomputable def ListingRel.moveS {T K K' : Type} [CommSemiringWithMonus K] [CommSemiringWithMonus K'] {f : K →+* K'} (D : ListingRel f T) (S : Finset ℕ) : Finset ℕ

The positions a listing pair moves a set of positions to.

Equations

• D.moveS S = Finset.map Fin.valEmbedding (Finset.map D.move.toEmbedding (finsOf S))

The worlds of two related towers correspond

@[reducible, inline]

abbrev PEntry (T K K' : Type) : Type

A decision about a node, over a bag of pairs.

Equations

• PEntry T K K' = ((j : ℕ) × NodeKey T K j × Multiset ((NestInner T K' j × K' × NestInner T K j) × K × Bool))

def addNodeP {T K K' : Type} (Zf : (j : ℕ) → NodeKey T K j → Multiset ((NestInner T K' j × K' × NestInner T K j) × K)) (κ : (j : ℕ) × NodeKey T K j) (acc : Multiset (Multiset (PEntry T K K'))) : Multiset (Multiset (PEntry T K K'))

One more node, decided over its chosen pairs.

Equations

• One or more equations did not get rendered due to their size.

instance instLeftCommutativeSigmaNatNodeKeyMultisetPEntryAddNodeP {T K K' : Type} (Zf : (j : ℕ) → NodeKey T K j → Multiset ((NestInner T K' j × K' × NestInner T K j) × K)) : LeftCommutative (addNodeP Zf)

def entK {T K K' : Type} (e : PEntry T K K') : (j : ℕ) × NodeKey T K j × Multiset (NestInner T K j × K × Bool)

The source side of a decision about a node.

Equations

• entK e = ⟨e.fst, (e.snd.1, Multiset.map (fun (m : (NestInner T K' e.fst × K' × NestInner T K e.fst) × K × Bool) => (m.1.2.2, m.2.1, m.2.2)) e.snd.2)⟩

noncomputable def entK' {T K K' : Type} [CommSemiringWithMonus K] [CommSemiringWithMonus K'] (f : K →+* K') (lp : LeafKey T K → ListingRel f T) (LG : AggExpr T K' → AggExpr T K → Prop) (NG : (j : ℕ) → NestNode T K' (NestInner T K' j) → NestNode T K (NestInner T K j) → Prop) (e : PEntry T K K') : (j : ℕ) × NodeKey T K' j × Multiset (NestInner T K' j × K' × Bool)

The target side of a decision about a node.

Equations

• One or more equations did not get rendered due to their size.

def KeysFaithful {T K K' : Type} [CommSemiringWithMonus K] [CommSemiringWithMonus K'] (f : K →+* K') (lp : LeafKey T K → ListingRel f T) (LG : AggExpr T K' → AggExpr T K → Prop) (NG : (j : ℕ) → NestNode T K' (NestInner T K' j) → NestNode T K (NestInner T K j) → Prop) : Prop

What a pair of related towers asks of its families: two related expression families have one key on one side exactly when they have one on the other, and so do two related nodes.

Equations

• One or more equations did not get rendered due to their size.

theorem wcorr_of_rel {T K K' : Type} [ValueType T] [CommSemiringWithMonus K] [CommSemiringWithMonus K'] [DecidableEq K] [DecidableEq K'] {f : K →+* K'} {lp : LeafKey T K → ListingRel f T} {LG : AggExpr T K' → AggExpr T K → Prop} {NG : (j : ℕ) → NestNode T K' (NestInner T K' j) → NestNode T K (NestInner T K j) → Prop} (hK : KeysFaithful f lp LG NG) {j : ℕ} {N' : NestNode T K' (NestInner T K' j)} {N : NestNode T K (NestInner T K j)} (hr : NestInner.Rel f lp LG NG (j + 1) (Sum.inr N') (Sum.inr N)) : NestedValue.WCorr f (NestedValue.ofNode N') (NestedValue.ofNode N)

Two related towers have corresponding worlds. The source's worlds and the target's are the images of one bag of indices: a decision over the pairs of the root's occurrences, a set of positions of each expression family the source holds – moved, on the target, by the family's listing pair – and a decision over the chosen pairs of each node it holds.

Home · Documentation · Publications · Contributors · Source · Cite