Removed Unused Files & Minor Refactoring

Author: Rickerd1234

Design.md

@@ -8,28 +8,17 @@ Relational Algebra (RA) is the theoretical foundation of SQL and a cornerstone o
 
 This project formalizes:
 
-- The core constructs of Relational Algebra (e.g. selection, projection, join, union, difference, renaming).
+- The core constructs of Relational Algebra (i.e. selection, projection, join, renaming, union, difference).
 - A corresponding fragment of First-Order Logic with active domain semantics.
 - The expressive equivalence between RA and FOL under this interpretation.
 
 The formalization is developed in [Lean 4](https://leanprover.github.io), using its dependent type theory framework and the [mathlib4](https://github.com/leanprover-community/mathlib4) library where possible.
 
 ## ✅ Goals
 
-- ✅ Formalize SPJR algebra.
-- ✅ Formalize SPJRU algebra.
-- ✅ Formalize complete relational algebra.
+- ✅ Formalize relational algebra.
 - ✅ Formalize equivalent fragments of FOL.
 - ✅ Prove equivalence theorems between RA and FOL expressions.
 - 🔄 Ensure reusable and well-documented Lean definitions.
 
-## 🧠 Design Rationale
-
-The design decisions behind the formalization — such as how tuples, schemas, and relational operations are represented in Lean — are documented in the [`Design.md`](./Design.md) file. This includes:
-
-- Key trade-offs (e.g., bundled vs. unbundled representations)
-- Justification for using partial functions and specific Lean constructs
-
-Reading `Design.md` is recommended if you're contributing to the codebase or want to understand the reasoning behind implementation choices.
-
 ---

README.md

@@ -1,5 +1,4 @@
 import RelationalAlgebra.Equivalence.FOLtoRA.Adom
-import RelationalAlgebra.Equivalence.FOLtoRA.FreshAtts
 import RelationalAlgebra.Equivalence.FOLtoRA.FRan
 import RelationalAlgebra.Equivalence.FOLtoRA.Relation
 import RelationalAlgebra.Equivalence.FOLtoRA.Term
@@ -91,15 +90,15 @@ variable [Inhabited ρ] [LinearOrder ρ]
 /- Proof `toRA` evaluation for `Set` of tuples to be equivalent to `RealizeDomSet` for the distinct cases -/
 theorem toRA.falsum_def [Nonempty ↑(adomRs dbi.schema)] [folStruc dbi (μ := μ)] [Fintype ↑(adomRs dbi.schema)] :
     (toRA (BoundedFormula.falsum (L := fol dbi.schema) (n := n)) rs brs).evaluateT dbi =
-      {t | ∃h, RealizeDomSet (BoundedFormula.falsum (L := fol dbi.schema) (n := n)) rs brs t h} := by
+      RealizeDomSet (BoundedFormula.falsum (L := fol dbi.schema) (n := n)) rs brs := by
         have : (RA.Query.evaluateT dbi (adom dbi.schema rs)) \ (RA.Query.evaluateT dbi (adom dbi.schema rs)) = ∅ := Set.diff_self
         simp_rw [toRA, RA.Query.evaluateT, differenceT, this]
         simp [RealizeDomSet, BoundedFormula.Realize]
 
 
 theorem toRA.equal_def [Nonempty ↑(adomRs dbi.schema)] [Fintype ↑(adomRs dbi.schema)] [folStruc dbi (μ := μ)] {t₁ t₂ : (fol dbi.schema).Term (α ⊕ Fin n)}
   (h : (t₁ =' t₂).freeVarFinset ∪ FRan (FreeMap n brs) ⊆ rs) :
-    (toRA (t₁ =' t₂) rs brs).evaluateT dbi = {t | ∃h, RealizeDomSet (t₁ =' t₂) rs brs t h} := by
+    (toRA (t₁ =' t₂) rs brs).evaluateT dbi = RealizeDomSet (t₁ =' t₂) rs brs := by
       simp_rw [Term.bdEqual, toRA, RA.Query.evaluateT, selectionT]
       simp_rw [RealizeDomSet]
 
@@ -146,9 +145,9 @@ theorem toRA.equal_def [Nonempty ↑(adomRs dbi.schema)] [Fintype ↑(adomRs dbi
 
 theorem toRA.imp_def [Nonempty ↑(adomRs dbi.schema)] [folStruc dbi (μ := μ)] [Fintype ↑(adomRs dbi.schema)]
   (hμ : ∀v : μ, v ∈ dbi.domain)
-  (ih₁ : (toRA (dbs := dbi.schema) q₁ rs brs).evaluateT dbi = {t | ∃h, RealizeDomSet q₁ rs brs t h})
-  (ih₂ : (toRA (dbs := dbi.schema) q₂ rs brs).evaluateT dbi = {t | ∃h, RealizeDomSet q₂ rs brs t h}) :
-    (toRA (q₁.imp q₂) rs brs).evaluateT dbi = {t | ∃h, RealizeDomSet (q₁.imp q₂) rs brs t h} := by
+  (ih₁ : (toRA (dbs := dbi.schema) q₁ rs brs).evaluateT dbi = RealizeDomSet q₁ rs brs)
+  (ih₂ : (toRA (dbs := dbi.schema) q₂ rs brs).evaluateT dbi = RealizeDomSet q₂ rs brs) :
+    (toRA (q₁.imp q₂) rs brs).evaluateT dbi = RealizeDomSet (q₁.imp q₂) rs brs := by
       ext t
       simp only [toRA, RA.Query.evaluateT, differenceT, adom.complete_def, Set.mem_diff, Set.mem_setOf_eq,
         not_and, not_not, RealizeDomSet, BoundedFormula.realize_imp, exists_and_right]
@@ -157,21 +156,21 @@ theorem toRA.imp_def [Nonempty ↑(adomRs dbi.schema)] [folStruc dbi (μ := μ)]
         TupleToFun.tuple_eq_self]
       apply Iff.intro
       · intro a_1
-        simp_all only [Finset.coe_inj, TupleToFun.tuple_eq_self, implies_true, exists_const, and_self]
+        simp_all only [implies_true, exists_const, and_self]
       · intro ⟨⟨w_1, h_1⟩, right⟩
         simp_all [Finset.coe_inj, TupleToFun.tuple_eq_self, implies_true, and_self]
         apply adom.exists_tuple_from_value hμ
 
 theorem toRA.not_def [Nonempty ↑(adomRs dbi.schema)] [Fintype ↑(adomRs dbi.schema)] [folStruc dbi (μ := μ)]
   (hμ : ∀v : μ, v ∈ dbi.domain)
-  (ih : (toRA (dbs := dbi.schema) q rs brs).evaluateT dbi = {t | ∃h, RealizeDomSet q rs brs t h}) :
-    (toRA q.not rs brs).evaluateT dbi = {t | ∃h, RealizeDomSet (q.not) rs brs t h} := by
+  (ih : (toRA (dbs := dbi.schema) q rs brs).evaluateT dbi = RealizeDomSet q rs brs) :
+    (toRA q.not rs brs).evaluateT dbi = RealizeDomSet (q.not) rs brs := by
       exact imp_def hμ ih falsum_def
 
 theorem toRA.all_def [Nonempty ↑(adomRs dbi.schema)] [folStruc dbi (μ := μ)] [Fintype ↑(adomRs dbi.schema)] {q : (fol dbi.schema).BoundedFormula α (n + 1)}
   (hμ : ∀v : μ, v ∈ dbi.domain) (hn : n + depth (∀'q) < brs.card) (h : (FreeMap (n + 1) brs) (Fin.last n) ∉ q.freeVarFinset)
-  (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}) :
-    (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
+  (ih : (toRA q (q.freeVarFinset ∪ FRan (FreeMap (n + 1) brs)) brs).evaluateT dbi = RealizeDomSet q (q.freeVarFinset ∪ FRan (FreeMap (n + 1) brs)) brs) :
+    (toRA q.all (q.freeVarFinset ∪ FRan (FreeMap n brs)) brs).evaluateT dbi = RealizeDomSet (q.all) (q.freeVarFinset ∪ FRan (FreeMap n brs)) brs := by
       simp only [toRA, RA.Query.evaluateT, Finset.union_assoc, differenceT]
       rw [FreeMap.FRan_union_add_one (by grind), ih]
 

RelationalAlgebra/Equivalence/FOLtoRA/Conversion.lean

@@ -1,12 +1,10 @@
 import RelationalAlgebra.Equivalence.FOLtoRA.FRan
-import RelationalAlgebra.Equivalence.FOLtoRA.FreshAtts
 import RelationalAlgebra.FOL.ModelTheoryExtensions
 
 /-
 To simplify the conversion and proof, we decided to allow for the assumption that the attributes used to represent the bound variables (`brs`)
   is disjoint from the named attributes used in any of the relations AND there is no intersection between free variables and relation attributes used in the query.
-This assumption is a short-cut, given we use `FreshAtts` to generate `brs` which avoids these variables.
-However, due to deadlines we decided to leave this proof as future work.
+This assumption simplifies the proof without real loss of generality, since in practice renaming of attributes/variables could resolve the issues that would occur.
 -/
 
 open FOL FirstOrder Language Term RM

RelationalAlgebra/Equivalence/FOLtoRA/Disjoint.lean

@@ -1,5 +1,4 @@
 import RelationalAlgebra.Equivalence.FOLtoRA.FRan
-import RelationalAlgebra.Equivalence.FOLtoRA.FreshAtts
 import RelationalAlgebra.FOL.ModelTheoryExtensions
 
 /-

RelationalAlgebra/Equivalence/FOLtoRA/FreshAtts.lean

@@ -1,6 +1,5 @@
 import RelationalAlgebra.Equivalence.FOLtoRA.Adom
 import RelationalAlgebra.Equivalence.FOLtoRA.Disjoint
-import RelationalAlgebra.Equivalence.FOLtoRA.FreshAtts
 import RelationalAlgebra.Equivalence.FOLtoRA.FRan
 import RelationalAlgebra.Equivalence.FOLtoRA.NonemptyR
 import RelationalAlgebra.Equivalence.FOLtoRA.Conversion
@@ -116,12 +115,11 @@ theorem toRA.isWellTyped_def_IsPrenex [Nonempty ρ] {q : (fol dbs).BoundedFormul
         simp only [adom.isWellTyped_def, adom.schema_def, toRA.schema_def, true_and, and_true, *]
         exact Finset.union_subset_union_right (FreeMap.FRan_sub_add_one (by grind))
 
-/- Proof that `toRA` evaluation is equivalent to the `Set` of tuples satisfying `RealizeDomSet` for the distinct prenex form cases -/
+/- Proof that `toRA` evaluation is equivalent to the `Set` of tuples of `RealizeDomSet` for the distinct prenex form cases -/
 theorem toRA.evalT_def_IsAtomic [Nonempty ρ] [Inhabited μ] [Nonempty ↑(adomRs dbi.schema)] [folStruc dbi] {q : (fol dbi.schema).BoundedFormula α n}
   (hq : q.IsAtomic) [Fintype (adomRs dbi.schema)] (h : (q.freeVarFinset ∪ FRan (FreeMap n brs)) ⊆ rs) (hn : n + depth q < brs.card)
   (hdisj : disjointSchema brs q) (hdef : default ∉ rs) (hne : NonemptyR q) :
-    (toRA q rs brs).evaluateT dbi =
-      {t | ∃h, RealizeDomSet q rs brs t h} := by
+    (toRA q rs brs).evaluateT dbi = RealizeDomSet q rs brs := by
       induction hq with
       | equal t₁ t₂ => exact equal_def h
       | rel R ts =>
@@ -153,8 +151,7 @@ theorem toRA.evalT_def_IsAtomic [Nonempty ρ] [Inhabited μ] [Nonempty ↑(adomR
 theorem toRA.evalT_def_IsQF [Nonempty ρ] [Inhabited μ] [folStruc dbi] {q : (fol dbi.schema).BoundedFormula α n}
   (hμ : ∀v, v ∈ dbi.domain) (hq : q.IsQF) [Fintype (adomRs dbi.schema)] [Nonempty ↑(adomRs dbi.schema)]
   (h : (q.freeVarFinset ∪ FRan (FreeMap n brs)) ⊆ rs) (hn : n + depth q < brs.card) (hdisj : disjointSchema brs q) (hdef : default ∉ rs) (hne : NonemptyR q) :
-    (toRA q rs brs).evaluateT dbi =
-      {t | ∃h, RealizeDomSet q rs brs t h} := by
+    (toRA q rs brs).evaluateT dbi = RealizeDomSet q rs brs := by
       induction hq with
       | falsum => exact falsum_def
       | of_isAtomic h_at => exact toRA.evalT_def_IsAtomic h_at h hn hdisj hdef hne
@@ -168,8 +165,7 @@ theorem toRA.evalT_def_IsQF [Nonempty ρ] [Inhabited μ] [folStruc dbi] {q : (fo
 
 theorem toRA.evalT_def_IsPrenex [Nonempty ρ] [Inhabited μ] [folStruc dbi] {q : (fol dbi.schema).BoundedFormula α n} [Fintype (adomRs dbi.schema)] [Nonempty ↑(adomRs dbi.schema)]
   (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) (hne : NonemptyR q) :
-    (toRA q (q.freeVarFinset ∪ FRan (FreeMap n brs)) brs).evaluateT dbi =
-      {t | ∃h, RealizeDomSet q (q.freeVarFinset ∪ FRan (FreeMap n brs)) brs t h} := by
+    (toRA q (q.freeVarFinset ∪ FRan (FreeMap n brs)) brs).evaluateT dbi = RealizeDomSet q (q.freeVarFinset ∪ FRan (FreeMap n brs)) brs := by
         induction hq with
         | of_isQF hqf =>
           rename_i n' q

RelationalAlgebra/Equivalence/FOLtoRA/NonemptyR.lean

@@ -4,10 +4,9 @@ import RelationalAlgebra.Equivalence.FOLtoRA.FRan
 open RM FOL FirstOrder Language
 
 /--
-Whether a `BoundedFormula` is satisfied by a tuple `t` given `t.Dom = rs`
-  AND whether all values of `t` are part of the active domain.
+The set of tuples (`t : α →. μ`) satisfying a `BoundedFormula` with given `t.Dom = rs` and `t.ran ⊆ dbi.domain`.
 -/
 @[simp]
 def RealizeDomSet {dbi : DatabaseInstance ρ α μ} [LinearOrder α] [Inhabited α] [folStruc dbi] [Inhabited μ]
-  (q : (fol dbi.schema).BoundedFormula α n) (rs brs : Finset α) (t : α →. μ) (h : t.Dom = rs) : Prop :=
-    q.Realize (TupleToFun h) (TupleToFun h ∘ FreeMap n brs) ∧ t.ran ⊆ dbi.domain
+  (q : (fol dbi.schema).BoundedFormula α n) (rs brs : Finset α) : Set (α →. μ) :=
+    {t : α →. μ | ∃h : t.Dom = rs, q.Realize (TupleToFun h) (TupleToFun h ∘ FreeMap n brs) ∧ t.ran ⊆ dbi.domain}