Simplified FOL Relation Implementation

Author: Rickerd1234

RelationalAlgebra/Equivalence/FOLtoRA/Relation.lean

@@ -887,7 +887,6 @@ theorem relToRA.evalT_def {dbi : DatabaseInstance ρ α μ} [Nonempty (adomRs db
     RA.Query.evaluateT dbi (relToRA ts rs brs) =
     {t | ∃h, RealizeDomSet (μ := μ) (Relations.boundedFormula (relations.R rn) ts) rs brs t h} := by
       simp_rw [RealizeDomSet, BoundedFormula.realize_rel]
-      rw [← fol.Rel]
       simp_rw [folStruc_apply_RelMap, ArityToTuple.def_dite, exists_and_right]
 
       have h₁ : ∀ (i : Fin (dbi.schema rn).card), TermtoAtt brs (ts i) ∈ rs := by

RelationalAlgebra/Equivalence/RAtoFOL/Relation.lean

@@ -7,12 +7,11 @@ theorem ra_to_fol_evalT.R_def.mp :
     ∀t, (ra_to_fol_query dbi.schema (.R rn)).RealizeMin dbi t → t ∈ RA.Query.evaluateT dbi (.R rn) := by
       intro t
       simp_all only [FOL.Query.RealizeMin, FOL.BoundedQuery.Realize, ra_to_fol_query,
-        FOL.BoundedQuery.toFormula.eq_1, FOL.fol.Rel,
-        FirstOrder.Language.BoundedFormula.realize_rel, Function.comp_apply, FOL.outVar.def,
-        FirstOrder.Language.Term.realize_var, Sum.elim_inl, FOL.BoundedQuery.schema.R_def,
-        FirstOrder.Language.Term.varFinsetLeft.eq_1, Finset.mem_singleton,
-        RM.RelationSchema.Dom_sub_fromIndex, Finset.toFinset_coe, RA.Query.evaluateT,
-        forall_exists_index]
+        FOL.BoundedQuery.toFormula.eq_1, FirstOrder.Language.BoundedFormula.realize_rel,
+        Function.comp_apply, FOL.outVar.def, FirstOrder.Language.Term.realize_var, Sum.elim_inl,
+        FOL.BoundedQuery.schema.R_def, FirstOrder.Language.Term.varFinsetLeft.eq_1,
+        Finset.mem_singleton, RM.RelationSchema.Dom_sub_fromIndex, Finset.toFinset_coe,
+        RA.Query.evaluateT, forall_exists_index]
       intro h a_1
       rw [@FOL.folStruc.RelMap_R] at a_1
       convert a_1

RelationalAlgebra/FOL/ModelTheory.lean

@@ -115,11 +115,6 @@ def Language.fol (dbs : ρ → Finset α) : Language :=
     Relations := relations dbs }
   deriving Language.IsRelational
 
-@[simp]
-def fol.Rel {dbs: ρ → Finset α} (rn: ρ) : (Language.fol dbs).Relations (dbs rn).card :=
-  relations.R rn
-
-
 open Language
 
 section struc
@@ -142,8 +137,8 @@ class folStruc (dbi : DatabaseInstance ρ α μ) extends (fol dbi.schema).Struct
         )
 
 @[simp]
-theorem folStruc_apply_RelMap (dbi : DatabaseInstance ρ α μ) [folStruc dbi] {rn} {va : Fin (dbi.schema rn).card → μ} :
-  Structure.RelMap (fol.Rel rn) va ↔ ArityToTuple va ∈ (dbi.relations rn).tuples
+theorem folStruc_apply_RelMap (dbi : DatabaseInstance ρ α μ) [s : folStruc dbi] {rn} {va : Fin (dbi.schema rn).card → μ} :
+  s.RelMap (.R rn) va ↔ ArityToTuple va ∈ (dbi.relations rn).tuples
     := (folStruc.RelMap_R rn va)
 
 @[simp]

RelationalAlgebra/FOL/Query.lean

@@ -34,7 +34,7 @@ def BoundedQuery.exs : ∀ {n}, BoundedQuery dbs n → Query dbs
 /-- `BoundedQuery` conversion to `BoundedFormula`. -/
 @[simp]
 def BoundedQuery.toFormula : (q : BoundedQuery dbs n) → (fol dbs).BoundedFormula α n
-  | .R name vMap => Relations.boundedFormula (fol.Rel name) vMap
+  | .R name vMap => Relations.boundedFormula (.R name) vMap
   | .tEq t₁ t₂ => .equal t₁ t₂
   | .and q1 q2 => q1.toFormula ⊓ q2.toFormula
   | .ex q => .ex q.toFormula

RelationalAlgebra/FOL/RealizeProperties.lean

@@ -16,7 +16,7 @@ theorem BoundedFormula.Realize.equiv [folStruc dbi] {q : (fol dbi.schema).Bounde
         next rn =>
           simp at ht
           rw [BoundedFormula.Realize, BoundedFormula.Realize]
-          rw [← fol.Rel, folStruc_apply_RelMap, folStruc_apply_RelMap]
+          rw [folStruc_apply_RelMap, folStruc_apply_RelMap]
           have : (fun i ↦ realize (Sum.elim t₁ iv₁) (ts i)) = (fun i ↦ realize (Sum.elim t₂ iv₂) (ts i)) := by
             ext i
             have ⟨k, hk⟩ := Term.cases (ts i)
@@ -78,7 +78,7 @@ theorem BoundedQuery.Realize.enlarge [folStruc dbi] {rs rs' : Finset α} {tup tu
   : q.Realize dbi (TupleToFun h'.symm) iv ↔ q.Realize dbi (TupleToFun h.symm) iv := by
     induction q with
     | R rn vMap =>
-      simp only [Realize, toFormula, fol.Rel, BoundedFormula.realize_rel, folStruc.RelMap_R,
+      simp only [Realize, toFormula, BoundedFormula.realize_rel, folStruc.RelMap_R,
         ArityToTuple.def_dite]
       rw [@iff_eq_eq]
       apply congr rfl
@@ -225,7 +225,7 @@ theorem BoundedQuery.Realize.restrict [folStruc dbi] {rs : Finset α} {q : Bound
 
     induction q with
     | R rn ts =>
-        simp_all only [toFormula, fol.Rel, BoundedFormula.realize_rel]
+        simp_all only [toFormula, BoundedFormula.realize_rel]
         simp only [folStruc.RelMap_R, iff_eq_eq]
         apply congr rfl
         ext a v