From 84faef5d5d54cb86a8c4c623a2c88001a0078935 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 14 May 2015 18:25:20 -0700 Subject: [PATCH] feat(library/tactic/rewrite_tactic): rewrite tactic with 'iff' lemmas --- src/library/constants.cpp | 4 +++ src/library/constants.h | 1 + src/library/constants.txt | 1 + src/library/tactic/rewrite_tactic.cpp | 37 ++++++++++++++++------- src/library/util.cpp | 5 +++- src/library/util.h | 4 +++ tests/lean/run/iff_rw.lean | 11 +++++++ tests/lean/run/true_imp_rw.lean | 7 +++++ tests/lean/run/tut_104.lean | 42 +++++++++++++++++++++++++++ 9 files changed, 101 insertions(+), 11 deletions(-) create mode 100644 tests/lean/run/iff_rw.lean create mode 100644 tests/lean/run/true_imp_rw.lean create mode 100644 tests/lean/run/tut_104.lean diff --git a/src/library/constants.cpp b/src/library/constants.cpp index 0f3cd309c6..d518721940 100644 --- a/src/library/constants.cpp +++ b/src/library/constants.cpp @@ -61,6 +61,7 @@ name const * g_prod = nullptr; name const * g_prod_mk = nullptr; name const * g_prod_pr1 = nullptr; name const * g_prod_pr2 = nullptr; +name const * g_propext = nullptr; name const * g_sigma = nullptr; name const * g_sigma_mk = nullptr; name const * g_string = nullptr; @@ -190,6 +191,7 @@ void initialize_constants() { g_prod_mk = new name{"prod", "mk"}; g_prod_pr1 = new name{"prod", "pr1"}; g_prod_pr2 = new name{"prod", "pr2"}; + g_propext = new name{"propext"}; g_sigma = new name{"sigma"}; g_sigma_mk = new name{"sigma", "mk"}; g_string = new name{"string"}; @@ -320,6 +322,7 @@ void finalize_constants() { delete g_prod_mk; delete g_prod_pr1; delete g_prod_pr2; + delete g_propext; delete g_sigma; delete g_sigma_mk; delete g_string; @@ -449,6 +452,7 @@ name const & get_prod_name() { return *g_prod; } name const & get_prod_mk_name() { return *g_prod_mk; } name const & get_prod_pr1_name() { return *g_prod_pr1; } name const & get_prod_pr2_name() { return *g_prod_pr2; } +name const & get_propext_name() { return *g_propext; } name const & get_sigma_name() { return *g_sigma; } name const & get_sigma_mk_name() { return *g_sigma_mk; } name const & get_string_name() { return *g_string; } diff --git a/src/library/constants.h b/src/library/constants.h index 896f874cc2..7c4cbe1511 100644 --- a/src/library/constants.h +++ b/src/library/constants.h @@ -63,6 +63,7 @@ name const & get_prod_name(); name const & get_prod_mk_name(); name const & get_prod_pr1_name(); name const & get_prod_pr2_name(); +name const & get_propext_name(); name const & get_sigma_name(); name const & get_sigma_mk_name(); name const & get_string_name(); diff --git a/src/library/constants.txt b/src/library/constants.txt index 7e5d297e9c..e03222e90a 100644 --- a/src/library/constants.txt +++ b/src/library/constants.txt @@ -56,6 +56,7 @@ prod prod.mk prod.pr1 prod.pr2 +propext sigma sigma.mk string diff --git a/src/library/tactic/rewrite_tactic.cpp b/src/library/tactic/rewrite_tactic.cpp index f464b412f9..38eb200100 100644 --- a/src/library/tactic/rewrite_tactic.cpp +++ b/src/library/tactic/rewrite_tactic.cpp @@ -876,7 +876,7 @@ class rewrite_fn { return replace(e, [&](expr const & e, unsigned) { if (!has_metavar(e)) { return some_expr(e); // done - } else if (is_binding(e)) { + } else if (is_lambda(e)) { unsigned next_idx = m_esubst.size(); expr r = mk_idx_meta(next_idx, m_tc->infer(e).first); m_esubst.push_back(none_expr()); @@ -909,14 +909,21 @@ class rewrite_fn { } else { // Remark: we discard constraints generated producing the pattern. // Patterns are only used to locate positions where the rule should be applied. - expr rule = get_rewrite_rule(e); - expr rule_type = m_relaxed_tc->whnf(m_relaxed_tc->infer(rule).first).first; - while (is_pi(rule_type)) { - expr meta = mk_meta(binding_domain(rule_type)); - rule_type = m_relaxed_tc->whnf(instantiate(binding_body(rule_type), meta)).first; + expr rule = get_rewrite_rule(e); + expr rule_type = m_relaxed_tc->infer(rule).first; + expr new_rule_type = m_relaxed_tc->whnf(rule_type).first; + while (is_pi(new_rule_type)) { + rule_type = new_rule_type; + expr meta = mk_meta(binding_domain(rule_type)); + rule_type = instantiate(binding_body(rule_type), meta); + new_rule_type = m_relaxed_tc->whnf(rule_type).first; } - if (!is_eq(rule_type)) + if (is_standard(m_env)) { + if (!is_eq(rule_type) && !is_iff(rule_type)) + throw_rewrite_exception("invalid rewrite tactic, given lemma is not an equality or iff"); + } else if (!is_eq(rule_type)) { throw_rewrite_exception("invalid rewrite tactic, given lemma is not an equality"); + } if (get_rewrite_info(e).symm()) { return to_meta_idx(app_arg(rule_type)); } else { @@ -1097,8 +1104,12 @@ class rewrite_fn { buffer cs; to_buffer(rcs.second, cs); constraint_seq cs_seq; - expr rule_type = m_relaxed_tc->whnf(m_relaxed_tc->infer(rule, cs_seq), cs_seq); - while (is_pi(rule_type)) { + expr rule_type = m_relaxed_tc->infer(rule, cs_seq); + constraint_seq new_cs_seq; + expr new_rule_type = m_relaxed_tc->whnf(rule_type, new_cs_seq); + while (is_pi(new_rule_type)) { + rule_type = new_rule_type; + cs_seq += new_cs_seq; expr meta; if (binding_info(rule_type).is_inst_implicit()) { auto mc = mk_class_instance_elaborator(binding_domain(rule_type)); @@ -1107,9 +1118,15 @@ class rewrite_fn { } else { meta = mk_meta(binding_domain(rule_type)); } - rule_type = m_relaxed_tc->whnf(instantiate(binding_body(rule_type), meta), cs_seq); + rule_type = instantiate(binding_body(rule_type), meta); + new_rule_type = m_relaxed_tc->whnf(rule_type , cs_seq); rule = mk_app(rule, meta); } + lean_assert(is_eq(rule_type) || (is_standard(m_env) && is_iff(rule_type))); + if (is_standard(m_env) && is_iff(rule_type)) { + rule = apply_propext(rule, rule_type); + rule_type = mk_eq(*m_relaxed_tc, app_arg(app_fn(rule_type)), app_arg(rule_type)); + } lean_assert(is_eq(rule_type)); bool symm = get_rewrite_info(orig_elem).symm(); expr src; diff --git a/src/library/util.cpp b/src/library/util.cpp index ec38c61d38..b3deee54ba 100644 --- a/src/library/util.cpp +++ b/src/library/util.cpp @@ -393,10 +393,13 @@ bool is_iff(expr const & e) { expr mk_iff(expr const & lhs, expr const & rhs) { return mk_app(mk_constant(get_iff_name()), lhs, rhs); } - expr mk_iff_refl(expr const & a) { return mk_app(mk_constant(get_iff_refl_name()), a); } +expr apply_propext(expr const & iff_pr, expr const & iff_term) { + lean_assert(is_iff(iff_term)); + return mk_app(mk_constant(get_propext_name()), app_arg(app_fn(iff_term)), app_arg(iff_term), iff_pr); +} expr mk_eq(type_checker & tc, expr const & lhs, expr const & rhs) { expr A = tc.whnf(tc.infer(lhs).first).first; diff --git a/src/library/util.h b/src/library/util.h index 96eaedb1e2..4dc6f1d62e 100644 --- a/src/library/util.h +++ b/src/library/util.h @@ -153,6 +153,10 @@ bool is_heq(expr const & e, expr & A, expr & lhs, expr & B, expr & rhs); bool is_iff(expr const & e); expr mk_iff(expr const & lhs, expr const & rhs); expr mk_iff_refl(expr const & a); +/** \brief Given iff_pr : iff_term, where \c iff_term is of the form l <-> r, + return the term propext l r iff_pr +*/ +expr apply_propext(expr const & iff_pr, expr const & iff_term); /** \brief If in HoTT mode, apply lift.down. The no_confusion constructions uses lifts in the proof relevant version (aka HoTT mode). diff --git a/tests/lean/run/iff_rw.lean b/tests/lean/run/iff_rw.lean new file mode 100644 index 0000000000..67453f8636 --- /dev/null +++ b/tests/lean/run/iff_rw.lean @@ -0,0 +1,11 @@ +import logic + +example (a b : Prop) : a ∧ b → b ∧ a := +begin + intros, rewrite and.comm, assumption +end + +example (a b c : Prop) : a ∧ b ∧ c → b ∧ a ∧ c := +begin + intros, rewrite [-and.assoc, {b ∧ a}and.comm, and.assoc], assumption +end diff --git a/tests/lean/run/true_imp_rw.lean b/tests/lean/run/true_imp_rw.lean new file mode 100644 index 0000000000..57b60b3c8b --- /dev/null +++ b/tests/lean/run/true_imp_rw.lean @@ -0,0 +1,7 @@ +import logic + +example (a b c : Prop) (h : a) : true → true → a := +begin + rewrite *true_imp, + exact h +end diff --git a/tests/lean/run/tut_104.lean b/tests/lean/run/tut_104.lean new file mode 100644 index 0000000000..ae626f987f --- /dev/null +++ b/tests/lean/run/tut_104.lean @@ -0,0 +1,42 @@ +import data.set +namespace function +section +open set +variables {A B : Type} +set_option pp.beta false +definition bijective (f : A → B) := injective f ∧ surjective f + +lemma injective_eq_inj_on_univ₁ (f : A → B) : injective f = inj_on f univ := + begin + esimp [injective, inj_on, univ, mem], + apply propext, + apply iff.intro, + intro Pl a1 a2, + rewrite *true_imp, + exact Pl a1 a2, + intro Pr a1 a2, + exact Pr trivial trivial + end + +lemma injective_eq_inj_on_univ₂ (f : A → B) : injective f = inj_on f univ := + begin + esimp [injective, inj_on, univ, mem], + apply propext, + apply iff.intro, + intro Pl a1 a2, + rewrite *(propext !true_imp), + exact Pl a1 a2, + intro Pr a1 a2, + exact Pr trivial trivial + end + +lemma injective_eq_inj_on_univ₃ (f : A → B) : injective f = inj_on f univ := + begin + esimp [injective, inj_on, univ, mem], + apply propext, + repeat (apply forall_congr; intros), + rewrite *(propext !true_imp) + end +end + +end function