feat(kernel): add is_bool predicate

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

src/kernel/builtin.cpp

@@ -66,6 +66,9 @@ public:
 };
 expr const Bool = mk_value(*(new bool_type_value()));
 expr mk_bool_type() { return Bool; }
+bool is_bool(expr const & e) {
+    return e == Bool || (is_constant(e) && const_name(e) == to_value(Bool).get_name());
+}
 // =======================================
 
 // =======================================

src/kernel/builtin.h

@@ -31,6 +31,7 @@ extern expr const TypeU;
 /** \brief Return the Lean Boolean type. */
 expr mk_bool_type();
 extern expr const Bool;
+bool is_bool(expr const & e);
 
 /** \brief Create a Lean Boolean value (true/false) */
 expr mk_bool_value(bool v);

src/kernel/type_checker.cpp

@@ -69,12 +69,12 @@ class type_checker::imp {
     expr check_type(expr const & e, expr const & s, context const & ctx) {
         if (is_type(e))
             return e;
-        if (e == Bool)
+        if (is_bool(e))
             return Type();
         expr u = normalize(e, ctx);
         if (is_type(u))
             return u;
-        if (u == Bool)
+        if (is_bool(u))
             return Type();
         if (has_metavar(u) && m_menv) {
             justification jst = mk_type_expected_justification(ctx, s);

src/library/elaborator/elaborator.cpp

@@ -659,7 +659,7 @@ class elaborator::imp {
        an equality constraint.
     */
     bool is_actual_lower(expr const & a) {
-        return is_type(a) || is_metavar(a) || a == Bool || (is_pi(a) && is_actual_lower(abst_body(a)));
+        return is_type(a) || is_metavar(a) || is_bool(a) || (is_pi(a) && is_actual_lower(abst_body(a)));
     }
 
     /**
@@ -942,7 +942,7 @@ class elaborator::imp {
         return
             is_convertible(c) &&
             is_metavar(convertible_to(c)) &&
-            (convertible_from(c) == Bool || is_type(convertible_from(c)));
+            (is_bool(convertible_from(c)) || is_type(convertible_from(c)));
     }
 
     /** \brief Process constraint of the form <tt>ctx |- a << ?m</tt>, where \c a is Type or Bool */
@@ -952,7 +952,7 @@ class elaborator::imp {
             // We approximate and only consider the most useful ones.
             justification new_jst(new destruct_justification(c));
             unification_constraint new_c;
-            if (a == Bool) {
+            if (is_bool(a)) {
                 expr choices[5] = { Bool, Type(), Type(level() + 1), TypeM, TypeU };
                 new_c = mk_choice_constraint(get_context(c), b, 5, choices, new_jst);
             } else {
@@ -1111,7 +1111,7 @@ class elaborator::imp {
             process_simple_ho_match(ctx, b, a, false, c))
             return true;
 
-        if (!eq && a == Bool && is_type(b))
+        if (!eq && is_bool(a) && is_type(b))
             return true;
 
         if (a.kind() == b.kind()) {
@@ -1254,9 +1254,9 @@ class elaborator::imp {
             push_front(mk_max_constraint(get_context(c), new_lhs1, new_lhs2, new_rhs, new_jst));
             return true;
         }
-        if (lhs1 == Bool)
+        if (is_bool(lhs1))
             lhs1 = Type();
-        if (lhs2 == Bool)
+        if (is_bool(lhs2))
             lhs2 = Type();
         if (is_type(lhs1) && is_type(lhs2)) {
             justification new_jst(new normalize_justification(c));

src/library/type_inferer.cpp

@@ -38,12 +38,12 @@ class type_inferer::imp {
     expr check_type(expr const & e, expr const & s, context const & ctx) {
         if (is_type(e))
             return e;
-        if (e == Bool)
+        if (is_bool(e))
             return Type();
         expr u = normalize(e, ctx);
         if (is_type(u))
             return u;
-        if (u == Bool)
+        if (is_bool(u))
             return Type();
         if (has_metavar(u) && m_menv) {
             justification jst = mk_type_expected_justification(ctx, s);
@@ -237,6 +237,15 @@ public:
         m_menv           = nullptr;
         m_menv_timestamp = 0;
     }
+
+    bool is_proposition(expr const & e, context const & ctx) {
+        buffer<unification_constraint> uc;
+        expr t = operator()(e, ctx, nullptr, uc);
+        if (is_bool(t))
+            return true;
+        else
+            return is_bool(normalize(e, ctx));
+    }
 };
 type_inferer::type_inferer(environment const & env):m_ptr(new imp(env)) {}
 type_inferer::~type_inferer() {}
@@ -248,9 +257,7 @@ expr type_inferer::operator()(expr const & e, context const & ctx) {
     return operator()(e, ctx, nullptr, uc);
 }
 bool type_inferer::is_proposition(expr const & e, context const & ctx) {
-    expr t = operator()(e, ctx);
-    // TODO(Leo): consider replacing the following test with is_convertible(t, Bool);
-    return t == Bool;
+    return m_ptr->is_proposition(e, ctx);
 }
 void type_inferer::clear() { m_ptr->clear(); }
 }

src/tests/frontends/lean/frontend.cpp

@@ -136,13 +136,13 @@ static void tst9() {
     f.add_definition("x", Bool, True);
     object const & obj = f.get_object("x");
     lean_assert(obj.get_name() == "x");
-    lean_assert(obj.get_type() == Bool);
+    lean_assert(is_bool(obj.get_type()));
     lean_assert(obj.get_value() == True);
     try { f.get_object("y"); lean_unreachable(); }
     catch (exception &) {}
     lean_assert(!f.find_object("y"));
     f.add_definition("y", False);
-    lean_assert(f.find_object("y").get_type() == Bool);
+    lean_assert(is_bool(f.find_object("y").get_type()));
     lean_assert(f.has_object("y"));
     lean_assert(!f.has_object("z"));
     bool found = false;

src/tests/library/type_inferer.cpp

@@ -34,7 +34,7 @@ static void tst1() {
     env.add_var("f", Int >> (Int >> Int));
     lean_assert(type_of(f(a, a)) == Int);
     lean_assert(type_of(f(a)) == Int >> Int);
-    lean_assert(type_of(And(a, f(a))) == Bool);
+    lean_assert(is_bool(type_of(And(a, f(a)))));
     lean_assert(type_of(Fun({a, Int}, iAdd(a, iVal(1)))) == Int >> Int);
     lean_assert(type_of(Let({a, iVal(10)}, iAdd(a, b))) == Int);
     lean_assert(type_of(Type()) == Type(level() + 1));