From 5342fee2d7a00f4937b550ed5b2ea17698d25802 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Sat, 10 Jan 2026 09:55:22 +0000 Subject: [PATCH 1/9] feat: parse and check a lean4export file --- Main.lean | 22 +++++++++++++++++++++- lake-manifest.json | 45 +++++++++++++++++++++++++-------------------- lakefile.toml | 5 +++++ lean-toolchain | 2 +- 4 files changed, 52 insertions(+), 22 deletions(-) diff --git a/Main.lean b/Main.lean index de5784b..91055f8 100644 --- a/Main.lean +++ b/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 @@ -305,11 +306,30 @@ 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" + if compare then + throw <| IO.userError s!"--import and --compare 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 env ← Lean.mkEmptyEnvironment + 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 } env.toKernelEnv none + println! "checked {n} declarations" + return 0 + + initSearchPath (← findSysroot) let targets ← do match args with | [] => pure [← getCurrentModule] diff --git a/lake-manifest.json b/lake-manifest.json index 0b26296..d023692 100644 --- a/lake-manifest.json +++ b/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": "24241822ef9d3e7f6a3bcc53ad136e12663db8f3", + "name": "batteries", + "manifestFile": "lake-manifest.json", + "inputRev": "v4.26.0", + "inherited": false, + "configFile": "lakefile.toml"}], + "name": "lean4lean", + "lakeDir": ".lake"} diff --git a/lakefile.toml b/lakefile.toml index bc3cbfc..c253b3f 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -6,6 +6,11 @@ name = "batteries" git = "https://github.com/leanprover-community/batteries" rev = "v4.26.0" +[[require]] +scope = "leanprover" +name = "lean4export" +rev = "joachim_parse_fixes" + [[lean_lib]] name = "Lean4Lean" diff --git a/lean-toolchain b/lean-toolchain index e59446d..fb18a7f 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.26.0 +leanprover/lean4:v4.27.0-rc1 \ No newline at end of file From d2d5b337dae12b03cd7e3e0f6b52097dc1d2ee67 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Sat, 10 Jan 2026 10:03:53 +0000 Subject: [PATCH 2/9] Manually set toolchain. Stop messing with that, lake! --- lean-toolchain | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lean-toolchain b/lean-toolchain index fb18a7f..e59446d 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.27.0-rc1 \ No newline at end of file +leanprover/lean4:v4.26.0 From 4d291a8eba9ecbaa61070ea5a848ff3715a42561 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Sat, 10 Jan 2026 11:59:13 +0000 Subject: [PATCH 3/9] Simplify --- Main.lean | 5 +---- 1 file changed, 1 insertion(+), 4 deletions(-) diff --git a/Main.lean b/Main.lean index 91055f8..b317136 100644 --- a/Main.lean +++ b/Main.lean @@ -314,18 +314,15 @@ unsafe def main (args : List String) : IO UInt32 := do if readImport then if fresh then throw <| IO.userError s!"--import and --fresh cannot be used together" - if compare then - throw <| IO.userError s!"--import and --compare 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 env ← Lean.mkEmptyEnvironment 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 } env.toKernelEnv none + let (n, _) ← replay { newConstants := constMap, verbose, compare } (.empty .anonymous) none println! "checked {n} declarations" return 0 From 0471841e6244fce390a77cc7705d23be911a281b Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Mon, 12 Jan 2026 20:52:05 +0000 Subject: [PATCH 4/9] Hack: Remove checkQuotInit --- Main.lean | 11 ----------- 1 file changed, 11 deletions(-) diff --git a/Main.lean b/Main.lean index b317136..0b37ae9 100644 --- a/Main.lean +++ b/Main.lean @@ -223,16 +223,6 @@ def checkPostponedRecursors : M Unit := do unless info == info' do throw <| IO.userError s!"Invalid recursor {ctor}" | _, _ => throw <| IO.userError s!"No such recursor {ctor}" -/-- -Check that at the end of (any) file, the quotient module is initialized by the end. -(It will already be initialized at the beginning, unless this is the very first file, -`Init.Core`, which is responsible for initializing it.) -This is needed because it is an assumption in `finalizeImport`. --/ -def checkQuotInit : M Unit := do - unless (← get).env.quotInit do - throw <| IO.userError s!"initial import (Init.Core) didn't initialize quotient module" - /-- "Replay" some constants into an `Environment`, sending them to the kernel for checking. -/ def replay (ctx : Context) (env : Environment) (decl : Option Name := none) : IO (Nat × Environment) := do @@ -251,7 +241,6 @@ def replay (ctx : Context) (env : Environment) (decl : Option Name := none) : replayConstant n checkPostponedConstructors checkPostponedRecursors - checkQuotInit return (s.numAdded, s.env) open private ImportedModule.mk from Lean.Environment in From 258fbf4b9cad882adebb781dc56f0a3ebd5974af Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Thu, 15 Jan 2026 09:16:13 +0000 Subject: [PATCH 5/9] hack for the arena: recognize and decline newer prelude for now --- Main.lean | 3 +++ 1 file changed, 3 insertions(+) diff --git a/Main.lean b/Main.lean index 0b37ae9..0b28f75 100644 --- a/Main.lean +++ b/Main.lean @@ -311,6 +311,9 @@ unsafe def main (args : List String) : IO UInt32 := do -- 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 + if constMap.contains `WellFounded.Nat.fix && constMap.contains `Nat.gcd then + println! "post v4.26 prelude detected, declining" + return 2 let (n, _) ← replay { newConstants := constMap, verbose, compare } (.empty .anonymous) none println! "checked {n} declarations" return 0 From d59dc96d0c6219aab537ab1da86212533cdc085b Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Fri, 16 Jan 2026 15:08:54 +0000 Subject: [PATCH 6/9] replay: treat a string literal as a dependecy on String.ofList and Char.ofNat --- Main.lean | 18 ++++++++++++++++-- 1 file changed, 16 insertions(+), 2 deletions(-) diff --git a/Main.lean b/Main.lean index 0b28f75..dee7335 100644 --- a/Main.lean +++ b/Main.lean @@ -144,6 +144,12 @@ deriving instance BEq for ConstructorVal deriving instance BEq for RecursorRule deriving instance BEq for RecursorVal +def Lean.Expr.hasStrLit (e : Expr) : Bool := + e.find? (isStringLit) |>.isSome + +def Lean.ConstantInfo.hasStrLit (ci : ConstantInfo) : Bool := + ci.type.hasStrLit || ci.value?.any (·.hasStrLit) + mutual /-- Check if a `Name` still needs to be processed (i.e. is in `remaining`). @@ -157,7 +163,15 @@ and add it to the environment. partial def replayConstant (name : Name) : M Unit := do if ← isTodo name then let some ci := (← read).newConstants[name]? | unreachable! - replayConstants ci.getUsedConstants + let mut usedConstants := ci.getUsedConstants + -- We want `String.ofList` to be available when encountering string literals. + -- Presumably faster to first check if we already have it, before traversing + -- the declaration + unless (← get).env.contains ``String.ofList do + if ci.hasStrLit then + usedConstants := usedConstants.insert ``String.ofList + usedConstants := usedConstants.insert ``Char.ofNat + replayConstants usedConstants -- Check that this name is still pending: a mutual block may have taken care of it. if (← get).pending.contains name then match ci with @@ -311,7 +325,7 @@ unsafe def main (args : List String) : IO UInt32 := do -- 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 - if constMap.contains `WellFounded.Nat.fix && constMap.contains `Nat.gcd then + if constMap.contains `WellFounded.Nat.fix && (constMap.contains `Nat.gcd || constMap.contains `Nat.bitwise) then println! "post v4.26 prelude detected, declining" return 2 let (n, _) ← replay { newConstants := constMap, verbose, compare } (.empty .anonymous) none From d7fd9884388464076ecb0698060b3503de01f922 Mon Sep 17 00:00:00 2001 From: Mario Carneiro Date: Wed, 21 Jan 2026 00:15:22 +0000 Subject: [PATCH 7/9] chore: update lean --- Lean4Lean/Expr.lean | 2 +- Lean4Lean/Primitive.lean | 74 ++++++++++++++++++++++++++++- Lean4Lean/Verify/Expr.lean | 2 +- Lean4Lean/Verify/Typing/Lemmas.lean | 6 +-- lake-manifest.json | 35 ++++++-------- lakefile.toml | 2 +- lean-toolchain | 2 +- 7 files changed, 94 insertions(+), 29 deletions(-) diff --git a/Lean4Lean/Expr.lean b/Lean4Lean/Expr.lean index a101fc2..e9bf4da 100644 --- a/Lean4Lean/Expr.lean +++ b/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 diff --git a/Lean4Lean/Primitive.lean b/Lean4Lean/Primitive.lean index e81e0bc..fae0c93 100644 --- a/Lean4Lean/Primitive.lean +++ b/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) diff --git a/Lean4Lean/Verify/Expr.lean b/Lean4Lean/Verify/Expr.lean index cb9dccc..3495d9f 100644 --- a/Lean4Lean/Verify/Expr.lean +++ b/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 diff --git a/Lean4Lean/Verify/Typing/Lemmas.lean b/Lean4Lean/Verify/Typing/Lemmas.lean index 7c503c3..7a6e936 100644 --- a/Lean4Lean/Verify/Typing/Lemmas.lean +++ b/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⟩ diff --git a/lake-manifest.json b/lake-manifest.json index 0b26296..3d24284 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -1,20 +1,15 @@ -{ - "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-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"} diff --git a/lakefile.toml b/lakefile.toml index bc3cbfc..fa455a6 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -4,7 +4,7 @@ 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" [[lean_lib]] name = "Lean4Lean" diff --git a/lean-toolchain b/lean-toolchain index e59446d..bd19bde 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.26.0 +leanprover/lean4:v4.27.0-rc1 From 94aeb7d51b8acf3baa43e5984516c84f11aa5575 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Wed, 21 Jan 2026 13:55:19 +0000 Subject: [PATCH 8/9] Edited wrong line --- Main.lean | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/Main.lean b/Main.lean index fb79a57..0611233 100644 --- a/Main.lean +++ b/Main.lean @@ -285,8 +285,7 @@ unsafe def replayFromImports (module : Name) (verbose := false) (compare := fals let mut newConstants := {} for name in mod.constNames, ci in mod.constants do newConstants := newConstants.insert name ci - let checkQuot := newConstants.contains `Quot - let (n, env') ← replay { newConstants, verbose, compare, checkQuot } env + let (n, env') ← replay { newConstants, verbose, compare } env (Environment.ofKernelEnv env').freeRegions region.free pure n @@ -341,7 +340,7 @@ unsafe def main (args : List String) : IO UInt32 := do -- 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 } (.empty .anonymous) none + let (n, _) ← replay { newConstants := constMap, verbose, compare, checkQuot := false } (.empty .anonymous) none println! "checked {n} declarations" return 0 From 7ded588f563d4e97abc6dffc3f48daede5d0fb93 Mon Sep 17 00:00:00 2001 From: Mario Carneiro Date: Wed, 21 Jan 2026 00:15:22 +0000 Subject: [PATCH 9/9] chore: update lean --- Lean4Lean/Expr.lean | 2 +- Lean4Lean/Primitive.lean | 74 ++++++++++++++++++++++++++++- Lean4Lean/Verify/Expr.lean | 2 +- Lean4Lean/Verify/Typing/Lemmas.lean | 6 +-- lake-manifest.json | 35 ++++++-------- lakefile.toml | 2 +- lean-toolchain | 2 +- 7 files changed, 94 insertions(+), 29 deletions(-) diff --git a/Lean4Lean/Expr.lean b/Lean4Lean/Expr.lean index a101fc2..e9bf4da 100644 --- a/Lean4Lean/Expr.lean +++ b/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 diff --git a/Lean4Lean/Primitive.lean b/Lean4Lean/Primitive.lean index e81e0bc..fae0c93 100644 --- a/Lean4Lean/Primitive.lean +++ b/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) diff --git a/Lean4Lean/Verify/Expr.lean b/Lean4Lean/Verify/Expr.lean index cb9dccc..3495d9f 100644 --- a/Lean4Lean/Verify/Expr.lean +++ b/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 diff --git a/Lean4Lean/Verify/Typing/Lemmas.lean b/Lean4Lean/Verify/Typing/Lemmas.lean index 7c503c3..7a6e936 100644 --- a/Lean4Lean/Verify/Typing/Lemmas.lean +++ b/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⟩ diff --git a/lake-manifest.json b/lake-manifest.json index 0b26296..3d24284 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -1,20 +1,15 @@ -{ - "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-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"} diff --git a/lakefile.toml b/lakefile.toml index bc3cbfc..fa455a6 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -4,7 +4,7 @@ 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" [[lean_lib]] name = "Lean4Lean" diff --git a/lean-toolchain b/lean-toolchain index e59446d..bd19bde 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.26.0 +leanprover/lean4:v4.27.0-rc1