How are universe levels defined

Stream: new members

[Xiang Li]

Universe levels are indexed by natural numbers. Does it imply that a structure of "natural numbers" is defined in advance without use of Types? How are these numbers defined?

[Mario Carneiro]

The arithmetic of levels is a simple axiomatic system, weaker than peano, where you can prove things by case analysis on natural numbers. The language is quite impoverished, containing only 0, succ, max, imax and variables, but the axiomatic system is complete for that language.

[Mario Carneiro]

the rules are described in section 2.2 of https://github.com/digama0/lean-type-theory/releases/tag/v1.0

[Mario Carneiro]

Technically lean doesn't actually implement this entire axiomatic system, so there are some level inequalities that it cannot verify, but can be verified by external typecheckers like trepplein that implement the full decision procedure

[Mario Carneiro]

universes u v w
-- fails even though it is true for all u,v,w
#check Sort.{imax (max u v) w} = Sort.{imax u (imax v w)}

[Xiang Li]

Thank you very much! I will study that thesis. :+1:

[Xiang Li]

Mario Carneiro said:

The arithmetic of levels is a simple axiomatic system, weaker than peano, where you can prove things by case analysis on natural numbers. The language is quite impoverished, containing only 0, succ, max, imax and variables, but the axiomatic system is complete for that language.

screenshot-2020-08-23-17.12.30.png
I'm wondering if I understand correctly: α and β here are expression variables. I can replace Γ by Γ, e : α in a judgement only if I have derived e : α from a judgement. And the judgements of ⊢ Γ ok provides an easy way to form Γ, a well-formed sequence of type assignments but this is not necessary in our axiom.

[Mario Carneiro]

@Xiang Li

I'm wondering if I understand correctly: α and β here are expression variables.

Yes. (I use α and β to denote expressions that represent types, but this is no additional syntactic restriction.)

The expression e : α always makes sense even if α is not a Type -- it appears in the judgements.

e : α itself isn't an expression, it is a fragment of the judgment Γ ⊢ e : α, which is well formed but false if α is not a type.

judgements of ⊢ Γ ok provide an easy way to form a well-formed sequence of type assignments, but this is not necessary in the axiom.
Also, I cannot figure out the way to prove "If Γ ⊢ e : α, then ⊢ Γ ok", what does that mean by by induction on the judgments?

Right, ⊢ Γ ok is not needed in the definition of Γ ⊢ e : α, but due to the setup of the rules the latter implies the former.

The proof of this is by induction on the typing judgment Γ ⊢ e : α. Most rules keep Γ the same so you have the inductive hypothesis already; the universe typing rule has no context so it is ok; and rules that extend the context like the typing rule for lambda and pi have a side condition Γ ⊢ α : U_l that is the requirement to show that the extended context is still ok.

[Mario Carneiro]

Oh, actually I've got it backward. Since we are proving by induction on the typing judgment the interesting rules are the ones that extend the context reading top down; there are only two such rules, the weakening rule and the hypothesis rule, and in both cases the final context Γ, x : α is ok because we have an explicit hypothesis Γ ⊢ α : U_l in the rule and Γ ok from the induction hypothesis.

[Xiang Li]

@Mario Carneiro
Thank you very much for your detailed explanation :smile: :smile:
I think there is a problem with typing rule for lambda, because the only induction hypothesis is ⊢ Γ, x : α ok but the goal is ⊢ Γ ok.

[Mario Carneiro]

induction hypothesis is ⊢ Γ, x : α ok but the goal is ⊢ Γ ok.

You can use inversion on that hypothesis to prove ⊢ Γ ok

[Mario Carneiro]

that is, cases in lean

[Mario Carneiro]

To prove e : α ⊢ e : α, you need to use the hypothesis rule, which requires ⊢ α : U_l

[Mario Carneiro]

My comprehension is that Γ, x : e can only be formed if Γ ⊢ x : e is deduced, so Γ cannot be e : α, is that right?

No, there are no syntactic restrictions on the formation of contexts, but Γ ⊢ x : α implies that all parts of it are well formed (Γ is ok, and α is a type in context Γ)

[Mario Carneiro]

In practice we want to restrict attention to only the well formed contexts, types and expressions

[Xiang Li]

that is, cases in lean

cases tactic sometimes does many things at once that needs to be longly proved using rec_on, cases_on and dcases_on. Is there a specific example using inversion in lean?

[Mario Carneiro]

It is an application of cases_on

[Xiang Li]

Thank you! I'm much clear now.

[Mario Carneiro]

Here's a fragment of the definition sufficient to show how the proof goes:

def lev : Type := sorry
inductive exp : Type
| sort : lev → exp
| var : ℕ → exp
| lam : exp → exp → exp
| pi : exp → exp → exp

def lft : exp → exp := sorry
def context := list exp

inductive has_type : context → exp → exp → Prop
| var {Γ α l} : has_type Γ α (exp.sort l) → has_type (α :: Γ) (exp.var 0) (lft α)
| lam {Γ e α β} : has_type (α :: Γ) e β → has_type Γ (exp.lam α e) (exp.pi α β)

inductive is_type (Γ : context) : exp → Prop
| mk {Γ α l} : has_type Γ α (exp.sort l) → is_type α

inductive context.ok : context → Prop
| nil : context.ok []
| cons {Γ α} : context.ok Γ → is_type Γ α → context.ok (α :: Γ)

example {Γ e α} (h : has_type Γ e α) : context.ok Γ :=
begin
  induction h,
  { constructor,
    { assumption },
    { constructor, assumption } },
  { cases h_ih,
    assumption },
end

[Mario Carneiro]

the real thing is of course more complicated, in particular because has_type is mutually recursive with defeq

[Xiang Li]

Ok! I'm considering to formalise "The Type Theory of Lean" in lean. Thank you again!

[Mario Carneiro]

I would like that very much :)

[Marc Huisinga]

when reading mario's msc thesis i found the recursor to be the hardest definition to parse. the natural language description in the lean reference manual helps: https://leanprover.github.io/reference/declarations.html#inductive-families
some things are also implicitly defined in an equation, e.g. p[b] and pi_i[b, x] in 2.6.3 (this took me a while to understand :sweat_smile: ).
i'd also love to see a formalization of it.

[Reid Barton]

By the way, there's a stream #Type theory which would be a good place to discuss such a formalization.

[Mario Carneiro]

@Marc Huisinga The definition of the recursor in my thesis is based very closely on Dybjer's Inductive families, which uses a lot of :: in order to deal with the many "telescopes" that appear in the definition, which might be a little easier to read. I rewrote it as a series of inductive rules specifically to ease formalization efforts like an encoding in lean, or an encoding in MM0.

[Marc Huisinga]

once i understood all the nuances of your notation it was honestly pretty good to read and straight to the point.

[Xiang Li]

@Mario Carneiro Did you default alpha equivalent in the thesis? I didn't see it in defeq.
When you write

$$\dfrac {Γ , x : α ⊢ e : β} {Γ⊢λx:α.e:∀x:α.β}$$

do you mean the x's are the same symbol (sorry this question is not important).
Since I need to define β[e/x], I have to include the bounded variable in the definitions of lam and pi:

inductive exp : Type
| sort : lev → exp
| var : ℕ → exp
| app : exp → exp → exp
| lam : ℕ → exp → exp → exp
| pi : ℕ → exp → exp → exp

open exp
def subst : exp → ℕ → exp → exp
| (sort l) x e := sort l
| (var x) y e := if x = y then e else (var x)
| (app e1 e2) x e := app (subst e1 x e) (subst e2 x e)
| (lam x e1 e2) y e := if x = y then lam x e1 e2 else lam x (subst e1 y e) (subst e2 y e)
| (pi x e1 e2) y e := if x = y then pi x e1 e2 else pi x (subst e1 y e) (subst e2 y e)

[Mario Carneiro]

Formally, the terms are all in de bruijn representation, so alpha equality is just actual equality

[Mario Carneiro]

the sketch I gave above indicates some of this

[Mario Carneiro]

the lft function in the sketch is the lift operator, which increases the indexes of all variables that are not bound by 1

[Mario Carneiro]

Here's a basic implementation of lift and subst for de bruijn terms:

def lev : Type := sorry
inductive exp : Type
| sort : lev → exp
| var : ℕ → exp
| app : exp → exp → exp
| lam : exp → exp → exp
| pi : exp → exp → exp

def exp.liftn : ℕ → exp → exp
| _ e@(exp.sort _) := e
| n e@(exp.var m) := if m < n then e else exp.var (m + 1)
| n (exp.app e₁ e₂) := exp.lam (exp.liftn n e₁) (exp.liftn n e₂)
| n (exp.lam A e) := exp.lam (exp.liftn n A) (exp.liftn (n+1) A)
| n (exp.pi A e) := exp.pi (exp.liftn n A) (exp.liftn (n+1) A)

def exp.lift : exp → exp := exp.liftn 0

def exp.substn (a : exp) : ℕ → exp → exp
| _ e@(exp.sort _) := e
| n e@(exp.var m) := if m < n then e else if m = n then exp.lift^[n] a else exp.var (m - 1)
| n (exp.app e₁ e₂) := exp.lam (exp.substn n e₁) (exp.substn n e₂)
| n (exp.lam A e) := exp.lam (exp.substn n A) (exp.substn (n+1) A)
| n (exp.pi A e) := exp.pi (exp.substn n A) (exp.substn (n+1) A)

-- e[a / #0]
def exp.subst (e a : exp) : exp := exp.substn a 0 e

[Xiang Li]

Thank you! That helps me a lot. I studied de bruijn representation just now.

[Xiang Li]

@Mario Carneiro I am defining the admissible definition of constants in 2.5.

For a constant definition constant $c_{\bar u} : \alpha$ to be admissible, we require that $⊢ α : U_l$, where the
universe variables in $α$ and $l$ are contained in $\bar u$ ̄.

inductive lev : Type
| univ_var : ℕ → lev
| zero : lev
| S : lev → lev
| max : lev → lev → lev
| imax : lev → lev → lev

def univ_vars := {u // ∃ n, u = lev.univ_var n}

inductive exp : Type
| sort : lev → exp
| var : ℕ → exp
| app : exp → exp → exp
| lam : exp → exp → exp
| pi : exp → exp → exp
| Let : exp → exp → exp → exp
| c : ℕ → list univ_vars → exp

def consts := {C // ∃ n l, C = exp.c n l}

The only way of taking the list $\bar u$ from $c_{\bar u}$ I can think of is to use classical.some. Is there any way to avoid it?

[Mario Carneiro]

the way it is implemented in lean is more like the regular variables. You have a context of variables that are legal and then the term typechecks in that context

[Mario Carneiro]

Since all universe variables have the same "type" you really only need to keep track of their number

[Mario Carneiro]

That is, you can define a function lvl.ubound : lvl -> nat, exp.ubound : exp -> nat which calculates the smallest n such that every universe variable in the level or expression is less than n

[Mario Carneiro]

and then the admissibility criterion says A.ubound <= k where k is the number of universe variables in the constant declaration

[Mario Carneiro]

I assume the nat in exp.c is the "name" of the constant? I think you want it to have type | c : nat -> list lvl -> exp, where the list represents the substitutions to universe variables in the constant definition

[Mario Carneiro]

You might also want to consider giving it the type c : nat -> list lvl -> exp -> exp where the final exp is the type of the constant; this is not strictly speaking correct, but allows you to define typechecking without a global environment

[Xiang Li]

Thank you :smile: . I will try it.

[Xiang Li]

@Mario Carneiro
This is part of the code I have written -- maybe my understanding is not right :

inductive lev : Type
| univ_var : ℕ → lev
| zero : lev
| S : lev → lev
| max : lev → lev → lev
| imax : lev → lev → lev

inductive exp : Type
| sort : lev → exp
| var : ℕ → exp
| app : exp → exp → exp
| lam : exp → exp → exp
| pi : exp → exp → exp
| Let : exp → exp → exp → exp
| c : ℕ → list lev → exp

def context := list exp

open lev exp

def lev.ubound : lev → ℕ
| (univ_var v) := v + 1
| zero := 0
| (S l) := lev.ubound l
| (max l1 l2) := max (lev.ubound l1) (lev.ubound l2)
| (imax l1 l2) := max (lev.ubound l1) (lev.ubound l2)

def list_lev.ubound : list lev → ℕ
| [] := 0
| (h :: t) := max (lev.ubound h) (list_lev.ubound t)

def exp.ubound : exp → ℕ
| (sort l) := lev.ubound l
| (var _) := 0
| (app e1 e2) := max (exp.ubound e1) (exp.ubound e2)
| (lam e1 e2) := max (exp.ubound e1) (exp.ubound e2)
| (pi e1 e2) := max (exp.ubound e1) (exp.ubound e2)
| (Let e1 e2 e3) := max (max (exp.ubound e1) (exp.ubound e2)) (exp.ubound e3)
| (c _ lst) := list_lev.ubound lst

mutual inductive has_type, admis_const, admis_def
with has_type : context → exp → exp → Prop
| c1 {α lst n} : admis_const (c n lst) α → has_type [] (c n lst) α
| c2 {α e lst n} : admis_def (c n lst) α e → has_type [] (c n lst) α
with admis_const : exp → exp → Prop
| mk {α l lst n} : has_type [] α (sort l) → lev.ubound l ≤ (lst : list lev).length →
  exp.ubound α ≤ lst.length → admis_const (c n lst) α
with admis_def : exp → exp → exp → Prop
| mk {α e lst n} : has_type [] e α → exp.ubound e ≤ (lst : list lev).length → exp.ubound α ≤ lst.length
  → admis_def (c n lst) α e

Is the criteria has_type [] α (sort l) of admis_const free of context, or it should be has_type Γ α (sort l)?

[Mario Carneiro]

@Xiang Li In lean, constants must be valid in the empty context, but they can contain free universe variables, up to the universe number in the constant definition

[Mario Carneiro]

I don't think admis_const needs to be mutual with has_type. In order to make sure that all constants are interpreted consistently, I think you need a global context, which for now can just be a list of constant definitions. Then has_type can just assume that these constants are all well typed, and you can use typing to define what it means for the constants to be admissible

[Mario Carneiro]

inductive cdef
| cnst (uvars : ℕ) (ty : exp) : cdef
| defn (uvars : ℕ) (ty val : exp) : cdef

inductive cdef.as_const : cdef → ℕ → exp → Prop
| cnst (uvars ty) : cdef.as_const (cdef.cnst uvars ty) uvars ty
| defn (uvars ty val) : cdef.as_const (cdef.defn uvars ty val) uvars ty

def exp.usubst : list lev → exp → exp := sorry
def exp.subst : exp → exp → exp := sorry

variable (consts : list cdef)

inductive has_type : context → exp → exp → Prop
| c {lst n cd uvars ty} :
  consts.nth n = some cd →
  cdef.as_const cd uvars ty →
  has_type [] (c n lst) (exp.usubst lst ty)
-- ...

def is_type (Γ α) := ∃ l, has_type consts Γ α (sort l)

inductive cdef.admis : cdef → Prop
| cnst {us ty} : is_type consts [] ty → exp.ubound ty ≤ us →
  cdef.admis (cdef.cnst us ty)
| defn {us ty val} : has_type consts [] ty val → exp.ubound ty ≤ us → exp.ubound val ≤ us →
  cdef.admis (cdef.defn us ty val)

inductive consts.admis : list cdef → Prop
| nil : consts.admis []
| cons {C cd} : consts.admis C → cdef.admis C cd → consts.admis (C ++ [cd])

[Xiang Li]

Thank you for your help again!

[Mario Carneiro]

Oh, I forgot to add the constraint in has_type.c that lst.length = uvars

[Xiang Li]

And also lev.ubound l ≤ us in cdef.admis.cnst.
exp.usubst just means changing univ_var u by the uth element in the list, right?

[Mario Carneiro]

And also lev.ubound l ≤ us in cdef.admis.cnst.

Actually that's implied from the first bound, although the proof is only easily obtainable as a corollary of the main theorem in the paper

[Mario Carneiro]

exp.usubst just means changing univ_var u by the uth element in the list, right?

Yes