michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(library/simplifier): we can "rewrite" with transitive relations

Browse source 
The simplifier does not really need the relation to be an equivalence.
Transitivity is the main required property (we need to chain rewrites
together).
This commit is contained in:
Leonardo de Moura 2015-07-12 14:24:05 -04:00
parent f8d472c9f1
commit 3cb8568fb5
3 changed files with 11 additions and 11 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

18
src/library/simplifier/ceqv.cpp
View file

@ -31,10 +31,10 @@ class to_ceqvs_fn {
return is_sort(m_tc.whnf(m_tc.infer(e).first).first); return is_sort(m_tc.whnf(m_tc.infer(e).first).first);
} }
bool is_equivalence(expr const & e) { bool is_transitive(expr const & e) {
if (!is_app(e)) return false; if (!is_app(e)) return false;
expr const & fn = get_app_fn(e); expr const & fn = get_app_fn(e);
return is_constant(fn) && ::lean::is_equivalence(m_env, const_name(fn)) && is_type(e); return is_constant(fn) && ::lean::is_trans_relation(m_env, const_name(fn)) && is_type(e);
} }
list<expr_pair> lift(expr const & local, list<expr_pair> const & l) { list<expr_pair> lift(expr const & local, list<expr_pair> const & l) {
@ -46,7 +46,7 @@ class to_ceqvs_fn {
list<expr_pair> apply(expr const & e, expr const & H) { list<expr_pair> apply(expr const & e, expr const & H) {
expr c, Hdec, A, arg1, arg2; expr c, Hdec, A, arg1, arg2;
if (is_equivalence(e)) { if (is_transitive(e)) {
return mk_singleton(e, H); return mk_singleton(e, H);
} else if (is_standard(m_env) && is_not(m_env, e, arg1)) { } else if (is_standard(m_env) && is_not(m_env, e, arg1)) {
expr new_e = mk_iff(e, mk_false()); expr new_e = mk_iff(e, mk_false());
@ -110,10 +110,10 @@ list<expr_pair> to_ceqvs(type_checker & tc, expr const & e, expr const & H) {
return to_ceqvs_fn(tc)(e, H); return to_ceqvs_fn(tc)(e, H);
} }
bool is_equivalence(environment const & env, expr const & e, expr & rel, expr & lhs, expr & rhs) { bool is_transitive(environment const & env, expr const & e, expr & rel, expr & lhs, expr & rhs) {
buffer<expr> args; buffer<expr> args;
rel = get_app_args(e, args); rel = get_app_args(e, args);
if (!is_constant(rel) || !is_equivalence(env, const_name(rel))) if (!is_constant(rel) || !is_trans_relation(env, const_name(rel)))
return false; return false;
relation_info const * rel_info = get_relation_info(env, const_name(rel)); relation_info const * rel_info = get_relation_info(env, const_name(rel));
if (!rel_info || rel_info->get_lhs_pos() >= args.size() || rel_info->get_rhs_pos() >= args.size()) if (!rel_info || rel_info->get_lhs_pos() >= args.size() || rel_info->get_rhs_pos() >= args.size())
@ -123,9 +123,9 @@ bool is_equivalence(environment const & env, expr const & e, expr & rel, expr &
return true; return true;
} }
bool is_equivalence(environment const & env, expr const & e, expr & lhs, expr & rhs) { bool is_transitive(environment const & env, expr const & e, expr & lhs, expr & rhs) {
expr rel; expr rel;
return is_equivalence(env, e, rel, lhs, rhs); return is_transitive(env, e, rel, lhs, rhs);
} }
bool is_ceqv(type_checker & tc, expr e) { bool is_ceqv(type_checker & tc, expr e) {
@ -167,7 +167,7 @@ bool is_ceqv(type_checker & tc, expr e) {
e = instantiate(binding_body(e), local); e = instantiate(binding_body(e), local);
} }
expr lhs, rhs; expr lhs, rhs;
if (!is_equivalence(env, e, lhs, rhs)) if (!is_transitive(env, e, lhs, rhs))
return false; return false;
// traverse lhs, and remove found variables from to_find // traverse lhs, and remove found variables from to_find
for_each(lhs, visitor_fn); for_each(lhs, visitor_fn);
@ -230,7 +230,7 @@ bool is_permutation_ceqv(environment const & env, expr e) {
num_args++; num_args++;
} }
expr lhs, rhs; expr lhs, rhs;
if (is_equivalence(env, e, lhs, rhs)) { if (is_transitive(env, e, lhs, rhs)) {
buffer<optional<unsigned>> permutation; buffer<optional<unsigned>> permutation;
permutation.resize(num_args); permutation.resize(num_args);
return is_permutation(lhs, rhs, 0, permutation); return is_permutation(lhs, rhs, 0, permutation);

2
src/library/simplifier/ceqv.h
View file

@ -8,7 +8,7 @@ Author: Leonardo de Moura
#include "kernel/type_checker.h" #include "kernel/type_checker.h"
namespace lean { namespace lean {
bool is_equivalence(environment const & env, expr const & e, expr & rel, expr & lhs, expr & rhs); bool is_transitive(environment const & env, expr const & e, expr & rel, expr & lhs, expr & rhs);
/** \brief Given (H : e), return a list of (h_i : e_i) where e_i can be viewed as /** \brief Given (H : e), return a list of (h_i : e_i) where e_i can be viewed as
a "conditional" rewriting rule. Any equivalence relation registered using a "conditional" rewriting rule. Any equivalence relation registered using
the relation_manager is considered. the relation_manager is considered.

2
src/library/simplifier/rewrite_rule_set.cpp
View file

@ -117,7 +117,7 @@ rewrite_rule_sets add_core(type_checker & tc, rewrite_rule_sets const & s,
new_e = instantiate(binding_body(new_e), mvar); new_e = instantiate(binding_body(new_e), mvar);
} }
expr rel, lhs, rhs; expr rel, lhs, rhs;
if (is_equivalence(env, new_e, rel, lhs, rhs) && is_constant(rel)) { if (is_transitive(env, new_e, rel, lhs, rhs) && is_constant(rel)) {
new_s.insert(const_name(rel), rewrite_rule(id, univ_metas, to_list(metas), lhs, rhs, new_h, is_perm)); new_s.insert(const_name(rel), rewrite_rule(id, univ_metas, to_list(metas), lhs, rhs, new_h, is_perm));
} }
} }