Skip to content

Commit df55308

Browse files
Rickerd1234Rickerd1234
committed
Refactoring
1 parent 9abd90d commit df55308

5 files changed

Lines changed: 27 additions & 27 deletions

File tree

‎RelationalAlgebra/Equivalence/RAtoFOL/Conversion.lean‎

Lines changed: 10 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -1,14 +1,14 @@
11
import RelationalAlgebra.Equivalence.RAtoFOL.ProjectionDef
22
import RelationalAlgebra.FOL.RelabelProperties
33

4-
open RM
4+
open RM FOL
55

66
variable {ρ α : Type} [LinearOrder α]
77

88
/-- Function to handle conversion of all Relational Algebra query cases. -/
99
def toFOL (dbs : ρ → Finset α) : RA.Query ρ α → FOL.Query dbs
10-
| .R rn => .R rn (FOL.outVar ∘ RelationSchema.fromIndex)
11-
| .s a b sq => .and (toFOL dbs sq) (.tEq (FOL.outVar a) (FOL.outVar b))
10+
| .R rn => .R rn (freeVar ∘ RelationSchema.fromIndex)
11+
| .s a b sq => .and (toFOL dbs sq) (.tEq (freeVar a) (freeVar b))
1212
| .p rs sq => projectQuery (toFOL dbs sq) rs
1313
| .j sq₁ sq₂ => .and (toFOL dbs sq₁) (toFOL dbs sq₂)
1414
| .r f sq => (toFOL dbs sq).relabel (Sum.inl ∘ f)
@@ -21,8 +21,8 @@ theorem toFOL.schema_def {dbs : ρ → Finset α} {raQ : RA.Query ρ α} (h : ra
2121
induction raQ with
2222
| R rn =>
2323
ext a
24-
simp_all only [RA.Query.isWellTyped, toFOL, FOL.BoundedQuery.schema.R_def,
25-
Function.comp_apply, FOL.outVar.def, FirstOrder.Language.Term.varFinsetLeft.eq_1,
24+
simp_all only [RA.Query.isWellTyped, toFOL, BoundedQuery.schema.R_def,
25+
Function.comp_apply, freeVar.def, FirstOrder.Language.Term.varFinsetLeft.eq_1,
2626
Finset.mem_singleton, Set.mem_toFinset, Set.mem_setOf_eq, RA.Query.schema]
2727
apply Iff.intro
2828
· intro ⟨w, h⟩
@@ -39,14 +39,14 @@ theorem toFOL.schema_def {dbs : ρ → Finset α} {raQ : RA.Query ρ α} (h : ra
3939
simp_all only [forall_const]
4040

4141
| r f sq ih => simp_all only [RA.Query.isWellTyped, toFOL,
42-
FOL.BoundedQuery.relabel_schema, Function.comp_apply, Sum.getLeft?_inl, Part.coe_some,
42+
BoundedQuery.relabel_schema, Function.comp_apply, Sum.getLeft?_inl, Part.coe_some,
4343
Finset.pimage_some, RA.Query.schema]
4444

45-
| s => simp_all only [RA.Query.isWellTyped, toFOL, FOL.outVar.def,
46-
FOL.BoundedQuery.schema.and_def, FOL.BoundedQuery.schema.tEq_def,
45+
| s => simp_all only [RA.Query.isWellTyped, toFOL, freeVar.def,
46+
BoundedQuery.schema.and_def, BoundedQuery.schema.tEq_def,
4747
FirstOrder.Language.Term.varFinsetLeft, Finset.union_singleton, Finset.union_insert,
4848
Finset.insert_eq_of_mem, RA.Query.schema]
4949

50-
| _ => simp_all only [RA.Query.isWellTyped, toFOL, FOL.BoundedQuery.or,
51-
FOL.BoundedQuery.schema.not_def, FOL.BoundedQuery.schema.and_def, Finset.union_idempotent,
50+
| _ => simp_all only [RA.Query.isWellTyped, toFOL, BoundedQuery.or,
51+
BoundedQuery.schema.not_def, BoundedQuery.schema.and_def, Finset.union_idempotent,
5252
RA.Query.schema]

‎RelationalAlgebra/Equivalence/RAtoFOL/Relation.lean‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -8,7 +8,7 @@ theorem toFOL.evalT_def.R_def.mp :
88
intro t
99
simp_all only [FOL.Query.RealizeMin, FOL.BoundedQuery.Realize, toFOL,
1010
FOL.BoundedQuery.toFormula.eq_1, FirstOrder.Language.BoundedFormula.realize_rel,
11-
Function.comp_apply, FOL.outVar.def, FirstOrder.Language.Term.realize_var, Sum.elim_inl,
11+
Function.comp_apply, FOL.freeVar.def, FirstOrder.Language.Term.realize_var, Sum.elim_inl,
1212
FOL.BoundedQuery.schema.R_def, FirstOrder.Language.Term.varFinsetLeft.eq_1,
1313
Finset.mem_singleton, RM.RelationSchema.Dom_sub_fromIndex, Finset.toFinset_coe,
1414
RA.Query.evaluateT, forall_exists_index]
@@ -25,7 +25,7 @@ theorem toFOL.evalT_def.R_def.mpr (h : RA.Query.isWellTyped dbi.schema (.R rn))
2525

2626
simp only [toFOL]
2727
simp_all only [FOL.BoundedQuery.Realize, FOL.BoundedQuery.toFormula,
28-
FirstOrder.Language.BoundedFormula.realize_rel, Function.comp_apply, FOL.outVar.def,
28+
FirstOrder.Language.BoundedFormula.realize_rel, Function.comp_apply, FOL.freeVar.def,
2929
FirstOrder.Language.Term.realize_var, Sum.elim_inl, FOL.BoundedQuery.schema.R_def,
3030
FirstOrder.Language.Term.varFinsetLeft.eq_1, Finset.mem_singleton,
3131
RM.RelationSchema.Dom_sub_fromIndex, Finset.toFinset_coe, FOL.folStruc_apply_RelMap]

‎RelationalAlgebra/Equivalence/RAtoFOL/Selection.lean‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -7,7 +7,7 @@ theorem toFOL.evalT_def.s_def.mp (h : RA.Query.isWellTyped dbi.schema (.s a b q)
77
(ih: ∀t, (toFOL dbi.schema q).RealizeMin dbi t → t ∈ RA.Query.evaluateT dbi q) :
88
∀t, (toFOL dbi.schema (.s a b q)).RealizeMin dbi t → t ∈ RA.Query.evaluateT dbi (.s a b q) := by
99
intro t
10-
simp only [RA.Query.isWellTyped, toFOL, FOL.outVar.def, FOL.Query.RealizeMin.ex_def,
10+
simp only [RA.Query.isWellTyped, toFOL, FOL.freeVar.def, FOL.Query.RealizeMin.ex_def,
1111
FOL.BoundedQuery.Realize, FOL.BoundedQuery.toFormula,
1212
FirstOrder.Language.BoundedFormula.realize_inf, FOL.BoundedQuery.schema.and_def,
1313
FOL.BoundedQuery.schema.tEq_def, FirstOrder.Language.Term.varFinsetLeft, Finset.coe_union,
@@ -39,7 +39,7 @@ theorem toFOL.evalT_def.s_def.mpr (h : RA.Query.isWellTyped dbi.schema (.s a b q
3939
(by simp_all [toFOL.schema_def])
4040

4141
simp only [toFOL, FOL.BoundedQuery.Realize]
42-
simp_all only [FOL.Query.RealizeMin.ex_def, RA.Query.evaluateT, FOL.outVar.def]
42+
simp_all only [FOL.Query.RealizeMin.ex_def, RA.Query.evaluateT, FOL.freeVar.def]
4343
obtain ⟨left, right⟩ := h
4444
obtain ⟨left_1, right⟩ := right
4545
simp_all [FOL.BoundedQuery.Realize, selectionT]

‎RelationalAlgebra/FOL/Examples.lean‎

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -21,9 +21,9 @@ open FOL Language
2121

2222
abbrev exFol := (fol exDatabase.schema)
2323

24-
def x : exFol.Term (String ⊕ Fin 0) := outVar "x"
25-
def y : exFol.Term (String ⊕ Fin 0) := outVar "y"
26-
def z : exFol.Term (String ⊕ Fin 1) := inVar 0
24+
def x : exFol.Term (String ⊕ Fin 0) := freeVar "x"
25+
def y : exFol.Term (String ⊕ Fin 0) := freeVar "y"
26+
def z : exFol.Term (String ⊕ Fin 1) := boundVar 0
2727

2828
-- Explore formula concepts
2929
def n_xy : exFol.BoundedFormula String 0 := ∼(x =' y)
@@ -51,7 +51,7 @@ example [struc: exFol.Structure (String)] : ex_n_xy_and_yz.Realize v' := by
5151
rfl
5252

5353
example [struc: exFol.Structure (String)] : all_xz_or_yz.Realize v' := by
54-
simp only [Formula.Realize, all_xz_or_yz, x, y, z, outVar, inVar]
54+
simp only [Formula.Realize, all_xz_or_yz, x, y, z, freeVar, boundVar]
5555
simp
5656
use ""
5757
simp [Term.liftAt, Fin.snoc]
@@ -61,7 +61,7 @@ example [struc: exFol.Structure (String)] : all_xz_or_yz.Realize v' := by
6161
def v := PFun.res v' {"x", "y"}
6262

6363
-- Relation with variables
64-
def F : Query exDatabase.schema := (.R "employee" [outVar "x", outVar "y"].get)
64+
def F : Query exDatabase.schema := (.R "employee" [freeVar "x", freeVar "y"].get)
6565

6666
example (h : a ∈ exDatabase.schema "employee") :
6767
RelationSchema.index h < (exDatabase.schema "employee").card := by

‎RelationalAlgebra/FOL/Variable.lean‎

Lines changed: 8 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -7,27 +7,27 @@ open FirstOrder Language RM
77
variable {α : Type}
88

99
/-- Helper definition used for a free variable, part of the 'output'. -/
10-
def outVar {n: ℕ} (v : α) : (fol dbs).Term (α ⊕ Fin n) := Term.var (Sum.inl v)
10+
def freeVar {n: ℕ} (v : α) : (fol dbs).Term (α ⊕ Fin n) := Term.var (Sum.inl v)
1111

1212
@[simp]
13-
theorem outVar.def {n} (v : α) : (outVar v : (fol dbs).Term (α ⊕ Fin n)) = Term.var (Sum.inl v) := rfl
13+
theorem freeVar.def {n} (v : α) : (freeVar v : (fol dbs).Term (α ⊕ Fin n)) = Term.var (Sum.inl v) := rfl
1414

1515
/-- Helper definition used for a bound variable, not part of the 'output', bound to quantifier `∃` or `∀`. -/
16-
def inVar {n: ℕ} (i: Fin n) : (fol dbs).Term (α ⊕ Fin n) := Term.var (Sum.inr i)
16+
def boundVar {n: ℕ} (i: Fin n) : (fol dbs).Term (α ⊕ Fin n) := Term.var (Sum.inr i)
1717

1818
@[simp]
19-
theorem inVar.def {n : ℕ} (i: Fin n) : (inVar i : (fol dbs).Term (α ⊕ Fin n)) = Term.var (Sum.inr i) := rfl
19+
theorem boundVar.def {n : ℕ} (i: Fin n) : (boundVar i : (fol dbs).Term (α ⊕ Fin n)) = Term.var (Sum.inr i) := rfl
2020

21-
def outVar? {n : ℕ} : (vt : (fol dbs).Term (α ⊕ Fin n)) → Option α
21+
def freeVar? {n : ℕ} : (vt : (fol dbs).Term (α ⊕ Fin n)) → Option α
2222
| .var x => x.getLeft?
2323
| _ => none
2424

25-
def inVar? {n : ℕ} : (vt : (fol dbs).Term (α ⊕ Fin n)) → Option (Fin n)
25+
def boundVar? {n : ℕ} : (vt : (fol dbs).Term (α ⊕ Fin n)) → Option (Fin n)
2626
| .var x => x.getRight?
2727
| _ => none
2828

29-
theorem outVar?.injective {n : ℕ} (a a' : (fol dbs).Term (α ⊕ Fin n)) : ∀ b ∈ outVar? a, b ∈ outVar? a' → a = a' :=
29+
theorem freeVar?.injective {n : ℕ} (a a' : (fol dbs).Term (α ⊕ Fin n)) : ∀ b ∈ freeVar? a, b ∈ freeVar? a' → a = a' :=
3030
by
3131
intro b a_1 a_2
32-
simp_all only [Option.mem_def, outVar?]
32+
simp_all only [Option.mem_def, freeVar?]
3333
aesop

0 commit comments

Comments
 (0)