From 139536896caccd6519c2a9bf414070292e0df771 Mon Sep 17 00:00:00 2001 From: Daniel Selsam Date: Sat, 28 Nov 2015 21:33:09 -0800 Subject: [PATCH] feat(library/light_lt_manager): light wrappers for ordered rewriting --- src/emacs/lean-syntax.el | 1 + src/frontends/lean/builtin_cmds.cpp | 13 ++ src/frontends/lean/decl_attributes.cpp | 8 + src/frontends/lean/decl_attributes.h | 1 + src/frontends/lean/token_table.cpp | 2 +- src/frontends/lean/tokens.cpp | 4 + src/frontends/lean/tokens.h | 1 + src/frontends/lean/tokens.txt | 1 + src/library/CMakeLists.txt | 2 +- src/library/blast/blast.cpp | 12 ++ src/library/blast/blast.h | 3 + src/library/blast/simplifier/simplifier.cpp | 2 +- src/library/init_module.cpp | 3 + src/library/light_lt_manager.cpp | 204 ++++++++++++++++++ src/library/light_lt_manager.h | 37 ++++ tests/lean/simplifier_light.lean | 62 ++++++ tests/lean/simplifier_light.lean.expected.out | 5 + 17 files changed, 358 insertions(+), 3 deletions(-) create mode 100644 src/library/light_lt_manager.cpp create mode 100644 src/library/light_lt_manager.h create mode 100644 tests/lean/simplifier_light.lean create mode 100644 tests/lean/simplifier_light.lean.expected.out diff --git a/src/emacs/lean-syntax.el b/src/emacs/lean-syntax.el index efc647463..890dbf621 100644 --- a/src/emacs/lean-syntax.el +++ b/src/emacs/lean-syntax.el @@ -164,6 +164,7 @@ (,(rx "\[priority " (one-or-more (not (any "\]"))) "\]") . font-lock-doc-face) (,(rx "\[recursor " (one-or-more (not (any "\]"))) "\]") . font-lock-doc-face) (,(rx "\[unfold " (one-or-more (not (any "\]"))) "\]") . font-lock-doc-face) + (,(rx "\[light " (one-or-more (not (any "\]"))) "\]") . font-lock-doc-face) ;; Constants which have a keyword as subterm (,(rx (or "∘if")) . 'font-lock-constant-face) ;; Keywords diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp index 2d9cae490..1e0271b9f 100644 --- a/src/frontends/lean/builtin_cmds.cpp +++ b/src/frontends/lean/builtin_cmds.cpp @@ -24,6 +24,7 @@ Author: Leonardo de Moura #include "library/coercion.h" #include "library/constants.h" #include "library/reducible.h" +#include "library/light_lt_manager.h" #include "library/normalize.h" #include "library/print.h" #include "library/noncomputable.h" @@ -290,6 +291,8 @@ static void print_attributes(parser const & p, name const & n) { out << " [simp]"; if (is_congr_rule(env, n)) out << " [congr]"; + if (auto light_arg = is_light_rule(env, n)) + out << " [light " << *light_arg << "]"; if (is_backward_rule(env, n)) out << " [backward]"; if (is_no_pattern(env, n)) @@ -536,6 +539,12 @@ static void print_congr_rules(parser & p) { out << s.pp_congr(out.get_formatter()); } +static void print_light_rules(parser & p) { + io_state_stream out = p.regular_stream(); + light_rule_set lrs = get_light_rule_set(p.env()); + out << lrs; +} + static void print_backward_rules(parser & p) { io_state_stream out = p.regular_stream(); blast::backward_rule_set brs = get_backward_rule_set(p.env()); @@ -671,6 +680,10 @@ environment print_cmd(parser & p) { } else if (p.curr_is_token(get_congr_attr_tk())) { p.next(); print_congr_rules(p); + } else if (p.curr_is_token(get_light_attr_tk())) { + p.next(); + p.check_token_next(get_rbracket_tk(), "invalid 'print [light]', ']' expected"); + print_light_rules(p); } else if (p.curr_is_token(get_backward_attr_tk())) { p.next(); print_backward_rules(p); diff --git a/src/frontends/lean/decl_attributes.cpp b/src/frontends/lean/decl_attributes.cpp index aaad2084d..9acfe8f0e 100644 --- a/src/frontends/lean/decl_attributes.cpp +++ b/src/frontends/lean/decl_attributes.cpp @@ -11,6 +11,7 @@ Author: Leonardo de Moura #include "library/relation_manager.h" #include "library/user_recursors.h" #include "library/coercion.h" +#include "library/light_lt_manager.h" #include "library/blast/simplifier/simp_rule_set.h" #include "library/blast/backward/backward_rule_set.h" #include "library/blast/forward/pattern.h" @@ -139,6 +140,10 @@ void decl_attributes::parse(parser & p) { } else if (p.curr_is_token(get_congr_attr_tk())) { p.next(); m_congr = true; + } else if (p.curr_is_token(get_light_attr_tk())) { + p.next(); + m_light_arg = p.parse_small_nat(); + p.check_token_next(get_rbracket_tk(), "light attribute has form '[light ]'"); } else if (p.curr_is_token(get_backward_attr_tk())) { p.next(); m_backward = true; @@ -234,6 +239,9 @@ environment decl_attributes::apply(environment env, io_state const & ios, name c else env = add_congr_rule(env, d, LEAN_SIMP_DEFAULT_PRIORITY, m_persistent); } + if (m_light_arg) { + env = add_light_rule(env, d, *m_light_arg, m_persistent); + } if (m_backward) { if (m_priority) env = add_backward_rule(env, d, *m_priority, m_persistent); diff --git a/src/frontends/lean/decl_attributes.h b/src/frontends/lean/decl_attributes.h index b966fbe4d..2d277267c 100644 --- a/src/frontends/lean/decl_attributes.h +++ b/src/frontends/lean/decl_attributes.h @@ -36,6 +36,7 @@ class decl_attributes { bool m_no_pattern; optional m_recursor_major_pos; optional m_priority; + optional m_light_arg; list m_unfold_hint; public: decl_attributes(bool is_abbrev = false, bool persistent = true); diff --git a/src/frontends/lean/token_table.cpp b/src/frontends/lean/token_table.cpp index 39a6d3d9b..fb2a88221 100644 --- a/src/frontends/lean/token_table.cpp +++ b/src/frontends/lean/token_table.cpp @@ -108,7 +108,7 @@ void init_token_table(token_table & t) { {"theorem", "axiom", "axioms", "variable", "protected", "private", "reveal", "definition", "example", "coercion", "abbreviation", "noncomputable", "variables", "parameter", "parameters", "constant", "constants", - "[persistent]", "[visible]", "[instance]", "[trans_instance]", + "[persistent]", "[visible]", "[instance]", "[trans_instance]", "[light", "[none]", "[class]", "[coercion]", "[reducible]", "[irreducible]", "[semireducible]", "[quasireducible]", "[simp]", "[congr]", "[parsing_only]", "[multiple_instances]", "[symm]", "[trans]", "[refl]", "[subst]", "[recursor", "evaluate", "check", "eval", "[wf]", "[whnf]", "[priority", "[unfold_full]", "[unfold_hints]", "[backward]", diff --git a/src/frontends/lean/tokens.cpp b/src/frontends/lean/tokens.cpp index 0495a6522..c142bb51a 100644 --- a/src/frontends/lean/tokens.cpp +++ b/src/frontends/lean/tokens.cpp @@ -120,6 +120,7 @@ static name const * g_refl_tk = nullptr; static name const * g_subst_tk = nullptr; static name const * g_simp_attr_tk = nullptr; static name const * g_congr_attr_tk = nullptr; +static name const * g_light_attr_tk = nullptr; static name const * g_backward_attr_tk = nullptr; static name const * g_no_pattern_attr_tk = nullptr; static name const * g_forward_attr_tk = nullptr; @@ -277,6 +278,7 @@ void initialize_tokens() { g_subst_tk = new name{"[subst]"}; g_simp_attr_tk = new name{"[simp]"}; g_congr_attr_tk = new name{"[congr]"}; + g_light_attr_tk = new name{"[light"}; g_backward_attr_tk = new name{"[backward]"}; g_no_pattern_attr_tk = new name{"[no_pattern]"}; g_forward_attr_tk = new name{"[forward]"}; @@ -435,6 +437,7 @@ void finalize_tokens() { delete g_subst_tk; delete g_simp_attr_tk; delete g_congr_attr_tk; + delete g_light_attr_tk; delete g_backward_attr_tk; delete g_no_pattern_attr_tk; delete g_forward_attr_tk; @@ -592,6 +595,7 @@ name const & get_refl_tk() { return *g_refl_tk; } name const & get_subst_tk() { return *g_subst_tk; } name const & get_simp_attr_tk() { return *g_simp_attr_tk; } name const & get_congr_attr_tk() { return *g_congr_attr_tk; } +name const & get_light_attr_tk() { return *g_light_attr_tk; } name const & get_backward_attr_tk() { return *g_backward_attr_tk; } name const & get_no_pattern_attr_tk() { return *g_no_pattern_attr_tk; } name const & get_forward_attr_tk() { return *g_forward_attr_tk; } diff --git a/src/frontends/lean/tokens.h b/src/frontends/lean/tokens.h index ebfbe6a13..380966895 100644 --- a/src/frontends/lean/tokens.h +++ b/src/frontends/lean/tokens.h @@ -122,6 +122,7 @@ name const & get_refl_tk(); name const & get_subst_tk(); name const & get_simp_attr_tk(); name const & get_congr_attr_tk(); +name const & get_light_attr_tk(); name const & get_backward_attr_tk(); name const & get_no_pattern_attr_tk(); name const & get_forward_attr_tk(); diff --git a/src/frontends/lean/tokens.txt b/src/frontends/lean/tokens.txt index d2065a5e5..655472a0e 100644 --- a/src/frontends/lean/tokens.txt +++ b/src/frontends/lean/tokens.txt @@ -115,6 +115,7 @@ refl [refl] subst [subst] simp_attr [simp] congr_attr [congr] +light_attr [light backward_attr [backward] no_pattern_attr [no_pattern] forward_attr [forward] diff --git a/src/library/CMakeLists.txt b/src/library/CMakeLists.txt index 8adc13649..5412495f5 100644 --- a/src/library/CMakeLists.txt +++ b/src/library/CMakeLists.txt @@ -18,4 +18,4 @@ add_library(library OBJECT deep_copy.cpp expr_lt.cpp io_state.cpp aux_recursors.cpp norm_num.cpp decl_stats.cpp meng_paulson.cpp norm_num.cpp class_instance_resolution.cpp type_context.cpp tmp_type_context.cpp fun_info_manager.cpp congr_lemma_manager.cpp - abstract_expr_manager.cpp) + abstract_expr_manager.cpp light_lt_manager.cpp) diff --git a/src/library/blast/blast.cpp b/src/library/blast/blast.cpp index eb23baee3..cc596bd31 100644 --- a/src/library/blast/blast.cpp +++ b/src/library/blast/blast.cpp @@ -17,6 +17,7 @@ Author: Leonardo de Moura #include "library/relation_manager.h" #include "library/congr_lemma_manager.h" #include "library/abstract_expr_manager.h" +#include "library/light_lt_manager.h" #include "library/projection.h" #include "library/tactic/goal.h" #include "library/blast/expr.h" @@ -62,6 +63,7 @@ class blastenv { fun_info_manager m_fun_info_manager; congr_lemma_manager m_congr_lemma_manager; abstract_expr_manager m_abstract_expr_manager; + light_lt_manager m_light_lt_manager; relation_info_getter m_rel_getter; refl_info_getter m_refl_getter; symm_info_getter m_symm_getter; @@ -442,6 +444,7 @@ public: m_fun_info_manager(*m_tmp_ctx), m_congr_lemma_manager(m_app_builder, m_fun_info_manager), m_abstract_expr_manager(m_fun_info_manager), + m_light_lt_manager(env), m_rel_getter(mk_relation_info_getter(env)), m_refl_getter(mk_refl_info_getter(env)), m_symm_getter(mk_symm_info_getter(env)), @@ -550,6 +553,10 @@ public: return m_abstract_expr_manager.is_equal(e1, e2); } + bool is_light_lt(expr const & e1, expr const & e2) { + return m_light_lt_manager.is_lt(e1, e2); + } + /** \brief Convert an external expression into a blast expression It converts meta-variables to blast meta-variables, and ensures the expressions are maximally shared. @@ -756,6 +763,11 @@ bool abstract_is_equal(expr const & e1, expr const & e2) { return g_blastenv->abstract_is_equal(e1, e2); } +bool is_light_lt(expr const & e1, expr const & e2) { + lean_assert(g_blastenv); + return g_blastenv->is_light_lt(e1, e2); +} + void display_curr_state() { curr_state().display(env(), ios()); display("\n"); diff --git a/src/library/blast/blast.h b/src/library/blast/blast.h index 015a8f623..e6a1c1992 100644 --- a/src/library/blast/blast.h +++ b/src/library/blast/blast.h @@ -113,6 +113,9 @@ fun_info get_fun_info(expr const & fn, unsigned nargs); unsigned abstract_hash(expr const & e); bool abstract_is_equal(expr const & e1, expr const & e2); +/** \brief Order on expressions that supports the "light" annotation */ +bool is_light_lt(expr const & e1, expr const & e2); + /** \brief Display the current state of the blast tactic in the diagnostic channel. */ void display_curr_state(); /** \brief Display the given expression in the diagnostic channel. */ diff --git a/src/library/blast/simplifier/simplifier.cpp b/src/library/blast/simplifier/simplifier.cpp index 1da6a4cb6..dbe78995b 100644 --- a/src/library/blast/simplifier/simplifier.cpp +++ b/src/library/blast/simplifier/simplifier.cpp @@ -614,7 +614,7 @@ result simplifier::rewrite(expr const & e, simp_rule const & sr) { expr new_rhs = tmp_tctx->instantiate_uvars_mvars(sr.get_rhs()); if (sr.is_perm()) { - if (!is_lt(new_rhs, new_lhs, false)) + if (!is_light_lt(new_rhs, new_lhs)) return result(e); } diff --git a/src/library/init_module.cpp b/src/library/init_module.cpp index c31015d51..68aa6bf23 100644 --- a/src/library/init_module.cpp +++ b/src/library/init_module.cpp @@ -28,6 +28,7 @@ Author: Leonardo de Moura #include "library/idx_metavar.h" #include "library/sorry.h" #include "library/placeholder.h" +#include "library/light_lt_manager.h" #include "library/print.h" #include "library/fingerprint.h" #include "library/util.h" @@ -89,9 +90,11 @@ void initialize_library_module() { initialize_norm_num(); initialize_class_instance_resolution(); initialize_type_context(); + initialize_light_rule_set(); } void finalize_library_module() { + finalize_light_rule_set(); finalize_type_context(); finalize_class_instance_resolution(); finalize_norm_num(); diff --git a/src/library/light_lt_manager.cpp b/src/library/light_lt_manager.cpp new file mode 100644 index 000000000..84d1d9f98 --- /dev/null +++ b/src/library/light_lt_manager.cpp @@ -0,0 +1,204 @@ +/* +Copyright (c) 2015 Daniel Selsam. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Author: Daniel Selsam +*/ +#include "library/light_lt_manager.h" +#include "util/sstream.h" +#include "util/name_set.h" +#include "util/safe_arith.h" +#include "kernel/error_msgs.h" +#include "kernel/instantiate.h" +#include "library/scoped_ext.h" +#include + +namespace lean { + +static unsigned add_weight(unsigned num, expr const * args) { + unsigned r = 0; + for (unsigned i = 0; i < num; i++) + r = safe_add(r, get_weight(args[i])); + return r; +} + +unsigned light_lt_manager::get_weight_core(expr const & e) { + switch (e.kind()) { + case expr_kind::Var: case expr_kind::Constant: case expr_kind::Sort: + case expr_kind::Meta: case expr_kind::Local: + return 1; + case expr_kind::Lambda: case expr_kind::Pi: + return safe_add(1, safe_add(get_weight(binding_domain(e)), get_weight(binding_body(e)))); + case expr_kind::Macro: + return safe_add(1, add_weight(macro_num_args(e), macro_args(e))); + case expr_kind::App: + buffer args; + expr fn = get_app_args(e, args); + if (is_constant(fn)) { + unsigned const * light_arg = m_lrs.find(const_name(fn)); + if (light_arg && args.size() > *light_arg) return get_weight(args[*light_arg]); + } + return safe_add(1, safe_add(get_weight(app_fn(e)), get_weight(app_arg(e)))); + } + lean_unreachable(); // LCOV_EXCL_LINE +} + +unsigned light_lt_manager::get_weight(expr const & e) { + auto it = m_weight_cache.find(e); + if (it != m_weight_cache.end()) return it->second; + unsigned w = get_weight_core(e); + m_weight_cache.insert(mk_pair(e, w)); + return w; +} + +bool light_lt_manager::is_lt(expr const & a, expr const & b) { + if (is_eqp(a, b)) return false; + unsigned wa = get_weight(a); + unsigned wb = get_weight(b); + if (wa < wb) return true; + if (wa > wb) return false; + if (is_constant(get_app_fn(a))) { + unsigned const * light_arg = m_lrs.find(const_name(get_app_fn(a))); + if (light_arg) { + buffer args; + get_app_args(a, args); + if (args.size() > *light_arg) return is_lt(args[*light_arg], b); + } + } + if (is_constant(get_app_fn(b))) { + unsigned const * light_arg = m_lrs.find(const_name(get_app_fn(b))); + if (light_arg) { + buffer args; + get_app_args(b, args); + if (args.size() > *light_arg) return !is_lt(args[*light_arg], a); + } + } + if (a.kind() != b.kind()) return a.kind() < b.kind(); + if (a == b) return false; + switch (a.kind()) { + case expr_kind::Var: + return var_idx(a) < var_idx(b); + case expr_kind::Constant: + if (const_name(a) != const_name(b)) + return const_name(a) < const_name(b); + else + return ::lean::is_lt(const_levels(a), const_levels(b), false); + case expr_kind::App: + if (app_fn(a) != app_fn(b)) + return is_lt(app_fn(a), app_fn(b)); + else + return is_lt(app_arg(a), app_arg(b)); + case expr_kind::Lambda: case expr_kind::Pi: + if (binding_domain(a) != binding_domain(b)) + return is_lt(binding_domain(a), binding_domain(b)); + else + return is_lt(binding_body(a), binding_body(b)); + case expr_kind::Sort: + return ::lean::is_lt(sort_level(a), sort_level(b), false); + case expr_kind::Local: case expr_kind::Meta: + if (mlocal_name(a) != mlocal_name(b)) + return mlocal_name(a) < mlocal_name(b); + else + return is_lt(mlocal_type(a), mlocal_type(b)); + case expr_kind::Macro: + if (macro_def(a) != macro_def(b)) + return macro_def(a) < macro_def(b); + if (macro_num_args(a) != macro_num_args(b)) + return macro_num_args(a) < macro_num_args(b); + for (unsigned i = 0; i < macro_num_args(a); i++) { + if (macro_arg(a, i) != macro_arg(b, i)) + return is_lt(macro_arg(a, i), macro_arg(b, i)); + } + return false; + } + lean_unreachable(); // LCOV_EXCL_LINE +} + +static name * g_class_name = nullptr; +static std::string * g_key = nullptr; + +struct lrs_state { + light_rule_set m_lrs; + void add(environment const &, io_state const &, name const & id, unsigned light_arg) { + m_lrs.insert(id, light_arg); + } +}; + +struct lrs_entry { + name m_id; + unsigned m_light_arg; + lrs_entry() {} + lrs_entry(name const & id, unsigned light_arg): m_id(id), m_light_arg(light_arg) { } +}; + +struct lrs_config { + typedef lrs_entry entry; + typedef lrs_state state; + static void add_entry(environment const & env, io_state const & ios, state & s, entry const & e) { + s.add(env, ios, e.m_id, e.m_light_arg); + } + static name const & get_class_name() { + return *g_class_name; + } + static std::string const & get_serialization_key() { + return *g_key; + } + static void write_entry(serializer & s, entry const & e) { + s << e.m_id << e.m_light_arg; + } + static entry read_entry(deserializer & d) { + entry e; d >> e.m_id >> e.m_light_arg; return e; + } + static optional get_fingerprint(entry const & e) { + return some(e.m_id.hash()); + } +}; + +template class scoped_ext; +typedef scoped_ext lrs_ext; + +environment add_light_rule(environment const & env, name const & id, unsigned light_arg, bool persistent) { + return lrs_ext::add_entry(env, get_dummy_ios(), lrs_entry(id, light_arg), persistent); +} + +optional is_light_rule(environment const & env, name const & n) { + unsigned const * light_arg = lrs_ext::get_state(env).m_lrs.find(n); + if (light_arg) return optional(*light_arg); + else return optional(); +} + +light_rule_set get_light_rule_set(environment const & env) { + return lrs_ext::get_state(env).m_lrs; +} + +light_rule_set get_light_rule_set(environment const & env, io_state const &, name const & ns) { + light_rule_set lrs; + list const * entries = lrs_ext::get_entries(env, ns); + if (entries) { + for (auto const & e : *entries) { + lrs.insert(e.m_id, e.m_light_arg); + } + } + return lrs; +} + +io_state_stream const & operator<<(io_state_stream const & out, light_rule_set const & lrs) { + out << "light rules\n"; + lrs.for_each([&](name const & id, unsigned const & light_arg) { + out << id << " @ " << light_arg << "\n"; + }); + return out; +} + +void initialize_light_rule_set() { + g_class_name = new name("lrs"); + g_key = new std::string("lrs"); + lrs_ext::initialize(); +} + +void finalize_light_rule_set() { + lrs_ext::finalize(); + delete g_key; + delete g_class_name; +} + +} diff --git a/src/library/light_lt_manager.h b/src/library/light_lt_manager.h new file mode 100644 index 000000000..1f84ecb21 --- /dev/null +++ b/src/library/light_lt_manager.h @@ -0,0 +1,37 @@ +/* +Copyright (c) 2015 Daniel Selsam. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Author: Daniel Selsam +*/ +#pragma once +#include "kernel/expr.h" +#include "kernel/expr_maps.h" +#include "library/io_state_stream.h" +#include "util/name_map.h" + +namespace lean { + +typedef name_map light_rule_set; + +environment add_light_rule(environment const & env, name const & id, unsigned light_arg, bool persistent); +optional is_light_rule(environment const & env, name const & n); +light_rule_set get_light_rule_set(environment const & env); +light_rule_set get_light_rule_set(environment const & env, io_state const & ios, name const & ns); + +io_state_stream const & operator<<(io_state_stream const & out, light_rule_set const & r); + +void initialize_light_rule_set(); +void finalize_light_rule_set(); + +class light_lt_manager { + light_rule_set m_lrs; + expr_map m_weight_cache; + unsigned get_weight_core(expr const & e); + unsigned get_weight(expr const & e); + +public: + light_lt_manager(environment const & env): m_lrs(get_light_rule_set(env)) {} + bool is_lt(expr const & a, expr const & b); +}; + +} diff --git a/tests/lean/simplifier_light.lean b/tests/lean/simplifier_light.lean new file mode 100644 index 000000000..2c178da39 --- /dev/null +++ b/tests/lean/simplifier_light.lean @@ -0,0 +1,62 @@ +-- Test [light] annotation +-- Remark: it will take some additional work to get ⁻¹ to rewrite well +-- when there is a proof obligation. +import algebra.simplifier algebra.field data.set data.finset +open algebra simplifier.ac +attribute neg [light 2] +attribute inv [light 2] + +attribute add.right_inv [simp] +attribute add_neg_cancel_left [simp] + +attribute mul.right_inv [simp] +attribute mul_inv_cancel_left [simp] + +namespace ag +universe l +constants (A : Type.{l}) (s1 : add_comm_group A) (s2 : has_one A) +attribute s1 [instance] +attribute s2 [instance] +constants (x y z w v : A) + +#simplify eq env 0 x + y + - x + -y + z + -z +#simplify eq env 0 -100 + -v + -v + x + -v + y + - x + -y + z + -z + v + v + v + 100 +end ag + +namespace mg +universe l +constants (A : Type.{l}) (s1 : comm_group A) (s2 : has_add A) +attribute s1 [instance] +attribute s2 [instance] +constants (x y z w v : A) + +#simplify eq env 0 x⁻¹ * y⁻¹ * z⁻¹ * 100⁻¹ * x * y * z * 100 + +end mg + +namespace s +open set +universe l +constants (A : Type.{l}) (x y z v w : set A) +attribute complement [light 1] + +-- TODO(dhs, leo): Where do we put this group of simp rules? +attribute union_comp_self [simp] +lemma union_comp_self_left [simp] {X : Type} (s t : set X) : s ∪ (-s ∪ t)= univ := sorry + +attribute union.comm [simp] +attribute union.assoc [simp] +attribute union.left_comm [simp] + +#simplify eq env 0 x ∪ y ∪ z ∪ -x + +attribute inter_comp_self [simp] +lemma inter_comp_self_left [simp] {X : Type} (s t : set X) : s ∩ (-s ∩ t)= empty := sorry + +attribute inter.comm [simp] +attribute inter.assoc [simp] +attribute inter.left_comm [simp] + +#simplify eq env 0 x ∩ y ∩ z ∩ -x + +end s diff --git a/tests/lean/simplifier_light.lean.expected.out b/tests/lean/simplifier_light.lean.expected.out new file mode 100644 index 000000000..1bc3323c5 --- /dev/null +++ b/tests/lean/simplifier_light.lean.expected.out @@ -0,0 +1,5 @@ +0 +0 +1 +univ +∅