Divergences from the Lean Kernel

This is a list of places where lean4lean deliberately has different behavior from the kernel. Unless specified here, any divergence between lean4lean and lean4 is a bug.

• Lean4Lean.TypeChecker.Inner.reduceNative: Lean4lean does not support reduction of reduceBool. This would involve implementing verified compilation, which while possible would be an additional chunk of work comparable to this entire repo.
• Lean4Lean.Primitive.checkDef, checkInductive: Lean does not check that primitives are declared with the correct types and definitional behavior, except in the case of Eq which is used in the declaration of Quot. This is required for soundness, but Lean is able to get away with it because Lean ships its prelude and using an alternative prelude is not supported.
• Lean4Lean.TypeChecker.Inner.inferType', literal case: The original code was not checking that the literal type actually exists. Again, this is okay provided that the prelude is trusted.
• Lean4Lean.TypeChecker.Inner.tryStringLitExpansionCore: there is a counterproductive whnf call in this function which is removed in Lean4lean.
• Lean4Lean.TypeChecker.Inner.isDefEqApp: lean4lean compares the two argument counts before the two heads, where type_checker::is_def_eq_app compares the heads first. Both answer false when the counts differ, so the decision is the same.
• Lean4Lean.TypeChecker.Inner.inferType', application case: lean4lean checks isDefEq dType aType, where infer_app checks is_def_eq(a_type, d_type). Definitional equality is symmetric, so this cannot change the answer, but this avoids some needless left-right flipping.
• Lean.Level.normalize, isEquiv, geq, instantiateLevelParams: Lean4lean uses the level operations from Lean's standard library, which differ from the C++ kernel's; leanprover/lean4#14356 tracks aligning them. This has two separate consequences. The comparison operations decide slightly different sets of (in)equalities than the kernel's is_equiv/is_geq (but see the next point). And because instantiateLevelParams builds levels with mkLevelMax'/mkLevelIMax' rather than the kernel's mk_max/mk_imax, unfolding a universe-polymorphic constant can produce a term that means the same as the kernel's but is not syntactically equal to it, and so does not share its Expr.hash.
• Lean.Level.normalize', isEquiv', geq': Lean4lean implements a new algorithm for level normalization. These run the standard library's operation as a fast path and fall back to a complete decision procedure for level algebra, so lean4lean decides level equality and ≥ for more pairs than either the standard library or the kernel — it accepts declarations the kernel rejects for reasons of level incompleteness, never the other way around.
• Lean4Lean.checkConstantVal: The original implementation would call check which sets the level params and then unsets them afterward, and then ensure_sort would run in a context without any level params. In lean4lean the monad is parameterized over level params, so they remain the same across the two calls.
• Lean4Lean.TypeChecker.Inner.inferProj, toCtorWhenStruct: both kernels recognize Prop up to universe normalization (leanprover/lean4#14613), but they differ on levels that are neither always nor never zero: lean4lean tests isNeverZero where Lean tests !isAlwaysZero. Lean4lean's rule keeps Expr.proj no more powerful than the recursor the kernel generates for the same type. For MaybeProp.{u} : Sort u with a field in PUnit.{u}, the kernel cannot rule out that the type is a proposition, so it emits MaybeProp.rec : {motive : MaybeProp → Prop} → ... — small elimination only — and fun x => x.0 : MaybeProp.{u} → PUnit.{u} cannot be written with it. Lean accepts that projection anyway, so under Lean's rule proj computes something the type's own eliminator cannot. Lean's choice is still sound, but only because the constructor universe bound in inductive.cpp separately rejects inductive T.{u} : Sort u where mk : Bool → T, which would otherwise give an analogue of the construction in #14613; testing isNeverZero makes the projection check independent of that bound. Reconciling the two in the other direction — letting the recursor eliminate large whenever every field's universe is bounded by the inductive's, which is exactly what makes such a projection sound — would be the complete answer, but that is a change to recursor generation rather than to this check.
• Lean4Lean.EquivManager.isEquiv, Lean4Lean.TypeChecker.Inner.isDefEqCore', reduceProj: when comparing two projections, and when reducing one, lean4lean uses only the projection index, while the C++ kernel also compares the structure name (leanprover/lean4#14631, #14632). The name has already been checked by the time either happens: inferProj rejects .proj S i e unless the type of e whnfs to an application of S itself. Comparison and reduction only ever see projections that have been through type inference, so re-comparing the name there is redundant.
• Lean4Lean.Environment.addInductive: leanprover/lean4#14621 rechecks the declarations produced by nested-inductive elimination — the restored constructor types, the restored recursor types and the recursor rules' right-hand sides. Lean4lean does not. Upstream describes these as redundant sanity checks that "may prevent soundness bugs if the nested-inductive code is still missing any required validations"; they establish no precondition that a later step consumes. Lean4lean aims to prove the elimination correct rather than to recheck its output, and a speculative check would only add proof obligations without contributing an invariant. The check of the nested applications I Ds from #14577 is kept, because those arguments are dropped from the auxiliary declarations and so are not covered by checking the block.
• Lean4Lean.checkNoNestedAux: leanprover/lean4#14616 rejects the reserved _nested prefix in both the inductive types and the constructor types of a declaration; lean4lean checks only the constructor types. The bug that check fixes is specific to constructors: nested occurrences are rewritten to the auxiliary types in constructor types only (replaceAllNested), and rewritten back the same way (restoreNested), so an inductive's own type is carried through both directions verbatim and cannot acquire a type it was not checked at. A _nested name written in an inductive type also cannot resolve in the first place: the auxiliary types are declared in the same block, so they are not in the environment while that block's types are checked (unlike constructor types, which are checked once the block's types, auxiliaries included, are present), and they never survive into the final environment. Lean's check additionally reserves the whole _nested namespace against unrelated user declarations, which lean4lean does not.
• Lean4Lean.ElimNestedInductive.Result.restoreNested, restoreCtorName: leanprover/lean4#14632 turned the lean_asserts in the nested-inductive restoration into kernel exceptions; lean4lean keeps unreachable! and assert!. The branches are unreachable: restoreCtorName runs only for the recursors of the auxiliary types the elimination generates, whose constructors are exactly the keys of aux2nested, and the nested occurrences stored there are applications of a constant by construction. Upstream's stated motivation is that the assertions vanish in a release build and the C++ consumers then read out of bounds; the corresponding accesses here are total, so there is nothing to read out of bounds. Note that if one of these invariants were broken anyway, unreachable! would continue with a default value rather than reject; the restored constructor and recursor types are re-checked in the final environment (#14621), which lean4lean retains, but a restored rule constructor name is not covered by that pass.
• Lean4Lean.FuelConfig: since leanprover/lean4#13956, the native kernel bounds mutually recursive checking through the maxRecDepth option. Lean4lean exposes several independent fuel counters instead, because its Lean definitions also need explicit termination witnesses. Replay comparison therefore uses each implementation's default bound unless an explicit lean4lean fuel configuration is supplied.
• Lean4Lean.addDefinition (unsafe branch), addMutual: an unsafe/partial definition may be recursive, so its body is checked in an environment that already contains the declaration. The C++ kernel adds constant_info(d) there -- the full definition, value included -- so the body can delta-unfold the very constant being defined. Lean4lean adds it as an axiom of the same type instead: the body may still refer to the block's constants, but cannot unfold them. So for example unsafe def foo : Nat := (fun (_ : foo = 1) => 1) rfl is accepted by the C++ kernel, but rejected by L4L: checking the argument requires foo =?= 1, which succeeds by unfolding foo to its own body and reducing. Read literally, that rule makes a typing fact about the constant available while establishing it, and implementing this in IsDefEq directly degenerates completely, allowing even things like unsafe def bar : Nat := "hi" by using the typing judgment to justify itself. The gap is confined to unsafe/partial code, which carries no logical content.
• Lean4Lean.addMutual: lean4lean requires the declarations of a mutual block to carry the same universe parameters and to have distinct names. Both checks are in kernel PRs that are not yet released (leanprover/lean4#14608, #14632); the released kernel checks only that the safety annotations agree. Lean4lean needs them rather than merely matching them: the block is checked under a single M.run, whose level parameters are fixed for the whole run, and the model adds the block's constants one at a time with VEnv.addConsts, which fails on a repeated name.