Skip to content

Commit c1a58ab

Browse files
Rickerd1234Rickerd1234
committed
Code Quality
1 parent 051a016 commit c1a58ab

4 files changed

Lines changed: 27 additions & 38 deletions

File tree

‎RelationalAlgebra/Equivalence/Equivalence.lean‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -88,7 +88,7 @@ theorem fol_to_ra_eval (brs_disj : folQ.schema ∩ brs = ∅) (brs_depth : 0 + F
8888
simp only [RA.Query.evaluate, FOL.Query.evaluateAdom, RelationInstance.mk.injEq]
8989
apply And.intro
9090
· exact fol_to_ra_query.schema_def folQ
91-
· exact fol_to_ra_query.evalT folQ hμ hdisj hdef brs_disj brs_depth brs_def
91+
· exact fol_to_ra_query.evalT_def folQ hμ hdisj hdef brs_disj brs_depth brs_def
9292

9393
/-- Query expressivity equivalence -/
9494
theorem fol_to_ra (brs : Finset α) (brs_disj : folQ.schema ∩ brs = ∅) (brs_depth : 0 + FOL.depth (toPrenex folQ) < brs.card) (brs_def : default ∉ brs)
@@ -97,4 +97,5 @@ theorem fol_to_ra (brs : Finset α) (brs_disj : folQ.schema ∩ brs = ∅) (brs_
9797
use fol_to_ra_query folQ brs
9898
use fol_to_ra_query.isWellTyped_def folQ brs_disj brs_depth
9999
exact fol_to_ra_eval folQ brs brs_disj brs_depth brs_def hμ hdisj hdef
100+
100101
end FOLtoRA

‎RelationalAlgebra/Equivalence/FOLtoRA/Conversion.lean‎

Lines changed: 1 addition & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -229,15 +229,7 @@ theorem toRA.all_def [Nonempty ↑(adomRs dbi.schema)] [folStruc dbi] [Fintype
229229
by_contra hc'
230230
rw [FreeMap.mem_FRan_add_one_cases (by grind)] at hc'
231231
simp_all
232-
. simp [PFun.ran, t'', Set.subset_def]
233-
intro v a hv
234-
split at hv
235-
. apply right_1
236-
simp [PFun.ran]
237-
use a
238-
. split at hv
239-
. simp [hμ]
240-
. simp at hv
232+
. simp [PFun.ran, t'', Set.subset_def, hμ]
241233

242234
. by_contra hc'
243235
apply hc

‎RelationalAlgebra/Equivalence/FOLtoRA/Prenex.lean‎

Lines changed: 22 additions & 26 deletions
Original file line numberDiff line numberDiff line change
@@ -23,7 +23,7 @@ theorem toPrenex.freeVarFinset_def {q : FOL.Query dbs} : (toPrenex q).freeVarFin
2323
variable [Inhabited α] [Inhabited ρ] [LinearOrder ρ]
2424

2525
/- Proof that `toRA` is well typed for the distinct prenex form cases -/
26-
theorem toRA.isWellTyped_def_IsAtomic [Nonempty ρ] {q : (fol dbs).BoundedFormula α n}
26+
theorem toRA.isWellTyped_def_IsAtomic {q : (fol dbs).BoundedFormula α n}
2727
(hq : q.IsAtomic) (h' : (q.freeVarFinset ∪ FRan (FreeMap n brs)) ⊆ rs)
2828
[Fintype (adomRs dbs)] [Nonempty (adomRs dbs)] :
2929
(toRA q rs brs).isWellTyped dbs := by
@@ -71,7 +71,7 @@ theorem toRA.isWellTyped_def_IsAtomic [Nonempty ρ] {q : (fol dbs).BoundedFormul
7171
cases R with
7272
| R rn => simp [Relations.boundedFormula, toRA, relToRA.isWellTyped_def]
7373

74-
theorem toRA.isWellTyped_def_IsQF [Nonempty ρ] [Fintype (adomRs dbs)] [Nonempty (adomRs dbs)] {q : (fol dbs).BoundedFormula α n}
74+
theorem toRA.isWellTyped_def_IsQF [Fintype (adomRs dbs)] [Nonempty (adomRs dbs)] {q : (fol dbs).BoundedFormula α n}
7575
(hq : q.IsQF) (h' : (q.freeVarFinset ∪ FRan (FreeMap n brs)) ⊆ rs) :
7676
(toRA q rs brs).isWellTyped dbs := by
7777
induction hq with
@@ -86,36 +86,36 @@ theorem toRA.isWellTyped_def_IsQF [Nonempty ρ] [Fintype (adomRs dbs)] [Nonempty
8686
have : q₂.freeVarFinset ∪ FRan (FreeMap n brs) ⊆ rs := Finset.union_subset_right h'
8787
simp_all [adom.isWellTyped_def, adom.schema_def, toRA.schema_def]
8888

89-
theorem toRA.isWellTyped_def_IsPrenex [Nonempty ρ] {q : (fol dbs).BoundedFormula α n}
90-
(hq : q.IsPrenex) (h' : q.freeVarFinset ⊆ rs) (h'' : q.freeVarFinset ∩ brs = ∅) (hn : n + depth q < brs.card)
89+
theorem toRA.isWellTyped_def_IsPrenex {q : (fol dbs).BoundedFormula α n}
90+
(hq : q.IsPrenex) (h'' : q.freeVarFinset ∩ brs = ∅) (hn : n + depth q < brs.card)
9191
[Fintype (adomRs dbs)] [Nonempty (adomRs dbs)] :
92-
(toRA q (rs ∪ FRan (FreeMap n brs)) brs).isWellTyped dbs := by
92+
(toRA q (q.freeVarFinset ∪ FRan (FreeMap n brs)) brs).isWellTyped dbs := by
9393
induction hq with
9494
| of_isQF h_qf => exact isWellTyped_def_IsQF h_qf (by grind)
9595
| all =>
9696
simp [toRA]
9797
simp at hn
9898
rename_i inst_1 n_1 φ h_1 h_ih
9999

100-
have wt := h_ih h' h'' (by grind)
101-
have sch : (rs ∪ (FRan (FreeMap n_1 brs) ∪ FRan (FreeMap (n_1 + 1) brs))) = (rs ∪ FRan (FreeMap (n_1 + 1) brs)) := by rw [FreeMap.FRan_union_add_one (by grind)]
100+
have wt := h_ih h'' (by grind)
101+
have sch : (φ.freeVarFinset ∪ (FRan (FreeMap n_1 brs) ∪ FRan (FreeMap (n_1 + 1) brs))) = (φ.freeVarFinset ∪ FRan (FreeMap (n_1 + 1) brs)) := by rw [FreeMap.FRan_union_add_one (by grind)]
102102

103103
simp only [adom.isWellTyped_def, adom.schema_def, toRA.schema_def, true_and, and_true, *]
104104
exact Finset.union_subset_union_right (FreeMap.FRan_sub_add_one (by grind))
105105

106106
| ex =>
107107
simp [toRA]
108108
rename_i inst_1 n_1 φ h_1 h_ih
109-
simp at h' h'' hn
109+
simp at h'' hn
110110

111-
have wt := h_ih h' h'' (by grind)
112-
have sch : (rs ∪ (FRan (FreeMap n_1 brs) ∪ FRan (FreeMap (n_1 + 1) brs))) = (rs ∪ FRan (FreeMap (n_1 + 1) brs)) := by rw [FreeMap.FRan_union_add_one (by grind)]
111+
have wt := h_ih h'' (by grind)
112+
have sch : (φ.freeVarFinset ∪ (FRan (FreeMap n_1 brs) ∪ FRan (FreeMap (n_1 + 1) brs))) = (φ.freeVarFinset ∪ FRan (FreeMap (n_1 + 1) brs)) := by rw [FreeMap.FRan_union_add_one (by grind)]
113113

114114
simp only [adom.isWellTyped_def, adom.schema_def, toRA.schema_def, true_and, and_true, *]
115-
exact Finset.union_subset_union_right (FreeMap.FRan_sub_add_one (by grind))
115+
exact Finset.union_subset_union_right (FreeMap.FRan_sub_add_one (by simp_all; grind))
116116

117117
/- Proof that `toRA` evaluation is equivalent to the `Set` of tuples of `RealizeDomSet` for the distinct prenex form cases -/
118-
theorem toRA.evalT_def_IsAtomic [Nonempty ρ] [Inhabited μ] [Nonempty ↑(adomRs dbi.schema)] [folStruc dbi] {q : (fol dbi.schema).BoundedFormula α n}
118+
theorem toRA.evalT_def_IsAtomic [Inhabited μ] [Nonempty ↑(adomRs dbi.schema)] [folStruc dbi] {q : (fol dbi.schema).BoundedFormula α n}
119119
(hμ : ∀v, v ∈ dbi.domain) (hq : q.IsAtomic) [Fintype (adomRs dbi.schema)] (h : (q.freeVarFinset ∪ FRan (FreeMap n brs)) ⊆ rs) (hn : n + depth q < brs.card)
120120
(hdisj : disjointSchema brs q) (hdef : default ∉ rs) :
121121
(toRA q rs brs).evaluateT dbi = RealizeDomSet q rs brs := by
@@ -147,7 +147,7 @@ theorem toRA.evalT_def_IsAtomic [Nonempty ρ] [Inhabited μ] [Nonempty ↑(adomR
147147
. apply (hdisj.2)
148148
exact FreeMap.mem_def (by grind)
149149

150-
theorem toRA.evalT_def_IsQF [Nonempty ρ] [Inhabited μ] [folStruc dbi] {q : (fol dbi.schema).BoundedFormula α n}
150+
theorem toRA.evalT_def_IsQF [Inhabited μ] [folStruc dbi] {q : (fol dbi.schema).BoundedFormula α n}
151151
(hμ : ∀v, v ∈ dbi.domain) (hq : q.IsQF) [Fintype (adomRs dbi.schema)] [Nonempty ↑(adomRs dbi.schema)]
152152
(h : (q.freeVarFinset ∪ FRan (FreeMap n brs)) ⊆ rs) (hn : n + depth q < brs.card) (hdisj : disjointSchema brs q) (hdef : default ∉ rs) :
153153
(toRA q rs brs).evaluateT dbi = RealizeDomSet q rs brs := by
@@ -162,7 +162,7 @@ theorem toRA.evalT_def_IsQF [Nonempty ρ] [Inhabited μ] [folStruc dbi] {q : (fo
162162
(ih₁ (Finset.union_subset_iff.mpr ⟨h.1.1, h.2⟩) (by simp at hn; grind) (by simp at hdisj; exact ⟨hdisj.1.1, hdisj.2⟩))
163163
(ih₂ (Finset.union_subset_iff.mpr ⟨h.1.2, h.2⟩) (by simp at hn; grind) (by simp at hdisj; exact ⟨hdisj.1.2, hdisj.2⟩))
164164

165-
theorem toRA.evalT_def_IsPrenex [Nonempty ρ] [Inhabited μ] [folStruc dbi] {q : (fol dbi.schema).BoundedFormula α n} [Fintype (adomRs dbi.schema)] [Nonempty ↑(adomRs dbi.schema)]
165+
theorem toRA.evalT_def_IsPrenex [Inhabited μ] [folStruc dbi] {q : (fol dbi.schema).BoundedFormula α n} [Fintype (adomRs dbi.schema)] [Nonempty ↑(adomRs dbi.schema)]
166166
(hμ : ∀v, v ∈ dbi.domain) (hq : q.IsPrenex) (h' : brs ∩ q.freeVarFinset = ∅) (hn : n + depth q < brs.card) (hdisj : disjointSchema brs q) (hdef : default ∉ q.freeVarFinset ∪ brs) :
167167
(toRA q (q.freeVarFinset ∪ FRan (FreeMap n brs)) brs).evaluateT dbi = RealizeDomSet q (q.freeVarFinset ∪ FRan (FreeMap n brs)) brs := by
168168
induction hq with
@@ -213,27 +213,25 @@ theorem toRA.evalT_def_IsPrenex [Nonempty ρ] [Inhabited μ] [folStruc dbi] {q :
213213

214214
/-- Complete conversion definition, `FOL.Query dbs → RA.Query ρ α` -/
215215
@[simp]
216-
def fol_to_ra_query [Nonempty ρ] (q : FOL.Query dbs) [Fintype (adomRs dbs)] (brs : Finset α) : RA.Query ρ α :=
216+
def fol_to_ra_query (q : FOL.Query dbs) [Fintype (adomRs dbs)] (brs : Finset α) : RA.Query ρ α :=
217217
toRA (toPrenex q) q.schema brs
218218

219219
/-- Conversion schema equivalence proof -/
220220
@[simp]
221-
theorem fol_to_ra_query.schema_def [Nonempty ρ] (q : FOL.Query dbs) [Fintype (adomRs dbs)] : (fol_to_ra_query q brs).schema dbs = q.schema := by
221+
theorem fol_to_ra_query.schema_def (q : FOL.Query dbs) [Fintype (adomRs dbs)] : (fol_to_ra_query q brs).schema dbs = q.schema := by
222222
rw [fol_to_ra_query, BoundedQuery.schema, ← freeVarFinset_toPrenex, toRA.schema_def]
223223

224224
/-- Conversion well-typed query proof -/
225-
theorem fol_to_ra_query.isWellTyped_def [Nonempty ρ] (q : FOL.Query dbs) [Fintype (adomRs dbs)] [Nonempty (adomRs dbs)]
225+
theorem fol_to_ra_query.isWellTyped_def (q : FOL.Query dbs) [Fintype (adomRs dbs)] [Nonempty (adomRs dbs)]
226226
(hbrs : q.schema ∩ brs = ∅) (hdepth : 0 + depth (toPrenex q) < brs.card) :
227227
(fol_to_ra_query q brs).isWellTyped dbs := by
228228
have : (BoundedQuery.toFormula q).toPrenex.freeVarFinset ∪ FRan (FreeMap 0 brs) = (BoundedQuery.toFormula q).toPrenex.freeVarFinset := by simp [FRan]
229229
rw [fol_to_ra_query, BoundedQuery.schema, ← freeVarFinset_toPrenex, ← this]
230-
apply toRA.isWellTyped_def_IsPrenex ?_ ?_ ?_ hdepth
231-
. simp [BoundedFormula.toPrenex_isPrenex]
232-
. simp
230+
apply toRA.isWellTyped_def_IsPrenex q.toFormula.toPrenex_isPrenex ?_ hdepth
233231
. simp; simp [BoundedQuery.schema] at hbrs; grind
234232

235233
/-- Conversion evaluation `Set` tuples equivalence proof (all tuples are restricted to `DatabaseInstance.domain`) -/
236-
theorem fol_to_ra_query.evalT [folStruc dbi] [Fintype (adomRs dbi.schema)] [Nonempty ↑(adomRs dbi.schema)] [Inhabited μ] [Nonempty ρ]
234+
theorem fol_to_ra_query.evalT_def [folStruc dbi] [Fintype (adomRs dbi.schema)] [Nonempty ↑(adomRs dbi.schema)] [Inhabited μ]
237235
(q : FOL.Query dbi.schema) (hμ : ∀v, v ∈ dbi.domain) (hdisj : disjointSchema brs q.toFormula) (hdef : default ∉ q.schema)
238236
(hbrs : q.schema ∩ brs = ∅) (hdepth : 0 + depth (toPrenex q) < brs.card) (hdef' : default ∉ brs) :
239237
RA.Query.evaluateT dbi (fol_to_ra_query q brs) = FOL.Query.evaluateT dbi q ∩ {t | t.ran ⊆ dbi.domain} := by
@@ -244,10 +242,9 @@ theorem fol_to_ra_query.evalT [folStruc dbi] [Fintype (adomRs dbi.schema)] [None
244242
rw [fol_to_ra_query, BoundedQuery.schema]
245243
simp_rw [toPrenex]
246244

247-
have hq := BoundedFormula.toPrenex_isPrenex (BoundedQuery.toFormula q)
248-
have helper : (BoundedQuery.toFormula q).toPrenex.freeVarFinset ∪ FRan (FreeMap 0 brs)
249-
= (BoundedQuery.toFormula q).toPrenex.freeVarFinset := by simp [FRan]
250-
rw [← freeVarFinset_toPrenex, ← helper, toRA.evalT_def_IsPrenex hμ hq ?_ ?_ ?_ ?_]
245+
have hq := q.toFormula.toPrenex_isPrenex
246+
have helper : q.toFormula.toPrenex.freeVarFinset ∪ FRan (FreeMap 0 brs) = q.toFormula.toPrenex.freeVarFinset := by simp [FRan]
247+
rw [← freeVarFinset_toPrenex, ← helper, toRA.evalT_def_IsPrenex hμ hq ?_ hdepth ?_ ?_]
251248

252249
rw [Set.mem_setOf_eq]
253250
simp only [BoundedFormula.realize_toPrenex, RealizeDomSet]
@@ -258,7 +255,6 @@ theorem fol_to_ra_query.evalT [folStruc dbi] [Fintype (adomRs dbi.schema)] [None
258255
. simp
259256
. simp only [BoundedQuery.schema, freeVarFinset_toPrenex] at hbrs ⊢;
260257
rw [Finset.inter_comm, hbrs]
261-
. exact hdepth
262258
. exact ⟨(disjointSchemaL.toPrenex (BoundedQuery.toFormula q)).mpr hdisj.1, hdisj.2⟩
263259
. simp only [freeVarFinset_toPrenex, Finset.mem_union, not_or]
264260
exact ⟨hdef, hdef'⟩

‎RelationalAlgebra/Equivalence/FOLtoRA/RealizeDomSet.lean‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -8,5 +8,5 @@ The set of tuples (`t : α →. μ`) satisfying a `BoundedFormula` with given `t
88
-/
99
@[simp]
1010
def RealizeDomSet {dbi : DatabaseInstance ρ α μ} [LinearOrder α] [Inhabited α] [folStruc dbi] [Inhabited μ]
11-
(q : (fol dbi.schema).BoundedFormula α n) (rs brs : Finset α) : Set (α →. μ) :=
12-
{t : α →. μ | ∃h : t.Dom = rs, q.Realize (TupleToFun h) (TupleToFun h ∘ FreeMap n brs) ∧ t.ran ⊆ dbi.domain}
11+
(f : (fol dbi.schema).BoundedFormula α n) (rs brs : Finset α) : Set (α →. μ) :=
12+
{t : α →. μ | ∃h : t.Dom = rs, f.Realize (TupleToFun h) (TupleToFun h ∘ FreeMap n brs) ∧ t.ran ⊆ dbi.domain}

0 commit comments

Comments
 (0)