Bug in kernel level normalization

Stream: lean4

[Parth Shastri]

https://github.com/leanprover/lean4/blob/084a173a47266b5c108dae1ba721bb22149843bd/src/kernel/level.cpp#L492-L496

level normalize(level const & l) {
    auto p = to_offset(l);
    level const & r = p.first;
    switch (kind(r)) {
...
    case level_kind::IMax: {
        auto l1 = normalize(imax_lhs(r));
        auto l2 = normalize(imax_rhs(r));
        return mk_imax(l1, l2);
    }

The result only takes into consideration the level offset p.first and not the offset p.second. The corresponding code in lean includes addOffset, which is missing here:
https://github.com/leanprover/lean4/blob/e44fd19074259018b9ddcbdb00209492416bc8ac/src/Lean/Level.lean#L380-L382

        let l₁ := normalize l₁
        let l₂ := normalize l₂
        addOffset (mkIMaxAux l₁ l₂) k

I believe the correct code should be return mk_succ(mk_imax(l1, l2), p.second);.

A consequence of this is that the following code

example : Sort (imax u v + 1) := Unit -> Sort (imax u v)

results in this error

(kernel) declaration type mismatch, '_example' has type
  Type (max 0 (imax u v))
but it is expected to have type
  Type (imax u v)

The type of the value is Sort (imax 1 (imax u v + 1)), which the Lean version correctly simplifies to Sort (imax u v + 1) = Type (imax u v). However, the kernel seems to incorrectly simplify it to Sort (max 1 (imax u v)), where the + 1 is missing (I'm not entirely sure where the max 0 is coming from).

(On a side note, is there any way to pass a term directly to the kernel without the intermediate type checking step done in Lean?)

[Parth Shastri]

I figured out how to directly send declarations to the kernel.

syntax "kdef " ident (".{" ident,+ "}")? " : " term " := " term : command

open Lean Elab Command Term in
elab_rules : command | `(kdef $name $[.{ $levelParams?,* }]? : $type := $value) => do
  let levelParams :=
    if let some levelParams := levelParams?
    then levelParams.getElems.toList.map (·.getId)
    else []
  let (type, value) ← runTermElabM fun _ => do
    setLevelNames levelParams
    let type ← elabTermAndSynthesize type none
    let value ← elabTermAndSynthesize value none
    return (type, value)
  liftCoreM <| addDecl <| .defnDecl {
    name := name.getId
    levelParams
    type
    value
    hints := .abbrev
    safety := .safe
  }

I'm curious if it is possible to provide a proof of False with this. We can already define a term e := Sort l₁ such that e := Sort l₂ for any constants l₁ and l₂, though I'm unsure of how Girard's paradox could be implemented.

kdef bug'.{u} : Sort (imax 1 u + 2) := Sort (imax 1 u + 1)
def bug := bug'.{0}

#check bug      -- bug : Type 1
#reduce bug     -- Type

[Mario Carneiro]

No, addDecl goes to the kernel, and the kernel checks that things are valid for the type theory, so you should not be able to prove False if lean is consistent

[James Gallicchio]

(To be clear, this all typechecks in Lean4 nightly; I think Parth found a consistency bug, albeit a small one)

[Mario Carneiro]

Although, since the environment is itself implemented in lean I think you can bypass the kernel by calling Environment.add instead of addDecl

[Mario Carneiro]

Great, I knew I proved girard's paradox for a reason. (Thanks mathport!)

import Lean
syntax "kdef " ident (".{" ident,+ "}")? " : " term " := " term : command

open Lean Elab Command Term in
elab_rules : command | `(kdef $name $[.{ $levelParams?,* }]? : $type := $value) => do
  let levelParams :=
    if let some levelParams := levelParams?
    then levelParams.getElems.toList.map (·.getId)
    else []
  let (type, value) ← runTermElabM fun _ => do
    setLevelNames levelParams
    let type ← elabTermAndSynthesize type none
    let value ← elabTermAndSynthesize value none
    return (type, value)
  liftCoreM <| addDecl <| .defnDecl {
    name := name.getId
    levelParams
    type
    value
    hints := .abbrev
    safety := .safe
  }

kdef Univ'.{u} : Sort (imax 1 u + 1) := Sort (imax 1 u + 1)
def Univ := Univ'.{0}
#check (Univ : Univ) -- !!!

abbrev Set (X) := X → Prop

syntax "{" ident (":" term)? "|" term "}" : term
macro_rules | `({$x $[: $ty]?| $p}) => `(λ $x $[: $ty]? => $p)
macro_rules | `($x ∈ $p) => `($p $x)

theorem iff_of_eq (e : a = b) : a ↔ b := e ▸ .rfl

/-- **Girard's paradox**: there are no universes `u` such that `Type u : Type u`.
Since we can't actually change the type of Lean's `Π` operator, we assume the existence of
`pi`, `lam`, `app` and the `beta` rule equivalent to the `Π` and `app` constructors of type theory.
-/
theorem girard
    (pi : (Type u → Type u) → Type u)
    (lam : ∀ {A : Type u → Type u}, (∀ x, A x) → pi A)
    (app : ∀ {A}, pi A → ∀ x, A x)
    (beta : ∀ {A : Type u → Type u} (f : ∀ x, A x) (x), app (lam f) x = f x) : False :=
  let F (X) := (Set (Set X) → X) → Set (Set X)
  let U := pi F
  let G (T : Set (Set U)) (X) : F X := fun f => { p | { x : U | f (app x X f) ∈ p } ∈ T }
  let τ (T : Set (Set U)) : U := lam (G T)
  let σ (S : U) : Set (Set U) := app S U τ
  have στ : ∀ {s S}, s ∈ σ (τ S) ↔ { x | τ (σ x) ∈ s } ∈ S := @fun s S =>
    iff_of_eq (congrArg (fun f : F U => s ∈ f τ) (beta (G S) U) : _)
  let ω : Set (Set U) := { p | ∀ x, p ∈ σ x → x ∈ p }
  let δ (S : Set (Set U)) := ∀ p, p ∈ S → τ S ∈ p
  have : δ ω := fun p d => d (τ ω) <| στ.2 fun x h => d (τ (σ x)) (στ.2 h)
  this { y | ¬δ (σ y) } (fun x e f => f _ e fun p h => f _ (στ.1 h)) fun p h => this _ (στ.1 h)

theorem contradiction : False := girard
  (pi := fun F => ∀ x : (Univ : Univ), F x)
  (lam := fun f _ => f _) (app := fun f _ => f _) (beta := fun _ _ => rfl)

#print axioms contradiction
-- 'contradiction' does not depend on any axioms

[Mario Carneiro]

It would be nice to try this out on an external checker. cc: @Gabriel Ebner, does trepplein work on lean 4 proofs?

[Mario Carneiro]

The analogous code fails as expected in lean 3:

open tactic level expr

#eval do
  add_decl (declaration.defn `bad' [`u]
    (sort (succ (imax (succ zero) (param `u))))
    (sort (succ (succ (imax (succ zero) (param `u)))))
    reducibility_hints.abbrev
    ff)
-- type mismatch at definition 'bad'', has type
--   Type ((imax 1 u)+2)
-- but is expected to have type
--   Type (imax 1 u)

[Mario Carneiro]

lean4#1781

[Rish Vaishnav]

FWIW, our WIP Yatima typechecker (based on NbE) that I'm working on with @Gabriel Barreto seems to (correctly?) fail at the definition of Univ':

× contradiction (theorem) typechecks
    Expected '"ok _"' but got '"error Expected (Sort 1+(imax 1 (u#0))), found (Sort 2+(imax 1 (u#0)))"'
× Univ (definition) typechecks
    Expected '"ok _"' but got '"error Expected (Sort 1+(imax 1 (u#0))), found (Sort 2+(imax 1 (u#0)))"'
× Univ' (definition) typechecks
   Expected '"ok _"' but got '"error Expected (Sort 1+(imax 1 (u#0))), found (Sort 2+(imax 1 (u#0)))"'

[Rish Vaishnav]

(this was from a commit where we just got the prelude to typecheck, we're in the midst of a refactor right now)