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

fix(library/simplifier/ceqv): polish conditional rewrite internalization procedure

Browse source
This commit is contained in:
Leonardo de Moura 2015-07-13 16:40:18 -04:00
parent ebe6ec0017
commit 58291024a9
1 changed files with 29 additions and 13 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -37,6 +37,10 @@ class to_ceqvs_fn {
return is_constant(fn) && ::lean::is_trans_relation(m_env, const_name(fn)) && is_type(e);
}
bool is_relation(expr const & e) {
return is_transitive(e);
}
list<expr_pair> lift(expr const & local, list<expr_pair> const & l) {
lean_assert(is_local(local));
return map(l, [&](expr_pair const & e_H) {
@ -44,26 +48,32 @@ class to_ceqvs_fn {
});
}
list<expr_pair> apply(expr const & e, expr const & H) {
bool is_prop(expr const & e) {
constraint_seq cs;
return m_tc.is_prop(e, cs) && !cs;
}
// If restricted is true, we don't use (e <-> true) rewrite
list<expr_pair> apply(expr const & e, expr const & H, bool restrited) {
expr c, Hdec, A, arg1, arg2;
if (is_transitive(e)) {
if (is_relation(e)) {
return mk_singleton(e, H);
} 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(arg1, mk_false());
expr new_H = mk_app(mk_constant(get_iff_false_intro_name()), arg1, H);
return mk_singleton(new_e, new_H);
} else if (is_standard(m_env) && is_and(e, arg1, arg2)) {
// TODO(Leo): we can extend this trick to any type that has only one constructor
expr H1 = mk_app(mk_constant(get_and_elim_left_name()), arg1, arg2, H);
expr H2 = mk_app(mk_constant(get_and_elim_right_name()), arg1, arg2, H);
auto r1 = apply(arg1, H1);
auto r2 = apply(arg2, H2);
auto r1 = apply(arg1, H1, restrited);
auto r2 = apply(arg2, H2, restrited);
return append(r1, r2);
} else if (is_pi(e)) {
expr local = mk_local(m_tc.mk_fresh_name(), binding_name(e), binding_domain(e), binding_info(e));
expr new_e = instantiate(binding_body(e), local);
expr new_H = mk_app(H, local);
auto r = apply(new_e, new_H);
auto r = apply(new_e, new_H, restrited);
unsigned len = length(r);
if (len == 0) {
return r;
@ -72,7 +82,7 @@ class to_ceqvs_fn {
} else {
return lift(local, r);
}
} else if (is_standard(m_env) && is_ite(e, c, Hdec, A, arg1, arg2)) {
} else if (is_standard(m_env) && is_ite(e, c, Hdec, A, arg1, arg2) && is_prop(e)) {
// TODO(Leo): support HoTT mode if users request
expr not_c = mk_not(m_tc, c);
expr Hc = mk_local(m_tc.mk_fresh_name(), c);
@ -81,28 +91,34 @@ class to_ceqvs_fn {
c, arg1, arg2, Hdec, e, Hc});
expr H2 = mk_app({mk_constant(get_implies_of_if_neg_name()),
c, arg1, arg2, Hdec, e, Hnc});
auto r1 = lift(Hc, apply(arg1, H1));
auto r2 = lift(Hnc, apply(arg2, H2));
auto r1 = lift(Hc, apply(arg1, H1, restrited));
auto r2 = lift(Hnc, apply(arg2, H2, restrited));
return append(r1, r2);
} else {
} else if (!restrited) {
constraint_seq cs;
expr new_e = m_tc.whnf(e, cs);
if (new_e != e && !cs) {
return apply(new_e, H);
} else if (is_standard(m_env)) {
if (auto r = apply(new_e, H, true))
return r;
}
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);
return mk_singleton(new_e, new_H);
} else {
return list<expr_pair>();
}
} else {
return list<expr_pair>();
}
}
public:
to_ceqvs_fn(type_checker & tc):m_env(tc.env()), m_tc(tc) {}
list<expr_pair> operator()(expr const & e, expr const & H) {
return filter(apply(e, H), [&](expr_pair const & p) { return is_ceqv(m_tc, p.first); });
bool restrited = false;
list<expr_pair> lst = apply(e, H, restrited);
return filter(lst, [&](expr_pair const & p) { return is_ceqv(m_tc, p.first); });
}
};