Tuples, relations, and databases

This file defines the basic relational model used throughout the library.

Main definitions

• Tuple T n – a tuple of arity n over value type T, represented as a function Fin n → T
• Relation T n – a multiset of tuples of arity n
• Database T – a mapping from relation names (natural numbers) to relations of the corresponding arities

def Tuple (T : Type) (n : ℕ) : Type

Equations

• Tuple T n = (Fin n → T)

def Tuple.repr {T : Type} {n : ℕ} [Repr T] (t : Tuple T n) : ℕ → Std.Format

Equations

• t.repr x✝ = Std.Format.bracket "[" (Std.Format.joinSep (List.map (fun (i : Fin n) => reprArg (t i)) (List.finRange n)) (Std.Format.text ", ")) "]"

def Tuple.cast {T : Type} {n m : ℕ} (heq : n = m) (t : Tuple T n) : Tuple T m

Equations

• Tuple.cast heq t = heq ▸ t

theorem Tuple.apply_cast {n m : ℕ} {α : Sort u_1} {T : Type} (heq : n = m) (f : Tuple T m → α) (t : Tuple T n) : f (cast heq t) = _root_.cast ⋯ f t

theorem Tuple.cast_get {n m : ℕ} {T : Type} (heq : n = m) (t : Tuple T n) (k : Fin m) : cast heq t k = t (Fin.cast ⋯ k)

@[implicit_reducible]

instance instDecidableEqTuple {T : Type} {n : ℕ} [DecidableEq T] : DecidableEq (Tuple T n)

Equations

• instDecidableEqTuple = instDecidableEqTuple._aux_1

@[implicit_reducible]

instance instReprTuple {α : Type} {n : ℕ} [Repr α] : Repr (Tuple α n)

Equations

• instReprTuple = { reprPrec := Tuple.repr }

@[implicit_reducible]

instance instZeroTuple {T : Type} [ValueType T] {n : ℕ} : Zero (Tuple T n)

Equations

• instZeroTuple = { zero := fun (x : Fin n) => 0 }

@[implicit_reducible]

instance instLTTuple {T : Type} {n : ℕ} [LT T] : LT (Tuple T n)

Equations

• instLTTuple = { lt := fun (a b : Tuple T n) => ∃ (i : Fin n), (∀ j < i, a j = b j) ∧ a i < b i }

@[implicit_reducible]

instance instLETupleOfLT {T : Type} {n : ℕ} [LT T] : LE (Tuple T n)

Equations

• instLETupleOfLT = { le := fun (a b : Tuple T n) => a < b ∨ a = b }

@[implicit_reducible]

instance instToStringTuple {T : Type} {n : ℕ} [ToString T] : ToString (Tuple T n)

Equations

• instToStringTuple = { toString := fun (t : Tuple T n) => "(" ++ ", ".intercalate (List.ofFn fun (i : Fin n) => toString (t i)) ++ ")" }

@[implicit_reducible]

instance instDecidableRelTupleLt {T : Type} {n : ℕ} [LinearOrder T] : DecidableRel fun (t₁ t₂ : Tuple T n) => t₁ < t₂

Equations

• instDecidableRelTupleLt f g = if h : ∃ (i : Fin n), (∀ j < i, f j = g j) ∧ f i < g i then isTrue h else isFalse h

@[implicit_reducible]

instance instLinearOrderTuple {T : Type} {n : ℕ} [LinearOrder T] : LinearOrder (Tuple T n)

Equations

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

def Relation (T : Type) (arity : ℕ) : Type

Equations

• Relation T arity = Multiset (Tuple T arity)

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

Equations

• Relation.cast heq r = heq ▸ r

def Relation.cast_eq {T : Type} {n m : ℕ} (r : Relation T n) (s : Relation T m) (heq : n = m) : s = cast heq r ↔ s = Multiset.map (fun (t : Tuple T n) => Tuple.cast heq t) r

Equations

• ⋯ = ⋯

@[implicit_reducible]

instance instAddRelation {T : Type} {arity : ℕ} : Add (Relation T arity)

Equations

• instAddRelation = { add := instAddRelation._aux_1 }

@[implicit_reducible]

instance instSubRelation {T : Type} [ValueType T] {arity : ℕ} : Sub (Relation T arity)

Equations

• instSubRelation = { sub := instSubRelation._aux_1 }

@[implicit_reducible]

instance instHMulRelationHAddNat {T : Type} {a₁ a₂ : ℕ} : HMul (Relation T a₁) (Relation T a₂) (Relation T (a₁ + a₂))

Equations

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

@[implicit_reducible]

instance instZeroRelation {T : Type} {n : ℕ} : Zero (Relation T n)

Equations

• instZeroRelation = { zero := ∅ }

@[implicit_reducible]

instance instZeroSigmaNatRelation {T : Type} : Zero ((n : ℕ) × Relation T n)

Equations

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

def Database (T : Type) : Type

Equations

• Database T = List (String × (n : ℕ) × Relation T n)

def Database.find {T : Type} (n : ℕ) (s : String) (d : Database T) : Option (Relation T n)

Equations

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

def Database.find.f {T : Type} (n : ℕ) (s : String) : Database T → Option (Relation T n)

Equations

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

def sortedInsert {α : Type u_1} [LinearOrder α] (x : α) (l : { l : List α // List.Pairwise (fun (x1 x2 : α) => x1 ≤ x2) l }) : { l : List α // List.Pairwise (fun (x1 x2 : α) => x1 ≤ x2) l }

Equations

• sortedInsert x l = ⟨List.orderedInsert (fun (x1 x2 : α) => x1 ≤ x2) x ↑l, ⋯⟩

instance instLeftCommutativeSubtypeListPairwiseLeSortedInsert {α : Type u_1} [LinearOrder α] : LeftCommutative sortedInsert

@[implicit_reducible]

instance instToStringRelationOfLinearOrder {T : Type} {n : ℕ} [LinearOrder T] [ToString T] : ToString (Relation T n)

Equations

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

Home · Documentation · Publications · Contributors · Source · Cite