diff --git a/src/library/tactic/simp_lemmas.cpp b/src/library/tactic/simp_lemmas.cpp index 06f8562dec..e80907462e 100644 --- a/src/library/tactic/simp_lemmas.cpp +++ b/src/library/tactic/simp_lemmas.cpp @@ -38,6 +38,7 @@ struct simp_lemma_cell { expr m_lhs; expr m_rhs; + expr m_proof; unsigned m_priority; MK_LEAN_RC(); // Declare m_rc counter void dealloc(); @@ -45,38 +46,27 @@ struct simp_lemma_cell { simp_lemma_cell(simp_lemma_kind k, name const & id, levels const & umetas, list const & emetas, list const & instances, expr const & lhs, expr const & rhs, - unsigned priority): + expr const & proof, unsigned priority): m_kind(k), m_id(id), m_umetas(umetas), m_emetas(emetas), m_instances(instances), - m_lhs(lhs), m_rhs(rhs), m_priority(priority), m_rc(0) {} + m_lhs(lhs), m_rhs(rhs), m_proof(proof), m_priority(priority), m_rc(0) {} }; -struct simp_lemma_with_proof_cell : public simp_lemma_cell { - expr m_proof; - simp_lemma_with_proof_cell(simp_lemma_kind k, - name const & id, levels const & umetas, list const & emetas, - list const & instances, expr const & lhs, expr const & rhs, - expr const & proof, unsigned priority): - simp_lemma_cell(k, id, umetas, emetas, instances, lhs, rhs, priority), - m_proof(proof) { - } -}; - -struct regular_simp_lemma_cell : public simp_lemma_with_proof_cell { +struct regular_simp_lemma_cell : public simp_lemma_cell { bool m_is_permutation; regular_simp_lemma_cell(name const & id, levels const & umetas, list const & emetas, list const & instances, expr const & lhs, expr const & rhs, expr const & proof, bool is_perm, unsigned priority): - simp_lemma_with_proof_cell(simp_lemma_kind::Simp, id, umetas, emetas, instances, lhs, rhs, proof, priority), + simp_lemma_cell(simp_lemma_kind::Simp, id, umetas, emetas, instances, lhs, rhs, proof, priority), m_is_permutation(is_perm) { } }; -struct congr_lemma_cell : public simp_lemma_with_proof_cell { +struct congr_lemma_cell : public simp_lemma_cell { list m_congr_hyps; congr_lemma_cell(name const & id, levels const & umetas, list const & emetas, list const & instances, expr const & lhs, expr const & rhs, expr const & proof, list const & congr_hyps, unsigned priority): - simp_lemma_with_proof_cell(simp_lemma_kind::Congr, id, umetas, emetas, instances, lhs, rhs, proof, priority), + simp_lemma_cell(simp_lemma_kind::Congr, id, umetas, emetas, instances, lhs, rhs, proof, priority), m_congr_hyps(congr_hyps) { } }; @@ -84,7 +74,7 @@ struct congr_lemma_cell : public simp_lemma_with_proof_cell { void simp_lemma_cell::dealloc() { switch (m_kind) { case simp_lemma_kind::Simp: - delete static_cast(this); + delete static_cast(this); break; case simp_lemma_kind::Congr: delete static_cast(this); @@ -171,8 +161,7 @@ bool simp_lemma::is_permutation() const { } expr const & simp_lemma::get_proof() const { - lean_assert(kind() == simp_lemma_kind::Congr || kind() == simp_lemma_kind::Simp); - return static_cast(m_ptr)->m_proof; + return m_ptr->m_proof; } list const & simp_lemma::get_congr_hyps() const { @@ -221,10 +210,10 @@ simp_lemma mk_simp_lemma(name const & id, levels const & umetas, list cons } simp_lemma mk_rfl_lemma(name const & id, levels const & umetas, list const & emetas, - list const & instances, expr const & lhs, expr const & rhs, + list const & instances, expr const & lhs, expr const & rhs, expr const & proof, unsigned priority) { return simp_lemma(new simp_lemma_cell(simp_lemma_kind::Refl, id, umetas, emetas, - instances, lhs, rhs, priority)); + instances, lhs, rhs, proof, priority)); } simp_lemma mk_congr_lemma(name const & id, levels const & umetas, list const & emetas, @@ -751,6 +740,7 @@ static simp_lemmas add_core(type_context & ctx, simp_lemmas const & s, name cons declaration const & d = env.get(cname); levels ls = mk_tmp_levels_for(ctx, d); expr type = instantiate_type_univ_params(d, ls); + expr proof = mk_constant(cname, ls); if (is_rfl_lemma(env, cname)) { buffer emetas; buffer instances; @@ -759,15 +749,15 @@ static simp_lemmas add_core(type_context & ctx, simp_lemmas const & s, name cons emetas.push_back(mvar); instances.push_back(binding_info(type).is_inst_implicit()); type = instantiate(binding_body(type), mvar); + proof = mk_app(proof, mvar); } expr lhs, rhs; lean_verify(is_eq(type, lhs, rhs)); simp_lemmas new_s = s; new_s.insert(get_eq_name(), mk_rfl_lemma(cname, ls, to_list(emetas), to_list(instances), - lhs, rhs, priority)); + lhs, rhs, proof, priority)); return new_s; } else { - expr proof = mk_constant(cname, ls); return add_core(ctx, s, cname, ls, type, proof, priority); } } diff --git a/src/library/tactic/simp_lemmas.h b/src/library/tactic/simp_lemmas.h index efa9b13af5..3df3805d53 100644 --- a/src/library/tactic/simp_lemmas.h +++ b/src/library/tactic/simp_lemmas.h @@ -23,7 +23,7 @@ private: list const & instances, expr const & lhs, expr const & rhs, expr const & proof, bool is_perm, unsigned priority); friend simp_lemma mk_rfl_lemma(name const & id, levels const & umetas, list const & emetas, - list const & instances, expr const & lhs, expr const & rhs, + list const & instances, expr const & lhs, expr const & rhs, expr const & proof, unsigned priority); friend simp_lemma mk_congr_lemma(name const & id, levels const & umetas, list const & emetas, list const & instances, expr const & lhs, expr const & rhs, diff --git a/src/library/tactic/simplify.cpp b/src/library/tactic/simplify.cpp index 35be07036c..5e3f2919d5 100644 --- a/src/library/tactic/simplify.cpp +++ b/src/library/tactic/simplify.cpp @@ -591,12 +591,8 @@ simp_result simplify_core_fn::rewrite_core(expr const & e, simp_lemma const & sl } } - if (sl.is_refl()) { - return simp_result(new_rhs); - } else { - expr pf = tmp_ctx.instantiate_mvars(sl.get_proof()); - return simp_result(new_rhs, pf); - } + expr pf = tmp_ctx.instantiate_mvars(sl.get_proof()); + return simp_result(new_rhs, pf); } simp_result simplify_core_fn::rewrite(expr const & e, simp_lemma const & sl) { diff --git a/tests/lean/run/simp_refl_lemma_perf_issue.lean b/tests/lean/run/simp_refl_lemma_perf_issue.lean new file mode 100644 index 0000000000..93daf4a335 --- /dev/null +++ b/tests/lean/run/simp_refl_lemma_perf_issue.lean @@ -0,0 +1,15 @@ +def foo (a : nat) (b : nat) := b +def g (a : nat) := foo (1000000000000 + 1) a +def f (a : nat) := foo (1 + 1000000000000) a + +lemma foo_lemma (a b : nat) : foo b a = foo (1 + 1000000000000) a := +rfl + +lemma f_fold_lemma (a : nat) : foo (1 + 1000000000000) a = f a := +rfl + +lemma ex (a : nat) (p : nat → Prop) (h : p (f a)) : p (g a) := +begin + simp only [g, foo_lemma, f_fold_lemma], + exact h, +end