feat(library/light_lt_manager): light wrappers for ordered rewriting

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

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);

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 <i>]'");
         } 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);

src/frontends/lean/decl_attributes.h

@@ -36,6 +36,7 @@ class decl_attributes {
     bool               m_no_pattern;
     optional<unsigned> m_recursor_major_pos;
     optional<unsigned> m_priority;
+    optional<unsigned> m_light_arg;
     list<unsigned>     m_unfold_hint;
 public:
     decl_attributes(bool is_abbrev = false, bool persistent = true);

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]",

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; }

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();

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]

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)

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");

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. */

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);
     }
 

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();

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 <string>
+
+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<expr> 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<expr> 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<expr> 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<unsigned> get_fingerprint(entry const & e) {
+        return some(e.m_id.hash());
+    }
+};
+
+template class scoped_ext<lrs_config>;
+typedef scoped_ext<lrs_config> 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<unsigned> 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<unsigned>(*light_arg);
+    else return optional<unsigned>();
+}
+
+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<lrs_entry> 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;
+}
+
+}

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<unsigned> light_rule_set;
+
+environment add_light_rule(environment const & env, name const & id, unsigned light_arg,  bool persistent);
+optional<unsigned> 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<unsigned> 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);
+};
+
+}

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

tests/lean/simplifier_light.lean.expected.out

@@ -0,0 +1,5 @@
+0
+0
+1
+univ
+∅