Skip to content

Commit e556cef

Browse files
Rickerd1234Rickerd1234
committed
Code Quality & Consistency
1 parent a4c7fdf commit e556cef

5 files changed

Lines changed: 51 additions & 52 deletions

File tree

‎RelationalAlgebra/Equivalence/FOLtoRA/Adom.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -111,7 +111,7 @@ theorem EmptyTupleFromRelations.evaluateT_def [DecidableEq α] :
111111
simp [EmptyTupleFromRelations]
112112
induction rns with
113113
| nil =>
114-
simp only [List.foldr_nil, Query.evaluateT.eq_7, diffT,
114+
simp only [List.foldr_nil, Query.evaluateT.eq_7, differenceT,
115115
EmptyTupleFromRelation.evaluateT_def, exists_and_right]
116116
ext t
117117
simp_all

‎RelationalAlgebra/Equivalence/FOLtoRA/Conversion.lean‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -61,7 +61,7 @@ theorem toRA.falsum_def [Nonempty μ] [Nonempty ρ] [Nonempty ↑(adomRs dbi.sch
6161
(toRA (BoundedFormula.falsum (L := fol dbi.schema) (n := n)) rs brs).evaluateT dbi =
6262
{t | ∃h, RealizeDomSet (BoundedFormula.falsum (L := fol dbi.schema) (n := n)) rs brs t h} := by
6363
have : (RA.Query.evaluateT dbi (adom dbi.schema rs)) \ (RA.Query.evaluateT dbi (adom dbi.schema rs)) = ∅ := Set.diff_self
64-
simp_rw [toRA, RA.Query.evaluateT, diffT, this]
64+
simp_rw [toRA, RA.Query.evaluateT, differenceT, this]
6565
simp [RealizeDomSet, BoundedFormula.Realize]
6666

6767
theorem toRA.term_equal_def [Nonempty μ] [folStruc dbi (α := String) (μ := μ)] {t₁ t₂ : (fol dbi.schema).Term (String ⊕ Fin n)} {t : String →. μ} {rs : Finset String}
@@ -146,7 +146,7 @@ theorem toRA.imp_def [Nonempty μ] [Nonempty ρ] [Nonempty ↑(adomRs dbi.schema
146146
(ih₂ : (toRA (dbs := dbi.schema) q₂ rs brs).evaluateT dbi = {t | ∃h, RealizeDomSet q₂ rs brs t h}) :
147147
(toRA (q₁.imp q₂) rs brs).evaluateT dbi = {t | ∃h, RealizeDomSet (q₁.imp q₂) rs brs t h} := by
148148
ext t
149-
simp only [toRA, RA.Query.evaluateT, diffT, adom.complete_def, Set.mem_diff, Set.mem_setOf_eq,
149+
simp only [toRA, RA.Query.evaluateT, differenceT, adom.complete_def, Set.mem_diff, Set.mem_setOf_eq,
150150
not_and, not_not, RealizeDomSet, BoundedFormula.realize_imp, exists_and_right]
151151
simp_all only [nonempty_subtype, RealizeDomSet, Finset.coe_inj, exists_and_right,
152152
Set.mem_setOf_eq, and_true, and_imp, forall_exists_index, exists_true_left,
@@ -168,7 +168,7 @@ theorem toRA.all_def [Nonempty μ] [Nonempty ρ] [Nonempty ↑(adomRs dbi.schema
168168
(hμ : ∀v : μ, v ∈ dbi.domain) (hn : n + depth (∀'q) < brs.card) (h : (FreeMap (n + 1) brs) (Fin.last n) ∉ q.freeVarFinset)
169169
(ih : (toRA q (q.freeVarFinset ∪ FRan (FreeMap (n + 1) brs)) brs).evaluateT dbi = {t | ∃h, RealizeDomSet q (q.freeVarFinset ∪ FRan (FreeMap (n + 1) brs)) brs t h}) :
170170
(toRA q.all (q.freeVarFinset ∪ FRan (FreeMap n brs)) brs).evaluateT dbi = {t | ∃h, RealizeDomSet (q.all) (q.freeVarFinset ∪ FRan (FreeMap n brs)) brs t h} := by
171-
simp only [toRA, RA.Query.evaluateT, Finset.union_assoc, diffT]
171+
simp only [toRA, RA.Query.evaluateT, Finset.union_assoc, differenceT]
172172
rw [FreeMap.FRan_union_add_one (by grind), ih]
173173

174174
ext t

‎RelationalAlgebra/RA/Examples.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -181,7 +181,7 @@ theorem hQueryDifference : exQueryUnion.isWellTyped exDatabase.schema := by
181181
#simp [Query.evaluate, Query.schema] (exQueryDifference.schema exDatabase.schema)
182182

183183
example : ¬∃t, t ∈ (exQueryDifference.evaluate exDatabase hQueryDifference).tuples := by
184-
simp only [Query.evaluate, Query.evaluateT, diffT, exDatabase, exQueryDifference]
184+
simp only [Query.evaluate, Query.evaluateT, differenceT, exDatabase, exQueryDifference]
185185
simp only [String.reduceEq, imp_self]
186186

187187
simp

‎RelationalAlgebra/RA/Query.lean‎

Lines changed: 39 additions & 38 deletions
Original file line numberDiff line numberDiff line change
@@ -50,51 +50,52 @@ def Query.evaluateT (dbi : DatabaseInstance ρ α μ) (q : Query ρ α) : Set (
5050
| .j sq₁ sq₂ => joinT (sq₁.evaluateT dbi) (sq₂.evaluateT dbi)
5151
| .r f sq => renameT (sq.evaluateT dbi) f
5252
| .u sq₁ sq₂ => unionT (sq₁.evaluateT dbi) (sq₂.evaluateT dbi)
53-
| .d sq₁ sq₂ => diffT (sq₁.evaluateT dbi) (sq₂.evaluateT dbi)
53+
| .d sq₁ sq₂ => differenceT (sq₁.evaluateT dbi) (sq₂.evaluateT dbi)
5454

5555
/-- Proof that each well-typed query will result in tuples with the correct schema -/
56-
theorem Query.evaluate.validSchema [DecidableEq α] (q : Query ρ α) (h : q.isWellTyped dbi.schema) : ∀t, t ∈ q.evaluateT dbi → PFun.Dom t = ↑(q.schema dbi.schema) := by
57-
induction q with
58-
| R rn =>
59-
intro t h_t
60-
simp_all only [isWellTyped, evaluateT, schema, ← DatabaseInstance.validSchema]
61-
exact (dbi.relations rn).validSchema t h_t
62-
| s a b sq ih =>
63-
simp_all only [isWellTyped, evaluateT, selectionT, schema]
64-
simp_all only [forall_const, Set.mem_setOf_eq, implies_true]
65-
| p rs sq ih =>
66-
intro t h_t
67-
simp_all [isWellTyped, evaluateT, projectionT, schema]
68-
apply projectionDom ⟨sq.schema dbi.schema, evaluateT dbi sq, ih⟩ ?_ h.2
69-
. simp_all only [projectionT, Set.mem_setOf_eq]
70-
| j sq₁ sq₂ ih₁ ih₂ =>
71-
intro t h_t
72-
simp_all only [isWellTyped, forall_const]
73-
apply joinDom
74-
⟨sq₁.schema dbi.schema, evaluateT dbi sq₁, ih₁⟩
75-
⟨sq₂.schema dbi.schema, evaluateT dbi sq₂, ih₂⟩
76-
h_t
77-
| r f sq ih =>
78-
intro t h_t
79-
apply renameDom ⟨sq.schema dbi.schema, evaluateT dbi sq, (by simp_all)⟩ h.2.2
80-
simp_all only [evaluateT, renameT, Set.mem_setOf_eq]
81-
| u sq₁ sq₂ ih =>
82-
intro _ ht
83-
simp [isWellTyped, evaluateT, unionT, schema] at *
84-
cases ht
85-
all_goals simp_all only
86-
| d sq₁ sq₂ ih =>
87-
intro _ ht
88-
simp [isWellTyped, evaluateT, diffT, schema] at *
89-
cases ht
90-
all_goals simp_all only
56+
theorem Query.evaluate.validSchema {dbi : DatabaseInstance ρ α μ} [DecidableEq α] (q : Query ρ α) (h : q.isWellTyped dbi.schema) :
57+
∀t, t ∈ q.evaluateT dbi → PFun.Dom t = ↑(q.schema dbi.schema) := by
58+
induction q with
59+
| R rn =>
60+
intro t h_t
61+
simp_all only [isWellTyped, evaluateT, schema, ← DatabaseInstance.validSchema]
62+
exact (dbi.relations rn).validSchema t h_t
63+
| s a b sq ih =>
64+
simp_all only [isWellTyped, evaluateT, selectionT, schema]
65+
simp_all only [forall_const, Set.mem_setOf_eq, implies_true]
66+
| p rs sq ih =>
67+
intro t h_t
68+
simp_all [isWellTyped, evaluateT, projectionT, schema]
69+
apply projectionDom ⟨sq.schema dbi.schema, evaluateT dbi sq, ih⟩ ?_ h.2
70+
. simp_all only [projectionT, Set.mem_setOf_eq]
71+
| j sq₁ sq₂ ih₁ ih₂ =>
72+
intro t h_t
73+
simp_all only [isWellTyped, forall_const]
74+
apply joinDom
75+
⟨sq₁.schema dbi.schema, evaluateT dbi sq₁, ih₁⟩
76+
⟨sq₂.schema dbi.schema, evaluateT dbi sq₂, ih₂⟩
77+
h_t
78+
| r f sq ih =>
79+
intro t h_t
80+
apply renameDom ⟨sq.schema dbi.schema, evaluateT dbi sq, (by simp_all)⟩ h.2.2
81+
simp_all only [evaluateT, renameT, Set.mem_setOf_eq]
82+
| u sq₁ sq₂ ih =>
83+
intro _ ht
84+
simp [isWellTyped, evaluateT, unionT, schema] at *
85+
cases ht
86+
all_goals simp_all only
87+
| d sq₁ sq₂ ih =>
88+
intro _ ht
89+
simp [isWellTyped, evaluateT, differenceT, schema] at *
90+
cases ht
91+
all_goals simp_all only
9192

9293
/-- Query evaluation for `RelationInstance` -/
9394
def Query.evaluate [DecidableEq α] (dbi : DatabaseInstance ρ α μ) (q : Query ρ α) (h : q.isWellTyped dbi.schema) : RelationInstance α μ :=
9495
⟨
9596
q.schema dbi.schema,
9697
q.evaluateT dbi,
97-
by exact fun t a ↦ evaluate.validSchema q h t a
98+
evaluate.validSchema q h
9899
⟩
99100

100101

@@ -178,4 +179,4 @@ theorem Query.evaluateT.dbi_domain [DecidableEq α] [Nonempty α] {dbi : Databas
178179
| inr ht₂ => exact ih₂ t ht₂
179180

180181
| d q nq ih nih =>
181-
simp_all only [isWellTyped, evaluateT, diffT, Set.mem_diff, implies_true]
182+
simp_all only [isWellTyped, evaluateT, differenceT, Set.mem_diff, implies_true]

‎RelationalAlgebra/RA/RelationalAlgebra.lean‎

Lines changed: 7 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -20,29 +20,27 @@ variable {α μ : Type}
2020
def selectionT (inTuples : Set (α →. μ)) (x y : α) : Set (α →. μ) :=
2121
{t | t ∈ inTuples ∧ t x = t y}
2222

23-
theorem selectionDom {x y t} {inst : RelationInstance α μ} (h : t ∈ selectionT inst.tuples x y) :
24-
PFun.Dom t = inst.schema := by
25-
simp_all only [selectionT, Set.mem_setOf_eq]
26-
all_goals exact inst.validSchema t h.1
27-
2823
/-- Selection on `R : RelationInstance` (`σ (x = y) R`) -/
2924
def selection (inst : RelationInstance α μ) (x y : α) : RelationInstance α μ :=
3025
⟨
3126
inst.schema,
3227
selectionT inst.tuples x y,
33-
fun _ ht ↦ selectionDom ht
28+
by
29+
intro t h
30+
simp_all only [selectionT, Set.mem_setOf_eq]
31+
exact inst.validSchema t h.1
3432
⟩
3533

3634
/-- Difference on `S₁ S₂ : Set` of tuples. Result: tuples `t` where `t ∈ S₁ ∧ t ∉ S₂` -/
3735
@[simp]
38-
def diffT (inTuplesA inTuplesB : Set (α →. μ)) : Set (α →. μ) :=
36+
def differenceT (inTuplesA inTuplesB : Set (α →. μ)) : Set (α →. μ) :=
3937
inTuplesA \ inTuplesB
4038

4139
/-- Difference on `R₁ R₂ : RelationInstance` (`R₁ - R₂`) -/
42-
def diff (inst inst' : RelationInstance α μ) : RelationInstance α μ :=
40+
def difference (inst inst' : RelationInstance α μ) : RelationInstance α μ :=
4341
⟨
4442
inst.schema,
45-
diffT inst.tuples inst'.tuples,
43+
differenceT inst.tuples inst'.tuples,
4644
by
4745
intro t a
4846
exact inst.validSchema t a.1

0 commit comments

Comments
 (0)