From 94fa987814608ea82b36fde40ffdf6228d5ec539 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 15 Jan 2014 11:02:47 -0800 Subject: [PATCH] fix(kernel/type_checker): is_proposition method was still assuming that a Pi never has type Bool The method is_proposition was using an optimization that became incorrect after we identified Pi and forall. It was assuming that any Pi expression is not a proposition. This is not true anymore. Now, (Pi x : A, B) is a proposition if B is a proposition. Signed-off-by: Leonardo de Moura --- src/kernel/environment.cpp | 4 ++++ src/kernel/environment.h | 5 +++++ src/kernel/type_checker.cpp | 11 ++++++++--- src/library/kernel_bindings.cpp | 11 +++++++++++ tests/lua/is_prop1.lua | 27 +++++++++++++++++++++++++++ 5 files changed, 55 insertions(+), 3 deletions(-) create mode 100644 tests/lua/is_prop1.lua diff --git a/src/kernel/environment.cpp b/src/kernel/environment.cpp index 1c48867944..7c5d39365c 100644 --- a/src/kernel/environment.cpp +++ b/src/kernel/environment.cpp @@ -530,6 +530,10 @@ expr environment_cell::normalize(expr const & e, context const & ctx, bool unfol return m_type_checker->get_normalizer()(e, ctx, unfold_opaque); } +bool environment_cell::is_proposition(expr const & e, context const & ctx) const { + return m_type_checker->is_proposition(e, ctx); +} + bool environment_cell::already_imported(name const & n) const { if (m_imported_modules.find(n) != m_imported_modules.end()) return true; diff --git a/src/kernel/environment.h b/src/kernel/environment.h index 3df18e934f..4dad4418b1 100644 --- a/src/kernel/environment.h +++ b/src/kernel/environment.h @@ -230,6 +230,11 @@ public: */ expr normalize(expr const & e, context const & ctx = context(), bool unfold_opaque = false) const; + /** + \brief Return true iff \c e is a proposition. + */ + bool is_proposition(expr const & e, context const & ctx = context()) const; + /** \brief Low-level function for accessing objects. Consider using iterators. */ diff --git a/src/kernel/type_checker.cpp b/src/kernel/type_checker.cpp index 46da9c1c0c..96c69ddf8e 100644 --- a/src/kernel/type_checker.cpp +++ b/src/kernel/type_checker.cpp @@ -421,9 +421,14 @@ public: bool is_proposition(expr const & e, context const & ctx, optional const & menv) { // Catch easy cases switch (e.kind()) { - case expr_kind::Lambda: case expr_kind::Pi: case expr_kind::Type: return false; - case expr_kind::HEq: return true; - default: break; + case expr_kind::Lambda: case expr_kind::Type: + return false; + case expr_kind::HEq: + return true; + case expr_kind::Pi: + return is_proposition(abst_body(e), extend(ctx, abst_name(e), abst_domain(e)), menv); + default: + break; } expr t = infer_type(e, ctx, menv, nullptr); if (is_bool(t)) diff --git a/src/library/kernel_bindings.cpp b/src/library/kernel_bindings.cpp index 389ed7727a..7d3e389b02 100644 --- a/src/library/kernel_bindings.cpp +++ b/src/library/kernel_bindings.cpp @@ -1123,6 +1123,16 @@ static int environment_infer_type(lua_State * L) { return push_expr(L, env->infer_type(to_expr(L, 2), to_context(L, 3))); } +static int environment_is_proposition(lua_State * L) { + int nargs = lua_gettop(L); + ro_shared_environment env(L, 1); + if (nargs == 2) + lua_pushboolean(L, env->is_proposition(to_expr(L, 2))); + else + lua_pushboolean(L, env->is_proposition(to_expr(L, 2), to_context(L, 3))); + return 1; +} + static int environment_tostring(lua_State * L) { ro_shared_environment env(L, 1); std::ostringstream out; @@ -1213,6 +1223,7 @@ static const struct luaL_Reg environment_m[] = { {"type_check", safe_function}, {"infer_type", safe_function}, {"normalize", safe_function}, + {"is_proposition", safe_function}, {"objects", safe_function}, {"local_objects", safe_function}, {"set_opaque", safe_function}, diff --git a/tests/lua/is_prop1.lua b/tests/lua/is_prop1.lua new file mode 100644 index 0000000000..b483696291 --- /dev/null +++ b/tests/lua/is_prop1.lua @@ -0,0 +1,27 @@ +local env = get_environment() +assert(env:is_proposition(Const("true"))) +assert(env:is_proposition(Const("false"))) +assert(not env:is_proposition(nVal(0))) +assert(env:is_proposition(parse_lean([[forall x : Nat, x > 0]]))) +parse_lean_cmds([[ + variable f : Nat -> Nat -> Nat + variable p : Nat -> Bool + variables a b c : Nat + definition B := Bool + variable q : B +]]) +assert(env:is_proposition(parse_lean([[p (f a 0)]]))) +assert(env:is_proposition(parse_lean([[p (f a 0) /\ a > 0]]))) +assert(not env:is_proposition(parse_lean([[fun x, p (f x 0) /\ a > 0]]))) +assert(env:is_proposition(parse_lean([[forall x : Bool, x]]))) +assert(not env:is_proposition(parse_lean([[forall x : Nat, Nat]]))) +assert(not env:is_proposition(parse_lean([[forall T : Type, T]]))) +assert(env:is_proposition(parse_lean([[forall x y z, x /\ z /\ y]]))) +assert(env:is_proposition(parse_lean([[true -> false]]))) +assert(env:is_proposition(parse_lean([[Nat -> false]]))) +assert(not env:is_proposition(parse_lean([[true -> Nat]]))) +assert(not env:is_proposition(parse_lean([[Type]]))) +assert(env:is_proposition(parse_lean([[0 == 1]]))) +assert(env:is_proposition(parse_lean([[q]]))) + +