Lax Lean Archive

While this submission is a draft, it cannot be used by other submissions.

Relations and databases with multiset semantics

Lax392996.Databases · concepts/Lax392996/Databases.lean · lax-392996

definition

Loading review…

Community review

Flags

Each flag is tied to a public ORCID identity and explains why this concept may be incorrect.

No flags have been submitted.

    Community review

    Flag this concept

    State precisely what appears incorrect. This explanation will be public under your ORCID name.

    No source line selected.

    Natural Language Statement

    Definition

    Values are drawn from a value type: a linearly ordered type with a zero, an addition, a subtraction and a multiplication, over which the arithmetic of query terms is read. A tuple of arity kk is a map {0,…,k−1}→V\{0, \dots, k-1\} \to \mathcal{V}, tuples being ordered lexicographically; a relation of arity kk is a finite multiset of kk-tuples, with multiset union and the cross product of multisets; a database is a finite list of named relations, each with its arity, looked up by name and arity.

    Concept map
    1 concept; 13 descendants hidden
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

    In the paper

    • page 3 of this submission's paper

    Lean source view on GitHub

    1import Mathlib.Algebra.Group.Defs
    2import Mathlib.Order.Defs.LinearOrder
    3import Mathlib.Data.Multiset.Basic
    4import Mathlib.Data.Set.Finite.Basic
    5import Mathlib.Data.Multiset.AddSub
    6import Mathlib.Data.Multiset.Bind
    7import Mathlib.Data.Fin.Tuple.Basic
    8import Mathlib.Data.Fintype.Basic
    9
    10/-!
    11---
    12title: Relations and databases with multiset semantics
    13type: definition
    14---
    15Values are drawn from a value type: a linearly ordered type with a zero,
    16an addition, a subtraction and a multiplication, over which the arithmetic
    17of query terms is read. A tuple of arity kk is a map {0,…,k−1}→V\{0, \dots, k-1\} \to \mathcal{V}
    18, tuples being ordered lexicographically; a relation of
    19arity kk is a finite multiset of kk-tuples, with multiset union and the
    20cross product of multisets; a database is a finite list of named
    21relations, each with its arity, looked up by name and arity.
    22-/
    23
    24namespace Lax392996.Databases
    25
    26/-- The values of a database: a linearly ordered type with a zero, an
    27addition, a subtraction and a multiplication, the arithmetic of terms. -/
    28class ValueType (T : Type) extends Zero T, AddCommSemigroup T, Sub T, Mul T, LinearOrder T
    29
    30variable {T : Type} [ValueType T] {n m : ℕ}
    31
    32/-- A tuple of arity `n` over `T`. -/
    33def Tuple (T : Type) (n: ℕ) := Fin n → T
    34
    35instance instDecidableEqTuple [DecidableEq T] : DecidableEq (Tuple T n) := by
    36 show DecidableEq (Fin n → T)
    37 infer_instance
    38
    39/-- The lexicographic strict order on tuples. -/
    40instance instLTTuple : LT (Tuple T n) :=
    41 ⟨λ a b ↦ ∃ i : Fin n, (∀ j, j < i → a j = b j) ∧ a i < b i⟩
    42
    43instance instLETuple : LE (Tuple T n) := ⟨λ a b ↦ a < b ∨ a = b⟩
    44
    45instance instDecidableRelTupleLt : DecidableRel (λ (t₁ t₂: Tuple T n) => t₁ < t₂) :=
    46 λ f g ↦
    47 let _ : DecidablePred (fun i : Fin n => (∀ j, j < i → f j = g j) ∧ f i < g i) :=
    48 fun i => @instDecidableAnd _ _
    49 (@Fintype.decidableForallFintype (Fin n) (fun j => j < i → f j = g j)
    50 (fun _j => inferInstance) _)
    51 inferInstance
    52 if h : ∃ i : Fin n, (∀ j, j < i → f j = g j) ∧ f i < g i then
    53 isTrue (h)
    54 else
    55 isFalse (h)
    56
    57/-- Tuples are linearly ordered, lexicographically. -/
    58instance instLinearOrderTuple : LinearOrder (Tuple T n) where
    59 le_refl := by simp[(· ≤ ·)]
    60
    61 le_antisymm := by
    62 simp[(· ≤ ·)]
    63 intro a b hab hba
    64 cases hab with
    65 | inl hab' =>
    66 cases hba with
    67 | inl hba' =>
    68 simp only[(· < ·)] at *
    69 rcases hab' with ⟨iab,hiab⟩
    70 rcases hba' with ⟨iba,hiba⟩
    71 by_cases h : iab=iba
    72 . rw[h] at hiab
    73 have := lt_trans hiab.right hiba.right
    74 have := lt_asymm (lt_trans hiab.right hiba.right)
    75 contradiction
    76 . by_cases h' : iab<iba
    77 . have heq := hiba.left iab h'
    78 have := hiab.right
    79 rw[heq] at this
    80 have := lt_asymm this
    81 contradiction
    82 . have h'' : iba<iab := by
    83 refine lt_iff_le_and_ne.mpr ?_
    84 constructor
    85 . exact le_of_not_gt h'
    86 . exact fun a ↦ h (id (Eq.symm a))
    87 have heq := hiab.left iba h''
    88 have := hiba.right
    89 rw[heq] at this
    90 have := lt_asymm this
    91 contradiction
    92 | inr hba' => exact Eq.symm hba'
    93 | inr hab' => exact hab'
    94
    95 le_trans := by
    96 intro a b c
    97 simp only[(· ≤ ·),(· < ·)]
    98 intro hab hbc
    99 cases hab with
    100 | inl habl =>
    101 cases hbc with
    102 | inl hbcl =>
    103 apply Or.inl
    104 rcases habl with ⟨iab,hiab⟩
    105 rcases hbcl with ⟨ibc,hibc⟩
    106 let i := min iab ibc
    107 use i
    108 have h : ∀ (j : Fin n), j < i → a j = c j := by
    109 intro j hj
    110 have hx := hiab.left j (lt_min_iff.mp hj).left
    111 have hy := hibc.left j (lt_min_iff.mp hj).right
    112 rw[hy] at hx; exact hx
    113 use h
    114 by_cases heq : iab = i
    115 . by_cases heq' : ibc = i
    116 . rw[heq] at hiab
    117 rw[heq'] at hibc
    118 exact lt_trans hiab.right hibc.right
    119 . have h' : i < ibc := lt_of_le_of_ne (min_le_right iab ibc) (ne_comm.mpr heq')
    120 have hab := hiab.right
    121 rw[heq] at hab
    122 have hbc := hibc.left i h'
    123 rw[hbc] at hab
    124 exact hab
    125 . have heq'' : ibc = i := by
    126 have choice : iab = i ∨ ibc = i := by
    127 rcases min_choice iab ibc with hc | hc
    128 . exact Or.inl hc.symm
    129 . exact Or.inr hc.symm
    130 tauto
    131 have h' : i < iab := lt_of_le_of_ne (min_le_left iab ibc) (ne_comm.mpr heq)
    132 have hbc := hibc.right
    133 rw[heq''] at hbc
    134 have hab := hiab.left i h'
    135 rw[hab]
    136 exact hbc
    137 | inr hbcr =>
    138 rw[← hbcr]
    139 exact Or.inl habl
    140 | inr habr =>
    141 rw[habr]
    142 exact hbc
    143
    144 le_total := by
    145 intro a b
    146 simp only[(· ≤ ·)]
    147 by_cases heq: a=b
    148 . tauto
    149 . by_cases h: ∃ i, (∀ j < i, a j = b j) ∧ a i < b i
    150 . apply Or.inl; apply Or.inl
    151 simp only[(· < ·)]
    152 tauto
    153 . apply Or.inr; apply Or.inl
    154 simp only[(· < ·)]
    155 have hexists : ∃ k, ¬ a k = b k := by
    156 refine Classical.byContradiction fun hne => ?_
    157 simp at hne
    158 exact heq (funext hne)
    159 have hdec : DecidablePred (fun j : Fin n => ¬ a j = b j) := fun j => instDecidableNot
    160 obtain ⟨k, hk⟩ : ∃ k, k = Fin.find (λ j ↦ ¬ a j = b j) hexists := ⟨_, rfl⟩
    161 use k
    162 have hspec : ¬ a k = b k := by rw [hk]; exact Fin.find_spec hexists
    163 have hmin_ab : ∀ j < k, a j = b j := by
    164 intro j hj
    165 rw [hk] at hj
    166 have := Fin.find_min hexists hj
    167 simp at this
    168 exact this
    169 have hmin_ba : ∀ j < k, b j = a j := fun j hj => (hmin_ab j hj).symm
    170 refine ⟨hmin_ba, ?_⟩
    171 simp at h
    172 have hle : b k ≤ a k := h k hmin_ab
    173 exact lt_iff_le_and_ne.mpr ⟨hle, fun h => hspec h.symm⟩
    174
    175 lt_iff_le_not_ge := by
    176 intro a b
    177 simp only[(· ≤ ·)]
    178 apply Iff.intro
    179 . intro hab
    180 constructor
    181 . tauto
    182 . simp only[(· < ·)] at *
    183 rcases hab with ⟨i, hi⟩
    184 simp
    185 constructor
    186 . intro k h
    187 cases hki : compare k i with
    188 | eq =>
    189 simp at hki
    190 rw[hki]
    191 exact le_of_lt hi.right
    192 | lt =>
    193 simp[compare] at hki
    194 have := hi.left k hki
    195 simp[this]
    196 | gt =>
    197 simp only[compare,compareOfLessAndEq] at hki
    198 by_cases hki' : k < i
    199 . simp[hki'] at hki
    200 . by_cases hki'' : k = i
    201 . rw[hki''] at hki
    202 simp at hki
    203 . simp[hki'] at hki
    204 have hgt : k>i := by
    205 have hle := le_of_not_gt hki'
    206 apply lt_of_le_of_ne
    207 . exact hle
    208 . exact fun a ↦ hki'' (id (Eq.symm a))
    209 have h' := h i hgt
    210 rw[h'] at hi
    211 have hc : a i < a i := hi.right
    212 simp at hc
    213 . intro heq
    214 rw[heq] at hi
    215 simp at hi
    216 . intro ⟨h₁,h₂⟩
    217 simp at h₂
    218 have hne : a ≠ b := by
    219 rw[ne_comm]; exact h₂.right
    220 simp[hne] at h₁
    221 exact h₁
    222
    223 toDecidableLE :=
    224 λ a b ↦
    225 match (inferInstance : Decidable (a<b)), (inferInstance : Decidable (a=b)) with
    226 | isTrue h₁, _ => isTrue (Or.inl h₁)
    227 | _, isTrue h₂ => isTrue (Or.inr h₂)
    228 | isFalse h₁, isFalse h₂ => isFalse (
    229 fun h ↦
    230 match h with
    231 | Or.inl h' => h₁ h'
    232 | Or.inr h' => h₂ h'
    233 )
    234
    235/-- A relation of arity `arity` over `T`: a finite multiset of tuples. -/
    236def Relation (T) (arity: ℕ) := Multiset (Tuple T arity)
    237
    238/-- Transport of a relation along an equality of arities. -/
    239def Relation.cast (heq: n=m) (r: Relation T n): Relation T m :=
    240 Eq.ndrec (motive := fun m => Relation T m) r heq
    241
    242instance instAddRelation {arity : ℕ} : Add (Relation T arity) := by
    243 show Add (Multiset (Tuple T arity))
    244 infer_instance
    245
    246/-- The cross product of two relations, concatenating the tuples. -/
    247instance instHMulRelationHAddNat {a₁ a₂ : ℕ} :
    248 HMul (Relation T a₁) (Relation T a₂) (Relation T (a₁+a₂)) where
    249 hMul r s :=
    250 Multiset.map (λ ((x,y) : (Tuple T a₁)×(Tuple T a₂)) ↦
    251 Fin.append x y
    252 ) (Multiset.product r s)
    253
    254/-- A database: a list of named relations, each with its arity. -/
    255def Database (T) := List (String × Σ n, Relation T n)
    256
    257/-- The relation named `s` of arity `n` in a database, if any. -/
    258def Database.find (n: ℕ) (s: String) (d: Database T) : Option (Relation T n) :=
    259 let rec f
    260 | [] => none
    261 | (s',rn)::tl => if h: n = rn.fst ∧ s=s' then some (Eq.mp (by rw[h.left]) rn.snd) else f tl
    262 f d
    263
    264end Lax392996.Databases
    265
    Builds on

    none

    Used by
    From Mathlib

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…