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 (strings) to relations of the corresponding arities

source

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

Type

Equations

Tuple T n = (Fin n → T)

Instances For

Dependency graph

source

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 ", ")) "]"

Instances For

Dependency graph

source

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

Tuple T m

Equations

Tuple.cast heq t = heq ▸ t

Instances For

Dependency graph

source

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

Dependency graph

source

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)

Dependency graph

source

@[instance_reducible]

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

DecidableEq (Tuple T n)

Equations

instDecidableEqTuple = instDecidableEqTuple._aux_1

Dependency graph

source

@[instance_reducible]

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

Repr (Tuple α n)

Equations

instReprTuple = { reprPrec := Tuple.repr }

Dependency graph

source

@[instance_reducible]

instance instZeroTuple {T : Type} [ValueType T] {n : ℕ} :

Zero (Tuple T n)

Equations

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

Dependency graph

source

@[instance_reducible]

instance instLTTuple {T : Type} [ValueType T] {n : ℕ} :

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 }

Dependency graph

source

@[instance_reducible]

instance instLETuple {T : Type} [ValueType T] {n : ℕ} :

LE (Tuple T n)

Equations

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

Dependency graph

source

@[instance_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)) ++ ")" }

Dependency graph

source

@[instance_reducible]

instance instDecidableRelTupleLt {T : Type} [ValueType T] {n : ℕ} :

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

Dependency graph

source

@[instance_reducible]

instance instLinearOrderTuple {T : Type} [ValueType T] {n : ℕ} :

LinearOrder (Tuple T n)

Equations

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

Dependency graph

source

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

Type

Equations

Relation T arity = Multiset (Tuple T arity)

Instances For

Dependency graph

source

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

Relation T m

Equations

Relation.cast heq r = heq ▸ r

Instances For

Dependency graph

source

theorem Relation.cast_eq {n m : ℕ} {S : Type} (r : Relation S n) (s : Relation S m) (heq : n = m) :

s = cast heq r ↔ s = Multiset.map (fun (t : Tuple S n) => Tuple.cast heq t) r

Dependency graph

source

@[instance_reducible]

instance instAddRelation {T : Type} {arity : ℕ} :

Add (Relation T arity)

Equations

instAddRelation = { add := instAddRelation._aux_1 }

Dependency graph

source

@[instance_reducible]

instance instSubRelation {T : Type} [ValueType T] {arity : ℕ} :

Sub (Relation T arity)

Equations

instSubRelation = { sub := instSubRelation._aux_1 }

Dependency graph

source

@[instance_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.

Dependency graph

source

@[instance_reducible]

instance instZeroRelation {T : Type} {n : ℕ} :

Zero (Relation T n)

Equations

instZeroRelation = { zero := ∅ }

Dependency graph

source

@[instance_reducible]

instance instZeroSigmaNatRelation {T : Type} :

Zero ((n : ℕ) × Relation T n)

Equations

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

Dependency graph

source

def Database (T : Type) :

Type

Equations

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

Instances For

Dependency graph

source

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

Instances For

Dependency graph

source

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

Instances For

Dependency graph

source

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, ⋯⟩

Instances For

Dependency graph

source

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

LeftCommutative sortedInsert

Dependency graph

source

@[instance_reducible]

instance instToStringRelation {T : Type} [ValueType T] {n : ℕ} [ToString T] :

ToString (Relation T n)

Equations

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

Dependency graph

Documentation

Provenance.Database

Tuples, relations, and databases #

Main definitions #