Remove NonEmptyR Assumption

Author: Rickerd1234

RelationalAlgebra/Equivalence/Equivalence.lean

@@ -73,7 +73,6 @@ Requires:
 - The value `default : α` is not contained in `brs`
 - `default` does not appear in the free variables of the query
 - `brs` is disjoint from all relation schemas and all relation schemas are disjoint from the free variables used for that relation
-- All relations referenced by the query have nonempty schemas (`FOL.NonemptyR folQ.toFormula`)
 -/
 section FOLtoRA
 
@@ -84,19 +83,18 @@ variable {ρ α μ : Type} [Inhabited α] [Inhabited ρ] [LinearOrder α] [Linea
 
 /-- Query evaluation equivalence for `RelationInstance` -/
 theorem fol_to_ra_eval (brs_disj : folQ.schema ∩ brs = ∅) (brs_depth : 0 + FOL.depth (toPrenex folQ) < brs.card) (brs_def : default ∉ brs)
-  (hμ : ∀v, v ∈ dbi.domain) (hdisj : FOL.disjointSchema brs (folQ.toFormula)) (hdef : default ∉ folQ.schema) (hne : FOL.NonemptyR folQ.toFormula) :
+  (hμ : ∀v, v ∈ dbi.domain) (hdisj : FOL.disjointSchema brs (folQ.toFormula)) (hdef : default ∉ folQ.schema) :
     (fol_to_ra_query folQ brs).evaluate dbi (fol_to_ra_query.isWellTyped_def folQ brs_disj brs_depth) = folQ.evaluateAdom dbi := by
       simp only [RA.Query.evaluate, FOL.Query.evaluateAdom, RelationInstance.mk.injEq]
       apply And.intro
       · exact fol_to_ra_query.schema_def folQ
-      · exact fol_to_ra_query.evalT folQ hμ hdisj hdef hne brs_disj brs_depth brs_def
+      · exact fol_to_ra_query.evalT folQ hμ hdisj hdef brs_disj brs_depth brs_def
 
 /-- Query expressivity equivalence -/
 theorem fol_to_ra (brs : Finset α) (brs_disj : folQ.schema ∩ brs = ∅) (brs_depth : 0 + FOL.depth (toPrenex folQ) < brs.card) (brs_def : default ∉ brs)
-  (hμ : ∀v, v ∈ dbi.domain) (hdisj : FOL.disjointSchema brs (folQ.toFormula)) (hdef : default ∉ folQ.schema) (hne : FOL.NonemptyR folQ.toFormula) :
+  (hμ : ∀v, v ∈ dbi.domain) (hdisj : FOL.disjointSchema brs (folQ.toFormula)) (hdef : default ∉ folQ.schema) :
     ∃raQ : RA.Query _ _, ∃(h' : raQ.isWellTyped dbi.schema), raQ.evaluate dbi h' = folQ.evaluateAdom dbi := by
       use fol_to_ra_query folQ brs
       use fol_to_ra_query.isWellTyped_def folQ brs_disj brs_depth
-      exact fol_to_ra_eval folQ brs brs_disj brs_depth brs_def hμ hdisj hdef hne
-
+      exact fol_to_ra_eval folQ brs brs_disj brs_depth brs_def hμ hdisj hdef
 end FOLtoRA

RelationalAlgebra/Equivalence/FOLtoRA/Adom.lean

@@ -52,23 +52,6 @@ theorem RA.Query.foldr_union_evalT (xs : List β) (qb : β → RA.Query ρ α) (
 def adomRs (dbs : ρ → Finset α) : Set ρ :=
   {rn | dbs rn ≠ ∅}
 
-/-- All attributes in the database schema -/
-def adomAtts (dbs : ρ → Finset α) : Set α :=
-  {a | ∃rn, a ∈ dbs rn}
-
-/-- Helper to demonstrate that Fintype adomRs → Fintype adomAtts -/
-theorem adomAtts.biUnion_adomRs : ra ∈ adomAtts dbs ↔ ∃rn ∈ adomRs dbs, ra ∈ dbs rn := by
-  simp [adomRs, adomAtts]
-  grind
-
-/-- Fintype adomRs → Fintype adomAtts -/
-instance {dbs : ρ → Finset α} [Fintype (adomRs dbs)] [DecidableEq α] : Fintype (adomAtts dbs) := by
-  have : adomAtts dbs = {ra | ∃rn ∈ adomRs dbs, ra ∈ dbs rn} := by
-    simp [Set.ext_iff, adomAtts.biUnion_adomRs]
-  rw [this]
-  apply Fintype.ofFinset ((adomRs dbs).toFinset.biUnion (λ r => dbs r))
-  simp only [Finset.mem_biUnion, Set.mem_toFinset, Set.mem_setOf_eq, implies_true]
-
 
 /-- Empty tuple for a relation -/
 def EmptyTupleFromRelation (rn : ρ) : RA.Query ρ α :=

RelationalAlgebra/Equivalence/FOLtoRA/NonemptyR.lean

@@ -1,7 +1,6 @@
 import RelationalAlgebra.Equivalence.FOLtoRA.Adom
 import RelationalAlgebra.Equivalence.FOLtoRA.Disjoint
 import RelationalAlgebra.Equivalence.FOLtoRA.FRan
-import RelationalAlgebra.Equivalence.FOLtoRA.NonemptyR
 import RelationalAlgebra.Equivalence.FOLtoRA.Conversion
 import RelationalAlgebra.FOL.Schema
 import RelationalAlgebra.FOL.Evaluate
@@ -117,15 +116,15 @@ theorem toRA.isWellTyped_def_IsPrenex [Nonempty ρ] {q : (fol dbs).BoundedFormul
 
 /- 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) :
+  (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)
+  (hdisj : disjointSchema brs q) (hdef : default ∉ rs) :
     (toRA q rs brs).evaluateT dbi = RealizeDomSet q rs brs := by
       induction hq with
       | equal t₁ t₂ => exact equal_def h
       | rel R ts =>
         cases R with
         | R rn =>
-          apply relToRA.evalT_def h hdef ?_ hne
+          apply relToRA.evalT_def h hdef ?_ hμ
 
           simp [Relations.boundedFormula, disjointSchema, Finset.ext_iff] at hdisj
 
@@ -150,21 +149,21 @@ 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) :
+  (h : (q.freeVarFinset ∪ FRan (FreeMap n brs)) ⊆ rs) (hn : n + depth q < brs.card) (hdisj : disjointSchema brs q) (hdef : default ∉ rs) :
     (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
+      | of_isAtomic h_at => exact toRA.evalT_def_IsAtomic hμ h_at h hn hdisj hdef
 
       | imp h_qf₁ h_qf₂ ih₁ ih₂ =>
         rw [Finset.union_subset_iff, BoundedFormula.freeVarFinset, Finset.union_subset_iff] at h
 
         exact toRA.imp_def hμ
-          (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⟩) (hne.1))
-          (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⟩) (hne.2))
+          (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⟩))
+          (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⟩))
 
 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) :
+  (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) :
     (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 =>
@@ -173,14 +172,14 @@ theorem toRA.evalT_def_IsPrenex [Nonempty ρ] [Inhabited μ] [folStruc dbi] {q :
             simp at ⊢ hdef;
             apply And.intro hdef.1 (FreeMap.notMem_notMem_FRan ?_ hdef.2)
             grind
-          exact evalT_def_IsQF hμ hqf (fun ⦃a⦄ a ↦ a) hn hdisj hdef' hne
+          exact evalT_def_IsQF hμ hqf (fun ⦃a⦄ a ↦ a) hn hdisj hdef'
 
         | all hφ ih =>
           apply all_def hμ (by grind) ?_
 
           . simp [← Nat.add_assoc] at hn
 
-            exact ih h' hn hdisj hdef hne
+            exact ih h' hn hdisj hdef
 
           . simp [Finset.eq_empty_iff_forall_notMem] at h'
             apply h'
@@ -200,10 +199,10 @@ theorem toRA.evalT_def_IsPrenex [Nonempty ρ] [Inhabited μ] [folStruc dbi] {q :
 
           . rw [helper φ]
             simp_rw [BoundedFormula.freeVarFinset, Finset.union_empty] at h' ⊢ hdef
-            simp at hdisj hne
+            simp at hdisj
             simp [← Nat.add_assoc] at hn
 
-            exact ih h' hn hdisj hdef hne
+            exact ih h' hn hdisj hdef
 
           . simp [Finset.eq_empty_iff_forall_notMem] at h'
             simp
@@ -235,7 +234,7 @@ theorem fol_to_ra_query.isWellTyped_def [Nonempty ρ] (q : FOL.Query dbs) [Finty
 
 /-- Conversion evaluation `Set` tuples equivalence proof (all tuples are restricted to `DatabaseInstance.domain`) -/
 theorem fol_to_ra_query.evalT [folStruc dbi] [Fintype (adomRs dbi.schema)] [Nonempty ↑(adomRs dbi.schema)] [Inhabited μ] [Nonempty ρ]
-  (q : FOL.Query dbi.schema) (hμ : ∀v, v ∈ dbi.domain) (hdisj : disjointSchema brs q.toFormula) (hdef : default ∉ q.schema) (hne : NonemptyR q.toFormula)
+  (q : FOL.Query dbi.schema) (hμ : ∀v, v ∈ dbi.domain) (hdisj : disjointSchema brs q.toFormula) (hdef : default ∉ q.schema)
   (hbrs : q.schema ∩ brs = ∅)  (hdepth : 0 + depth (toPrenex q) < brs.card) (hdef' : default ∉ brs) :
     RA.Query.evaluateT dbi (fol_to_ra_query q brs) = FOL.Query.evaluateT dbi q ∩ {t | t.ran ⊆ dbi.domain} := by
       rw [FOL.Query.evaluateT, Set.ext_iff]
@@ -248,7 +247,7 @@ theorem fol_to_ra_query.evalT [folStruc dbi] [Fintype (adomRs dbi.schema)] [None
       have hq := BoundedFormula.toPrenex_isPrenex (BoundedQuery.toFormula q)
       have helper : (BoundedQuery.toFormula q).toPrenex.freeVarFinset ∪ FRan (FreeMap 0 brs)
         = (BoundedQuery.toFormula q).toPrenex.freeVarFinset := by simp [FRan]
-      rw [← freeVarFinset_toPrenex, ← helper, toRA.evalT_def_IsPrenex hμ hq ?_ ?_ ?_ ?_ ?_]
+      rw [← freeVarFinset_toPrenex, ← helper, toRA.evalT_def_IsPrenex hμ hq ?_ ?_ ?_ ?_]
 
       rw [Set.mem_setOf_eq]
       simp only [BoundedFormula.realize_toPrenex, RealizeDomSet]
@@ -263,4 +262,3 @@ theorem fol_to_ra_query.evalT [folStruc dbi] [Fintype (adomRs dbi.schema)] [None
       . exact ⟨(disjointSchemaL.toPrenex (BoundedQuery.toFormula q)).mpr hdisj.1, hdisj.2⟩
       . simp only [freeVarFinset_toPrenex, Finset.mem_union, not_or]
         exact ⟨hdef, hdef'⟩
-      . exact (NonemptyR.toPrenex (BoundedQuery.toFormula q)).mpr hne

RelationalAlgebra/Equivalence/FOLtoRA/Prenex.lean

@@ -883,7 +883,7 @@ theorem relToRA.isWellTyped_def [Nonempty ↑(adomRs dbs)] {ts : Fin (dbs rn).ca
     simp [relToRA, relJoinsMin.isWellTyped_def, adom.isWellTyped_def, adom.schema_def]
 
 theorem relToRA.evalT_def {dbi : DatabaseInstance ρ α μ} [Nonempty (adomRs dbi.schema)] [Fintype (adomRs dbi.schema)] [folStruc dbi] [Inhabited μ] {ts : Fin (dbi.schema rn).card → (fol dbi.schema).Term (α ⊕ Fin n)}
-  (hrs : (Finset.univ.biUnion fun i ↦ (ts i).varFinsetLeft) ∪ FRan (FreeMap n brs) ⊆ rs) (hu : default ∉ rs) (hdisj : (dbi.schema rn) ∩ (dbi.schema rn).image (renamer ts brs) = ∅) (hne : dbi.schema rn ≠ ∅) :
+  (hrs : (Finset.univ.biUnion fun i ↦ (ts i).varFinsetLeft) ∪ FRan (FreeMap n brs) ⊆ rs) (hu : default ∉ rs) (hdisj : (dbi.schema rn) ∩ (dbi.schema rn).image (renamer ts brs) = ∅) (hμ : ∀ (v : μ), v ∈ dbi.domain) :
     RA.Query.evaluateT dbi (relToRA ts rs brs) = RealizeDomSet (Relations.boundedFormula (relations.R rn) ts) rs brs := by
       simp_rw [RealizeDomSet, BoundedFormula.realize_rel]
       simp_rw [folStruc_apply_RelMap, ArityToTuple.def_dite, exists_and_right]
@@ -997,9 +997,6 @@ theorem relToRA.evalT_def {dbi : DatabaseInstance ρ α μ} [Nonempty (adomRs db
             . use t
               apply And.intro
               . simp [w_1, right]
-                use rn
-                apply And.intro
-                . simp [adomRs, hne]
-                . use t ∘ renamer ts brs
+                apply adom.exists_tuple_from_value hμ
               . exact joinSingleT.restrict t
           . simp [Part.eq_none_iff', Part.dom_iff_mem, ← PFun.mem_dom, w_1]