Lean4Lean progress

Stream: Type theory

[Mario Carneiro]

I wanted to share that Lean4Lean has just reached a major milestone: The inferType function has been proved correct. This constitutes about 1/3 of the main typechecker, excluding inductive types. The other two main functions are whnf and isDefEq.

I've also started cataloguing places where lean4lean intentionally differs from the lean kernel, often to fix bugs, as well as a trophy case of kernel bugs found in the course of formalization.

[Henrik Böving]

How confident are, you based on this proof, that the C++ equivalent in the upstream kernel is also correct?

[Mario Carneiro]

Very, modulo the documented issues. I have a file of axioms, some of which are known to be false, for example the one about substring reflexivity (lean4#10511). The divergences should be upstreamed though, because otherwise I'm proving things about a kernel that is not the one upstream

[Mario Carneiro]

Oh, I managed to turn that one into a native_decide unsoundness:

def f (n : Nat) : Expr := .mdata ⟨[(`_, .ofSyntax (.ident .none ⟨"", ⟨n⟩, 0⟩ `_ []))]⟩ (.sort .zero)
example : False :=
  have : (.mdata ⟨[(`_, .ofSyntax (.ident .none ⟨"", ⟨1⟩, 0⟩ `_ []))]⟩ (.sort .zero) == f 1) ≠
         (f 1 == f 1) := by native_decide
  this rfl

this happens because Expr assumes equality is reflexive to justify a pointer equality optimization

[Mario Carneiro]

so it's less that I know the upstream kernel is correct but I know it's incorrect and why

[Mario Carneiro]

The divergences about checking primitives aren't even something I have made an attempt to upstream, because I know what the core team will say: we don't care if the lean kernel is unsound if you have to rewrite the prelude, that's not a supported way to use lean

[Mario Carneiro]

Here are the list of axioms and sorries:

'Lean4Lean.TypeChecker.Inner.inferType'.WF' depends on axioms: [propext,
 sorryAx,
 Classical.choice,
 Quot.sound,
 Lean.Expr.abstractRange_eq,
 Lean.Expr.abstract_eq,
 Lean.Expr.eqv_eq,
 Lean.Expr.hasLevelParam_eq,
 Lean.Expr.hasLooseBVar_eq,
 Lean.Expr.instantiate1_eq,
 Lean.Expr.instantiateRevRange_eq,
 Lean.Expr.instantiateRev_eq,
 Lean.Expr.instantiate_eq,
 Lean.Expr.looseBVarRange_eq,
 Lean.Expr.lowerLooseBVars_eq,
 Lean.Expr.replace_eq,
 Lean.Level.hasMVar_eq,
 Lean.Level.hasParam_eq,
 Lean.Level.instLawfulBEqLevel,
 Lean.PersistentArray.toList'_push,
 Lean.PersistentHashMap.findAux_isSome,
 Lean.Substring.beq_refl,
 Lean.Syntax.structEq_eq,
 Lean.Expr.mkAppRangeAux.eq_def,
 Lean.PersistentHashMap.WF.find?_eq,
 Lean.PersistentHashMap.WF.toList'_insert]

VInductDecl.WF has sorry of type
  Prop
VEnv.addInduct has sorry of type
  Option VEnv
TrProj has sorry of type
  List VExpr → Name → Nat → VExpr → VExpr → Prop
VEnv.addInduct_WF has sorry of type
  env'.Ordered
inferProj.WF has sorry of type
  RecM.WF c s (inferProj st i e ety) fun ty x => ∃ ty', c.TrTyping (Expr.proj st i e) ty e' ty'
TrProj.weakN has sorry of type
  TrProj Γ' s i (VExpr.liftN n e k) (VExpr.liftN n e' k)
TrProj.wf has sorry of type
  VExpr.WF env U Γ e'
VEnv.IsDefEq.uniq has sorry of type
  ∃ u, env.IsDefEq U Γ A B (VExpr.sort u)
TrProj.uniq has sorry of type
  env.IsDefEqU U Γ₁ e₁' e₂'
TrProj.defeqDFC has sorry of type
  ∃ e', TrProj Γ₂ s i e₂ e'
TrProj.instL has sorry of type
  TrProj (List.map (VExpr.instL ls) Γ) s i (VExpr.instL ls e) (VExpr.instL ls e')
VEnv.IsDefEqU.weakN_iff has sorry of type
  env.IsDefEqU U Γ e1 e2
TrProj.weakN_inv has sorry of type
  TrProj Γ' s i (VExpr.liftN n e k) e' → ∃ e', TrProj Γ s i e e'
TrProj.instN has sorry of type
  TrProj Γ s i (e.inst e₀ k) (e'.inst e₀ k)
VEnv.IsDefEqU.forallE_inv has sorry of type
  (∃ u, env.IsDefEq U Γ A A' (VExpr.sort u)) ∧ ∃ u, env.IsDefEq U (A :: Γ) B B' (VExpr.sort u)

Obviously this is rather different in character from a pure math project. Most of the axioms are un-opaquing an opaque or partial definition. Most of the sorries have to do with support for inductives, plus the big questions about injectivity of type constructors and unique typing.