Provenance.QueryRewriting

def Query.rewriting {T : Type} {n : ℕ} {K : Type} [ValueType T] (q : Query T n) (hq : q.noAgg) :

Query (T ⊕ K) (n + 1)

Equations

One or more equations did not get rendered due to their size.
(Query.Rel n s).rewriting hq_2 = Query.Rel (n + 1) s
(Π ts q_2).rewriting hq_2 = (Π fun (k : Fin (n + 1)) => if h : ↑k < n then (ts ⟨↑k, h⟩).castToAnnotatedTuple else #(Fin.last q_2.arity)) (q_2.rewriting ⋯)
(σ φ q_2).rewriting hq_2 = σ φ.castToAnnotatedTuple (q_2.rewriting ⋯)
(q₁ ⊎ q₂).rewriting hq_2 = (q₁.rewriting ⋯ ⊎ q₂.rewriting ⋯)
(ε q_2).rewriting hq_2 = Query.Agg (fun (k : Fin n) => Fin.castLE ⋯ k) ![#(Fin.last n)] ![AggFunc.sum ] (q_2.rewriting ⋯)
(Query.Agg a a_1 a_2 a_3).rewriting hq_2 = False.elim hq_2

Instances For

theorem Query.rewriting_valid_prod_heqn {n₁ n₂ n : ℕ} (hn : n₁ + n₂ = n) :

n₁ + 1 + (n₂ + 1) = n + 2

theorem Query.rewriting_valid_prod0 {K T : Type} [Mul K] {n₁ n₂ n : ℕ} (hn : n₁ + n₂ = n) (heq : (Fin (n₁ + n₂) → T) = (Fin n → T)) (ar₁ : AnnotatedRelation T K n₁) (ar₂ : AnnotatedRelation T K n₂) :

theorem cast_apply {T : Type} {n : ℕ} {α : Sort u_1} {m : ℕ} (f : Tuple T n → α) (t : Tuple T m) (hn : n = m) :

cast ⋯ f t = f (Tuple.cast ⋯ t)

theorem Query.rewriting_valid_prod1 {T K : Type} {n₂ n₁ n : ℕ} [ValueType (T ⊕ K)] (hn : n₁ + 1 + (n₂ + 1) = n + 2) (f : Tuple (T ⊕ K) (n + 2) → Tuple (T ⊕ K) (n + 1)) (r : Relation (T ⊕ K) (n₁ + 1 + (n₂ + 1))) :

Multiset.map f (Relation.cast hn r) = Multiset.map (fun (t : Tuple (T ⊕ K) (n₁ + 1 + (n₂ + 1))) => f (Tuple.cast hn t)) r

theorem Query.rewriting_append_left {T : Type} {n₁ n₂ n : ℕ} (t₁ : Tuple T n₁) (t₂ : Tuple T n₂) (hn : n₁ + n₂ = n) (k : Fin n) (hk : ↑k < n₁) :

Eq.rec (motive := fun (x : ℕ) (h : n₁ + n₂ = x) => Fin x → T) (Fin.append t₁ t₂) hn k = t₁ (k.castLT hk)

theorem Query.rewriting_append_right {T : Type} {n₁ n₂ n : ℕ} (t₁ : Tuple T n₁) (t₂ : Tuple T n₂) (hn : n₁ + n₂ = n) (k : Fin n) (hk : ¬↑k < n₁) :

Eq.rec (motive := fun (x : ℕ) (h : n₁ + n₂ = x) => Fin x → T) (Fin.append t₁ t₂) hn k = t₂ ⟨↑k - n₁, ⋯⟩