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

feat(kernel): add proof irrelevance for classes

Browse source 
We can use this feature to implement proof irrelevance for Identity types.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-05-16 15:04:34 -07:00
parent 193aa4a83f
commit 69e72c278d
10 changed files with 87 additions and 35 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

24
src/kernel/converter.cpp
View file

@ -363,6 +363,13 @@ struct default_converter : public converter {
}
}
/** \brief Return true iff t is a constant named f_name or an application of the form (f_name a_1 ... a_k) */
bool is_app_of(expr t, name const & f_name) {
while (is_app(t))
t = app_fn(t);
return is_constant(t) && const_name(t) == f_name;
}
/** Return true iff t is definitionally equal to s. */
virtual bool is_def_eq(expr const & t, expr const & s, context & c, delayed_justification & jst) {
check_system("is_definitionally_equal");
@ -446,10 +453,21 @@ struct default_converter : public converter {
return true;
}
if (m_env.proof_irrel()) {
// Proof irrelevance support
if (m_env.prop_proof_irrel()) {
// Proof irrelevance support for Prop/Bool (aka Type.{0})
expr t_type = c.infer_type(t);
return is_prop(t_type, c) && is_def_eq(t_type, c.infer_type(s), c, jst);
if (is_prop(t_type, c) && is_def_eq(t_type, c.infer_type(s), c, jst))
return true;
}
list<name> const & cls_proof_irrel = m_env.cls_proof_irrel();
if (!is_nil(cls_proof_irrel)) {
// Proof irrelevance support for classes
expr t_type = whnf(c.infer_type(t), c);
if (std::any_of(cls_proof_irrel.begin(), cls_proof_irrel.end(),
[&](name const & cls_name) { return is_app_of(t_type, cls_name); }) &&
is_def_eq(t_type, c.infer_type(s), c, jst))
return true;
}
return false;

15
src/kernel/environment.cpp
View file

@ -21,8 +21,10 @@ public:
}
};
environment_header::environment_header(unsigned trust_lvl, bool proof_irrel, bool eta, bool impredicative, std::unique_ptr<normalizer_extension const> ext):
m_trust_lvl(trust_lvl), m_proof_irrel(proof_irrel), m_eta(eta), m_impredicative(impredicative), m_norm_ext(std::move(ext)) {}
environment_header::environment_header(unsigned trust_lvl, bool prop_proof_irrel, bool eta, bool impredicative,
list<name> const & cls_proof_irrel, std::unique_ptr<normalizer_extension const> ext):
m_trust_lvl(trust_lvl), m_prop_proof_irrel(prop_proof_irrel), m_eta(eta), m_impredicative(impredicative),
m_cls_proof_irrel(cls_proof_irrel), m_norm_ext(std::move(ext)) {}
environment_extension::~environment_extension() {}
@ -45,12 +47,13 @@ bool environment_id::is_descendant(environment_id const & id) const {
environment::environment(header const & h, environment_id const & ancestor, definitions const & d, name_set const & g, extensions const & exts):
m_header(h), m_id(environment_id::mk_descendant(ancestor)), m_definitions(d), m_global_levels(g), m_extensions(exts) {}
environment::environment(unsigned trust_lvl, bool proof_irrel, bool eta, bool impredicative):
environment(trust_lvl, proof_irrel, eta, impredicative, std::unique_ptr<normalizer_extension>(new noop_normalizer_extension()))
environment::environment(unsigned trust_lvl, bool prop_proof_irrel, bool eta, bool impredicative, list<name> const & cls_proof_irrel):
environment(trust_lvl, prop_proof_irrel, eta, impredicative, cls_proof_irrel, std::unique_ptr<normalizer_extension>(new noop_normalizer_extension()))
{}
environment::environment(unsigned trust_lvl, bool proof_irrel, bool eta, bool impredicative, std::unique_ptr<normalizer_extension> ext):
m_header(std::make_shared<environment_header>(trust_lvl, proof_irrel, eta, impredicative, std::move(ext))),
environment::environment(unsigned trust_lvl, bool prop_proof_irrel, bool eta, bool impredicative, list<name> const & cls_proof_irrel,
std::unique_ptr<normalizer_extension> ext):
m_header(std::make_shared<environment_header>(trust_lvl, prop_proof_irrel, eta, impredicative, cls_proof_irrel, std::move(ext))),
m_extensions(std::make_shared<environment_extensions const>())
{}

28
src/kernel/environment.h
View file

@ -43,18 +43,21 @@ class environment_header {
>= 1 means do not check imported modules, and do not check macros
with level less than the value of this field.
*/
unsigned m_trust_lvl; //!the given one.
bool m_proof_irrel; //!< true if the kernel assumes proof irrelevance
bool m_eta; //!< true if the kernel uses eta-reduction in convertability checks
bool m_impredicative; //!< true if the kernel should treat (universe level 0) as a impredicative Prop/Bool.
unsigned m_trust_lvl; //!the given one.
bool m_prop_proof_irrel; //!< true if the kernel assumes proof irrelevance for Bool/Type (aka Type(0))
bool m_eta; //!< true if the kernel uses eta-reduction in convertability checks
bool m_impredicative; //!< true if the kernel should treat (universe level 0) as a impredicative Prop/Bool.
list<name> m_cls_proof_irrel; //!< list of proof irrelevant classes, if we want Id types to be proof irrelevant, we the name 'Id' in this list.
std::unique_ptr<normalizer_extension const> m_norm_ext;
void dealloc();
public:
environment_header(unsigned trust_lvl, bool proof_irrel, bool eta, bool impredicative, std::unique_ptr<normalizer_extension const> ext);
environment_header(unsigned trust_lvl, bool prop_proof_irrel, bool eta, bool impredicative,
list<name> const & cls_proof_irrel, std::unique_ptr<normalizer_extension const> ext);
unsigned trust_lvl() const { return m_trust_lvl; }
bool proof_irrel() const { return m_proof_irrel; }
bool prop_proof_irrel() const { return m_prop_proof_irrel; }
bool eta() const { return m_eta; }
bool impredicative() const { return m_impredicative; }
list<name> const & cls_proof_irrel() const { return m_cls_proof_irrel; }
normalizer_extension const & norm_ext() const { return *(m_norm_ext.get()); }
};
@ -107,8 +110,10 @@ class environment {
environment(header const & h, environment_id const & id, definitions const & d, name_set const & global_levels, extensions const & ext);
public:
environment(unsigned trust_lvl = 0, bool proof_irrel = true, bool eta = true, bool impredicative = true);
environment(unsigned trust_lvl, bool proof_irrel, bool eta, bool impredicative, std::unique_ptr<normalizer_extension> ext);
environment(unsigned trust_lvl = 0, bool prop_proof_irrel = true, bool eta = true, bool impredicative = true,
list<name> const & cls_proof_irrel = list<name>());
environment(unsigned trust_lvl, bool prop_proof_irrel, bool eta, bool impredicative, list<name> const & cls_proof_irrel,
std::unique_ptr<normalizer_extension> ext);
~environment();
/** \brief Return the environment unique identifier. */
@ -120,8 +125,11 @@ 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 */
bool proof_irrel() const { return m_header->proof_irrel(); }
/** \brief Return true iff the environment assumes proof irrelevance for Type.{0} (i.e., Bool) */
bool prop_proof_irrel() const { return m_header->prop_proof_irrel(); }
/** \brief Return the list of classes marked as proof irrelevant */
list<name> const & cls_proof_irrel() const { return m_header->cls_proof_irrel(); }
/** \brief Return true iff the environment assumes Eta-reduction */
bool eta() const { return m_header->eta(); }

21
src/library/kernel_bindings.cpp
View file

@ -993,7 +993,8 @@ DEFINE_LUA_LIST(certified_definition, push_certified_definition, to_certified_de
DECL_UDATA(environment)
static int environment_is_descendant(lua_State * L) { return push_boolean(L, to_environment(L, 1).is_descendant(to_environment(L, 2))); }
static int environment_trust_lvl(lua_State * L) { return push_integer(L, to_environment(L, 1).trust_lvl()); }
static int environment_proof_irrel(lua_State * L) { return push_boolean(L, to_environment(L, 1).proof_irrel()); }
static int environment_prop_proof_irrel(lua_State * L) { return push_boolean(L, to_environment(L, 1).prop_proof_irrel()); }
static int environment_cls_proof_irrel(lua_State * L) { return push_list_name(L, to_environment(L, 1).cls_proof_irrel()); }
static int environment_eta(lua_State * L) { return push_boolean(L, to_environment(L, 1).eta()); }
static int environment_impredicative(lua_State * L) { return push_boolean(L, to_environment(L, 1).impredicative()); }
static int environment_add_global_level(lua_State * L) { return push_environment(L, to_environment(L, 1).add_global_level(to_name_ext(L, 2))); }
@ -1003,13 +1004,13 @@ static int environment_get(lua_State * L) { return push_definition(L, to_environ
static int environment_add(lua_State * L) { return push_environment(L, to_environment(L, 1).add(to_certified_definition(L, 2))); }
static int environment_replace(lua_State * L) { return push_environment(L, to_environment(L, 1).replace(to_certified_definition(L, 2))); }
static int mk_empty_environment(lua_State * L) {
unsigned trust_lvl = get_uint_named_param(L, 1, "trust_lvl", 0);
trust_lvl = get_uint_named_param(L, 1, "trust_level", trust_lvl);
bool proof_irrel = get_bool_named_param(L, 1, "proof_irrel", true);
proof_irrel = get_bool_named_param(L, 1, "proof_irrelevance", proof_irrel);
bool eta = get_bool_named_param(L, 1, "eta", true);
bool impredicative = get_bool_named_param(L, 1, "impredicative", true);
return push_environment(L, environment(trust_lvl, proof_irrel, eta, impredicative));
unsigned trust_lvl = get_uint_named_param(L, 1, "trust_lvl", 0);
trust_lvl = get_uint_named_param(L, 1, "trust_level", trust_lvl);
bool prop_proof_irrel = get_bool_named_param(L, 1, "prop_proof_irrel", true);
bool eta = get_bool_named_param(L, 1, "eta", true);
bool impredicative = get_bool_named_param(L, 1, "impredicative", true);
list<name> const & cls_proof_irrel = get_list_name_named_param(L, 1, "cls_proof_irrel", list<name>());
return push_environment(L, environment(trust_lvl, prop_proof_irrel, eta, impredicative, cls_proof_irrel));
}
static int environment_forget(lua_State * L) { return push_environment(L, to_environment(L, 1).forget()); }
@ -1018,8 +1019,8 @@ static const struct luaL_Reg environment_m[] = {
{"is_descendant", safe_function<environment_is_descendant>},
{"trust_lvl", safe_function<environment_trust_lvl>},
{"trust_level", safe_function<environment_trust_lvl>},
{"proof_irrel", safe_function<environment_proof_irrel>},
{"proof_irrelevance", safe_function<environment_proof_irrel>},
{"prop_proof_irrel", safe_function<environment_prop_proof_irrel>},
{"cls_proof_irrel", safe_function<environment_cls_proof_irrel>},
{"eta", safe_function<environment_eta>},
{"impredicative", safe_function<environment_impredicative>},
{"add_global_level", safe_function<environment_add_global_level>},

2
src/tests/kernel/environment.cpp
View file

@ -125,7 +125,7 @@ public:
};
static void tst3() {
environment env(0, true, true, true, std::unique_ptr<normalizer_extension>(new normalizer_extension_tst()));
environment env(0, true, true, true, list<name>(), std::unique_ptr<normalizer_extension>(new normalizer_extension_tst()));
expr A = Const("A");
expr x = Const("x");
expr id = Const("id");

22
src/util/lua_named_param.cpp
View file

@ -125,5 +125,27 @@ name_set get_name_set_named_param(lua_State * L, int idx, char const * opt_name,
return def_value;
}
}
list<name> get_list_name_named_param(lua_State * L, int idx, char const * opt_name, list<name> const & def_value) {
if (lua_istable(L, idx)) {
push_string(L, opt_name);
lua_gettable(L, idx);
if (is_list_name(L, -1) || lua_istable(L, -1)) {
list<name> result = to_list_name_ext(L, -1);
lua_pop(L, 1);
return result;
} else if (lua_isnil(L, -1)) {
lua_pop(L, 1);
return def_value;
} else {
lua_pop(L, 1);
throw exception(sstream() << "field '" << opt_name << "' must be a list of names in table at arg #" << idx);
}
} else if (idx <= lua_gettop(L) && !lua_isnil(L, idx)) {
throw exception(sstream() << "arg #" << idx << " must be a table");
} else {
return def_value;
}
}
}

1
src/util/lua_named_param.h
View file

@ -19,4 +19,5 @@ unsigned get_uint_named_param(lua_State * L, int idx, char const * opt_name, uns
optional<unsigned> get_opt_uint_named_param(lua_State * L, int idx, char const * opt_name,
optional<unsigned> const & def_value = optional<unsigned>());
name_set get_name_set_named_param(lua_State * L, int idx, char const * opt_name, name_set const & def_value = name_set());
list<name> get_list_name_named_param(lua_State * L, int idx, char const * opt_name, list<name> const & def_value);
}

2
tests/lua/env1.lua
View file

@ -5,5 +5,5 @@ local env2 = env:add_global_level("U")
assert(not env:is_global_level("U"))
assert(env2:is_global_level("U"))
assert(env:eta())
assert(env:proof_irrel())
assert(env:prop_proof_irrel())
assert(env:impredicative())

5
tests/lua/env2.lua
View file

@ -1,8 +1,7 @@
assert(not empty_environment({eta=false}):eta())
assert(empty_environment({eta=true}):eta())
assert(not empty_environment({proof_irrel=false}):proof_irrel())
assert(not empty_environment({proof_irrel=false}):proof_irrelevance())
assert(empty_environment({proof_irrel=true}):proof_irrelevance())
assert(not empty_environment({prop_proof_irrel=false}):prop_proof_irrel())
assert(empty_environment({prop_proof_irrel=true}):prop_proof_irrel())
assert(empty_environment({impredicative=true}):impredicative())
assert(not empty_environment({impredicative=false}):impredicative())
assert(empty_environment({trust_lvl=10}):trust_lvl() == 10)

2
tests/lua/env3.lua
View file

@ -14,7 +14,7 @@ local t = type_checker(env)
assert(t:is_def_eq(p, q))
assert(t:is_def_eq(And(p, q), And(q, p)))
env = init(empty_environment({proof_irrel=false}))
env = init(empty_environment({prop_proof_irrel=false}))
t = type_checker(env)
assert(not t:is_def_eq(p, q))
assert(not t:is_def_eq(And(p, q), And(q, p)))