feat: parse and check a lean4export file

Lean4Lean/Expr.lean

@@ -86,7 +86,7 @@ def strLitToConstructor (s : String) : Expr :=
   let listCons := .app (.const ``List.cons [.zero]) char
   let stringMk := .const ``String.ofList []
   let charOfNat := .const ``Char.ofNat []
-  .app stringMk <| s.foldr (init := listNil) fun c e =>
+  .app stringMk <| s.toList.foldr (init := listNil) fun c e => -- TODO: use String.foldr
     .app (.app listCons <| .app charOfNat (.lit (.natVal c.toNat))) e
 
 end Expr

Lean4Lean/Primitive.lean

@@ -173,6 +173,76 @@ def unfoldWellFounded (e : Expr) (fvs : Array Expr) (eq_def : Expr) (fail : ∀
   unless ← isDefEq (e1.app wfn') rhs do fail
   return (← getLCtx).mkLambda fvs rhs
 
+def lambdaTelescope (e : Expr) (k : Array Expr → Expr → M α) : M α := loop #[] e where
+  loop fvars
+  | .lam x dom body bi =>
+    let d := dom.instantiateRev fvars
+    withLocalDecl x bi d fun fv => do
+      let fvars := fvars.push fv
+      loop fvars body
+  | e => k fvars (e.instantiateRev fvars)
+
+def forallTelescope (e : Expr) (k : Array Expr → Expr → M α) : M α := loop #[] e where
+  loop fvars
+  | .forallE x dom body bi =>
+    let d := dom.instantiateRev fvars
+    withLocalDecl x bi d fun fv => do
+      let fvars := fvars.push fv
+      loop fvars body
+  | e => k fvars (e.instantiateRev fvars)
+
+def unfoldNatWellFounded (e : Expr) (fvs : Array Expr) (eq_def : Expr) (fail : ∀ {α}, M α) : M Expr := do
+  let succ := mkApp q(Nat.succ)
+  let defeq1 a b := isDefEq (.arrow q(Nat) a) (.arrow q(Nat) b)
+  let x := .bvar 0
+  let .app (.app _ lhs) rhs := eq_def.getForallBody.instantiateRev fvs | fail
+  let orig := lhs.getAppFn
+  let rhs := rhs.replace fun e' => if e' == orig then some e else none
+  let e1 ← whnfCore (mkAppN e fvs) -- get _unary
+  let e1 ← unfoldDefinition e1 -- get fix
+  (← whnfCore e1).withApp fun fix args => do
+  let .const ``WellFounded.Nat.fix [_, _] := fix | fail
+  let #[α,motive,f,F,a₀] := args | fail
+  let fixFn := mkAppN fix #[α,motive,f,F]
+  withLocalDecl `a .default (← inferType a₀) fun a => do
+  -- prove |- fix α motive f F a ≡ go α motive f F (eager (f a)) a [proof]
+  let e1 ← unfoldDefinition (.app fixFn a) -- get fix.go
+  let e1 ← whnfCore e1
+  e1.withApp fun fixGo args => do
+    let #[α',motive',f',F',fuel,a',_] := args | fail
+    unless (α, motive, f, F, a) == (α', motive', f', F', a') do fail
+    let .app eager n := fuel | fail
+    unless ← isDefEq n (succ (.app f a)) do fail
+    -- prove |- eager n = if beq n n = true then n else n
+    unless (← getEnv).contains ``Nat.beq do fail
+    let c := Condition.bool; c.check (fail) (ite := true)
+    unless ← defeq1 (mkApp eager x) (c.ite q(Nat) #[mkApp2 (.const ``Nat.beq []) x x] x x) do fail
+    -- prove |- go α motive f F (succ t) x hfuel ≡ F x fun y hy => go α motive f F t y [proof]
+    let go' ← unfoldDefinition fixGo -- get fix
+    lambdaTelescope go' fun fvs go' => do
+    let #[_,_,_,F,t] := fvs | fail
+    let .app natRec t' := go' | fail
+    unless !natRec.containsFVar t.fvarId! && t == t' do fail
+    _ ← checkType (succ t)
+    let gor ← whnfCore (.app natRec (succ t))
+    lambdaTelescope gor fun fvs gor => do
+    let #[x,_] := fvs | fail
+    let .app Fx ih := gor | fail
+    unless .app F x == Fx do fail
+    lambdaTelescope ih fun fvs ih => do
+    let #[y,_] := fvs | fail
+    let .app ih _ := ih | fail
+    unless ih == .app (.app natRec t) y do fail
+  -- prove |- rhs ≡ F x fun y _ => fix α motive f F y
+  let .forallE _ dom _ _ ← inferType (.app F a₀) | fail
+  let ih' ← forallTelescope dom fun fvs _ => do
+    let #[y,_] := fvs | fail
+    return (← getLCtx).mkLambda fvs (.app fixFn y)
+  have rhs' := mkApp2 F a₀ ih'
+  _ ← checkType rhs'
+  unless ← isDefEq rhs rhs' do fail
+  return (← getLCtx).mkLambda fvs rhs
+
 def checkPrimitiveDef (v : DefinitionVal) : M Bool := do
   let fail {α} : M α := throw <| .other s!"invalid form for primitive def {v.name}"
   let tru := q(true)
@@ -285,7 +355,7 @@ def checkPrimitiveDef (v : DefinitionVal) : M Bool := do
     unless ← isDefEq v.type q(Nat → Nat → Nat) do fail
     withLocalDecl `m .default q(Nat) fun m => do
     withLocalDecl `n .default q(Nat) fun n => do
-    let gcd' ← unfoldWellFounded v.value #[m, n] q(type_of% Nat.gcd.eq_def) fail
+    let gcd' ← unfoldNatWellFounded v.value #[m, n] q(type_of% Nat.gcd.eq_def) fail
     let gcd' := mkApp2 gcd'
     let gcd := mkApp2 v.value
     unless ← isDefEq (gcd' zero m) m do fail
@@ -315,7 +385,7 @@ def checkPrimitiveDef (v : DefinitionVal) : M Bool := do
     withLocalDecl `f .default q(Bool → Bool → Bool) fun f => do
     withLocalDecl `n .default q(Nat) fun n => do
     withLocalDecl `m .default q(Nat) fun m => do
-    let bitwise' ← unfoldWellFounded v.value #[f, n, m] q(type_of% Nat.bitwise.eq_def) fail
+    let bitwise' ← unfoldNatWellFounded v.value #[f, n, m] q(type_of% Nat.bitwise.eq_def) fail
     let bitwise := mkApp3 v.value
     let c := Condition.natEq; c.check fail (ite := true)
     let bc := Condition.bool; bc.check fail (ite := true)

Lean4Lean/Verify/Expr.lean

@@ -244,7 +244,7 @@ theorem toConstructor_hasLevelParam :
   cases l with simp [Literal.toConstructor]
   | natVal n => cases n <;> simp [natLitToConstructor, hasLevelParam', natZero, natSucc]
   | strVal s =>
-    simp [strLitToConstructor, hasLevelParam', String.foldr_eq]
+    simp [strLitToConstructor, hasLevelParam']
     induction s.toList <;> simp_all [hasLevelParam', Level.hasParam']
 
 protected theorem beq_iff_eq {m n : Literal} : m == n ↔ m = n := by

Lean4Lean/Verify/Typing/Lemmas.lean

@@ -49,11 +49,11 @@ theorem Closed.natLitToConstructor : Closed (.natLitToConstructor n) k := by
   cases n <;> simp [Closed, Expr.natLitToConstructor, Expr.natZero, Expr.natSucc]
 
 theorem FVarsIn.strLitToConstructor : FVarsIn P (.strLitToConstructor s) := by
-  simp [FVarsIn, String.foldr_eq, Expr.strLitToConstructor]
+  simp [FVarsIn, Expr.strLitToConstructor]
   induction s.toList <;> simp [*, FVarsIn, Level.hasMVar']
 
 theorem Closed.strLitToConstructor : Closed (.strLitToConstructor s) k := by
-  simp [Closed, String.foldr_eq, Expr.strLitToConstructor]
+  simp [Closed, Expr.strLitToConstructor]
   induction s.toList <;> simp [*, Closed]
 
 theorem FVarsIn.toConstructor : ∀ {l : Literal}, FVarsIn P l.toConstructor
@@ -1580,7 +1580,7 @@ theorem TrExprS.IsUnique.natLitToConstructor : ∀ {n : Nat}, IsUnique (.natLitT
   | _+1 => ⟨⟨⟩, ⟨⟩⟩
 
 theorem TrExprS.IsUnique.strLitToConstructor {s : String} : IsUnique (.strLitToConstructor s) := by
-  refine ⟨⟨⟩, ?_⟩; simp [String.foldr_eq]
+  refine ⟨⟨⟩, ?_⟩
   induction s.toList with simp
   | nil => exact ⟨⟨⟩, ⟨⟩⟩
   | cons _ _ ih => exact ⟨⟨⟨⟨⟩, ⟨⟩⟩, ⟨⟨⟩, ⟨⟩⟩⟩, ih⟩

Main.lean

@@ -7,6 +7,7 @@ import Lean.CoreM
 import Lean.Util.FoldConsts
 import Lean4Lean.Environment
 import Lake.Load.Manifest
+import Export.Parse
 
 namespace Lean
 
@@ -331,11 +332,27 @@ You can also use `lake exe lean4lean --fresh Mathlib.Data.Nat.Basic` to replay a
 but this can only be used on a single file.
 -/
 unsafe def main (args : List String) : IO UInt32 := do
-  initSearchPath (← findSysroot)
   let (flags, args) := args.partition fun s => s.startsWith "-"
   let verbose := "-v" ∈ flags || "--verbose" ∈ flags
   let fresh : Bool := "--fresh" ∈ flags
   let compare : Bool := "--compare" ∈ flags
+  let readImport : Bool := "--import" ∈ flags
+  if readImport then
+    if fresh then
+      throw <| IO.userError s!"--import and --fresh cannot be used together"
+    let [inputPath] := args |
+      throw <| IO.userError s!"--import expect a single file"
+    let handle ← IO.FS.Handle.mk inputPath .read
+    let solution ← Export.parseStream (.ofHandle handle)
+    let mut constMap := solution.constMap
+    -- Lean's kernel interprets just the addition of `Quot as adding all of these so adding them
+    -- multiple times leads to errors.
+    constMap := constMap.erase `Quot.mk |>.erase `Quot.lift |>.erase `Quot.ind
+    let (n, _) ← replay { newConstants := constMap, verbose, compare, checkQuot := false } (.empty .anonymous) none
+    println! "checked {n} declarations"
+    return 0
+
+  initSearchPath (← findSysroot)
   let targets ← do
     match args with
     | [] => pure [← getCurrentModule]

lake-manifest.json

@@ -1,20 +1,25 @@
-{
-  "version": "1.1.0",
-  "packagesDir": ".lake/packages",
-  "packages": [
-    {
-      "url": "https://github.com/leanprover-community/batteries",
-      "type": "git",
-      "subDir": null,
-      "scope": "",
-      "rev": "24241822ef9d3e7f6a3bcc53ad136e12663db8f3",
-      "name": "batteries",
-      "manifestFile": "lake-manifest.json",
-      "inputRev": "v4.26.0",
-      "inherited": false,
-      "configFile": "lakefile.toml"
-    }
-  ],
-  "name": "lean4lean",
-  "lakeDir": ".lake"
-}
+{"version": "1.1.0",
+ "packagesDir": ".lake/packages",
+ "packages":
+ [{"url": "https://github.com/leanprover/lean4export",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover",
+   "rev": "f8c6ed35d043b6253d66e7f0b4a1368f659ebc8e",
+   "name": "lean4export",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "joachim_parse_fixes",
+   "inherited": false,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/batteries",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "6254bed25866358ce4f841fa5a13b77de04ffbc8",
+   "name": "batteries",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v4.27.0-rc1",
+   "inherited": false,
+   "configFile": "lakefile.toml"}],
+ "name": "lean4lean",
+ "lakeDir": ".lake"}

lakefile.toml

@@ -4,7 +4,12 @@ defaultTargets = ["Lean4Lean", "lean4lean", "Lean4Lean.Theory", "Lean4Lean.Verif
 [[require]]
 name = "batteries"
 git = "https://github.com/leanprover-community/batteries"
-rev = "v4.26.0"
+rev = "v4.27.0-rc1"
+
+[[require]]
+scope = "leanprover"
+name = "lean4export"
+rev = "joachim_parse_fixes"
 
 [[lean_lib]]
 name = "Lean4Lean"

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.26.0
+leanprover/lean4:v4.27.0-rc1