update proven rules

uwdb · May 4, 2018 · a9ee8f8 · a9ee8f8
1 parent 6a88ae2
commit a9ee8f8
Show file tree

Hide file tree

Showing 8 changed files with 65 additions and 12 deletions.
diff --git 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
@@ -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
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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
 
diff --git a/uexp/src/uexp/rules/transitiveInferenceJoin.lean 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