feat(kernel): transparent theorems

closes #576

library/data/fintype.lean

@@ -185,8 +185,7 @@ private theorem mem_ltype_elems {A : Type} {s : list A} {a : ⟪s⟫}
       apply mem_cons
    end)
   (λ vainl : value a ∈ l,
-     have s₁  : l ⊆ s,                               from sub_of_cons_sub h,
+     have aux : a ∈ ltype_elems (sub_of_cons_sub h), from mem_ltype_elems (sub_of_cons_sub h) vainl,
-     have aux : a ∈ ltype_elems (sub_of_cons_sub h), from mem_ltype_elems s₁ vainl,
      mem_cons_of_mem _ aux)
 
 definition fintype_list_as_type [instance] {A : Type} [h : decidable_eq A] {s : list A} : fintype ⟪s⟫ :=

src/frontends/lean/decl_cmds.cpp

@@ -1057,7 +1057,7 @@ class definition_cmd_fn {
                     c_type  = expand_abbreviations(m_env, unfold_untrusted_macros(m_env, c_type));
                     c_value = expand_abbreviations(m_env, unfold_untrusted_macros(m_env, c_value));
                     if (m_kind == Theorem) {
-                        cd = check(mk_theorem(m_real_name, c_ls, c_type, c_value));
+                        cd = check(mk_theorem(m_env, m_real_name, c_ls, c_type, c_value));
                         if (m_p.keep_new_thms()) {
                             if (!m_is_private)
                                 m_p.add_decl_index(m_real_name, m_pos, m_p.get_cmd_token(), c_type);
@@ -1183,9 +1183,9 @@ class definition_cmd_fn {
                 m_env = module::add(m_env, check(mk_definition(m_env, m_real_aux_names[i], new_ls,
                                                                m_aux_types[i], aux_values[i])));
         } else {
-            m_env = module::add(m_env, check(mk_theorem(m_real_name, new_ls, m_type, m_value)));
+            m_env = module::add(m_env, check(mk_theorem(m_env, m_real_name, new_ls, m_type, m_value)));
             for (unsigned i = 0; i < aux_values.size(); i++)
-                m_env = module::add(m_env, check(mk_theorem(m_real_aux_names[i], new_ls,
+                m_env = module::add(m_env, check(mk_theorem(m_env, m_real_aux_names[i], new_ls,
                                                             m_aux_types[i], aux_values[i])));
         }
     }
@@ -1217,7 +1217,7 @@ class definition_cmd_fn {
                     m_type  = expand_abbreviations(m_env, unfold_untrusted_macros(m_env, m_type));
                     m_value = expand_abbreviations(m_env, unfold_untrusted_macros(m_env, m_value));
                     new_ls = append(m_ls, new_ls);
-                    auto cd = check(mk_theorem(m_real_name, new_ls, m_type, m_value));
+                    auto cd = check(mk_theorem(m_env, m_real_name, new_ls, m_type, m_value));
                     if (m_kind == Theorem) {
                         // Remark: we don't keep examples
                         if (m_p.keep_new_thms()) {

src/frontends/lean/migrate_cmd.cpp

@@ -225,9 +225,9 @@ struct migrate_cmd_fn {
             expr new_value = Fun(m_params, v);
             try {
                 if (d.is_axiom())
-                    m_env = module::add(m_env, check(m_env, mk_theorem(full_name, ls, new_type, new_value)));
+                    m_env = module::add(m_env, check(m_env, mk_theorem(m_env, full_name, ls, new_type, new_value)));
                 else if (d.is_theorem())
-                    m_env = module::add(m_env, check(m_env, mk_theorem(full_name, ls, new_type, new_value)));
+                    m_env = module::add(m_env, check(m_env, mk_theorem(m_env, full_name, ls, new_type, new_value)));
                 else
                     m_env = module::add(m_env, check(m_env, mk_definition(m_env, full_name, ls, new_type, new_value)));
                 m_p.add_decl_index(full_name, m_pos, d.is_theorem() ? name("theorem") : name("definition"), new_type);

src/frontends/lean/structure_cmd.cpp

@@ -857,7 +857,7 @@ struct structure_cmd_fn {
         expr eta_value           = Fun(m_params, Fun(st, rec));
         name eta_name(m_name, "eta");
 
-        declaration eta_decl     = mk_theorem(eta_name, lnames, eta_type, eta_value);
+        declaration eta_decl     = mk_theorem(m_env, eta_name, lnames, eta_type, eta_value);
         m_env = module::add(m_env, check(m_env, eta_decl));
         save_thm_info(eta_name);
         add_alias(eta_name);
@@ -888,7 +888,7 @@ struct structure_cmd_fn {
             expr proj_over_type     = infer_implicit(Pi(m_params, Pi(m_fields, eq)), m_params.size(), true);
             expr proj_over_value    = Fun(m_params, Fun(m_fields, refl));
 
-            declaration proj_over_decl = mk_theorem(proj_over_name, lnames, proj_over_type, proj_over_value);
+            declaration proj_over_decl = mk_theorem(m_env, proj_over_name, lnames, proj_over_type, proj_over_value);
             m_env = module::add(m_env, check(m_env, proj_over_decl));
             save_thm_info(proj_over_name);
             add_alias(proj_over_name);

src/frontends/lean/theorem_queue.cpp

@@ -31,7 +31,7 @@ void theorem_queue::add(environment const & env, name const & n, level_param_nam
             std::tie(type, value, new_ls) = m_parser.elaborate_definition_at(env, lls, n, t, v);
             new_ls = append(ls, new_ls);
             value  = expand_abbreviations(env, unfold_untrusted_macros(env, value));
-            auto r = check(env, mk_theorem(n, new_ls, type, value));
+            auto r = check(env, mk_theorem(env, n, new_ls, type, value));
             m_parser.cache_definition(n, t, v, new_ls, type, value);
             return r;
         });

src/kernel/declaration.cpp

@@ -65,8 +65,7 @@ declaration mk_definition(name const & n, level_param_names const & params, expr
                           unsigned weight, bool use_conv_opt) {
     return declaration(new declaration::cell(n, params, t, false, v, weight, use_conv_opt));
 }
-declaration mk_definition(environment const & env, name const & n, level_param_names const & params, expr const & t,
+static unsigned get_max_weight(environment const & env, expr const & v) {
-                          expr const & v, bool use_conv_opt) {
     unsigned w = 0;
     for_each(v, [&](expr const & e, unsigned) {
             if (is_constant(e)) {
@@ -76,10 +75,20 @@ declaration mk_definition(environment const & env, name const & n, level_param_n
             }
             return true;
         });
+    return w;
+}
+
+declaration mk_definition(environment const & env, name const & n, level_param_names const & params, expr const & t,
+                          expr const & v, bool use_conv_opt) {
+    unsigned w = get_max_weight(env, v);
     return mk_definition(n, params, t, v, w+1, use_conv_opt);
 }
-declaration mk_theorem(name const & n, level_param_names const & params, expr const & t, expr const & v) {
+declaration mk_theorem(environment const & env, name const & n, level_param_names const & params, expr const & t, expr const & v) {
-    return declaration(new declaration::cell(n, params, t, true, v, 0, false));
+    unsigned w = get_max_weight(env, v);
+    return declaration(new declaration::cell(n, params, t, true, v, w+1, false));
+}
+declaration mk_theorem(name const & n, level_param_names const & params, expr const & t, expr const & v, unsigned weight) {
+    return declaration(new declaration::cell(n, params, t, true, v, weight, false));
 }
 declaration mk_axiom(name const & n, level_param_names const & params, expr const & t) {
     return declaration(new declaration::cell(n, params, t, true));

src/kernel/declaration.h

@@ -57,7 +57,8 @@ public:
                                     expr const & v, bool use_conv_opt);
     friend declaration mk_definition(name const & n, level_param_names const & params, expr const & t, expr const & v,
                                     unsigned weight, bool use_conv_opt);
-    friend declaration mk_theorem(name const & n, level_param_names const & params, expr const & t, expr const & v);
+    friend declaration mk_theorem(environment const &, name const &, level_param_names const &, expr const &, expr const &);
+    friend declaration mk_theorem(name const &, level_param_names const &, expr const &, expr const &, unsigned);
     friend declaration mk_axiom(name const & n, level_param_names const & params, expr const & t);
     friend declaration mk_constant_assumption(name const & n, level_param_names const & params, expr const & t);
 };
@@ -70,7 +71,8 @@ declaration mk_definition(name const & n, level_param_names const & params, expr
                          unsigned weight = 0, bool use_conv_opt = true);
 declaration mk_definition(environment const & env, name const & n, level_param_names const & params, expr const & t, expr const & v,
                          bool use_conv_opt = true);
-declaration mk_theorem(name const & n, level_param_names const & params, expr const & t, expr const & v);
+declaration mk_theorem(environment const & env, name const & n, level_param_names const & params, expr const & t, expr const & v);
+declaration mk_theorem(name const & n, level_param_names const & params, expr const & t, expr const & v, unsigned w);
 declaration mk_axiom(name const & n, level_param_names const & params, expr const & t);
 declaration mk_constant_assumption(name const & n, level_param_names const & params, expr const & t);
 

src/kernel/default_converter.cpp

@@ -108,9 +108,7 @@ expr default_converter::whnf_core(expr const & e) {
     return r;
 }
 
-bool default_converter::is_opaque(declaration const & d) const {
+bool default_converter::is_opaque(declaration const &) const {
-    lean_assert(d.is_definition());
-    if (d.is_theorem()) return true;                               // theorems are always opaque
     return false;
 }
 

src/library/kernel_bindings.cpp

@@ -766,13 +766,6 @@ static int mk_axiom(lua_State * L) {
     else
         return push_declaration(L, mk_axiom(to_name_ext(L, 1), to_level_param_names(L, 2), to_expr(L, 3)));
 }
-static int mk_theorem(lua_State * L) {
-    int nargs = lua_gettop(L);
-    if (nargs == 3)
-        return push_declaration(L, mk_theorem(to_name_ext(L, 1), level_param_names(), to_expr(L, 2), to_expr(L, 3)));
-    else
-        return push_declaration(L, mk_theorem(to_name_ext(L, 1), to_level_param_names(L, 2), to_expr(L, 3), to_expr(L, 4)));
-}
 static void get_definition_args(lua_State * L, int idx, unsigned & weight, bool & use_conv_opt) {
     use_conv_opt = get_bool_named_param(L, idx, "use_conv_opt", use_conv_opt);
     weight       = get_uint_named_param(L, idx, "weight", weight);
@@ -806,6 +799,27 @@ static int mk_definition(lua_State * L) {
         }
     }
 }
+static void get_definition_args(lua_State * L, int idx, unsigned & weight) {
+    weight       = get_uint_named_param(L, idx, "weight", weight);
+}
+static int mk_theorem(lua_State * L) {
+    int nargs = lua_gettop(L);
+    unsigned weight = 0;
+    if (nargs == 3) {
+          return push_declaration(L, mk_theorem(to_name_ext(L, 1), level_param_names(), to_expr(L, 2), to_expr(L, 3), 0));
+    } else if (nargs == 4) {
+        if (is_expr(L, 4)) {
+            return push_declaration(L, mk_theorem(to_name_ext(L, 1), to_level_param_names(L, 2), to_expr(L, 3), to_expr(L, 4),
+                                                  weight));
+        } else {
+            get_definition_args(L, 4, weight);
+            return push_declaration(L, mk_theorem(to_name_ext(L, 1), level_param_names(), to_expr(L, 2), to_expr(L, 3), weight));
+        }
+    } else {
+        get_definition_args(L, 5, weight);
+        return push_declaration(L, mk_theorem(to_name_ext(L, 1), to_level_param_names(L, 2), to_expr(L, 3), to_expr(L, 4), weight));
+    }
+}
 
 static const struct luaL_Reg declaration_m[] = {
     {"__gc",             declaration_gc}, // never throws

src/library/kernel_serializer.cpp

@@ -290,8 +290,7 @@ serializer & operator<<(serializer & s, declaration const & d) {
     s << k << d.get_name() << d.get_univ_params() << d.get_type();
     if (d.is_definition()) {
         s << d.get_value();
-        if (!d.is_theorem())
+        s << d.get_weight();
-            s << d.get_weight();
     }
     return s;
 }
@@ -305,10 +304,10 @@ declaration read_declaration(deserializer & d) {
     expr t               = read_expr(d);
     if (has_value) {
         expr v      = read_expr(d);
+        unsigned w        = d.read_unsigned();
         if (is_th_ax) {
-            return mk_theorem(n, ps, t, v);
+            return mk_theorem(n, ps, t, v, w);
         } else {
-            unsigned w        = d.read_unsigned();
             bool use_conv_opt = (k & 2) != 0;
             return mk_definition(n, ps, t, v, w, use_conv_opt);
         }

src/library/reducible.cpp

@@ -84,8 +84,6 @@ static void check_declaration(environment const & env, name const & n) {
     declaration const & d = env.get(n);
     if (!d.is_definition())
         throw exception(sstream() << "invalid reducible command, '" << n << "' is not a definition");
-    if (d.is_theorem())
-        throw exception(sstream() << "invalid reducible command, '" << n << "' is a theorem");
 }
 
 environment set_reducible(environment const & env, name const & n, reducible_status s, bool persistent) {

src/library/unfold_macros.cpp

@@ -143,7 +143,8 @@ declaration unfold_untrusted_macros(environment const & env, declaration const &
         expr new_t = unfold_untrusted_macros(env, d.get_type(), trust_lvl);
         if (d.is_theorem()) {
             expr new_v = unfold_untrusted_macros(env, d.get_value(), trust_lvl);
-            return mk_theorem(d.get_name(), d.get_univ_params(), new_t, new_v);
+            return mk_theorem(d.get_name(), d.get_univ_params(), new_t, new_v,
+                              d.get_weight());
         } else if (d.is_definition()) {
             expr new_v = unfold_untrusted_macros(env, d.get_value(), trust_lvl);
             return mk_definition(d.get_name(), d.get_univ_params(), new_t, new_v,

src/library/update_declaration.cpp

@@ -28,7 +28,7 @@ static declaration update_declaration(declaration d, optional<level_param_names>
         if (is_eqp(d.get_type(), _type) && is_eqp(d.get_value(), _value) && is_eqp(d.get_univ_params(), _ps))
             return d;
         if (d.is_theorem())
-            return mk_theorem(d.get_name(), _ps, _type, _value);
+            return mk_theorem(d.get_name(), _ps, _type, _value, d.get_weight());
         else
             return mk_definition(d.get_name(), _ps, _type, _value,
                                  d.get_weight(), d.use_conv_opt());