From a9ee8f882934264e8913251eaab57891a9be77aa Mon Sep 17 00:00:00 2001 From: stechu Date: Thu, 3 May 2018 23:14:00 -0700 Subject: [PATCH] update proven rules --- dsl/ToLean.lhs | 3 +- uexp/src/uexp/TDP.lean | 3 +- uexp/src/uexp/extra_constants.lean | 3 +- uexp/src/uexp/rules/pushProjectPastSetOp.lean | 2 ++ .../rules/removeSemiJoinRightWithFilter.lean | 1 + .../uexp/rules/removeSemiJoinWithFilter.lean | 2 ++ .../transitiveInferenceComplexPredicate.lean | 32 +++++++++++++------ .../uexp/rules/transitiveInferenceJoin.lean | 31 ++++++++++++++++++ 8 files changed, 65 insertions(+), 12 deletions(-) create mode 100644 uexp/src/uexp/rules/transitiveInferenceJoin.lean diff --git a/dsl/ToLean.lhs b/dsl/ToLean.lhs index b7d9ad0..4fb298d 100644 --- a/dsl/ToLean.lhs +++ b/dsl/ToLean.lhs @@ -653,7 +653,8 @@ generate predicate declarations > "open Proj", > "open Pred", > "open SQL", -> "open tree \n", +> "open tree", +> "open binary_operators\n", > "notation `int` := datatypes.int \n"] > openDef :: String diff --git a/uexp/src/uexp/TDP.lean b/uexp/src/uexp/TDP.lean index 743641e..e70b7d1 100644 --- a/uexp/src/uexp/TDP.lean +++ b/uexp/src/uexp/TDP.lean @@ -1,5 +1,6 @@ import .u_semiring import .cosette_tactics +import .ucongr section TDP open tactic @@ -75,5 +76,5 @@ example {p q r s} {f : Tuple p → Tuple q → Tuple r → Tuple s → usr} : (∑ (a : Tuple p) (b : Tuple q) (c : Tuple r) (d : Tuple s), f a b c d) = (∑ (c : Tuple r) (a : Tuple p) (d : Tuple s) (b : Tuple q), f a b c d) := begin - TDP + TDP' tactic.ac_refl, end \ No newline at end of file diff --git a/uexp/src/uexp/extra_constants.lean b/uexp/src/uexp/extra_constants.lean index c9356ac..ed9dc99 100644 --- a/uexp/src/uexp/extra_constants.lean +++ b/uexp/src/uexp/extra_constants.lean @@ -37,7 +37,8 @@ end predicates namespace binary_operators -constant add : binary datatypes.int datatypes.int datatypes.int +constant add_ : binary datatypes.int datatypes.int datatypes.int +constant divide_ : binary datatypes.int datatypes.int datatypes.int end binary_operators diff --git a/uexp/src/uexp/rules/pushProjectPastSetOp.lean b/uexp/src/uexp/rules/pushProjectPastSetOp.lean index 722cd4c..0ed17bd 100644 --- a/uexp/src/uexp/rules/pushProjectPastSetOp.lean +++ b/uexp/src/uexp/rules/pushProjectPastSetOp.lean @@ -3,6 +3,8 @@ import ..tactics import ..u_semiring import ..extra_constants +set_option profiler true + open Expr open Proj open Pred diff --git a/uexp/src/uexp/rules/removeSemiJoinRightWithFilter.lean b/uexp/src/uexp/rules/removeSemiJoinRightWithFilter.lean index 7a0c0ef..31d50bf 100644 --- a/uexp/src/uexp/rules/removeSemiJoinRightWithFilter.lean +++ b/uexp/src/uexp/rules/removeSemiJoinRightWithFilter.lean @@ -6,6 +6,7 @@ import ..extra_constants import ..ucongr import ..TDP +set_option profiler true open Expr open Proj open Pred diff --git a/uexp/src/uexp/rules/removeSemiJoinWithFilter.lean b/uexp/src/uexp/rules/removeSemiJoinWithFilter.lean index 803c034..33dbc44 100644 --- a/uexp/src/uexp/rules/removeSemiJoinWithFilter.lean +++ b/uexp/src/uexp/rules/removeSemiJoinWithFilter.lean @@ -5,6 +5,8 @@ import ..extra_constants import ..ucongr import ..TDP +set_option profiler true + open Expr open Proj open Pred diff --git a/uexp/src/uexp/rules/transitiveInferenceComplexPredicate.lean b/uexp/src/uexp/rules/transitiveInferenceComplexPredicate.lean index f921997..fe208e6 100644 --- a/uexp/src/uexp/rules/transitiveInferenceComplexPredicate.lean +++ b/uexp/src/uexp/rules/transitiveInferenceComplexPredicate.lean @@ -2,22 +2,36 @@ import ..sql import ..tactics import ..u_semiring import ..extra_constants +import ..ucongr +import ..TDP + +set_option profiler true open Expr open Proj open Pred open SQL open tree +open binary_operators notation `int` := datatypes.int -constant integer_1: const int. -constant integer_2: const int. -constant integer_7: const int. -lemma rule: - forall ( Γ scm_t scm_account scm_bonus scm_dept scm_emp: Schema) (rel_t: relation scm_t) (rel_account: relation scm_account) (rel_bonus: relation scm_bonus) (rel_dept: relation scm_dept) (rel_emp: relation scm_emp) (t_k0 : Column int scm_t) (t_c1 : Column int scm_t) (t_f1_a0 : Column int scm_t) (t_f2_a0 : Column int scm_t) (t_f0_c0 : Column int scm_t) (t_f1_c0 : Column int scm_t) (t_f0_c1 : Column int scm_t) (t_f1_c2 : Column int scm_t) (t_f2_c3 : Column int scm_t) (account_acctno : Column int scm_account) (account_type : Column int scm_account) (account_balance : Column int scm_account) (bonus_ename : Column int scm_bonus) (bonus_job : Column int scm_bonus) (bonus_sal : Column int scm_bonus) (bonus_comm : Column int scm_bonus) (dept_deptno : Column int scm_dept) (dept_name : Column int scm_dept) (emp_empno : Column int scm_emp) (emp_ename : Column int scm_emp) (emp_job : Column int scm_emp) (emp_mgr : Column int scm_emp) (emp_hiredate : Column int scm_emp) (emp_comm : Column int scm_emp) (emp_sal : Column int scm_emp) (emp_deptno : Column int scm_emp) (emp_slacker : Column int scm_emp), - denoteSQL - ((SELECT1 (e2p (constantExpr integer_1)) FROM1 (product ((SELECT * FROM1 (table rel_emp) WHERE (and (and (castPred (combine (right⋅emp_deptno) (e2p (constantExpr integer_7)) ) predicates.gt) (equal (uvariable (right⋅emp_comm)) (uvariable (right⋅emp_deptno)))) (castPred (combine (e2p (binaryExpr add_ (uvariable (right⋅emp_comm)) (uvariable (right⋅emp_deptno)))) (e2p (binaryExpr divide_ (variable (right⋅emp_comm)) (constantExpr integer_2))) ) gt)))) ((SELECT * FROM1 (table rel_emp) WHERE (equal (variable (right⋅emp_sal)) (variable (right⋅emp_deptno)))))) WHERE (equal (variable (right⋅left⋅emp_deptno)) (variable (right⋅right⋅emp_deptno)))) : _ ⟧ = ⟦ Γ ⊢ (SELECT1 (e2p (constantExpr integer_1)) FROM1 (product ((SELECT * FROM1 (table rel_emp) WHERE (and (and (castPred (combine (right⋅emp_deptno) (e2p (constantExpr integer_7)) ) gt) (equal (variable (right⋅emp_comm)) (variable (right⋅emp_deptno)))) (castPred (combine (e2p (binaryExpr add_ (variable (right⋅emp_comm)) (variable (right⋅emp_deptno)))) (e2p (binaryExpr divide_ (variable (right⋅emp_comm)) (constantExpr integer_2))) ) gt)))) ((SELECT * FROM1 ((SELECT * FROM1 (table rel_emp) WHERE (equal (variable (right⋅emp_sal)) (variable (right⋅emp_deptno))))) WHERE (castPred (combine (right⋅emp_deptno) (e2p (constantExpr integer_7)) ) gt)))) WHERE (equal (variable (right⋅left⋅emp_deptno)) (variable (right⋅right⋅emp_deptno)))) : _ ⟧). - Defined. - Arguments Rule /. +variable integer_1: const datatypes.int +variable integer_2: const datatypes.int +variable integer_7: const datatypes.int + + +theorem rule: +forall ( Γ scm_t scm_account scm_bonus scm_dept scm_emp: Schema) (rel_t: relation scm_t) (rel_account: relation scm_account) (rel_bonus: relation scm_bonus) (rel_dept: relation scm_dept) (rel_emp: relation scm_emp) (t_k0 : Column int scm_t) (t_c1 : Column int scm_t) (t_f1_a0 : Column int scm_t) (t_f2_a0 : Column int scm_t) (t_f0_c0 : Column int scm_t) (t_f1_c0 : Column int scm_t) (t_f0_c1 : Column int scm_t) (t_f1_c2 : Column int scm_t) (t_f2_c3 : Column int scm_t) (account_acctno : Column int scm_account) (account_type : Column int scm_account) (account_balance : Column int scm_account) (bonus_ename : Column int scm_bonus) (bonus_job : Column int scm_bonus) (bonus_sal : Column int scm_bonus) (bonus_comm : Column int scm_bonus) (dept_deptno : Column int scm_dept) (dept_name : Column int scm_dept) (emp_empno : Column int scm_emp) (emp_ename : Column int scm_emp) (emp_job : Column int scm_emp) (emp_mgr : Column int scm_emp) (emp_hiredate : Column int scm_emp) (emp_comm : Column int scm_emp) (emp_sal : Column int scm_emp) (emp_deptno : Column int scm_emp) (emp_slacker : Column int scm_emp), +denoteSQL ((SELECT1 (e2p (constantExpr integer_1)) FROM1 (product ((SELECT * FROM1 (table rel_emp) WHERE (and (and (castPred (combine (right⋅emp_deptno) (e2p (constantExpr integer_7)) ) predicates.gt) (equal (uvariable (right⋅emp_comm)) (uvariable (right⋅emp_deptno)))) (castPred (combine (e2p (binaryExpr add_ (uvariable (right⋅emp_comm)) (uvariable (right⋅emp_deptno)))) (e2p (binaryExpr divide_ (uvariable (right⋅emp_comm)) (constantExpr integer_2))) ) predicates.gt)))) ((SELECT * FROM1 (table rel_emp) WHERE (equal (uvariable (right⋅emp_sal)) (uvariable (right⋅emp_deptno)))))) WHERE (equal (uvariable (right⋅left⋅emp_deptno)) (uvariable (right⋅right⋅emp_deptno)))) :SQL Γ _) += +denoteSQL ((SELECT1 (e2p (constantExpr integer_1)) FROM1 (product ((SELECT * FROM1 (table rel_emp) WHERE (and (and (castPred (combine (right⋅emp_deptno) (e2p (constantExpr integer_7)) ) predicates.gt) (equal (uvariable (right⋅emp_comm)) (uvariable (right⋅emp_deptno)))) (castPred (combine (e2p (binaryExpr add_ (uvariable (right⋅emp_comm)) (uvariable (right⋅emp_deptno)))) (e2p (binaryExpr divide_ (uvariable (right⋅emp_comm)) (constantExpr integer_2))) ) predicates.gt)))) ((SELECT * FROM1 ((SELECT * FROM1 (table rel_emp) WHERE (equal (uvariable (right⋅emp_sal)) (uvariable (right⋅emp_deptno))))) WHERE (castPred (combine (right⋅emp_deptno) (e2p (constantExpr integer_7)) ) predicates.gt)))) WHERE (equal (uvariable (right⋅left⋅emp_deptno)) (uvariable (right⋅right⋅emp_deptno)))) :SQL Γ _) := +begin + intros, + unfold_all_denotations, + funext, + try {simp}, + try {TDP' ucongr}, + sorry +end \ No newline at end of file diff --git a/uexp/src/uexp/rules/transitiveInferenceJoin.lean b/uexp/src/uexp/rules/transitiveInferenceJoin.lean new file mode 100644 index 0000000..9f11a6a --- /dev/null +++ b/uexp/src/uexp/rules/transitiveInferenceJoin.lean @@ -0,0 +1,31 @@ +import ..sql +import ..tactics +import ..u_semiring +import ..extra_constants +import ..ucongr +import ..TDP + +open Expr +open Proj +open Pred +open SQL +open tree + +notation `int` := datatypes.int + +variable integer_1: const datatypes.int +variable integer_7: const datatypes.int + + +theorem rule: +forall ( Γ scm_t scm_account scm_bonus scm_dept scm_emp: Schema) (rel_t: relation scm_t) (rel_account: relation scm_account) (rel_bonus: relation scm_bonus) (rel_dept: relation scm_dept) (rel_emp: relation scm_emp) (t_k0 : Column int scm_t) (t_c1 : Column int scm_t) (t_f1_a0 : Column int scm_t) (t_f2_a0 : Column int scm_t) (t_f0_c0 : Column int scm_t) (t_f1_c0 : Column int scm_t) (t_f0_c1 : Column int scm_t) (t_f1_c2 : Column int scm_t) (t_f2_c3 : Column int scm_t) (account_acctno : Column int scm_account) (account_type : Column int scm_account) (account_balance : Column int scm_account) (bonus_ename : Column int scm_bonus) (bonus_job : Column int scm_bonus) (bonus_sal : Column int scm_bonus) (bonus_comm : Column int scm_bonus) (dept_deptno : Column int scm_dept) (dept_name : Column int scm_dept) (emp_empno : Column int scm_emp) (emp_ename : Column int scm_emp) (emp_job : Column int scm_emp) (emp_mgr : Column int scm_emp) (emp_hiredate : Column int scm_emp) (emp_comm : Column int scm_emp) (emp_sal : Column int scm_emp) (emp_deptno : Column int scm_emp) (emp_slacker : Column int scm_emp), +denoteSQL ((SELECT1 (e2p (constantExpr integer_1)) FROM1 (product (table rel_emp) ((SELECT * FROM1 (table rel_emp) WHERE (castPred (combine (right⋅emp_deptno) (e2p (constantExpr integer_7)) ) predicates.gt)))) WHERE (equal (uvariable (right⋅left⋅emp_deptno)) (uvariable (right⋅right⋅emp_deptno)))) :SQL Γ _) += +denoteSQL ((SELECT1 (e2p (constantExpr integer_1)) FROM1 (product ((SELECT * FROM1 (table rel_emp) WHERE (castPred (combine (right⋅emp_deptno) (e2p (constantExpr integer_7)) ) predicates.gt))) ((SELECT * FROM1 (table rel_emp) WHERE (castPred (combine (right⋅emp_deptno) (e2p (constantExpr integer_7)) ) predicates.gt)))) WHERE (equal (uvariable (right⋅left⋅emp_deptno)) (uvariable (right⋅right⋅emp_deptno)))) :SQL Γ _) := +begin + intros, + unfold_all_denotations, + funext, + try {simp}, + TDP' tactic.ac_refl, -- Here is the problem +end \ No newline at end of file