Removed BoundedQuery.or Constructor

Author: Rickerd1234

RelationalAlgebra/Equivalence/RAtoFOL/Conversion.lean

@@ -47,5 +47,6 @@ theorem ra_to_fol_query_schema {dbs : ρ → Finset α} {raQ : RA.Query ρ α} (
         FirstOrder.Language.Term.varFinsetLeft, Finset.union_singleton, Finset.union_insert,
         Finset.insert_eq_of_mem, RA.Query.schema]
 
-    | _ => simp_all only [RA.Query.isWellTyped, ra_to_fol_query, FOL.BoundedQuery.schema.and_def,
-      FOL.BoundedQuery.schema.or_def, FOL.BoundedQuery.schema.not_def, Finset.union_idempotent, RA.Query.schema]
+    | _ => simp_all only [RA.Query.isWellTyped, ra_to_fol_query, FOL.BoundedQuery.or,
+        FOL.BoundedQuery.schema.not_def, FOL.BoundedQuery.schema.and_def, Finset.union_idempotent,
+        RA.Query.schema]

RelationalAlgebra/Equivalence/RAtoFOL/Union.lean

@@ -15,20 +15,4 @@ theorem ra_to_fol_evalT.u_def_eq (h : RA.Query.isWellTyped dbi.schema (.u q₁ q
       simp_all only [Set.mem_setOf_eq, Set.mem_union]
       obtain ⟨left, right⟩ := h
       obtain ⟨left_1, right⟩ := right
-      apply Iff.intro
-      · intro a
-        simp_all only [forall_true_left, true_and]
-        obtain ⟨left_2, right_1⟩ := a
-        convert right_1 left_2
-      · intro a
-        cases a with
-        | inl h =>
-          simp_all only [forall_true_left, true_and]
-          obtain ⟨left_2, right_1⟩ := h
-          apply Or.inl
-          convert right_1 left_2
-        | inr h_1 =>
-          simp_all only [forall_true_left, true_and]
-          obtain ⟨left_2, right_1⟩ := h_1
-          apply Or.inr
-          convert right_1 left_2
+      grind only [cases Or]

RelationalAlgebra/FOL/Query.lean

@@ -18,9 +18,16 @@ inductive BoundedQuery (dbs : ρ → Finset α) : ℕ → Type
   | and {n} (q1 q2 : BoundedQuery dbs n): BoundedQuery dbs n
   | tEq {n} : (t₁ t₂ : (fol dbs).Term (α ⊕ Fin n)) → BoundedQuery dbs n
   | ex {n} (q : BoundedQuery dbs (n + 1)) : BoundedQuery dbs n
-  | or {n} (q₁ q₂ : BoundedQuery dbs n) : BoundedQuery dbs n
   | not {n} (q : BoundedQuery dbs n) : BoundedQuery dbs n
 
+@[simp]
+def BoundedQuery.or (q₁ q₂ : BoundedQuery dbs n) : BoundedQuery dbs n :=
+  (q₁.not.and (q₂.not)).not
+
+@[simp]
+def BoundedQuery.all (q : BoundedQuery dbs (n + 1)) : BoundedQuery dbs n :=
+  q.not.ex.not
+
 /-- Syntax for a `Query` given a database schema `dbs` with bound `0`. Similar to `ModelTheory.Formula`. -/
 abbrev Query (dbs : ρ → Finset α) := BoundedQuery dbs 0
 
@@ -38,7 +45,6 @@ def BoundedQuery.toFormula : (q : BoundedQuery dbs n) → (fol dbs).BoundedFormu
   | .tEq t₁ t₂ => .equal t₁ t₂
   | .and q1 q2 => q1.toFormula ⊓ q2.toFormula
   | .ex q => .ex q.toFormula
-  | .or q1 q2 => q1.toFormula ⊔ q2.toFormula
   | .not q => .not q.toFormula
 
 @[simp]

RelationalAlgebra/FOL/RealizeProperties.lean

@@ -294,9 +294,4 @@ theorem BoundedQuery.Realize.restrict [folStruc dbi] {rs : Finset α} {q : Bound
       have : f₁.toFormula.freeVarFinset ⊆ rs := Finset.union_subset_left h_min
       have : f₂.toFormula.freeVarFinset ⊆ rs := Finset.union_subset_right h_min
       simp_all
-    | or f₁ f₂ ih₁ ih₂ =>
-      simp_all [BoundedQuery.toFormula]
-      have : f₁.toFormula.freeVarFinset ⊆ rs := Finset.union_subset_left h_min
-      have : f₂.toFormula.freeVarFinset ⊆ rs := Finset.union_subset_right h_min
-      simp_all
     | _ => simp_all

RelationalAlgebra/FOL/Relabel.lean

@@ -16,7 +16,6 @@ def BoundedQuery.mapTermRel {g : ℕ → ℕ} (ft : ∀ n, (fol dbs).Term (α 
   | _n, .tEq a b        => .tEq (ft _ a) (ft _ b)
   | _n, .and q1 q2      => .and (q1.mapTermRel ft h) (q2.mapTermRel ft h)
   | n,  .ex q           => (h n (q.mapTermRel ft h)).ex
-  | _n, .or q1 q2       => .or (q1.mapTermRel ft h) (q2.mapTermRel ft h)
   | _n, .not q          => (q.mapTermRel ft h).not
 
 /-- Casts `BoundedQuery dbs m` as `BoundedQuery dbs n`, where `m ≤ n`. -/
@@ -26,7 +25,6 @@ def BoundedQuery.castLE : ∀ {m n : ℕ} (_h : m ≤ n), BoundedQuery dbs m →
   | _m, _n, h, .tEq a b => .tEq (a.relabel (Sum.map id (Fin.castLE h))) (b.relabel (Sum.map id (Fin.castLE h)))
   | _m, _n, h, .and q₁ q₂ => (q₁.castLE h).and (q₂.castLE h)
   | _m, _n, h, .ex q => (q.castLE (add_le_add_right h 1)).ex
-  | _m, _n, h, .or q₁ q₂ => (q₁.castLE h).or (q₂.castLE h)
   | _m, _n, h, .not q => (q.castLE h).not
 
 /- Helper theorems for `castLE` and `mapTermRel` -/
@@ -44,7 +42,6 @@ theorem castLE_rfl {n} (h : n ≤ n) (φ : BoundedQuery dbs n) : φ.castLE h = 
   | tEq _ _ => simp
   | and _ _ ih₁ ih₂ => simp [ih₁, ih₂]
   | ex _ ih => simp [ih]
-  | or _ _ ih₁ ih₂ => simp [ ih₁, ih₂]
   | not _ ih => simp [ih]
 
 @[simp]
@@ -102,11 +99,6 @@ theorem BoundedQuery.relabel.ex_def (g : α → α ⊕ (Fin n)) {k} (φ : Bounde
     rw [relabel, mapTermRel, relabel]
     simp
 
-@[simp]
-theorem BoundedQuery.relabel.or_def (g : α → α ⊕ (Fin n)) {k} (φ ψ : BoundedQuery dbs k) :
-  (or φ ψ).relabel g = or (φ.relabel g) (ψ.relabel g) := by
-    rfl
-
 @[simp]
 theorem BoundedQuery.relabel.not_def (g : α → α ⊕ (Fin n)) {k} (φ : BoundedQuery dbs k) :
   (not φ).relabel g = not (φ.relabel g) := by

RelationalAlgebra/FOL/Schema.lean

@@ -48,10 +48,6 @@ theorem BoundedQuery.schema.and_def {n : ℕ} (q₁ q₂ : BoundedQuery dbs n) :
 theorem BoundedQuery.schema.ex_def {n : ℕ} (q : BoundedQuery dbs (n + 1)) :
   (ex q).schema = q.schema := by simp_all [schema]
 
-@[simp]
-theorem BoundedQuery.schema.or_def {n : ℕ} (q₁ q₂ : BoundedQuery dbs n) :
-  (or q₁ q₂).schema = q₁.schema ∪ q₂.schema := by simp_all [schema]
-
 @[simp]
 theorem BoundedQuery.schema.not_def {n : ℕ} (q : BoundedQuery dbs n) :
   (not q).schema = q.schema := by simp_all [schema]