refactor(kernel): remove unnecessary universe

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

src/builtin/kernel.lean

@@ -1,21 +1,14 @@
 import macros
 
-universe U   ≥ 1
-universe U' >= U + 1
+universe U ≥ 1
+definition TypeU  := (Type U)
 
 variable Bool : Type
 -- The following builtin declarations can be removed as soon as Lean supports inductive datatypes and match expressions
 builtin true : Bool
 builtin false : Bool
 
-definition TypeU  := (Type U)
-definition TypeU' := (Type U')
-
-builtin eq {A : (Type U')} (a b : A) : Bool
-infix 50 = : eq
-
 definition not (a : Bool) := a → false
-
 notation 40 ¬ _ : not
 
 definition or (a b : Bool) := ¬ a → b
@@ -28,11 +21,14 @@ infixr 35 && : and
 infixr 35 /\ : and
 infixr 35 ∧  : and
 
+definition implies (a b : Bool) := a → b
+
+builtin eq {A : (Type U)} (a b : A) : Bool
+infix 50 = : eq
+
 definition neq {A : TypeU} (a b : A) := ¬ (a = b)
 infix 50 ≠ : neq
 
-definition implies (a b : Bool) := a → b
-
 definition iff (a b : Bool) := a = b
 infixr 25 <-> : iff
 infixr 25 ↔   : iff
@@ -52,25 +48,25 @@ theorem em (a : Bool) : a ∨ ¬ a
 
 axiom case (P : Bool → Bool) (H1 : P true) (H2 : P false) (a : Bool) : P a
 
-axiom refl {A : TypeU'} (a : A) : a = a
+axiom refl {A : TypeU} (a : A) : a = a
 
-axiom subst {A : TypeU'} {a b : A} {P : A → Bool} (H1 : P a) (H2 : a = b) : P b
+axiom subst {A : TypeU} {a b : A} {P : A → Bool} (H1 : P a) (H2 : a = b) : P b
 
 -- Function extensionality
-axiom funext {A : TypeU'} {B : A → TypeU'} {f g : ∀ x : A, B x} (H : ∀ x : A, f x = g x) : f = g
+axiom funext {A : TypeU} {B : A → TypeU} {f g : ∀ x : A, B x} (H : ∀ x : A, f x = g x) : f = g
 
 -- Forall extensionality
 axiom allext {A : TypeU} {B C : A → Bool} (H : ∀ x : A, B x = C x) : (∀ x : A, B x) = (∀ x : A, C x)
 
 -- Alias for subst where we can provide P explicitly, but keep A,a,b implicit
-theorem substp {A : TypeU'} {a b : A} (P : A → Bool) (H1 : P a) (H2 : a = b) : P b
+theorem substp {A : TypeU} {a b : A} (P : A → Bool) (H1 : P a) (H2 : a = b) : P b
 := subst H1 H2
 
 -- We will mark not as opaque later
 theorem not_intro {a : Bool} (H : a → false) : ¬ a
 := H
 
-theorem eta {A : TypeU'} {B : A → TypeU} (f : ∀ x : A, B x) : (λ x : A, f x) = f
+theorem eta {A : TypeU} {B : A → TypeU} (f : ∀ x : A, B x) : (λ x : A, f x) = f
 := funext (λ x : A, refl (f x))
 
 theorem trivial : true
@@ -154,10 +150,10 @@ theorem or_elim {a b c : Bool} (H1 : a ∨ b) (H2 : a → c) (H3 : b → c) : c
 theorem refute {a : Bool} (H : ¬ a → false) : a
 := or_elim (em a) (λ H1 : a, H1) (λ H1 : ¬ a, false_elim a (H H1))
 
-theorem symm {A : TypeU'} {a b : A} (H : a = b) : b = a
+theorem symm {A : TypeU} {a b : A} (H : a = b) : b = a
 := subst (refl a) H
 
-theorem trans {A : TypeU'} {a b c : A} (H1 : a = b) (H2 : b = c) : a = c
+theorem trans {A : TypeU} {a b c : A} (H1 : a = b) (H2 : b = c) : a = c
 := subst H1 H2
 
 infixl 100 ⋈ : trans
@@ -177,13 +173,13 @@ theorem eqt_elim {a : Bool} (H : a = true) : a
 theorem eqf_elim {a : Bool} (H : a = false) : ¬ a
 := not_intro (λ Ha : a, H ◂ Ha)
 
-theorem congr1 {A : TypeU'} {B : A → TypeU'} {f g : ∀ x : A, B x} (a : A) (H : f = g) : f a = g a
+theorem congr1 {A : TypeU} {B : A → TypeU} {f g : ∀ x : A, B x} (a : A) (H : f = g) : f a = g a
 := substp (fun h : (∀ x : A, B x), f a = h a) (refl (f a)) H
 
-theorem congr2 {A B : TypeU'} {a b : A} (f : A → B) (H : a = b) : f a = f b
+theorem congr2 {A B : TypeU} {a b : A} (f : A → B) (H : a = b) : f a = f b
 := substp (fun x : A, f a = f x) (refl (f a)) H
 
-theorem congr {A B : TypeU'} {f g : A → B} {a b : A} (H1 : f = g) (H2 : a = b) : f a = g b
+theorem congr {A B : TypeU} {f g : A → B} {a b : A} (H1 : f = g) (H2 : a = b) : f a = g b
 := subst (congr2 f H2) (congr1 b H1)
 
 -- Recall that exists is defined as ¬ ∀ x : A, ¬ P x

src/kernel/kernel.cpp

@@ -16,8 +16,6 @@ namespace lean {
 // Bultin universe variables m and u
 static level u_lvl(name("U"));
 expr const TypeU = Type(u_lvl);
-static level up_lvl(name("U'"));
-expr const TypeUp = Type(up_lvl);
 // =======================================
 
 // =======================================
@@ -92,8 +90,8 @@ class eq_fn_value : public value {
     expr m_type;
     static expr mk_type() {
         expr A    = Const("A");
-        // Pi (A: TypeUp), A -> A -> Bool
-        return Pi({A, TypeUp}, (A >> (A >> Bool)));
+        // Pi (A: TypeU), A -> A -> Bool
+        return Pi({A, TypeU}, (A >> (A >> Bool)));
     }
 public:
     eq_fn_value():m_type(mk_type()) {}

src/kernel/kernel.h

@@ -11,7 +11,6 @@ Author: Leonardo de Moura
 namespace lean {
 // See src/builtin/kernel.lean for signatures.
 extern expr const TypeU;
-extern expr const TypeUp;
 
 /** \brief Return the Lean Boolean type. */
 expr mk_bool_type();

src/kernel/kernel_decls.cpp

@@ -6,14 +6,13 @@ Released under Apache 2.0 license as described in the file LICENSE.
 #include "kernel/environment.h"
 #include "kernel/decl_macros.h"
 namespace lean {
-MK_CONSTANT(Bool, name("Bool"));
 MK_CONSTANT(TypeU, name("TypeU"));
-MK_CONSTANT(TypeU_, name("TypeU_"));
+MK_CONSTANT(Bool, name("Bool"));
 MK_CONSTANT(not_fn, name("not"));
 MK_CONSTANT(or_fn, name("or"));
 MK_CONSTANT(and_fn, name("and"));
-MK_CONSTANT(neq_fn, name("neq"));
 MK_CONSTANT(implies_fn, name("implies"));
+MK_CONSTANT(neq_fn, name("neq"));
 MK_CONSTANT(iff_fn, name("iff"));
 MK_CONSTANT(exists_fn, name("exists"));
 MK_CONSTANT(em_fn, name("em"));

src/kernel/kernel_decls.h

@@ -5,12 +5,10 @@ Released under Apache 2.0 license as described in the file LICENSE.
 // Automatically generated file, DO NOT EDIT
 #include "kernel/expr.h"
 namespace lean {
-expr mk_Bool();
-bool is_Bool(expr const & e);
 expr mk_TypeU();
 bool is_TypeU(expr const & e);
-expr mk_TypeU_();
-bool is_TypeU_(expr const & e);
+expr mk_Bool();
+bool is_Bool(expr const & e);
 expr mk_not_fn();
 bool is_not_fn(expr const & e);
 inline bool is_not(expr const & e) { return is_app(e) && is_not_fn(arg(e, 0)); }
@@ -23,14 +21,14 @@ expr mk_and_fn();
 bool is_and_fn(expr const & e);
 inline bool is_and(expr const & e) { return is_app(e) && is_and_fn(arg(e, 0)); }
 inline expr mk_and(expr const & e1, expr const & e2) { return mk_app({mk_and_fn(), e1, e2}); }
-expr mk_neq_fn();
-bool is_neq_fn(expr const & e);
-inline bool is_neq(expr const & e) { return is_app(e) && is_neq_fn(arg(e, 0)); }
-inline expr mk_neq(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_neq_fn(), e1, e2, e3}); }
 expr mk_implies_fn();
 bool is_implies_fn(expr const & e);
 inline bool is_implies(expr const & e) { return is_app(e) && is_implies_fn(arg(e, 0)); }
 inline expr mk_implies(expr const & e1, expr const & e2) { return mk_app({mk_implies_fn(), e1, e2}); }
+expr mk_neq_fn();
+bool is_neq_fn(expr const & e);
+inline bool is_neq(expr const & e) { return is_app(e) && is_neq_fn(arg(e, 0)); }
+inline expr mk_neq(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_neq_fn(), e1, e2, e3}); }
 expr mk_iff_fn();
 bool is_iff_fn(expr const & e);
 inline bool is_iff(expr const & e) { return is_app(e) && is_iff_fn(arg(e, 0)); }

src/kernel/type_checker.cpp

@@ -48,7 +48,7 @@ class type_checker::imp {
             return u;
         if (has_metavar(u) && m_menv && m_uc) {
             justification jst = mk_type_expected_justification(ctx, s);
-            m_uc->push_back(mk_convertible_constraint(ctx, e, TypeUp, jst));
+            m_uc->push_back(mk_convertible_constraint(ctx, e, TypeU, jst));
             return u;
         }
         u = normalize(e, ctx, true);

src/library/elaborator/elaborator.cpp

@@ -1136,12 +1136,12 @@ class elaborator::imp {
             // We approximate and only consider the most useful ones.
             justification new_jst(new destruct_justification(c));
             if (is_bool(a)) {
-                expr choices[4] = { Bool, Type(), TypeU, TypeUp };
-                push_active(mk_choice_constraint(get_context(c), b, 4, choices, new_jst));
+                expr choices[3] = { Bool, Type(), TypeU };
+                push_active(mk_choice_constraint(get_context(c), b, 3, choices, new_jst));
                 return true;
             } else if (m_env->is_ge(ty_level(a), m_U)) {
-                expr choices[3] = { a, Type(ty_level(a) + 1), TypeUp };
-                push_active(mk_choice_constraint(get_context(c), b, 3, choices, new_jst));
+                expr choices[2] = { a, Type(ty_level(a) + 1) };
+                push_active(mk_choice_constraint(get_context(c), b, 2, choices, new_jst));
                 return true;
             } else {
                 expr choices[4] = { a, Type(ty_level(a) + 1), TypeU };
@@ -1210,10 +1210,6 @@ class elaborator::imp {
                 expr choices[4] = { TypeU, Type(level() + 1), Type(), Bool };
                 push_active(mk_choice_constraint(get_context(c), a, 4, choices, new_jst));
                 return true;
-            } else if (b == TypeUp) {
-                expr choices[5] = { TypeUp, TypeU, Type(level() + 1), Type(), Bool };
-                push_active(mk_choice_constraint(get_context(c), a, 5, choices, new_jst));
-                return true;
             } else {
                 level const & lvl = ty_level(b);
                 lean_assert(!lvl.is_bottom());