@[reducible, inline]

abbrev AnnotatedTuple (T : Type) (K : Type u_1) (n : ℕ) : Type u_1

Equations

• AnnotatedTuple T K n = Lex (Tuple T n × K)

instance instLinearOrderAnnotatedTuple {T : Type} [ValueType T] {K : Type} {n : ℕ} [LinearOrder K] : LinearOrder (AnnotatedTuple T K n)

Equations

• instLinearOrderAnnotatedTuple = inferInstance

instance instToStringAnnotatedTuple {T K : Type} {n : ℕ} [ToString T] [ToString K] : ToString (AnnotatedTuple T K n)

Equations

• instToStringAnnotatedTuple = { toString := fun (t : AnnotatedTuple T K n) => "(" ++ ", ".intercalate (List.ofFn fun (i : Fin n) => toString (t.1 i)) ++ ";" ++ toString t.2 ++ ")" }

instance instZeroAnnotatedTuple {T : Type} [ValueType T] {K : Type} [Zero K] {n : ℕ} : Zero (AnnotatedTuple T K n)

Equations

• instZeroAnnotatedTuple = { zero := (0, 0) }

def AnnotatedRelation (T : Type) (K : Type u_1) (arity : ℕ) : Type u_1

Equations

• AnnotatedRelation T K arity = Multiset (AnnotatedTuple T K arity)

def AnnotatedRelation.cast {T K : Type} {n m : ℕ} (heq : n = m) (r : AnnotatedRelation T K n) : AnnotatedRelation T K m

Equations

• AnnotatedRelation.cast heq r = heq ▸ r

instance instToStringAnnotatedRelationOfLinearOrder {T : Type} [ValueType T] {K : Type} {n : ℕ} [ToString T] [ToString K] [LinearOrder K] : ToString (AnnotatedRelation T K n)

Equations

• instToStringAnnotatedRelationOfLinearOrder = { toString := fun (r : AnnotatedRelation T K n) => "\n".intercalate (List.map toString ↑(Multiset.foldr sortedInsert ⟨[], ⋯⟩ r)) ++ "\n" }

def Relation.annotate {T K : Type} {n : ℕ} (f : Tuple T n → K) (r : Relation T n) : AnnotatedRelation T K n

Equations

• Relation.annotate f r = Multiset.map (fun (t : Tuple T n) => (t, f t)) r

instance instAddAnnotatedRelation {T K : Type} {arity : ℕ} : Add (AnnotatedRelation T K arity)

Equations

• instAddAnnotatedRelation = inferInstanceAs (Add (Multiset (AnnotatedTuple T K arity)))

instance instZeroAnnotatedRelation {T K : Type} {n : ℕ} : Zero (AnnotatedRelation T K n)

Equations

• instZeroAnnotatedRelation = { zero := ∅ }

instance instZeroSigmaNatAnnotatedRelation {T K : Type} : Zero ((n : ℕ) × AnnotatedRelation T K n)

Equations

• instZeroSigmaNatAnnotatedRelation = { zero := ⟨0, ∅⟩ }

def AnnotatedDatabase (T : Type) (K : Type u_1) : Type u_1

Equations

• AnnotatedDatabase T K = List (String × (n : ℕ) × AnnotatedRelation T K n)

def AnnotatedDatabase.find {T K : Type} (n : ℕ) (s : String) (d : AnnotatedDatabase T K) : Option (AnnotatedRelation T K n)

Equations

• AnnotatedDatabase.find n s d = AnnotatedDatabase.find.f n s d

def AnnotatedDatabase.find.f {T K : Type} (n : ℕ) (s : String) : AnnotatedDatabase T K → Option (AnnotatedRelation T K n)

Equations

• AnnotatedDatabase.find.f n s [] = none
• AnnotatedDatabase.find.f n s ((s', rn) :: tl) = if h : n = rn.fst ∧ s = s' then some (⋯.mp rn.snd) else AnnotatedDatabase.find.f n s tl

def AnnotatedTuple.toComposite {T K : Type} {n : ℕ} (p : AnnotatedTuple T K n) : Fin (n + Nat.succ 0) → T ⊕ K

Equations

• p.toComposite = Fin.append (fun (k : Fin n) => Sum.inl (p.1 k)) ![Sum.inr p.2]

def Tuple.fromComposite {T : Type} [ValueType T] {K : Type} [Zero K] {n : ℕ} (t : Tuple (T ⊕ K) (n + 1)) : AnnotatedTuple T K n

Equations

• t.fromComposite = (fun (k : Fin n) => match t (Fin.castLE ⋯ k) with | Sum.inl x => x | Sum.inr val => 0, match t (Fin.last n) with | Sum.inl val => 0 | Sum.inr x => x)

def AnnotatedRelation.toComposite {T K : Type} {n : ℕ} (ar : AnnotatedRelation T K n) : Relation (T ⊕ K) (n + 1)

Equations

• ar.toComposite = Multiset.map (fun (p : AnnotatedTuple T K n) => p.toComposite) ar

@[simp]

theorem AnnotatedRelation.toComposite_add {n : ℕ} {T K : Type} (ar₁ ar₂ : AnnotatedRelation T K n) : (ar₁ + ar₂).toComposite = ar₁.toComposite + ar₂.toComposite

def AnnotatedDatabase.toComposite {T K : Type} (d : AnnotatedDatabase T K) : Database (T ⊕ K)

Equations

• d.toComposite = List.map (fun (x : String × (n : ℕ) × AnnotatedRelation T K n) => match x with | (s, ⟨n', r⟩) => (s, ⟨n' + 1, r.toComposite⟩)) d

theorem AnnotatedDatabase.find_toComposite_none {T K : Type} (n : ℕ) (s : String) (d : AnnotatedDatabase T K) : find n s d = none ↔ Database.find (n + 1) s d.toComposite = none

theorem AnnotatedDatabase.find_toComposite_some {T K : Type} (n : ℕ) (s : String) (d : AnnotatedDatabase T K) (r : AnnotatedRelation T K n) : find n s d = some r ↔ Database.find (n + 1) s d.toComposite = some r.toComposite

theorem AnnotatedTuple.toComposite_join {n₁ n₂ : ℕ} {K T : Type} [ValueType T] [HasAltLinearOrder K] [SemiringWithMonus K] (ta₁ : AnnotatedTuple T K n₁) (ta₂ : AnnotatedTuple T K n₂) : toComposite (Fin.append ta₁.1 ta₂.1, ta₁.2 * ta₂.2) = fun (k : Fin (n₁ + n₂ + 1)) => if h : ↑k < n₁ then ta₁.toComposite (k.castLT ⋯) else if ↑k < n₁ + n₂ then ta₂.toComposite (Fin.ofNat (n₂ + 1) (k.toNat - n₁)) else ta₁.toComposite (Fin.last n₁) * ta₂.toComposite (Fin.last n₂)

theorem eq_imp_eq_equiv_eq {α✝ : Sort u_1} {y z x : α✝} : y = z → (x = y ↔ x = z)

theorem AnnotatedRelation.toComposite_map_product {n₁ n₂ : ℕ} {K T : Type} [ValueType T] [HasAltLinearOrder K] [SemiringWithMonus K] (ar₁ : AnnotatedRelation T K n₁) (ar₂ : AnnotatedRelation T K n₂) : toComposite (Multiset.map (fun (x : AnnotatedTuple T K n₁ × AnnotatedTuple T K n₂) => (Fin.append x.1.1 x.2.1, x.1.2 * x.2.2)) (Multiset.product ar₁ ar₂)) = Multiset.map (fun (x : Tuple (T ⊕ K) (n₁ + 1) × Tuple (T ⊕ K) (n₂ + 1)) (k : Fin (n₁ + n₂ + 1)) => if h : ↑k < n₁ then x.1 (k.castLT ⋯) else if ↑k < n₁ + n₂ then x.2 (Fin.ofNat (n₂ + 1) (k.toNat - n₁)) else x.1 (Fin.last n₁) * x.2 (Fin.last n₂)) (Multiset.product ar₁.toComposite ar₂.toComposite)

theorem AnnotatedRelation.cast_toComposite {n m : ℕ} {T K : Type} (ar : AnnotatedRelation T K n) (h' : n + 1 = m + 1) (h : n = m) : Relation.cast h' ar.toComposite = (cast h ar).toComposite