max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

refactor(library/tactic/defeq_simplifier): move defeq_simp_lemmas to library

Browse source 
This commit also renames them to "rfl_lemmas".
Reason: these lemmas will be used at type_context::is_def_eq and type_context::whnf
This commit is contained in:
Leonardo de Moura 2016-09-12 10:36:11 -07:00
parent 0b90ace9f8
commit d43764b6fb
17 changed files with 192 additions and 226 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/CMakeLists.txt
View file

@ -331,8 +331,6 @@ add_subdirectory(library)
set(LEAN_OBJS ${LEAN_OBJS} $<TARGET_OBJECTS:library>)
add_subdirectory(library/tactic)
set(LEAN_OBJS ${LEAN_OBJS} $<TARGET_OBJECTS:tactic>)
add_subdirectory(library/tactic/defeq_simplifier)
set(LEAN_OBJS ${LEAN_OBJS} $<TARGET_OBJECTS:defeq_simplifier>)
add_subdirectory(library/tactic/simplifier)
set(LEAN_OBJS ${LEAN_OBJS} $<TARGET_OBJECTS:simplifier>)
add_subdirectory(library/tactic/backward)

2
src/frontends/lean/builtin_cmds.cpp
View file

@ -35,8 +35,6 @@ Author: Leonardo de Moura
#include "library/compiler/vm_compiler.h"
#include "library/tactic/kabstract.h"
#include "library/tactic/elaborate.h"
#include "library/tactic/defeq_simplifier/defeq_simp_lemmas.h"
#include "library/tactic/defeq_simplifier/defeq_simplifier.h"
#include "library/tactic/simplifier/simp_extensions.h"
#include "library/tactic/tactic_state.h"
#include "frontends/lean/util.h"

8
src/frontends/lean/print_cmd.cpp
View file

@ -25,8 +25,8 @@ Author: Leonardo de Moura
#include "library/legacy_type_context.h"
#include "library/unification_hint.h"
#include "library/reducible.h"
#include "library/rfl_lemmas.h"
#include "library/tactic/kabstract.h"
#include "library/tactic/defeq_simplifier/defeq_simp_lemmas.h"
#include "library/tactic/simplifier/simp_lemmas.h"
#include "library/tactic/simplifier/simp_extensions.h"
#include "frontends/lean/parser.h"
@ -475,10 +475,10 @@ static void print_unification_hints(parser & p) {
out << pp_unification_hints(get_unification_hints(p.env()), out.get_formatter());
}
static void print_defeq_lemmas(parser & p) {
static void print_rfl_lemmas(parser & p) {
type_checker tc(p.env());
auto out = regular(p.env(), p.ios(), tc);
out << pp_defeq_simp_lemmas(*get_defeq_simp_lemmas(p.env()), out.get_formatter());
out << pp_rfl_lemmas(*get_rfl_lemmas(p.env()), out.get_formatter());
}
static void print_simp_rules(parser & p) {
@ -663,7 +663,7 @@ environment print_cmd(parser & p) {
else if (name == "unify")
print_unification_hints(p);
else if (name == "defeq")
print_defeq_lemmas(p);
print_rfl_lemmas(p);
else if (name == "simp")
print_simp_rules(p);
else if (name == "simp_ext")

2
src/library/CMakeLists.txt
View file

@ -14,7 +14,7 @@ add_library(library OBJECT deep_copy.cpp expr_lt.cpp io_state.cpp
local_context.cpp metavar_context.cpp type_context.cpp export_decl.cpp delayed_abstraction.cpp
fun_info.cpp congr_lemma.cpp defeq_canonizer.cpp scope_pos_info_provider.cpp
mpq_macro.cpp arith_instance_manager.cpp replace_visitor_with_tc.cpp
aux_definition.cpp inverse.cpp library_system.cpp
aux_definition.cpp inverse.cpp library_system.cpp rfl_lemmas.cpp
# Legacy -- The following files will be eventually deleted
normalize.cpp justification.cpp constraint.cpp metavar.cpp choice.cpp locals.cpp

4
src/library/equations_compiler/util.cpp
View file

@ -20,7 +20,7 @@ Author: Leonardo de Moura
#include "library/aux_definition.h"
#include "library/scope_pos_info_provider.h"
#include "library/compiler/vm_compiler.h"
#include "library/tactic/defeq_simplifier/defeq_simplifier.h"
#include "library/tactic/defeq_simplifier.h"
#include "library/equations_compiler/equations.h"
#include "library/equations_compiler/util.h"
@ -301,7 +301,7 @@ static environment add_equation_lemma(environment const & env, options const & o
if (use_dsimp) {
try {
type_context ctx(env, opts, mctx, lctx, transparency_mode::None);
defeq_simp_lemmas_ptr lemmas = get_defeq_simp_lemmas(env, g_eqn_sanitizer_token);
rfl_lemmas_ptr lemmas = get_rfl_lemmas(env, g_eqn_sanitizer_token);
new_type = defeq_simplify(ctx, *lemmas, type);
} catch (defeq_simplifier_exception & ex) {
throw nested_exception("equation compiler failed to simplify type of automatically generated lemma using "

3
src/library/init_module.cpp
View file

@ -48,6 +48,7 @@ Author: Leonardo de Moura
#include "library/mpq_macro.h"
#include "library/arith_instance_manager.h"
#include "library/inverse.h"
#include "library/rfl_lemmas.h"
// #include "library/congr_lemma_manager.h"
// #include "library/light_lt_manager.h"
@ -122,6 +123,7 @@ void initialize_library_module() {
// initialize_congr_lemma_manager();
initialize_fun_info();
initialize_unification_hint();
initialize_rfl_lemmas();
initialize_type_context();
initialize_delayed_abstraction();
initialize_mpq_macro();
@ -135,6 +137,7 @@ void finalize_library_module() {
finalize_mpq_macro();
finalize_delayed_abstraction();
finalize_type_context();
finalize_rfl_lemmas();
finalize_unification_hint();
finalize_fun_info();
// finalize_congr_lemma_manager();

100
src/library/tactic/defeq_simplifier/defeq_simp_lemmas.cpp → src/library/rfl_lemmas.cpp
View file

@ -15,26 +15,26 @@ Author: Daniel Selsam, Leonardo de Moura
#include "library/util.h"
#include "library/scoped_ext.h"
#include "library/type_context.h"
#include "library/tactic/defeq_simplifier/defeq_simp_lemmas.h"
#include "library/rfl_lemmas.h"
namespace lean {
defeq_simp_lemma::defeq_simp_lemma(name const & id, levels const & umetas, list<expr> const & emetas,
list<bool> const & instances, expr const & lhs, expr const & rhs, unsigned priority):
rfl_lemma::rfl_lemma(name const & id, levels const & umetas, list<expr> const & emetas,
list<bool> const & instances, expr const & lhs, expr const & rhs, unsigned priority):
m_id(id), m_umetas(umetas), m_emetas(emetas), m_instances(instances), m_lhs(lhs), m_rhs(rhs), m_priority(priority) {}
bool operator==(defeq_simp_lemma const & sl1, defeq_simp_lemma const & sl2) {
bool operator==(rfl_lemma const & sl1, rfl_lemma const & sl2) {
return sl1.get_lhs() == sl2.get_lhs() && sl1.get_rhs() == sl2.get_rhs();
}
static void throw_non_rfl_proof() {
throw exception("invalid [defeq] simp lemma: proof must be an application of either 'eq.refl' or 'rfl'");
throw exception("invalid reflexivity lemma: proof must be an application of either 'eq.refl' or 'rfl'");
}
static void on_add_defeq_simp_lemma(environment const & env, name const & decl_name, bool) {
static void on_add_rfl_lemma(environment const & env, name const & decl_name, bool) {
type_context ctx(env);
declaration const & d = env.get(decl_name);
if (!d.is_definition()) {
throw exception("invalid [defeq] simp lemma: must be a definition so that definitional equality can be verified");
throw exception("invalid reflexivity lemma: must be a definition so that definitional equality can be verified");
}
expr type = d.get_type();
expr pf = d.get_value();
@ -46,15 +46,15 @@ static void on_add_defeq_simp_lemma(environment const & env, name const & decl_n
}
expr lhs, rhs;
if (!is_eq(type, lhs, rhs))
throw exception("invalid [defeq] simp lemma: body must be an equality");
throw exception("invalid reflexivity lemma: body must be an equality");
if (!is_app_of(pf, get_eq_refl_name(), 2) && !is_app_of(pf, get_rfl_name(), 2))
throw_non_rfl_proof();
if (lhs == rhs)
throw exception("invalid [defeq] simp lemma: the two sides of the equality cannot be structurally equal");
throw exception("invalid reflexivity lemma: the two sides of the equality cannot be structurally equal");
}
static void add_lemma_core(tmp_type_context & ctx, name const & decl_name, unsigned priority,
defeq_simp_lemmas_ptr & result) {
rfl_lemmas_ptr & result) {
environment const & env = ctx.env();
declaration const & d = env.get(decl_name);
lean_assert(d.is_definition());
@ -75,16 +75,16 @@ static void add_lemma_core(tmp_type_context & ctx, name const & decl_name, unsig
}
expr lhs, rhs;
lean_verify(is_eq(type, lhs, rhs));
defeq_simp_lemma lemma(decl_name, to_list(umetas), to_list(emetas), to_list(instances), lhs, rhs, priority);
rfl_lemma lemma(decl_name, to_list(umetas), to_list(emetas), to_list(instances), lhs, rhs, priority);
result->insert(lhs, lemma);
}
static defeq_simp_lemmas_ptr get_defeq_simp_lemmas_from_attribute(type_context & ctx, name const & attr_name) {
static rfl_lemmas_ptr get_rfl_lemmas_from_attribute(type_context & ctx, name const & attr_name) {
environment const & env = ctx.env();
auto const & attr = get_attribute(env, attr_name);
buffer<name> lemmas;
attr.get_instances(env, lemmas);
defeq_simp_lemmas_ptr result = std::make_shared<defeq_simp_lemmas>();
rfl_lemmas_ptr result = std::make_shared<rfl_lemmas>();
unsigned i = lemmas.size();
while (i > 0) {
i--;
@ -96,28 +96,28 @@ static defeq_simp_lemmas_ptr get_defeq_simp_lemmas_from_attribute(type_context &
return result;
}
static defeq_simp_lemmas_ptr get_defeq_simp_lemmas_from_attribute(environment const & env, name const & attr_name) {
static rfl_lemmas_ptr get_rfl_lemmas_from_attribute(environment const & env, name const & attr_name) {
type_context ctx(env);
return get_defeq_simp_lemmas_from_attribute(ctx, attr_name);
return get_rfl_lemmas_from_attribute(ctx, attr_name);
}
static std::vector<name> * g_defeq_simp_attributes = nullptr;
static defeq_lemmas_token g_default_token;
static std::vector<name> * g_rfl_lemmas_attributes = nullptr;
static rfl_lemmas_token g_default_token;
defeq_lemmas_token register_defeq_simp_attribute(name const & attr_name) {
unsigned r = g_defeq_simp_attributes->size();
g_defeq_simp_attributes->push_back(attr_name);
register_system_attribute(basic_attribute::with_check(attr_name, "[defeq] simplification lemma",
on_add_defeq_simp_lemma));
rfl_lemmas_token register_defeq_simp_attribute(name const & attr_name) {
unsigned r = g_rfl_lemmas_attributes->size();
g_rfl_lemmas_attributes->push_back(attr_name);
register_system_attribute(basic_attribute::with_check(attr_name, "reflexivity lemma",
on_add_rfl_lemma));
return r;
}
class defeq_simp_lemmas_cache {
class rfl_lemmas_cache {
struct entry {
environment m_env;
name m_attr_name;
unsigned m_attr_fingerprint;
defeq_simp_lemmas_ptr m_lemmas;
environment m_env;
name m_attr_name;
unsigned m_attr_fingerprint;
rfl_lemmas_ptr m_lemmas;
entry(environment const & env, name const & attr_name):
m_env(env), m_attr_name(attr_name), m_attr_fingerprint(0) {}
};
@ -125,25 +125,25 @@ class defeq_simp_lemmas_cache {
public:
void expand(environment const & env, unsigned new_sz) {
for (unsigned i = m_entries.size(); i < new_sz; i++) {
m_entries.emplace_back(env, (*g_defeq_simp_attributes)[i]);
m_entries.emplace_back(env, (*g_rfl_lemmas_attributes)[i]);
}
}
defeq_simp_lemmas_ptr mk_lemmas(environment const & env, entry & C) {
lean_trace("defeq_simp_lemmas_cache", tout() << "make defeq simp lemmas [" << C.m_attr_name << "]\n";);
rfl_lemmas_ptr mk_lemmas(environment const & env, entry & C) {
lean_trace("rfl_lemmas_cache", tout() << "make reflexivity lemmas [" << C.m_attr_name << "]\n";);
C.m_env = env;
C.m_lemmas = get_defeq_simp_lemmas_from_attribute(env, C.m_attr_name);
C.m_lemmas = get_rfl_lemmas_from_attribute(env, C.m_attr_name);
C.m_attr_fingerprint = get_attribute_fingerprint(env, C.m_attr_name);
return C.m_lemmas;
}
defeq_simp_lemmas_ptr lemmas_of(entry const & C) {
lean_trace("defeq_simp_lemmas_cache", tout() << "reusing cached defeq simp lemmas [" << C.m_attr_name << "]\n";);
rfl_lemmas_ptr lemmas_of(entry const & C) {
lean_trace("rfl_lemmas_cache", tout() << "reusing cached reflexivity lemmas [" << C.m_attr_name << "]\n";);
return C.m_lemmas;
}
defeq_simp_lemmas_ptr get(environment const & env, defeq_lemmas_token token) {
lean_assert(token < g_defeq_simp_attributes->size());
rfl_lemmas_ptr get(environment const & env, rfl_lemmas_token token) {
lean_assert(token < g_rfl_lemmas_attributes->size());
if (token >= m_entries.size()) expand(env, token+1);
lean_assert(token < m_entries.size());
entry & C = m_entries[token];
@ -151,7 +151,7 @@ public:
if (is_eqp(env, C.m_env)) return lemmas_of(C);
if (!env.is_descendant(C.m_env) ||
get_attribute_fingerprint(env, C.m_attr_name) != C.m_attr_fingerprint) {
lean_trace("defeq_simp_lemmas_cache",
lean_trace("rfl_lemmas_cache",
bool c = (get_attribute_fingerprint(env, C.m_attr_name) == C.m_attr_fingerprint);
tout() << "creating new cache, is_descendant: " << env.is_descendant(C.m_env)
<< ", attribute fingerprint compatibility: " << c << "\n";);
@ -161,43 +161,43 @@ public:
}
};
MK_THREAD_LOCAL_GET_DEF(defeq_simp_lemmas_cache, get_cache);
MK_THREAD_LOCAL_GET_DEF(rfl_lemmas_cache, get_cache);
defeq_simp_lemmas_ptr get_defeq_simp_lemmas(environment const & env) {
rfl_lemmas_ptr get_rfl_lemmas(environment const & env) {
return get_cache().get(env, g_default_token);
}
defeq_simp_lemmas_ptr get_defeq_simp_lemmas(environment const & env, defeq_lemmas_token token) {
rfl_lemmas_ptr get_rfl_lemmas(environment const & env, rfl_lemmas_token token) {
return get_cache().get(env, token);
}
format defeq_simp_lemma::pp(formatter const & fmt) const {
format rfl_lemma::pp(formatter const & fmt) const {
format r;
r += format("#") + format(get_num_emeta());
r += format(m_id) + space() + format("#") + format(get_num_emeta());
if (get_priority() != LEAN_DEFAULT_PRIORITY)
r += space() + paren(format(get_priority()));
r += space() + paren(format("prio:") + space() + format(get_priority()));
format r1 = comma() + space() + fmt(get_lhs());
r1 += space() + format("↦") + pp_indent_expr(fmt, get_rhs());
r += group(r1);
return r;
}
format pp_defeq_simp_lemmas(defeq_simp_lemmas const & lemmas, formatter const & fmt) {
format pp_rfl_lemmas(rfl_lemmas const & lemmas, formatter const & fmt) {
format r;
r += format("defeq simp lemmas") + colon() + line();
lemmas.for_each_entry([&](head_index const &, defeq_simp_lemma const & lemma) {
r += format("reflexivity lemmas") + colon() + line();
lemmas.for_each_entry([&](head_index const &, rfl_lemma const & lemma) {
r += lemma.pp(fmt) + line();
});
return r;
}
void initialize_defeq_simp_lemmas() {
register_trace_class("defeq_simp_lemmas_cache");
g_defeq_simp_attributes = new std::vector<name>();
void initialize_rfl_lemmas() {
register_trace_class("rfl_lemmas_cache");
g_rfl_lemmas_attributes = new std::vector<name>();
g_default_token = register_defeq_simp_attribute("defeq");
}
void finalize_defeq_simp_lemmas() {
delete g_defeq_simp_attributes;
void finalize_rfl_lemmas() {
delete g_rfl_lemmas_attributes;
}
}

33
src/library/tactic/defeq_simplifier/defeq_simp_lemmas.h → src/library/rfl_lemmas.h
View file

@ -9,8 +9,7 @@ Author: Daniel Selsam
#include "library/head_map.h"
namespace lean {
class defeq_simp_lemma {
class rfl_lemma {
name m_id;
levels m_umetas;
list<expr> m_emetas;
@ -20,9 +19,9 @@ class defeq_simp_lemma {
expr m_rhs;
unsigned m_priority;
public:
defeq_simp_lemma() {}
defeq_simp_lemma(name const & id, levels const & umetas, list<expr> const & emetas,
list<bool> const & instances, expr const & lhs, expr const & rhs, unsigned priority);
rfl_lemma() {}
rfl_lemma(name const & id, levels const & umetas, list<expr> const & emetas,
list<bool> const & instances, expr const & lhs, expr const & rhs, unsigned priority);
name const & get_id() const { return m_id; }
unsigned get_num_umeta() const { return length(m_umetas); }
@ -42,24 +41,24 @@ public:
format pp(formatter const & fmt) const;
};
bool operator==(defeq_simp_lemma const & sl1, defeq_simp_lemma const & sl2);
inline bool operator!=(defeq_simp_lemma const & sl1, defeq_simp_lemma const & sl2) { return !operator==(sl1, sl2); }
bool operator==(rfl_lemma const & sl1, rfl_lemma const & sl2);
inline bool operator!=(rfl_lemma const & sl1, rfl_lemma const & sl2) { return !operator==(sl1, sl2); }
struct defeq_simp_lemma_prio_fn { unsigned operator()(defeq_simp_lemma const & sl) const { return sl.get_priority(); } };
typedef head_map_prio<defeq_simp_lemma, defeq_simp_lemma_prio_fn> defeq_simp_lemmas;
struct rfl_lemma_prio_fn { unsigned operator()(rfl_lemma const & sl) const { return sl.get_priority(); } };
typedef head_map_prio<rfl_lemma, rfl_lemma_prio_fn> rfl_lemmas;
typedef unsigned defeq_lemmas_token;
typedef unsigned rfl_lemmas_token;
/* Register a system level defeq attribute. This method must only be invoked during initialization.
It returns an internal "token" for retrieving the lemmas */
defeq_lemmas_token register_defeq_simp_attribute(name const & attr_name);
rfl_lemmas_token register_defeq_simp_attribute(name const & attr_name);
typedef std::shared_ptr<defeq_simp_lemmas> defeq_simp_lemmas_ptr;
defeq_simp_lemmas_ptr get_defeq_simp_lemmas(environment const & env);
defeq_simp_lemmas_ptr get_defeq_simp_lemmas(environment const & env, defeq_lemmas_token token);
typedef std::shared_ptr<rfl_lemmas> rfl_lemmas_ptr;
rfl_lemmas_ptr get_rfl_lemmas(environment const & env);
rfl_lemmas_ptr get_rfl_lemmas(environment const & env, rfl_lemmas_token token);
format pp_defeq_simp_lemmas(defeq_simp_lemmas const & lemmas, formatter const & fmt);
format pp_rfl_lemmas(rfl_lemmas const & lemmas, formatter const & fmt);
void initialize_defeq_simp_lemmas();
void finalize_defeq_simp_lemmas();
void initialize_rfl_lemmas();
void finalize_rfl_lemmas();
}

2
src/library/tactic/CMakeLists.txt
View file

@ -6,4 +6,4 @@ add_library(tactic OBJECT occurrences.cpp kabstract.cpp tactic_state.cpp
ac_tactics.cpp induction_tactic.cpp cases_tactic.cpp
generalize_tactic.cpp rewrite_tactic.cpp unfold_tactic.cpp
hsubstitution.cpp gexpr.cpp elaborate.cpp init_module.cpp
simp_result.cpp user_attribute.cpp)
simp_result.cpp user_attribute.cpp defeq_simplifier.cpp)

20
src/library/tactic/defeq_simplifier/defeq_simplifier.cpp → src/library/tactic/defeq_simplifier.cpp
View file

@ -15,7 +15,7 @@ Author: Daniel Selsam
#include "library/defeq_canonizer.h"
#include "library/vm/vm_expr.h"
#include "library/tactic/tactic_state.h"
#include "library/tactic/defeq_simplifier/defeq_simplifier.h"
#include "library/tactic/defeq_simplifier.h"
#ifndef LEAN_DEFAULT_DEFEQ_SIMPLIFY_MAX_SIMP_ROUNDS
#define LEAN_DEFAULT_DEFEQ_SIMPLIFY_MAX_SIMP_ROUNDS 5000
@ -75,7 +75,7 @@ static bool get_simplify_canonize_proofs(options const & o) {
class defeq_simplify_fn {
type_context & m_ctx;
defeq_simp_lemmas m_simp_lemmas;
rfl_lemmas m_simp_lemmas;
unsigned m_num_simp_rounds{0};
unsigned m_num_rewrite_rounds{0};
@ -246,19 +246,19 @@ class defeq_simplify_fn {
"the current limit is " << m_max_rewrite_rounds << ") "
"(use `set_option trace.defeq_simplifier true` to obtain more information");
}
list<defeq_simp_lemma> const * simp_lemmas_ptr = m_simp_lemmas.find(e);
list<rfl_lemma> const * simp_lemmas_ptr = m_simp_lemmas.find(e);
if (!simp_lemmas_ptr) return e;
buffer<defeq_simp_lemma> simp_lemmas;
buffer<rfl_lemma> simp_lemmas;
to_buffer(*simp_lemmas_ptr, simp_lemmas);
expr e_start = e;
for (defeq_simp_lemma const & sl : simp_lemmas) e = rewrite(e, sl);
for (rfl_lemma const & sl : simp_lemmas) e = rewrite(e, sl);
if (e == e_start) break;
}
return e;
}
expr rewrite(expr const & e, defeq_simp_lemma const & sl) {
expr rewrite(expr const & e, rfl_lemma const & sl) {
type_context::tmp_mode_scope scope(m_ctx, sl.get_num_umeta(), sl.get_num_emeta());
if (!m_ctx.is_def_eq(e, sl.get_lhs())) return e;
@ -320,7 +320,7 @@ class defeq_simplify_fn {
}
public:
defeq_simplify_fn(type_context & ctx, defeq_simp_lemmas const & simp_lemmas):
defeq_simplify_fn(type_context & ctx, rfl_lemmas const & simp_lemmas):
m_ctx(ctx),
m_simp_lemmas(simp_lemmas),
m_max_simp_rounds(get_simplify_max_simp_rounds(ctx.get_options())),
@ -346,7 +346,7 @@ public:
};
/* Entry point */
expr defeq_simplify(type_context & ctx, defeq_simp_lemmas const & simp_lemmas, expr const & e) {
expr defeq_simplify(type_context & ctx, rfl_lemmas const & simp_lemmas, expr const & e) {
return defeq_simplify_fn(ctx, simp_lemmas)(e);
}
@ -354,14 +354,14 @@ vm_obj tactic_defeq_simp(vm_obj const & m, vm_obj const & e, vm_obj const & s0)
type_context ctx = mk_type_context_for(s0, m);
tactic_state const & s = to_tactic_state(s0);
LEAN_TACTIC_TRY;
defeq_simp_lemmas_ptr lemmas = get_defeq_simp_lemmas(s.env());
rfl_lemmas_ptr lemmas = get_rfl_lemmas(s.env());
expr new_e = defeq_simplify(ctx, *lemmas, to_expr(e));
return mk_tactic_success(to_obj(new_e), s);
LEAN_TACTIC_CATCH(s);
}
expr defeq_simplify(type_context & ctx, expr const & e) {
defeq_simp_lemmas_ptr lemmas = get_defeq_simp_lemmas(ctx.env());
rfl_lemmas_ptr lemmas = get_rfl_lemmas(ctx.env());
return defeq_simplify(ctx, *lemmas, e);
}

4
src/library/tactic/defeq_simplifier/defeq_simplifier.h → src/library/tactic/defeq_simplifier.h
View file

@ -6,7 +6,7 @@ Author: Daniel Selsam
#pragma once
#include "kernel/expr.h"
#include "library/type_context.h"
#include "library/tactic/defeq_simplifier/defeq_simp_lemmas.h"
#include "library/rfl_lemmas.h"
namespace lean {
class defeq_simplifier_exception : public exception {
@ -17,7 +17,7 @@ public:
virtual void rethrow() const override { throw *this; }
};
expr defeq_simplify(type_context & ctx, defeq_simp_lemmas const & simp_lemmas, expr const & e);
expr defeq_simplify(type_context & ctx, rfl_lemmas const & simp_lemmas, expr const & e);
expr defeq_simplify(type_context & ctx, expr const & e);
void initialize_defeq_simplifier();
void finalize_defeq_simplifier();

1
src/library/tactic/defeq_simplifier/CMakeLists.txt
View file

@ -1 +0,0 @@
add_library(defeq_simplifier OBJECT init_module.cpp defeq_simp_lemmas.cpp defeq_simplifier.cpp)

20
src/library/tactic/defeq_simplifier/init_module.cpp
View file

@ -1,20 +0,0 @@
/*
Copyright (c) 2016 Daniel Selsam. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Daniel Selsam
*/
#include "library/tactic/defeq_simplifier/defeq_simplifier.h"
#include "library/tactic/defeq_simplifier/defeq_simp_lemmas.h"
namespace lean {
void initialize_defeq_simplifier_module() {
initialize_defeq_simp_lemmas();
initialize_defeq_simplifier();
}
void finalize_defeq_simplifier_module() {
finalize_defeq_simplifier();
finalize_defeq_simp_lemmas();
}
}

11
src/library/tactic/defeq_simplifier/init_module.h
View file

@ -1,11 +0,0 @@
/*
Copyright (c) 2016 Daniel Selsam. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Daniel Selsam
*/
#pragma once
namespace lean {
void initialize_defeq_simplifier_module();
void finalize_defeq_simplifier_module();
}

6
src/library/tactic/init_module.cpp
View file

@ -27,7 +27,7 @@ Author: Leonardo de Moura
#include "library/tactic/unfold_tactic.h"
#include "library/tactic/elaborate.h"
#include "library/tactic/user_attribute.h"
#include "library/tactic/defeq_simplifier/init_module.h"
#include "library/tactic/defeq_simplifier.h"
#include "library/tactic/simplifier/init_module.h"
#include "library/tactic/backward/init_module.h"
@ -54,7 +54,7 @@ void initialize_tactic_module() {
initialize_generalize_tactic();
initialize_rewrite_tactic();
initialize_unfold_tactic();
initialize_defeq_simplifier_module();
initialize_defeq_simplifier();
initialize_simplifier_module();
initialize_backward_module();
initialize_elaborate();
@ -65,7 +65,7 @@ void finalize_tactic_module() {
finalize_elaborate();
finalize_backward_module();
finalize_simplifier_module();
finalize_defeq_simplifier_module();
finalize_defeq_simplifier();
finalize_unfold_tactic();
finalize_rewrite_tactic();
finalize_generalize_tactic();

44
tests/lean/defeq_simp_lemmas1.lean.expected.out
View file

@ -1,22 +1,22 @@
defeq simp lemmas:
#4, d ?x_0 ?x_1 ?x_2 ?x_3 ↦ f (f ?x_0 ?x_1 ?x_2) (f ?x_1 ?x_2 ?x_3) (f ?x_0 ?x_3 ?x_2)
#3, f ?x_0 ?x_1 ?x_2 ↦ g (g ?x_0 ?x_1) ?x_2
#4, sizeof (?x_2 :: ?x_3) ↦ sizeof ?x_2 + sizeof ?x_3 + 1
#2, sizeof list.nil ↦ 1
#3, sizeof (some ?x_2) ↦ sizeof ?x_2 + 1
#2, sizeof none ↦ 1
#1, sizeof ?x_0 ↦ nat.of_num ?x_0
#1, sizeof ?x_0 ↦ nat.of_pos_num ?x_0
#1, sizeof ?x_0 ↦ 1
#1, sizeof ?x_0 ↦ 1
#1, sizeof ?x_0 ↦ 1
#6, sizeof (sigma.mk ?x_4 ?x_5) ↦ sizeof ?x_4 + sizeof ?x_5 + 1
#5, sizeof (sum.inr ?x_4) ↦ sizeof ?x_4 + 1
#5, sizeof (sum.inl ?x_4) ↦ sizeof ?x_4 + 1
#6, sizeof (?x_4, ?x_5) ↦ sizeof ?x_4 + sizeof ?x_5 + 1
#1, sizeof ?x_0 ↦ ?x_0
#2, sizeof ?x_1 ↦ 0
#2, id ?x_1 ↦ ?x_1
#2, g ?x_0 ?x_1 ↦ h ?x_1
#3, ?x_1 ≠ ?x_2 ↦ ¬?x_1 = ?x_2
#1, h ?x_0 ↦ q ?x_0
reflexivity lemmas:
foo.d.def #4, d ?x_0 ?x_1 ?x_2 ?x_3 ↦ f (f ?x_0 ?x_1 ?x_2) (f ?x_1 ?x_2 ?x_3) (f ?x_0 ?x_3 ?x_2)
foo.f.def #3, f ?x_0 ?x_1 ?x_2 ↦ g (g ?x_0 ?x_1) ?x_2
sizeof_list_cons_eq #4, sizeof (?x_2 :: ?x_3) ↦ sizeof ?x_2 + sizeof ?x_3 + 1
sizeof_list_nil_eq #2, sizeof list.nil ↦ 1
sizeof_option_some_eq #3, sizeof (some ?x_2) ↦ sizeof ?x_2 + 1
sizeof_option_none_eq #2, sizeof none ↦ 1
sizeof_num_eq #1, sizeof ?x_0 ↦ nat.of_num ?x_0
sizeof_pos_num_eq #1, sizeof ?x_0 ↦ nat.of_pos_num ?x_0
sizeof_bool_eq #1, sizeof ?x_0 ↦ 1
sizeof_poly_unit_eq #1, sizeof ?x_0 ↦ 1
sizeof_unit_eq #1, sizeof ?x_0 ↦ 1
sizeof_sigma_eq #6, sizeof (sigma.mk ?x_4 ?x_5) ↦ sizeof ?x_4 + sizeof ?x_5 + 1
sizeof_sum_eq_right #5, sizeof (sum.inr ?x_4) ↦ sizeof ?x_4 + 1
sizeof_sum_eq_left #5, sizeof (sum.inl ?x_4) ↦ sizeof ?x_4 + 1
sizeof_prod_eq #6, sizeof (?x_4, ?x_5) ↦ sizeof ?x_4 + sizeof ?x_5 + 1
sizeof_nat_eq #1, sizeof ?x_0 ↦ ?x_0
default_has_sizeof_eq #2, sizeof ?x_1 ↦ 0
id.def #2, id ?x_1 ↦ ?x_1
foo.g.def #2, g ?x_0 ?x_1 ↦ h ?x_1
ne.def #3, ?x_1 ≠ ?x_2 ↦ ¬?x_1 = ?x_2
foo.h.def #1, h ?x_0 ↦ q ?x_0

156
tests/lean/defeq_simp_lemmas2.lean.expected.out
View file

@ -1,78 +1,78 @@
defeq simp lemmas:
#4, d ?x_0 ?x_1 ?x_2 ?x_3 ↦ f (f ?x_0 ?x_1 ?x_2) (f ?x_1 ?x_2 ?x_3) (f ?x_0 ?x_3 ?x_2)
#4, d ?x_0 ?x_1 ?x_2 ?x_3 ↦ ?x_2
#3, f ?x_0 ?x_1 ?x_2 ↦ g (g ?x_0 ?x_1) ?x_2
#3, f ?x_0 ?x_1 ?x_2 ↦ ?x_2
#4, sizeof (?x_2 :: ?x_3) ↦ sizeof ?x_2 + sizeof ?x_3 + 1
#2, sizeof list.nil ↦ 1
#3, sizeof (some ?x_2) ↦ sizeof ?x_2 + 1
#2, sizeof none ↦ 1
#1, sizeof ?x_0 ↦ nat.of_num ?x_0
#1, sizeof ?x_0 ↦ nat.of_pos_num ?x_0
#1, sizeof ?x_0 ↦ 1
#1, sizeof ?x_0 ↦ 1
#1, sizeof ?x_0 ↦ 1
#6, sizeof (sigma.mk ?x_4 ?x_5) ↦ sizeof ?x_4 + sizeof ?x_5 + 1
#5, sizeof (sum.inr ?x_4) ↦ sizeof ?x_4 + 1
#5, sizeof (sum.inl ?x_4) ↦ sizeof ?x_4 + 1
#6, sizeof (?x_4, ?x_5) ↦ sizeof ?x_4 + sizeof ?x_5 + 1
#1, sizeof ?x_0 ↦ ?x_0
#2, sizeof ?x_1 ↦ 0
#2, id ?x_1 ↦ ?x_1
#2, g ?x_0 ?x_1 ↦ h ?x_1
#2, g ?x_0 ?x_1 ↦ ?x_1
#3, ?x_1 ≠ ?x_2 ↦ ¬?x_1 = ?x_2
#1, h ?x_0 ↦ q ?x_0
#1, h ?x_0 ↦ ?x_0
defeq simp lemmas:
#4 (1001), d ?x_0 ?x_1 ?x_2 ?x_3 ↦ ?x_2
#4, d ?x_0 ?x_1 ?x_2 ?x_3 ↦ f (f ?x_0 ?x_1 ?x_2) (f ?x_1 ?x_2 ?x_3) (f ?x_0 ?x_3 ?x_2)
#3 (1001), f ?x_0 ?x_1 ?x_2 ↦ ?x_2
#3, f ?x_0 ?x_1 ?x_2 ↦ g (g ?x_0 ?x_1) ?x_2
#4, sizeof (?x_2 :: ?x_3) ↦ sizeof ?x_2 + sizeof ?x_3 + 1
#2, sizeof list.nil ↦ 1
#3, sizeof (some ?x_2) ↦ sizeof ?x_2 + 1
#2, sizeof none ↦ 1
#1, sizeof ?x_0 ↦ nat.of_num ?x_0
#1, sizeof ?x_0 ↦ nat.of_pos_num ?x_0
#1, sizeof ?x_0 ↦ 1
#1, sizeof ?x_0 ↦ 1
#1, sizeof ?x_0 ↦ 1
#6, sizeof (sigma.mk ?x_4 ?x_5) ↦ sizeof ?x_4 + sizeof ?x_5 + 1
#5, sizeof (sum.inr ?x_4) ↦ sizeof ?x_4 + 1
#5, sizeof (sum.inl ?x_4) ↦ sizeof ?x_4 + 1
#6, sizeof (?x_4, ?x_5) ↦ sizeof ?x_4 + sizeof ?x_5 + 1
#1, sizeof ?x_0 ↦ ?x_0
#2, sizeof ?x_1 ↦ 0
#2, id ?x_1 ↦ ?x_1
#2 (1001), g ?x_0 ?x_1 ↦ ?x_1
#2, g ?x_0 ?x_1 ↦ h ?x_1
#3, ?x_1 ≠ ?x_2 ↦ ¬?x_1 = ?x_2
#1 (1001), h ?x_0 ↦ ?x_0
#1, h ?x_0 ↦ q ?x_0
defeq simp lemmas:
#4 (1001), d ?x_0 ?x_1 ?x_2 ?x_3 ↦ f (f ?x_0 ?x_1 ?x_2) (f ?x_1 ?x_2 ?x_3) (f ?x_0 ?x_3 ?x_2)
#4 (1001), d ?x_0 ?x_1 ?x_2 ?x_3 ↦ ?x_2
#3 (1001), f ?x_0 ?x_1 ?x_2 ↦ g (g ?x_0 ?x_1) ?x_2
#3 (1001), f ?x_0 ?x_1 ?x_2 ↦ ?x_2
#4, sizeof (?x_2 :: ?x_3) ↦ sizeof ?x_2 + sizeof ?x_3 + 1
#2, sizeof list.nil ↦ 1
#3, sizeof (some ?x_2) ↦ sizeof ?x_2 + 1
#2, sizeof none ↦ 1
#1, sizeof ?x_0 ↦ nat.of_num ?x_0
#1, sizeof ?x_0 ↦ nat.of_pos_num ?x_0
#1, sizeof ?x_0 ↦ 1
#1, sizeof ?x_0 ↦ 1
#1, sizeof ?x_0 ↦ 1
#6, sizeof (sigma.mk ?x_4 ?x_5) ↦ sizeof ?x_4 + sizeof ?x_5 + 1
#5, sizeof (sum.inr ?x_4) ↦ sizeof ?x_4 + 1
#5, sizeof (sum.inl ?x_4) ↦ sizeof ?x_4 + 1
#6, sizeof (?x_4, ?x_5) ↦ sizeof ?x_4 + sizeof ?x_5 + 1
#1, sizeof ?x_0 ↦ ?x_0
#2, sizeof ?x_1 ↦ 0
#2, id ?x_1 ↦ ?x_1
#2 (1001), g ?x_0 ?x_1 ↦ h ?x_1
#2 (1001), g ?x_0 ?x_1 ↦ ?x_1
#3, ?x_1 ≠ ?x_2 ↦ ¬?x_1 = ?x_2
#1 (1001), h ?x_0 ↦ q ?x_0
#1 (1001), h ?x_0 ↦ ?x_0
reflexivity lemmas:
foo.d.def #4, d ?x_0 ?x_1 ?x_2 ?x_3 ↦ f (f ?x_0 ?x_1 ?x_2) (f ?x_1 ?x_2 ?x_3) (f ?x_0 ?x_3 ?x_2)
foo.d.rfl #4, d ?x_0 ?x_1 ?x_2 ?x_3 ↦ ?x_2
foo.f.def #3, f ?x_0 ?x_1 ?x_2 ↦ g (g ?x_0 ?x_1) ?x_2
foo.f.rfl #3, f ?x_0 ?x_1 ?x_2 ↦ ?x_2
sizeof_list_cons_eq #4, sizeof (?x_2 :: ?x_3) ↦ sizeof ?x_2 + sizeof ?x_3 + 1
sizeof_list_nil_eq #2, sizeof list.nil ↦ 1
sizeof_option_some_eq #3, sizeof (some ?x_2) ↦ sizeof ?x_2 + 1
sizeof_option_none_eq #2, sizeof none ↦ 1
sizeof_num_eq #1, sizeof ?x_0 ↦ nat.of_num ?x_0
sizeof_pos_num_eq #1, sizeof ?x_0 ↦ nat.of_pos_num ?x_0
sizeof_bool_eq #1, sizeof ?x_0 ↦ 1
sizeof_poly_unit_eq #1, sizeof ?x_0 ↦ 1
sizeof_unit_eq #1, sizeof ?x_0 ↦ 1
sizeof_sigma_eq #6, sizeof (sigma.mk ?x_4 ?x_5) ↦ sizeof ?x_4 + sizeof ?x_5 + 1
sizeof_sum_eq_right #5, sizeof (sum.inr ?x_4) ↦ sizeof ?x_4 + 1
sizeof_sum_eq_left #5, sizeof (sum.inl ?x_4) ↦ sizeof ?x_4 + 1
sizeof_prod_eq #6, sizeof (?x_4, ?x_5) ↦ sizeof ?x_4 + sizeof ?x_5 + 1
sizeof_nat_eq #1, sizeof ?x_0 ↦ ?x_0
default_has_sizeof_eq #2, sizeof ?x_1 ↦ 0
id.def #2, id ?x_1 ↦ ?x_1
foo.g.def #2, g ?x_0 ?x_1 ↦ h ?x_1
foo.g.rfl #2, g ?x_0 ?x_1 ↦ ?x_1
ne.def #3, ?x_1 ≠ ?x_2 ↦ ¬?x_1 = ?x_2
foo.h.def #1, h ?x_0 ↦ q ?x_0
foo.h.rfl #1, h ?x_0 ↦ ?x_0
reflexivity lemmas:
foo.d.rfl #4 (prio: 1001), d ?x_0 ?x_1 ?x_2 ?x_3 ↦ ?x_2
foo.d.def #4, d ?x_0 ?x_1 ?x_2 ?x_3 ↦ f (f ?x_0 ?x_1 ?x_2) (f ?x_1 ?x_2 ?x_3) (f ?x_0 ?x_3 ?x_2)
foo.f.rfl #3 (prio: 1001), f ?x_0 ?x_1 ?x_2 ↦ ?x_2
foo.f.def #3, f ?x_0 ?x_1 ?x_2 ↦ g (g ?x_0 ?x_1) ?x_2
sizeof_list_cons_eq #4, sizeof (?x_2 :: ?x_3) ↦ sizeof ?x_2 + sizeof ?x_3 + 1
sizeof_list_nil_eq #2, sizeof list.nil ↦ 1
sizeof_option_some_eq #3, sizeof (some ?x_2) ↦ sizeof ?x_2 + 1
sizeof_option_none_eq #2, sizeof none ↦ 1
sizeof_num_eq #1, sizeof ?x_0 ↦ nat.of_num ?x_0
sizeof_pos_num_eq #1, sizeof ?x_0 ↦ nat.of_pos_num ?x_0
sizeof_bool_eq #1, sizeof ?x_0 ↦ 1
sizeof_poly_unit_eq #1, sizeof ?x_0 ↦ 1
sizeof_unit_eq #1, sizeof ?x_0 ↦ 1
sizeof_sigma_eq #6, sizeof (sigma.mk ?x_4 ?x_5) ↦ sizeof ?x_4 + sizeof ?x_5 + 1
sizeof_sum_eq_right #5, sizeof (sum.inr ?x_4) ↦ sizeof ?x_4 + 1
sizeof_sum_eq_left #5, sizeof (sum.inl ?x_4) ↦ sizeof ?x_4 + 1
sizeof_prod_eq #6, sizeof (?x_4, ?x_5) ↦ sizeof ?x_4 + sizeof ?x_5 + 1
sizeof_nat_eq #1, sizeof ?x_0 ↦ ?x_0
default_has_sizeof_eq #2, sizeof ?x_1 ↦ 0
id.def #2, id ?x_1 ↦ ?x_1
foo.g.rfl #2 (prio: 1001), g ?x_0 ?x_1 ↦ ?x_1
foo.g.def #2, g ?x_0 ?x_1 ↦ h ?x_1
ne.def #3, ?x_1 ≠ ?x_2 ↦ ¬?x_1 = ?x_2
foo.h.rfl #1 (prio: 1001), h ?x_0 ↦ ?x_0
foo.h.def #1, h ?x_0 ↦ q ?x_0
reflexivity lemmas:
foo.d.def #4 (prio: 1001), d ?x_0 ?x_1 ?x_2 ?x_3 ↦ f (f ?x_0 ?x_1 ?x_2) (f ?x_1 ?x_2 ?x_3) (f ?x_0 ?x_3 ?x_2)
foo.d.rfl #4 (prio: 1001), d ?x_0 ?x_1 ?x_2 ?x_3 ↦ ?x_2
foo.f.def #3 (prio: 1001), f ?x_0 ?x_1 ?x_2 ↦ g (g ?x_0 ?x_1) ?x_2
foo.f.rfl #3 (prio: 1001), f ?x_0 ?x_1 ?x_2 ↦ ?x_2
sizeof_list_cons_eq #4, sizeof (?x_2 :: ?x_3) ↦ sizeof ?x_2 + sizeof ?x_3 + 1
sizeof_list_nil_eq #2, sizeof list.nil ↦ 1
sizeof_option_some_eq #3, sizeof (some ?x_2) ↦ sizeof ?x_2 + 1
sizeof_option_none_eq #2, sizeof none ↦ 1
sizeof_num_eq #1, sizeof ?x_0 ↦ nat.of_num ?x_0
sizeof_pos_num_eq #1, sizeof ?x_0 ↦ nat.of_pos_num ?x_0
sizeof_bool_eq #1, sizeof ?x_0 ↦ 1
sizeof_poly_unit_eq #1, sizeof ?x_0 ↦ 1
sizeof_unit_eq #1, sizeof ?x_0 ↦ 1
sizeof_sigma_eq #6, sizeof (sigma.mk ?x_4 ?x_5) ↦ sizeof ?x_4 + sizeof ?x_5 + 1
sizeof_sum_eq_right #5, sizeof (sum.inr ?x_4) ↦ sizeof ?x_4 + 1
sizeof_sum_eq_left #5, sizeof (sum.inl ?x_4) ↦ sizeof ?x_4 + 1
sizeof_prod_eq #6, sizeof (?x_4, ?x_5) ↦ sizeof ?x_4 + sizeof ?x_5 + 1
sizeof_nat_eq #1, sizeof ?x_0 ↦ ?x_0
default_has_sizeof_eq #2, sizeof ?x_1 ↦ 0
id.def #2, id ?x_1 ↦ ?x_1
foo.g.def #2 (prio: 1001), g ?x_0 ?x_1 ↦ h ?x_1
foo.g.rfl #2 (prio: 1001), g ?x_0 ?x_1 ↦ ?x_1
ne.def #3, ?x_1 ≠ ?x_2 ↦ ¬?x_1 = ?x_2
foo.h.def #1 (prio: 1001), h ?x_0 ↦ q ?x_0
foo.h.rfl #1 (prio: 1001), h ?x_0 ↦ ?x_0