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 <leonardo@microsoft.com>

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;

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

src/kernel/type_checker.cpp

@@ -421,9 +421,14 @@ public:
     bool is_proposition(expr const & e, context const & ctx, optional<metavar_env> 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))

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<environment_type_check>},
     {"infer_type",     safe_function<environment_infer_type>},
     {"normalize",      safe_function<environment_normalize>},
+    {"is_proposition", safe_function<environment_is_proposition>},
     {"objects",        safe_function<environment_objects>},
     {"local_objects",  safe_function<environment_local_objects>},
     {"set_opaque",     safe_function<environment_set_opaque>},

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]])))
+
+