refactor(kernel): add level normalizer, is_equivalent predicate, switch to is_equivalent in the type checker, fix bugs in is_lt predicate

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

src/kernel/converter.cpp

@@ -316,10 +316,14 @@ struct default_converter : public converter {
                 return to_lbool(is_def_eq_binder(t, s, c, jst));
             case expr_kind::Sort:
                 // t and s are Sorts
-                if (is_trivial(sort_level(t), sort_level(s)))
+                if (is_equivalent(sort_level(t), sort_level(s))) {
                     return l_true;
-                c.add_cnstr(mk_level_cnstr(sort_level(t), sort_level(s), jst.get()));
+                } else if (has_meta(sort_level(t)) || has_meta(sort_level(s))) {
-                return l_true;
+                    c.add_cnstr(mk_level_cnstr(sort_level(t), sort_level(s), jst.get()));
+                    return l_true;
+                } else {
+                    return l_false;
+                }
             case expr_kind::Meta:
                 lean_unreachable(); // LCOV_EXCL_LINE
             case expr_kind::Var: case expr_kind::Local: case expr_kind::App:

src/kernel/level.cpp

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
+#include <utility>
 #include <algorithm>
 #include <vector>
 #include "util/safe_arith.h"
@@ -191,17 +192,35 @@ level mk_succ(level const & l) {
     return level(new level_succ(l));
 }
 
+/** \brief Convert (succ^k l) into (l, k). If l is not a succ, then return (l, 0) */
+std::pair<level, unsigned> to_offset(level l) {
+    unsigned k = 0;
+    while (is_succ(l)) {
+        l = succ_of(l);
+        k++;
+    }
+    return mk_pair(l, k);
+}
+
 level mk_max(level const & l1, level const & l2)  {
-    if (is_explicit(l1) && is_explicit(l2))
+    if (is_explicit(l1) && is_explicit(l2)) {
         return get_depth(l1) >= get_depth(l2) ? l1 : l2;
-    else if (l1 == l2)
+    } else if (l1 == l2) {
         return l1;
-    else if (is_zero(l1))
+    } else if (is_zero(l1)) {
         return l2;
-    else if (is_zero(l2))
+    } else if (is_zero(l2)) {
         return l1;
-    else
+    } else {
-        return level(new level_max_core(false, l1, l2));
+        auto p1 = to_offset(l1);
+        auto p2 = to_offset(l2);
+        if (p1.first == p2.first) {
+            lean_assert(p1.second != p2.second);
+            return p1.second > p2.second ? l1 : l2;
+        } else {
+            return level(new level_max_core(false, l1, l2));
+        }
+    }
 }
 
 level mk_imax(level const & l1, level const & l2) {
@@ -289,32 +308,45 @@ bool is_not_zero(level const & l) {
 }
 
 // Monotonic total order on universe level terms.
-bool is_lt(level const & a, level const & b) {
+bool is_lt(level const & a, level const & b, bool use_hash) {
     if (is_eqp(a, b))              return false;
     unsigned da = get_depth(a);
     unsigned db = get_depth(b);
     if (da < db)                   return true;
     if (da > db)                   return false;
     if (kind(a) != kind(b))        return kind(a) < kind(b);
-    if (hash(a) < hash(b))         return true;
+    if (use_hash) {
-    if (hash(a) > hash(b))         return false;
+        if (hash(a) < hash(b))         return true;
+        if (hash(a) > hash(b))         return false;
+    }
     if (a == b)                    return false;
     switch (kind(a)) {
     case level_kind::Zero:
-        return false;
+        lean_unreachable(); // LCOV_EXCL_LINE
     case level_kind::Param: case level_kind::Global: case level_kind::Meta:
         return to_param_core(a).m_id < to_param_core(b).m_id;
     case level_kind::Max: case level_kind::IMax:
         if (to_max_core(a).m_lhs != to_max_core(b).m_lhs)
-            return is_lt(to_max_core(a).m_lhs, to_max_core(b).m_lhs);
+            return is_lt(to_max_core(a).m_lhs, to_max_core(b).m_lhs, use_hash);
         else
-            return is_lt(to_max_core(a).m_rhs, to_max_core(b).m_rhs);
+            return is_lt(to_max_core(a).m_rhs, to_max_core(b).m_rhs, use_hash);
     case level_kind::Succ:
-        return is_lt(succ_of(a), succ_of(b));
+        return is_lt(succ_of(a), succ_of(b), use_hash);
     }
     lean_unreachable(); // LCOV_EXCL_LINE
 }
 
+bool is_lt(levels const & as, levels const & bs, bool use_hash) {
+    if (is_nil(as))
+        return !is_nil(bs);
+    if (is_nil(bs))
+        return false;
+    if (car(as) == car(bs))
+        return is_lt(cdr(as), cdr(bs), use_hash);
+    else
+        return is_lt(car(as), car(bs), use_hash);
+}
+
 class level_serializer : public object_serializer<level, level::ptr_hash, level::ptr_eq> {
     typedef object_serializer<level, level::ptr_hash, level::ptr_eq> super;
 public:
@@ -494,7 +526,7 @@ level instantiate(level const & l, param_names const & ps, levels const & ls) {
 static void print(std::ostream & out, level l);
 
 static void print_child(std::ostream & out, level const & l) {
-    if (is_explicit(l) || is_param(l) || is_meta(l)) {
+    if (is_explicit(l) || is_param(l) || is_meta(l) || is_global(l)) {
         print(out, l);
     } else {
         out << "(";
@@ -512,7 +544,7 @@ static void print(std::ostream & out, level l) {
         case level_kind::Zero:
             lean_unreachable(); // LCOV_EXCL_LINE
         case level_kind::Param: case level_kind::Global:
-            out << param_id(l); break;
+            out << to_param_core(l).m_id; break;
         case level_kind::Meta:
             out << "?" << meta_id(l); break;
         case level_kind::Succ:
@@ -522,15 +554,15 @@ static void print(std::ostream & out, level l) {
                 out << "max ";
             else
                 out << "imax ";
-            print_child(out, max_lhs(l));
+            print_child(out, to_max_core(l).m_lhs);
             // max and imax are right associative
-            while (kind(max_rhs(l)) == kind(l)) {
+            while (kind(to_max_core(l).m_rhs) == kind(l)) {
-                l = max_rhs(l);
+                l = to_max_core(l).m_rhs;
                 out << " ";
-                print_child(out, max_lhs(l));
+                print_child(out, to_max_core(l).m_lhs);
             }
             out << " ";
-            print_child(out, max_rhs(l));
+            print_child(out, to_max_core(l).m_rhs);
             break;
         }
     }
@@ -544,7 +576,7 @@ std::ostream & operator<<(std::ostream & out, level const & l) {
 format pp(level l, bool unicode, unsigned indent);
 
 static format pp_child(level const & l, bool unicode, unsigned indent) {
-    if (is_explicit(l) || is_param(l) || is_meta(l)) {
+    if (is_explicit(l) || is_param(l) || is_meta(l) || is_global(l)) {
         return pp(l, unicode, indent);
     } else {
         return paren(pp(l, unicode, indent));
@@ -560,20 +592,20 @@ format pp(level l, bool unicode, unsigned indent) {
         case level_kind::Zero:
             lean_unreachable(); // LCOV_EXCL_LINE
         case level_kind::Param: case level_kind::Global:
-            return format(param_id(l));
+            return format(to_param_core(l).m_id);
         case level_kind::Meta:
             return format{format("?"), format(meta_id(l))};
         case level_kind::Succ:
             return group(compose(format("succ"), nest(indent, compose(line(), pp_child(succ_of(l), unicode, indent)))));
         case level_kind::Max: case level_kind::IMax: {
             format r = format(is_max(l) ? "max" : "imax");
-            r += nest(indent, compose(line(), pp_child(max_lhs(l), unicode, indent)));
+            r += nest(indent, compose(line(), pp_child(to_max_core(l).m_lhs, unicode, indent)));
             // max and imax are right associative
-            while (kind(max_rhs(l)) == kind(l)) {
+            while (kind(to_max_core(l).m_rhs) == kind(l)) {
-                l = max_rhs(l);
+                l = to_max_core(l).m_rhs;
-                r += nest(indent, compose(line(), pp_child(max_lhs(l), unicode, indent)));
+                r += nest(indent, compose(line(), pp_child(to_max_core(l).m_lhs, unicode, indent)));
             }
-            r += nest(indent, compose(line(), pp_child(max_rhs(l), unicode, indent)));
+            r += nest(indent, compose(line(), pp_child(to_max_core(l).m_rhs, unicode, indent)));
             return group(r);
         }}
         lean_unreachable(); // LCOV_EXCL_LINE
@@ -593,32 +625,120 @@ format pp(level const & lhs, level const & rhs, options const & opts) {
     return pp(lhs, rhs, get_pp_unicode(opts), get_pp_indent(opts));
 }
 
-bool is_trivial(level const & lhs, level const & rhs) {
+// A total order on level expressions that has the following properties
-    check_system("level constraints");
+//  - succ(l) is an immediate successor of l.
-    if (is_zero(lhs) || lhs == rhs) {
+//  - zero is the minimal element.
-        // 0 <= l
+// This total order is used in the normalization procedure.
-        // l <= l
+static bool is_norm_lt(level const & a, level const & b) {
-        return true;
+    if (is_eqp(a, b)) return false;
-    } else if (is_succ(lhs) && is_succ(rhs)) {
+    auto p1 = to_offset(a);
-        // is_trivial(l <= r) implies   is_trivial(succ l <= succ r)
+    auto p2 = to_offset(b);
-        return is_trivial(succ_of(lhs), succ_of(rhs));
+    level const & l1 = p1.first;
-    } else if (is_succ(rhs)) {
+    level const & l2 = p2.first;
-        // is_trivial(l <= r)  implies is_trivial(l <= succ^k r)
+    if (l1 != l2) {
-        lean_assert(!is_succ(lhs));
+        if (kind(l1) != kind(l2)) return kind(l1) < kind(l2);
-        level it = succ_of(rhs);
+        switch (kind(l1)) {
-        while (is_succ(it))
+        case level_kind::Zero: case level_kind::Succ:
-            it = succ_of(it);
+            lean_unreachable(); // LCOV_EXCL_LINE
-        return is_trivial(lhs, it);
+        case level_kind::Param: case level_kind::Global: case level_kind::Meta:
-    } else if (is_max(rhs)) {
+            return to_param_core(l1).m_id < to_param_core(l2).m_id;
-        // is_trivial(l <= l1) implies  is_trivial(l <= max(l1, l2))
+        case level_kind::Max: case level_kind::IMax:
-        // is_trivial(l <= l2) implies  is_trivial(l <= max(l1, l2))
+            if (to_max_core(l1).m_lhs != to_max_core(l2).m_lhs)
-        return is_trivial(lhs, max_lhs(rhs)) || is_trivial(lhs, max_rhs(rhs));
+                return is_norm_lt(to_max_core(l1).m_lhs, to_max_core(l2).m_lhs);
-    } else if (is_imax(rhs)) {
+            else
-        // is_trivial(l <= l2) implies is_trivial(l <= imax(l1, l2))
+                return is_norm_lt(to_max_core(l1).m_rhs, to_max_core(l2).m_rhs);
-        return is_trivial(lhs, imax_rhs(rhs));
+        }
+        lean_unreachable(); // LCOV_EXCL_LINE
     } else {
-        return false;
+        return p1.second < p2.second;
     }
 }
+
+void push_max_args(level const & l, buffer<level> & r) {
+    if (is_max(l)) {
+        push_max_args(max_lhs(l), r);
+        push_max_args(max_rhs(l), r);
+    } else {
+        r.push_back(l);
+    }
+}
+
+level mk_max(buffer<level> const & args) {
+    lean_assert(!args.empty());
+    unsigned nargs = args.size();
+    if (nargs == 1) {
+        return args[0];
+    } else {
+        lean_assert(nargs >= 2);
+        level r = mk_max(args[nargs-2], args[nargs-1]);
+        unsigned i = nargs-2;
+        while (i > 0) {
+            --i;
+            r = mk_max(args[i], r);
+        }
+        return r;
+    }
+}
+
+level mk_succ(level l, unsigned k) {
+    while (k > 0) {
+        --k;
+        l = mk_succ(l);
+    }
+    return l;
+}
+
+level normalize(level const & l) {
+    auto p = to_offset(l);
+    level const & r = p.first;
+    switch (kind(r)) {
+    case level_kind::Succ:
+        lean_unreachable(); // LCOV_EXCL_LINE
+    case level_kind::Zero:   case level_kind::Param:
+    case level_kind::Global: case level_kind::Meta:
+        return l;
+    case level_kind::IMax: {
+        auto l1 = normalize(imax_lhs(r));
+        auto l2 = normalize(imax_rhs(r));
+        if (!is_eqp(l1, imax_lhs(r)) || !is_eqp(l2, imax_rhs(r)))
+            return mk_succ(mk_imax(l1, l2), p.second);
+        else
+            return l;
+    }
+    case level_kind::Max: {
+        buffer<level> todo;
+        buffer<level> args;
+        push_max_args(r, todo);
+        for (level const & a : todo)
+            push_max_args(normalize(a), args);
+        std::sort(args.begin(), args.end(), is_norm_lt);
+        buffer<level> & rargs = todo;
+        rargs.clear();
+        rargs.push_back(args[0]);
+        auto p_prev = to_offset(args[0]);
+        for (unsigned i = 1; i < args.size(); i++) {
+            auto p_curr = to_offset(args[i]);
+            if (p_prev.first == p_curr.first) {
+                if (p_prev.second < p_curr.second) {
+                    p_prev = p_curr;
+                    rargs.pop_back();
+                    rargs.push_back(args[i]);
+                }
+            } else {
+                p_prev = p_curr;
+                rargs.push_back(args[i]);
+            }
+        }
+        for (level & a : rargs)
+            a = mk_succ(a, p.second);
+        return mk_max(rargs);
+    }}
+    lean_unreachable(); // LCOV_EXCL_LINE
+}
+
+bool is_equivalent(level const & lhs, level const & rhs) {
+    check_system("level constraints");
+    return lhs == rhs || normalize(lhs) == normalize(rhs);
+}
 }
 void print(lean::level const & l) { std::cout << l << std::endl; }

src/kernel/level.h

@@ -86,9 +86,6 @@ level mk_param_univ(name const & n);
 level mk_global_univ(name const & n);
 level mk_meta_univ(name const & n);
 
-/** \brief An arbitrary (monotonic) total order on universe level terms. */
-bool is_lt(level const & l1, level const & l2);
-
 inline unsigned hash(level const & l) { return l.hash(); }
 inline level_kind kind(level const & l) { return l.kind(); }
 inline bool is_zero(level const & l)   { return kind(l) == level_kind::Zero; }
@@ -140,13 +137,12 @@ level update_succ(level const & l, level const & new_arg);
 level update_max(level const & l, level const & new_lhs, level const & new_rhs);
 
 /**
-   \brief Return true if lhs <= rhs is a trivial constraint.
+   \brief Return true if lhs and rhs denote the same level.
-   That is, it is a constraint that is always valid, and can be discarded.
+   The check is done by normalization.
-   This is not a complete procedure. It only "catches" the easy cases.
-
-   \remark The type checker produces many trivial constraints.
 */
-bool is_trivial(level const & lhs, level const & rhs);
+bool is_equivalent(level const & lhs, level const & rhs);
+/** \brief Return the given level expression normal form */
+level normalize(level const & l);
 
 typedef list<level> levels;
 
@@ -154,6 +150,10 @@ bool has_meta(levels const & ls);
 bool has_global(levels const & ls);
 bool has_param(levels const & ls);
 
+/** \brief An arbitrary (monotonic) total order on universe level terms. */
+bool is_lt(level const & l1, level const & l2, bool use_hash);
+bool is_lt(levels const & as, levels const & bs, bool use_hash);
+
 /** \brief Functional for applying <tt>F</tt> to each level expressions. */
 class for_each_level_fn {
     std::function<bool(level const &)>  m_f; // NOLINT

src/kernel/type_checker.cpp

@@ -452,25 +452,19 @@ static void check_name(environment const & env, name const & n) {
         throw_already_declared(env, n);
 }
 
-struct simple_constraint_handler : public constraint_handler {
-    std::vector<constraint> m_cnstrs;
-    virtual void add_cnstr(constraint const & c) { m_cnstrs.push_back(c); }
-};
-
 certified_definition check(environment const & env, definition const & d, name_generator const & g, name_set const & extra_opaque, bool memoize) {
     check_no_mlocal(env, d.get_type());
     if (d.is_definition())
         check_no_mlocal(env, d.get_value());
     check_name(env, d.get_name());
 
-    simple_constraint_handler chandler;
+    type_checker checker1(env, g, mk_default_converter(env, optional<module_idx>(), memoize, extra_opaque));
-    type_checker checker1(env, g, chandler, mk_default_converter(env, optional<module_idx>(), memoize, extra_opaque));
     checker1.check(d.get_type());
     if (d.is_definition()) {
         optional<module_idx> midx;
         if (d.is_opaque())
             midx = optional<module_idx>(d.get_module_idx());
-        type_checker checker2(env, g, chandler, mk_default_converter(env, midx, memoize, extra_opaque));
+        type_checker checker2(env, g, mk_default_converter(env, midx, memoize, extra_opaque));
         expr val_type = checker2.check(d.get_value());
         if (!checker2.is_def_eq(val_type, d.get_type())) {
             throw_kernel_exception(env, d.get_value(),
@@ -479,17 +473,6 @@ certified_definition check(environment const & env, definition const & d, name_g
                                    });
         }
     }
-
-    // TODO(Leo): solve universe level constraints
-    #if 1
-    // temporary code
-    for (auto c : chandler.m_cnstrs) {
-        std::cout << c << "\n";
-    }
-    if (!chandler.m_cnstrs.empty())
-        throw_kernel_exception(env, "invalid declaration, unsatisfied level constraints");
-    #endif
-
     return certified_definition(env.get_id(), d);
 }
 

src/library/expr_lt.cpp

@@ -8,45 +8,6 @@ Author: Leonardo de Moura
 #include "library/expr_lt.h"
 
 namespace lean {
-bool is_lt(level const & a, level const & b, bool use_hash) {
-    if (is_eqp(a, b))            return false;
-    if (kind(a) != kind(b))      return kind(a) < kind(b);
-    if (use_hash) {
-        if (hash(a) < hash(b))   return true;
-        if (hash(a) > hash(b))   return false;
-    }
-    if (a == b)                  return false;
-    switch (kind(a)) {
-    case level_kind::Zero:       return true;
-    case level_kind::Succ:       return is_lt(succ_of(a), succ_of(b), use_hash);
-    case level_kind::Param:      return param_id(a) < param_id(b);
-    case level_kind::Global:     return global_id(a) < global_id(b);
-    case level_kind::Meta:       return meta_id(a) < meta_id(b);
-    case level_kind::Max:
-        if (max_lhs(a) != max_lhs(b))
-            return is_lt(max_lhs(a), max_lhs(b), use_hash);
-        else
-            return is_lt(max_lhs(a), max_lhs(b), use_hash);
-    case level_kind::IMax:
-        if (imax_lhs(a) != imax_lhs(b))
-            return is_lt(imax_lhs(a), imax_lhs(b), use_hash);
-        else
-            return is_lt(imax_lhs(a), imax_lhs(b), use_hash);
-    }
-    lean_unreachable(); // LCOV_EXCL_LINE
-}
-
-bool is_lt(levels const & as, levels const & bs, bool use_hash) {
-    if (is_nil(as))
-        return !is_nil(bs);
-    if (is_nil(bs))
-        return false;
-    if (car(as) == car(bs))
-        return is_lt(cdr(as), cdr(bs), use_hash);
-    else
-        return is_lt(car(as), car(bs), use_hash);
-}
-
 bool is_lt(expr const & a, expr const & b, bool use_hash) {
     if (is_eqp(a, b))                    return false;
     unsigned da = get_depth(a);

src/library/expr_lt.h

@@ -19,7 +19,4 @@ inline bool operator<(expr const & a, expr const & b)  { return is_lt(a, b, true
 inline bool operator>(expr const & a, expr const & b)  { return is_lt(b, a, true); }
 inline bool operator<=(expr const & a, expr const & b) { return !is_lt(b, a, true); }
 inline bool operator>=(expr const & a, expr const & b) { return !is_lt(a, b, true); }
-
-bool is_lt(level const & a, level const & b, bool use_hash);
-bool is_lt(levels const & as, levels const & bs, bool use_hash);
 }

src/library/kernel_bindings.cpp

@@ -46,7 +46,10 @@ static int level_tostring(lua_State * L) {
 }
 
 static int level_eq(lua_State * L) { return push_boolean(L, to_level(L, 1) == to_level(L, 2)); }
-static int level_lt(lua_State * L) { return push_boolean(L, is_lt(to_level(L, 1), to_level(L, 2))); }
+static int level_lt(lua_State * L) {
+    int nargs = lua_gettop(L);
+    return push_boolean(L, is_lt(to_level(L, 1), to_level(L, 2), nargs == 3 && lua_toboolean(L, 3)));
+}
 static int mk_level_zero(lua_State * L)  { return push_level(L, mk_level_zero()); }
 static int mk_level_one(lua_State * L)   { return push_level(L, mk_level_one());  }
 static int mk_level_succ(lua_State * L)  { return push_level(L, mk_succ(to_level(L, 1))); }
@@ -67,8 +70,9 @@ LEVEL_PRED(is_explicit)
 LEVEL_PRED(has_meta)
 LEVEL_PRED(has_param)
 LEVEL_PRED(is_not_zero)
+static int level_normalize(lua_State * L)  { return push_level(L, normalize(to_level(L, 1))); }
 static int level_get_kind(lua_State * L) { return push_integer(L, static_cast<int>(kind(to_level(L, 1)))); }
-static int level_trivially_leq(lua_State * L) { return push_boolean(L, is_trivial(to_level(L, 1), to_level(L, 2))); }
+static int level_is_equivalent(lua_State * L) { return push_boolean(L, is_equivalent(to_level(L, 1), to_level(L, 2))); }
 static int level_is_eqp(lua_State * L) { return push_boolean(L, is_eqp(to_level(L, 1), to_level(L, 2))); }
 
 static int level_id(lua_State * L) {
@@ -125,13 +129,16 @@ static const struct luaL_Reg level_m[] = {
     {"has_meta",        safe_function<level_has_meta>},
     {"has_param",       safe_function<level_has_param>},
     {"is_not_zero",     safe_function<level_is_not_zero>},
-    {"trivially_leq",   safe_function<level_trivially_leq>},
+    {"is_equivalent",   safe_function<level_is_equivalent>},
     {"is_eqp",          safe_function<level_is_eqp>},
+    {"is_lt",           safe_function<level_lt>},
     {"id",              safe_function<level_id>},
     {"lhs",             safe_function<level_lhs>},
     {"rhs",             safe_function<level_rhs>},
     {"succ_of",         safe_function<level_succ_of>},
     {"instantiate",     safe_function<level_instantiate>},
+    {"normalize",       safe_function<level_normalize>},
+    {"norm",            safe_function<level_normalize>},
     {0, 0}
 };
 

src/tests/kernel/level.cpp

@@ -50,28 +50,14 @@ static void tst2() {
     level p1 = mk_param_univ("p1");
     level p2 = mk_param_univ("p2");
     level m1 = mk_meta_univ("m1");
-    lean_assert(is_trivial(zero, mk_succ(mk_max(p1, p2))));
+    lean_assert(is_equivalent(mk_succ(p2), mk_max(p2, mk_succ(p2))));
-    lean_assert(is_trivial(mk_succ(mk_max(p1, p2)), mk_succ(mk_max(p1, p2))));
+    lean_assert(is_equivalent(mk_max(p1, p2), mk_max(p2, p1)));
-    lean_assert(is_trivial(p1, mk_succ(mk_max(p1, p2))));
+    lean_assert(!is_equivalent(mk_imax(p1, p2), mk_imax(p2, p1)));
-    lean_assert(!is_trivial(p1, mk_succ(mk_imax(p1, p2))));
+    lean_assert(is_equivalent(mk_imax(mk_succ(p1), mk_succ(p2)), mk_imax(mk_succ(p2), mk_succ(p1))));
-    lean_assert(is_trivial(p2, mk_succ(mk_max(p1, p2))));
+    lean_assert(is_equivalent(mk_succ(mk_max(m1, p1)), mk_max(mk_succ(p1), mk_succ(m1))));
-    lean_assert(is_trivial(mk_succ(p2), mk_succ(mk_max(p1, p2))));
+    lean_assert(is_equivalent(one, mk_succ(zero)));
-    lean_assert(is_trivial(p2, mk_succ(mk_imax(p1, p2))));
+    lean_assert(!is_equivalent(zero, two));
-    lean_assert(is_trivial(mk_succ(p2), mk_succ(mk_imax(p1, p2))));
+    lean_assert(!is_equivalent(zero, p2));
-    lean_assert(!is_trivial(mk_succ(mk_succ(p2)), mk_succ(mk_max(p1, p2))));
-    lean_assert(!is_trivial(mk_succ(mk_max(p1, p2)), zero));
-    lean_assert(is_trivial(mk_succ(mk_succ(p1)), mk_succ(mk_succ(mk_succ(p1)))));
-    lean_assert(!is_trivial(mk_succ(mk_succ(p1)), mk_succ(mk_succ(mk_succ(p2)))));
-    lean_assert(!is_trivial(mk_succ(mk_succ(mk_succ(p1))), mk_succ(mk_succ(p1))));
-    lean_assert(is_trivial(p1, mk_max(m1, mk_max(p1, p2))));
-    lean_assert(!is_trivial(p1, mk_imax(m1, mk_imax(p1, p2))));
-    lean_assert(is_trivial(p2, mk_imax(m1, mk_imax(p1, p2))));
-    lean_assert(is_trivial(zero, one));
-    lean_assert(is_trivial(one, two));
-    lean_assert(!is_trivial(one, zero));
-    lean_assert(!is_trivial(two, one));
-    lean_assert(!is_trivial(m1, p1));
-    lean_assert(!is_trivial(p1, m1));
 }
 
 int main() {

tests/lua/level1.lua

@@ -19,9 +19,8 @@ assert(mk_level_imax(mk_param_univ("a"), mk_param_univ("b")):lhs() == mk_param_u
 assert(mk_level_imax(mk_param_univ("a"), mk_param_univ("b")):rhs() == mk_param_univ("b"))
 assert(mk_param_univ("a"):id() == name("a"))
 assert(mk_meta_univ("b"):id() == name("b"))
-assert(level():trivially_leq(mk_level_one()))
+assert(mk_level_succ(mk_level_zero()):is_equivalent(mk_level_one()))
-assert(level():trivially_leq(mk_param_univ("a")))
+assert(not mk_param_univ("b"):is_equivalent(mk_param_univ("a")))
-assert(not mk_param_univ("b"):trivially_leq(mk_param_univ("a")))
 assert(mk_level_one():kind() == level_kind.Succ)
 assert(not mk_level_one():has_meta())
 assert(not mk_level_succ(mk_param_univ("a")):has_meta())

tests/lua/level4.lua

@@ -0,0 +1,10 @@
+assert(not (mk_level_zero() < mk_level_zero()))
+local u = mk_global_univ("u")
+local v = mk_global_univ("v")
+local z   = mk_level_zero()
+local max = mk_level_max
+local imax = mk_level_imax
+local succ = mk_level_succ
+assert(max(succ(max(succ(v), u)), max(v, succ(succ(u)))):norm() == max(succ(succ(u)), succ(succ(v))))
+assert(imax(succ(succ(max(u, u))), v):norm() == imax(succ(succ(u)), v))
+assert(max(u, max(succ(succ(z)), max(u, succ(z)))):norm() == max(succ(succ(z)), u))