From 6c2c82f47c6636c18a36d333c6f65997db4eca5b Mon Sep 17 00:00:00 2001 From: Daniel Selsam Date: Sat, 7 Nov 2015 12:54:01 -0800 Subject: [PATCH] feat(library/blast/simplifier): conditional rewriting --- src/frontends/lean/builtin_cmds.cpp | 1 + src/library/blast/simplifier.cpp | 67 +++++++++++--------- src/library/simplifier/ceqv.cpp | 2 +- tests/lean/simplifier10.lean | 19 ++++++ tests/lean/simplifier10.lean.expected.out | 5 ++ tests/lean/simplifier11.lean | 74 +++++++++++++++++++++++ tests/lean/simplifier11.lean.expected.out | 5 ++ tests/lean/simplifier12.lean | 23 +++++++ tests/lean/simplifier12.lean.expected.out | 1 + tests/lean/simplifier9.lean.expected.out | 13 ++++ 10 files changed, 182 insertions(+), 28 deletions(-) create mode 100644 tests/lean/simplifier10.lean create mode 100644 tests/lean/simplifier10.lean.expected.out create mode 100644 tests/lean/simplifier11.lean create mode 100644 tests/lean/simplifier11.lean.expected.out create mode 100644 tests/lean/simplifier12.lean create mode 100644 tests/lean/simplifier12.lean.expected.out create mode 100644 tests/lean/simplifier9.lean.expected.out diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp index 17a51f074..64005d306 100644 --- a/src/frontends/lean/builtin_cmds.cpp +++ b/src/frontends/lean/builtin_cmds.cpp @@ -1335,6 +1335,7 @@ static environment simplify_cmd(parser & p) { } else { auto tc = mk_type_checker(p.env(), p.mk_ngen()); + expr pf_type = tc->check(r.get_proof(), ls).first; if (o == 0) p.regular_stream() << r.get_new() << endl; diff --git a/src/library/blast/simplifier.cpp b/src/library/blast/simplifier.cpp index 3d3d59219..88af4c01d 100644 --- a/src/library/blast/simplifier.cpp +++ b/src/library/blast/simplifier.cpp @@ -97,7 +97,6 @@ class simplifier { branch m_branch; name m_rel; - list m_local_ctx; simp_rule_sets m_ctx_srss; /* Logging */ @@ -250,7 +249,7 @@ result simplifier::simplify(expr const & e) { flet inc_depth(m_depth, m_depth+1); if (m_trace) { - ios().get_diagnostic_channel() << m_depth << "." << m_rel << "." << m_local_ctx << " " << e << "\n"; + ios().get_diagnostic_channel() << m_depth << "." << m_rel << ": " << e << "\n"; } if (m_num_steps > m_max_steps) @@ -335,7 +334,6 @@ result simplifier::simplify_pi(expr const & e) { result simplifier::simplify_app(expr const & e) { lean_assert(is_app(e)); - // TODO simplify operator as well, in cases (1) and (2) /* (1) Try user-defined congruences */ result r = try_congrs(e); @@ -419,8 +417,9 @@ result simplifier::rewrite(expr const & e, simp_rule const & sr) { if (m_trace) { expr new_lhs = tmp_tctx->instantiate_uvars_mvars(sr.get_lhs()); expr new_rhs = tmp_tctx->instantiate_uvars_mvars(sr.get_rhs()); - ios().get_diagnostic_channel() << "[" << sr.get_lhs() << " =?= " << sr.get_rhs() << "] ==> "; - ios().get_diagnostic_channel() << "[" << new_lhs << " =?= " << new_rhs << "]\n"; + ios().get_diagnostic_channel() + << "REW(" << sr.get_id() << ") " + << "[" << new_lhs << " =?= " << new_rhs << "]\n"; } /* Traverse metavariables backwards */ @@ -429,27 +428,39 @@ result simplifier::rewrite(expr const & e, simp_rule const & sr) { bool is_instance = sr.is_instance(i); if (is_instance) { - expr type = tmp_tctx->instantiate_uvars_mvars(tmp_tctx->infer(m)); - if (auto v = tmp_tctx->mk_class_instance(type)) { - if (!tmp_tctx->force_assign(m, *v)) + expr m_type = tmp_tctx->instantiate_uvars_mvars(tmp_tctx->infer(m)); + if (auto v = tmp_tctx->mk_class_instance(m_type)) { + if (!tmp_tctx->force_assign(m, *v)) { + if (m_trace) { + ios().get_diagnostic_channel() << "unable to assign instance for: " << m_type << "\n"; + } return result(e); + } } else { + if (m_trace) { + ios().get_diagnostic_channel() << "unable to synthesize instance for: " << m_type << "\n"; + } return result(e); } } if (tmp_tctx->is_mvar_assigned(i)) continue; - // TODO REMOVE DEBUG - expr m_assigned = tmp_tctx->instantiate_uvars_mvars(m); - - if (tmp_tctx->is_prop(tmp_tctx->infer(m))) { - // TODO try to prove - return result(e); + expr m_type = tmp_tctx->instantiate_uvars_mvars(tmp_tctx->infer(m)); + if (tmp_tctx->is_prop(m_type)) { + flet set_name(m_rel,get_iff_name()); + result r_cond = simplify(m_type); + if (is_constant(r_cond.get_new()) && const_name(r_cond.get_new()) == get_true_name()) { + auto pf = m_app_builder.mk_app(name("iff","elim_right"),finalize(r_cond).get_proof(),mk_constant(get_true_intro_name())); + lean_assert(pf); + bool success = tmp_tctx->is_def_eq(m,*pf); + lean_assert(success); + continue; + } } if (m_trace) { - ios().get_diagnostic_channel() << "failed to assign: " << m << "\n"; + ios().get_diagnostic_channel() << "failed to assign: " << m << " : " << m_type << "\n"; } /* We fail if there is a meta variable that we still cannot assign */ @@ -459,17 +470,23 @@ result simplifier::rewrite(expr const & e, simp_rule const & sr) { for (unsigned i = 0; i < sr.get_num_umeta(); i++) { if (!tmp_tctx->is_uvar_assigned(i)) return result(e); } - - expr e_s = tmp_tctx->instantiate_uvars_mvars(sr.get_rhs()); - if (sr.is_perm() && !is_lt(e_s,e,false)) return result(e); + expr new_lhs = tmp_tctx->instantiate_uvars_mvars(sr.get_lhs()); + expr new_rhs = tmp_tctx->instantiate_uvars_mvars(sr.get_rhs()); + + if (sr.is_perm()) { + if (!is_lt(new_rhs,new_lhs,false)) + return result(e); + } + expr pf = tmp_tctx->instantiate_uvars_mvars(sr.get_proof()); - return result(result(e_s,pf)); + return result(result(new_rhs,pf)); } /* Congruence */ + result simplifier::congr(result const & r_f, result const & r_arg) { lean_assert(!r_f.is_none() && !r_arg.is_none()); // theorem congr {A B : Type} {f₁ f₂ : A → B} {a₁ a₂ : A} (H₁ : f₁ = f₂) (H₂ : a₁ = a₂) : f₁ a₁ = f₂ a₂ @@ -546,11 +563,11 @@ result simplifier::try_congr(expr const & e, congr_rule const & cr) { for_each(congr_hyps,[&](expr const & m) { if (failed) return; buffer ls; - expr m_type = tmp_tctx->infer(m); + expr m_type = tmp_tctx->instantiate_uvars_mvars(tmp_tctx->infer(m)); while (is_pi(m_type)) { expr d = instantiate_rev(binding_domain(m_type), ls.size(), ls.data()); - expr l = tmp_tctx->mk_tmp_local(d,binding_info(e)); + expr l = tmp_tctx->mk_tmp_local(d,binding_info(m_type)); ls.push_back(l); m_type = instantiate(binding_body(m_type),l); } @@ -563,10 +580,7 @@ result simplifier::try_congr(expr const & e, congr_rule const & cr) { flet set_simplify_caches(m_simplify_caches,fresh_caches); flet set_name(m_rel,const_name(h_rel)); - buffer ls_instantiated; - for (unsigned i = 0; i < ls.size(); i++) ls_instantiated.push_back(tmp_tctx->instantiate_uvars_mvars(ls[i])); - - flet set_ctx_srss(m_ctx_srss,add_to_srss(m_ctx_srss,ls_instantiated)); + flet set_ctx_srss(m_ctx_srss,add_to_srss(m_ctx_srss,ls)); h_lhs = tmp_tctx->instantiate_uvars_mvars(h_lhs); result r_congr_hyp = simplify(h_lhs); @@ -579,8 +593,7 @@ result simplifier::try_congr(expr const & e, congr_rule const & cr) { simplified = true; } - hyp = Fun(ls_instantiated,hyp); - if (!tmp_tctx->is_def_eq(m,hyp)) failed = true; + if (!tmp_tctx->is_def_eq(m,Fun(ls,hyp))) failed = true; } }); diff --git a/src/library/simplifier/ceqv.cpp b/src/library/simplifier/ceqv.cpp index 5b19272b9..8af3ea535 100644 --- a/src/library/simplifier/ceqv.cpp +++ b/src/library/simplifier/ceqv.cpp @@ -100,7 +100,7 @@ class to_ceqvs_fn { } if (is_standard(m_env) && is_prop(e)) { expr new_e = mk_iff(e, mk_true()); - expr new_H = mk_app(mk_constant(get_iff_true_intro_name()), arg1, H); + expr new_H = mk_app(mk_constant(get_iff_true_intro_name()), e, H); return mk_singleton(new_e, new_H); } else { return list(); diff --git a/tests/lean/simplifier10.lean b/tests/lean/simplifier10.lean new file mode 100644 index 000000000..16fefaaa5 --- /dev/null +++ b/tests/lean/simplifier10.lean @@ -0,0 +1,19 @@ +import logic.connectives logic.quantifiers + +universe l +constants (T : Type.{l}) (x y z : T) (P : T → Prop) (Q : T → T → T → Prop) (R W V : T → T → Prop) +constants (px : P x) (wxz : W x z) (vzy : V z y) +constants (H : ∀ (x y z : T), P x → W x z → V z y → (Q z y x ↔ R x y)) +attribute px [simp] +attribute wxz [simp] +attribute vzy [simp] +attribute H [simp] + +#simplify iff 0 P x +#simplify iff 0 W x z +#simplify iff 0 V z y +#simplify iff 0 Q z y x +#simplify iff 0 V z y ↔ Q z y x + + + diff --git a/tests/lean/simplifier10.lean.expected.out b/tests/lean/simplifier10.lean.expected.out new file mode 100644 index 000000000..68d02e2b6 --- /dev/null +++ b/tests/lean/simplifier10.lean.expected.out @@ -0,0 +1,5 @@ +true +true +true +R x y +R x y diff --git a/tests/lean/simplifier11.lean b/tests/lean/simplifier11.lean new file mode 100644 index 000000000..d3ba5999c --- /dev/null +++ b/tests/lean/simplifier11.lean @@ -0,0 +1,74 @@ +-- Conditional congruence +import logic.connectives logic.quantifiers + +namespace if_congr +constants {A : Type} {b c : Prop} (dec_b : decidable b) (dec_c : decidable c) + {x y u v : A} (h_c : b ↔ c) (h_t : x = u) (h_e : y = v) + +local attribute dec_b [instance] +local attribute dec_c [instance] +local attribute h_c [simp] +local attribute h_t [simp] +local attribute h_e [simp] + +attribute if_congr [congr] + +#simplify eq 0 (ite b x y) +end if_congr + +namespace if_ctx_simp_congr +constants {A : Type} {b c : Prop} (dec_b : decidable b) + {x y u v : A} (h_c : b ↔ c) (h_t : c → x = u) (h_e : ¬c → y = v) + +local attribute dec_b [instance] +local attribute h_c [simp] +local attribute h_t [simp] +local attribute h_e [simp] + +attribute if_ctx_simp_congr [congr] + +#simplify eq 0 (ite b x y) + +end if_ctx_simp_congr + +namespace if_congr_prop +constants {b c x y u v : Prop} (dec_b : decidable b) (dec_c : decidable c) + (h_c : b ↔ c) (h_t : c → (x ↔ u)) (h_e : ¬c → (y ↔ v)) + +local attribute dec_b [instance] +local attribute dec_c [instance] +local attribute h_c [simp] +local attribute h_t [simp] +local attribute h_e [simp] + +attribute if_congr_prop [congr] + +#simplify iff 0 (ite b x y) +end if_congr_prop + +namespace if_ctx_simp_congr_prop +constants (b c x y u v : Prop) (dec_b : decidable b) + (h_c : b ↔ c) (h_t : c → (x ↔ u)) (h_e : ¬ c → (y ↔ v)) + +local attribute dec_b [instance] +local attribute h_c [simp] +local attribute h_t [simp] +local attribute h_e [simp] + +attribute if_ctx_simp_congr_prop [congr] +#simplify iff 0 (ite b x y) + +end if_ctx_simp_congr_prop + +namespace if_simp_congr_prop +constants (b c x y u v : Prop) (dec_b : decidable b) + (h_c : b ↔ c) (h_t : x ↔ u) (h_e : y ↔ v) + +local attribute dec_b [instance] +local attribute h_c [simp] +local attribute h_t [simp] +local attribute h_e [simp] + +attribute if_simp_congr_prop [congr] +#simplify iff 0 (ite b x y) +end if_simp_congr_prop diff --git a/tests/lean/simplifier11.lean.expected.out b/tests/lean/simplifier11.lean.expected.out new file mode 100644 index 000000000..bf06007e2 --- /dev/null +++ b/tests/lean/simplifier11.lean.expected.out @@ -0,0 +1,5 @@ +ite c u v +ite c u v +ite c u v +ite c u v +ite c u v diff --git a/tests/lean/simplifier12.lean b/tests/lean/simplifier12.lean new file mode 100644 index 000000000..d18fb6c07 --- /dev/null +++ b/tests/lean/simplifier12.lean @@ -0,0 +1,23 @@ +import algebra.ring +open algebra + +set_option simplify.max_steps 1000 +universe l +constants (T : Type.{l}) (s : algebra.comm_ring T) +constants (x1 x2 x3 x4 : T) (f g : T → T) +attribute s [instance] + +attribute add.comm [simp] +attribute add.assoc [simp] +attribute left_distrib [simp] +attribute right_distrib [simp] + +attribute mul.comm [simp] +attribute mul.assoc [simp] + +theorem add.o2 [simp] {A : Type} [s : add_comm_semigroup A] (a b c : A) : + a + (b + c) = b + (a + c) := sorry + +#simplify eq 0 x2 + (g x1 + (f x3 * 3 * (x2 + g x1 * 7) * x2)) + 5 * (x4 + f x1) + + diff --git a/tests/lean/simplifier12.lean.expected.out b/tests/lean/simplifier12.lean.expected.out new file mode 100644 index 000000000..63325e56d --- /dev/null +++ b/tests/lean/simplifier12.lean.expected.out @@ -0,0 +1 @@ +x2 + (g x1 + (x4 * 5 + (f x1 * 5 + (x2 * (f x3 * (x2 * 3)) + x2 * (f x3 * (3 * (g x1 * 7))))))) diff --git a/tests/lean/simplifier9.lean.expected.out b/tests/lean/simplifier9.lean.expected.out new file mode 100644 index 000000000..168531564 --- /dev/null +++ b/tests/lean/simplifier9.lean.expected.out @@ -0,0 +1,13 @@ +x = y → y = y +T → x = y → y = y +∀ (x_1 : T), x = x_1 → x_1 = y +∀ (x_1 : T), x_1 = x → x = x +T → T → x = y → y = y +T → T → x = y → P y +(∀ (x : T), P x ↔ Q x) → Q x +Prop → (∀ (x : T), P x ↔ Q x) → Prop → Q x +∀ (x_1 : Prop), (∀ (x : T), P x ↔ Q x) → x_1 ∨ Q x +(∀ (x : T), P x ↔ Q x) → Q x +(∀ (x : T), P x ↔ Q x) → Q x +∀ (x : T), T → (∀ (x : T), P x ↔ Q x) → Q x +∀ (x x_1 : T), x = x_1 → (∀ (w : T), P w ↔ Q w) → Q x_1