diff --git a/library/init/meta/environment.lean b/library/init/meta/environment.lean index c32492b910..eae0244202 100644 --- a/library/init/meta/environment.lean +++ b/library/init/meta/environment.lean @@ -13,8 +13,6 @@ namespace environment meta constant mk_std : nat → environment /- Return the trust level of the given environment -/ meta constant trust_lvl : environment → nat -/- Return tt iff it is a standard environment -/ -meta constant is_std : environment → bool /- Add a new declaration to the environment -/ meta constant add : environment → declaration → exceptional environment /- Retrieve a declaration from the environment -/ diff --git a/src/api/env.cpp b/src/api/env.cpp index 06be3bda4f..761c183267 100644 --- a/src/api/env.cpp +++ b/src/api/env.cpp @@ -51,10 +51,6 @@ unsigned lean_env_trust_level(lean_env e) { return e ? to_env_ref(e).trust_lvl() : 0; } -lean_bool lean_env_proof_irrel(lean_env e) { - return e && to_env_ref(e).prop_proof_irrel(); -} - lean_bool lean_env_contains_univ(lean_env e, lean_name n) { return e && n && to_env_ref(e).is_universe(to_name_ref(n)); } diff --git a/src/api/lean_env.h b/src/api/lean_env.h index 08de13f12b..7c46364fd5 100644 --- a/src/api/lean_env.h +++ b/src/api/lean_env.h @@ -46,8 +46,6 @@ void lean_env_del(lean_env e); /** \brief Return the trust level of the given environment */ unsigned lean_env_trust_level(lean_env e); -/** \brief Return true iff the given environment has a proof irrelevant Prop (i.e., Type.{0}). */ -lean_bool lean_env_proof_irrel(lean_env e); /** \brief Return true iff \c e contains a global universe with name \c n. */ lean_bool lean_env_contains_univ(lean_env e, lean_name n); diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp index bbedd1f3c8..415cae374b 100644 --- a/src/frontends/lean/builtin_cmds.cpp +++ b/src/frontends/lean/builtin_cmds.cpp @@ -372,8 +372,6 @@ static environment help_cmd(parser & p) { } static environment init_quotient_cmd(parser & p) { - if (!(p.env().prop_proof_irrel())) - throw parser_error("invalid init_quotient command, this command is only available for kernels containing an impredicative and proof irrelevant Prop", p.cmd_pos()); return module::declare_quotient(p.env()); } diff --git a/src/kernel/environment.cpp b/src/kernel/environment.cpp index 0a073cd10b..4e581ce930 100644 --- a/src/kernel/environment.cpp +++ b/src/kernel/environment.cpp @@ -12,8 +12,8 @@ Author: Leonardo de Moura #include "kernel/kernel_exception.h" namespace lean { -environment_header::environment_header(unsigned trust_lvl, bool prop_proof_irrel, std::unique_ptr ext): - m_trust_lvl(trust_lvl), m_prop_proof_irrel(prop_proof_irrel), m_norm_ext(std::move(ext)) {} +environment_header::environment_header(unsigned trust_lvl, std::unique_ptr ext): + m_trust_lvl(trust_lvl), m_norm_ext(std::move(ext)) {} environment_extension::~environment_extension() {} @@ -71,12 +71,12 @@ bool environment_id::is_descendant(environment_id const & id) const { environment::environment(header const & h, environment_id const & ancestor, declarations const & d, name_set const & g, extensions const & exts): m_header(h), m_id(environment_id::mk_descendant(ancestor)), m_declarations(d), m_global_levels(g), m_extensions(exts) {} -environment::environment(unsigned trust_lvl, bool prop_proof_irrel): - environment(trust_lvl, prop_proof_irrel, mk_id_normalizer_extension()) +environment::environment(unsigned trust_lvl): + environment(trust_lvl, mk_id_normalizer_extension()) {} -environment::environment(unsigned trust_lvl, bool prop_proof_irrel, std::unique_ptr ext): - m_header(std::make_shared(trust_lvl, prop_proof_irrel, std::move(ext))), +environment::environment(unsigned trust_lvl, std::unique_ptr ext): + m_header(std::make_shared(trust_lvl, std::move(ext))), m_extensions(std::make_shared()) {} diff --git a/src/kernel/environment.h b/src/kernel/environment.h index 2e3c69f2e2..7ee6e03a56 100644 --- a/src/kernel/environment.h +++ b/src/kernel/environment.h @@ -43,13 +43,11 @@ class environment_header { allow us to add declarations without type checking them (e.g., m_trust_lvl > LEAN_BELIEVER_TRUST_LEVEL) */ unsigned m_trust_lvl; - bool m_prop_proof_irrel; //!< true if the kernel assumes proof irrelevance for Prop (aka Type.{0}) std::unique_ptr m_norm_ext; void dealloc(); public: - environment_header(unsigned trust_lvl, bool prop_proof_irrel, std::unique_ptr ext); + environment_header(unsigned trust_lvl, std::unique_ptr ext); unsigned trust_lvl() const { return m_trust_lvl; } - bool prop_proof_irrel() const { return m_prop_proof_irrel; } normalizer_extension const & norm_ext() const { return *(m_norm_ext.get()); } bool is_recursor(environment const & env, name const & n) const { return m_norm_ext->is_recursor(env, n); } bool is_builtin(environment const & env, name const & n) const { return m_norm_ext->is_builtin(env, n); } @@ -93,7 +91,6 @@ public: \brief Lean core environment. An environment object can be extended/customized in different ways: 1- By providing a normalizer_extension when creating an empty environment. - 2- By setting the proof_irrel when creating an empty environment. 3- By attaching additional data as environment::extensions. The additional data can be added at any time. They contain information used by the automation (e.g., rewriting sets, unification hints, etc). */ @@ -120,8 +117,8 @@ class environment { */ environment add(declaration const & d) const; public: - environment(unsigned trust_lvl = 0, bool prop_proof_irrel = true); - environment(unsigned trust_lvl, bool prop_proof_irrel, std::unique_ptr ext); + environment(unsigned trust_lvl = 0); + environment(unsigned trust_lvl, std::unique_ptr ext); ~environment(); /** \brief Return the environment unique identifier. */ @@ -133,9 +130,6 @@ public: /** \brief Return the trust level of this environment. */ unsigned trust_lvl() const { return m_header->trust_lvl(); } - /** \brief Return true iff the environment assumes proof irrelevance for Type.{0} (i.e., Prop) */ - bool prop_proof_irrel() const { return m_header->prop_proof_irrel(); } - bool is_recursor(name const & n) const { return m_header->is_recursor(*this, n); } bool is_builtin(name const & n) const { return m_header->is_builtin(*this, n); } diff --git a/src/kernel/inductive/inductive.cpp b/src/kernel/inductive/inductive.cpp index 38b6482f03..faff29f44c 100644 --- a/src/kernel/inductive/inductive.cpp +++ b/src/kernel/inductive/inductive.cpp @@ -509,7 +509,7 @@ struct add_inductive_fn { /** \brief Initialize m_dep_elim flag. */ void set_dep_elim() { - if (m_env.prop_proof_irrel() && is_zero(m_it_level)) + if (is_zero(m_it_level)) m_dep_elim = false; else m_dep_elim = true; @@ -558,7 +558,6 @@ struct add_inductive_fn { // In the following for-loop we check if the intro rule // has 0 arguments. bool is_K_target = - m_env.prop_proof_irrel() && // Proof irrelevance is enabled is_zero(m_it_level) && // It is a Prop length(m_decl.m_intro_rules) == 1; // datatype has only one intro rule for (auto ir : m_decl.m_intro_rules) { diff --git a/src/kernel/type_checker.cpp b/src/kernel/type_checker.cpp index a40bffb7cd..d01e89d276 100644 --- a/src/kernel/type_checker.cpp +++ b/src/kernel/type_checker.cpp @@ -561,8 +561,6 @@ bool type_checker::is_def_eq_app(expr const & t, expr const & s) { /** \brief Return true if \c t and \c s are definitionally equal due to proof irrelevant. Return false otherwise. */ bool type_checker::is_def_eq_proof_irrel(expr const & t, expr const & s) { - if (!m_env.prop_proof_irrel()) - return false; // Proof irrelevance support for Prop (aka Type.{0}) expr t_type = infer_type(t); expr s_type = infer_type(s); diff --git a/src/library/constructions/no_confusion.cpp b/src/library/constructions/no_confusion.cpp index 9800fcaeb1..63854bbbaa 100644 --- a/src/library/constructions/no_confusion.cpp +++ b/src/library/constructions/no_confusion.cpp @@ -94,25 +94,20 @@ optional mk_no_confusion_type(environment const & env, name const & throw_corrupted(n); buffer rtype_hyp; // add equalities - if (env.prop_proof_irrel()) { - // proof irrelevance version using heterogeneous equality - for (unsigned i = 0; i < minor1_args.size(); i++) { - expr lhs = minor1_args[i]; - expr rhs = minor2_args[i]; - expr lhs_type = mlocal_type(lhs); - expr rhs_type = mlocal_type(rhs); - level l = sort_level(tc.ensure_type(lhs_type)); - expr h_type; - if (tc.is_def_eq(lhs_type, rhs_type)) { - h_type = mk_app(mk_constant(get_eq_name(), to_list(l)), lhs_type, lhs, rhs); - } else { - h_type = mk_app(mk_constant(get_heq_name(), to_list(l)), lhs_type, lhs, rhs_type, rhs); - } - rtype_hyp.push_back(mk_local(mk_fresh_name(), local_pp_name(lhs).append_after("_eq"), h_type, binder_info())); + // proof irrelevance version using heterogeneous equality + for (unsigned i = 0; i < minor1_args.size(); i++) { + expr lhs = minor1_args[i]; + expr rhs = minor2_args[i]; + expr lhs_type = mlocal_type(lhs); + expr rhs_type = mlocal_type(rhs); + level l = sort_level(tc.ensure_type(lhs_type)); + expr h_type; + if (tc.is_def_eq(lhs_type, rhs_type)) { + h_type = mk_app(mk_constant(get_eq_name(), to_list(l)), lhs_type, lhs, rhs); + } else { + h_type = mk_app(mk_constant(get_heq_name(), to_list(l)), lhs_type, lhs, rhs_type, rhs); } - } else { - // we use telescope equality (with casts) when proof irrelevance is not available - mk_telescopic_eq(tc, minor1_args, minor2_args, rtype_hyp); + rtype_hyp.push_back(mk_local(mk_fresh_name(), local_pp_name(lhs).append_after("_eq"), h_type, binder_info())); } inner_cases_on_args.push_back(Fun(minor2_args, mk_arrow(Pi(rtype_hyp, P), Pres))); } diff --git a/src/library/inductive_compiler/basic.cpp b/src/library/inductive_compiler/basic.cpp index 35598db2be..46c280ed9c 100644 --- a/src/library/inductive_compiler/basic.cpp +++ b/src/library/inductive_compiler/basic.cpp @@ -94,8 +94,7 @@ class add_basic_inductive_decl_fn { if (gen_cases_on) m_env = mk_cases_on(m_env, ind_name); - if (gen_cases_on && gen_no_confusion && has_eq - && ((m_env.prop_proof_irrel() && has_heq) || (!m_env.prop_proof_irrel() && has_lift))) { + if (gen_cases_on && gen_no_confusion && has_eq && has_heq) { m_env = mk_no_confusion(m_env, ind_name); } diff --git a/src/library/print.cpp b/src/library/print.cpp index c1d7ce09a7..bf83a6a6e0 100644 --- a/src/library/print.cpp +++ b/src/library/print.cpp @@ -102,7 +102,6 @@ name fix_internal_name(name const & a) { */ struct print_expr_fn { std::ostream & m_out; - bool m_type0_as_bool; std::ostream & out() { return m_out; } @@ -127,11 +126,8 @@ struct print_expr_fn { void print_sort(expr const & a) { if (is_zero(sort_level(a))) { - if (m_type0_as_bool) - out() << "Prop"; - else - out() << "Type"; - } else if (m_type0_as_bool && is_one(sort_level(a))) { + out() << "Prop"; + } else if (is_one(sort_level(a))) { out() << "Type"; } else { out() << "Type.{" << sort_level(a) << "}"; @@ -253,7 +249,7 @@ struct print_expr_fn { } } - print_expr_fn(std::ostream & out, bool type0_as_bool = true):m_out(out), m_type0_as_bool(type0_as_bool) {} + print_expr_fn(std::ostream & out):m_out(out) {} void operator()(expr const & e) { scoped_expr_caching set(false); @@ -265,7 +261,7 @@ formatter_factory mk_print_formatter_factory() { return [](environment const & env, options const & o, abstract_type_context &) { // NOLINT return formatter(o, [=](expr const & e, options const &) { std::ostringstream s; - print_expr_fn pr(s, env.prop_proof_irrel()); + print_expr_fn pr(s); pr(e); return format(s.str()); }); diff --git a/src/library/standard_kernel.cpp b/src/library/standard_kernel.cpp index ccd9672852..e85647f497 100644 --- a/src/library/standard_kernel.cpp +++ b/src/library/standard_kernel.cpp @@ -13,7 +13,6 @@ using inductive::inductive_normalizer_extension; /** \brief Create standard Lean environment */ environment mk_environment(unsigned trust_lvl) { return environment(trust_lvl, - true /* Type.{0} is proof irrelevant */, /* builtin support for inductive */ compose(std::unique_ptr(new inductive_normalizer_extension()), std::unique_ptr(new quotient_normalizer_extension()))); diff --git a/src/library/tactic/cases_tactic.cpp b/src/library/tactic/cases_tactic.cpp index 828eb8d84d..4693edab00 100644 --- a/src/library/tactic/cases_tactic.cpp +++ b/src/library/tactic/cases_tactic.cpp @@ -95,7 +95,7 @@ struct cases_tactic_fn { return false; if (!m_env.find(name{const_name(fn), "cases_on"}) || !m_env.find(get_eq_name())) return false; - if (is_standard(m_env) && !m_env.find(get_heq_name())) + if (!m_env.find(get_heq_name())) return false; init_inductive_info(const_name(fn)); if (args.size() != m_nindices + m_nparams) @@ -178,7 +178,6 @@ struct cases_tactic_fn { The original goal is solved if we can solve the produced goal. */ expr generalize_indices(expr const & mvar, expr const & h, buffer & new_indices_H, unsigned & num_eqs) { - lean_assert(is_standard(m_env)); metavar_decl g = *m_mctx.get_metavar_decl(mvar); type_context ctx = mk_type_context_for(g); expr h_type = ctx.relaxed_whnf(ctx.infer(h)); diff --git a/src/library/type_context.cpp b/src/library/type_context.cpp index 58bfa4f620..9097d036f6 100644 --- a/src/library/type_context.cpp +++ b/src/library/type_context.cpp @@ -1925,8 +1925,6 @@ bool type_context::is_def_eq_eta(expr const & e1, expr const & e2) { } bool type_context::is_def_eq_proof_irrel(expr const & e1, expr const & e2) { - if (!env().prop_proof_irrel()) - return false; expr e1_type = infer(e1); if (is_prop(e1_type)) { expr e2_type = infer(e2); diff --git a/src/library/util.cpp b/src/library/util.cpp index cb6785212c..032e2b2c4f 100644 --- a/src/library/util.cpp +++ b/src/library/util.cpp @@ -62,10 +62,6 @@ bool is_app_of(expr const & t, name const & f_name, unsigned nargs) { return is_constant(fn) && const_name(fn) == f_name && get_app_num_args(t) == nargs; } -bool is_standard(environment const & env) { - return env.prop_proof_irrel(); -} - optional unfold_term(environment const & env, expr const & e) { expr const & f = get_app_fn(e); if (!is_constant(f)) @@ -361,62 +357,6 @@ expr to_telescope(type_checker & ctx, expr type, buffer & telescope, optio return type; } -void mk_telescopic_eq(type_checker & tc, buffer const & t, buffer const & s, buffer & eqs) { - lean_assert(t.size() == s.size()); - lean_assert(std::all_of(s.begin(), s.end(), is_local)); - lean_assert(inductive::has_dep_elim(tc.env(), get_eq_name())); - buffer> t_aux; - name e_name("e"); - for (unsigned i = 0; i < t.size(); i++) { - expr s_i = s[i]; - expr s_i_ty = mlocal_type(s_i); - expr s_i_ty_a = abstract_locals(s_i_ty, i, s.data()); - expr t_i = t[i]; - t_aux.push_back(buffer()); - t_aux.back().push_back(t_i); - for (unsigned j = 0; j < i; j++) { - if (depends_on(s_i_ty, s[j])) { - // we need to "cast" - buffer ty_inst_args; - for (unsigned k = 0; k <= j; k++) - ty_inst_args.push_back(s[k]); - for (unsigned k = j + 1; k < i; k++) - ty_inst_args.push_back(t_aux[k][j+1]); - lean_assert(ty_inst_args.size() == i); - expr s_i_ty = instantiate_rev(s_i_ty_a, i, ty_inst_args.data()); - buffer rec_args; - rec_args.push_back(mlocal_type(s[j])); - rec_args.push_back(t_aux[j][j]); - rec_args.push_back(Fun(s[j], Fun(eqs[j], s_i_ty))); // type former ("promise") - rec_args.push_back(t_i); // minor premise - rec_args.push_back(s[j]); - rec_args.push_back(eqs[j]); - level rec_l1 = get_level(tc, s_i_ty); - level rec_l2 = get_level(tc, mlocal_type(s[j])); - t_i = mk_app(mk_constant(get_eq_rec_name(), {rec_l1, rec_l2}), rec_args.size(), rec_args.data()); - } - t_aux.back().push_back(t_i); - } - expr eq = mk_local(mk_fresh_name(), e_name.append_after(i+1), mk_eq(tc, t_i, s_i), binder_info()); - eqs.push_back(eq); - } -} - -void mk_telescopic_eq(type_checker & tc, buffer const & t, buffer & eqs) { - lean_assert(std::all_of(t.begin(), t.end(), is_local)); - lean_assert(inductive::has_dep_elim(tc.env(), get_eq_name())); - buffer s; - for (unsigned i = 0; i < t.size(); i++) { - expr ty = mlocal_type(t[i]); - ty = abstract_locals(ty, i, t.data()); - ty = instantiate_rev(ty, i, s.data()); - expr local = mk_local(mk_fresh_name(), local_pp_name(t[i]).append_after("'"), ty, local_info(t[i])); - s.push_back(local); - } - return mk_telescopic_eq(tc, t, s, eqs); -} - - /* ---------------------------------------------- Helper functions for creating basic operations diff --git a/src/library/util.h b/src/library/util.h index c6b6828f38..4a547c5625 100644 --- a/src/library/util.h +++ b/src/library/util.h @@ -41,9 +41,6 @@ optional unfold_app(environment const & env, expr const & e); \pre is_not_zero(l) */ optional dec_level(level const & l); -/** \brief Return true iff \c env has been configured with an impredicative and proof irrelevant Prop. */ -bool is_standard(environment const & env); - bool has_poly_unit_decls(environment const & env); bool has_eq_decls(environment const & env); bool has_heq_decls(environment const & env); @@ -135,12 +132,6 @@ expr fun_to_telescope(expr const & e, buffer & telescope, optional & telescope, optional const & binfo = optional()); -/** \brief Create a telescope equality for HoTT library. - This procedure assumes eq supports dependent elimination. - For HoTT, we can't use heterogeneous equality. */ -void mk_telescopic_eq(type_checker & tc, buffer const & t, buffer const & s, buffer & eqs); -void mk_telescopic_eq(type_checker & tc, buffer const & t, buffer & eqs); - /** \brief Return the universe where inductive datatype resides \pre \c ind_type is of the form Pi (a_1 : A_1) (a_2 : A_2[a_1]) ..., Type.{lvl} */ level get_datatype_level(expr ind_type); diff --git a/src/library/vm/vm_environment.cpp b/src/library/vm/vm_environment.cpp index 0e2a3d9b7f..30733f84dd 100644 --- a/src/library/vm/vm_environment.cpp +++ b/src/library/vm/vm_environment.cpp @@ -45,10 +45,6 @@ vm_obj environment_trust_lvl(vm_obj const & env) { return mk_vm_nat(to_env(env).trust_lvl()); } -vm_obj environment_is_std(vm_obj const & env) { - return mk_vm_bool(is_standard(to_env(env))); -} - vm_obj environment_add(vm_obj const & env, vm_obj const & decl) { try { return mk_vm_exceptional_success(to_obj(module::add(to_env(env), check(to_env(env), to_declaration(decl))))); @@ -187,7 +183,6 @@ vm_obj environment_symm_for(vm_obj const & env, vm_obj const & n) { void initialize_vm_environment() { DECLARE_VM_BUILTIN(name({"environment", "mk_std"}), environment_mk_std); DECLARE_VM_BUILTIN(name({"environment", "trust_lvl"}), environment_trust_lvl); - DECLARE_VM_BUILTIN(name({"environment", "is_std"}), environment_is_std); DECLARE_VM_BUILTIN(name({"environment", "add"}), environment_add); DECLARE_VM_BUILTIN(name({"environment", "get"}), environment_get); DECLARE_VM_BUILTIN(name({"environment", "fold"}), environment_fold); diff --git a/tests/lean/run/meta_env1.lean b/tests/lean/run/meta_env1.lean index 044f0a8b95..ce21e9eaee 100644 --- a/tests/lean/run/meta_env1.lean +++ b/tests/lean/run/meta_env1.lean @@ -5,7 +5,6 @@ meta definition e := environment.mk_std 0 definition hints := reducibility_hints.regular 10 tt vm_eval environment.trust_lvl e -vm_eval environment.is_std e vm_eval (environment.add e (declaration.defn `foo [] (expr.sort (level.succ (level.zero)))