From cc68288358a6d49a2d5a723a1ef2fba308a98f51 Mon Sep 17 00:00:00 2001 From: PratherConid Date: Tue, 31 Dec 2024 17:52:07 +0800 Subject: [PATCH 1/4] test code for previous works --- Auto/EvaluateAuto/CommandAnalysis.lean | 96 ++++++++++++++++++++++++++ Auto/EvaluateAuto/ConstAnalysis.lean | 11 +++ Auto/EvaluateAuto/EnvAnalysis.lean | 9 +++ Auto/EvaluateAuto/Result.lean | 32 +++++++++ Auto/EvaluateAuto/TestCode.lean | 26 +------ 5 files changed, 151 insertions(+), 23 deletions(-) create mode 100644 Auto/EvaluateAuto/CommandAnalysis.lean create mode 100644 Auto/EvaluateAuto/Result.lean diff --git a/Auto/EvaluateAuto/CommandAnalysis.lean b/Auto/EvaluateAuto/CommandAnalysis.lean new file mode 100644 index 0000000..01c0d2c --- /dev/null +++ b/Auto/EvaluateAuto/CommandAnalysis.lean @@ -0,0 +1,96 @@ +import Lean +import Auto.EvaluateAuto.EnvAnalysis +import Auto.EvaluateAuto.Result +open Lean + +namespace EvalAuto + +open Elab Frontend +def runWithEffectOfCommandsCore + (cnt? : Option Nat) + (action : Context → State → State → ConstantInfo → IO (Option α)) : FrontendM (Array α) := do + let mut done := false + let mut ret := #[] + let mut cnt := 0 + while !done do + if cnt?.isSome && cnt >= cnt?.getD 0 then + break + let prev ← get + done ← Frontend.processCommand + let post ← get + let newConsts := Environment.newLocalConstants prev.commandState.env post.commandState.env + for newConst in newConsts do + if let .some result ← action (← read) prev post newConst then + cnt := cnt + 1 + ret := ret.push result + if cnt?.isSome && cnt >= cnt?.getD 0 then + break + return ret + +/-- + Given a Lean4 file `fileName` with content `input` consisting of + a header and a series of commands, first parse the header. Then, + for each command `cmd`, record the states `st₁, st₂` before and + after executing the command, and run `action` on the `ConstantInfo`s produced + by `cmd`, together with `st₁, st₂` and the `InputContext`.\ + An additional `cnt?` can be supplied to control termination. + When the number of times `action` returns `.some _` reaches `cnt?`, + the procedure is terminated. +-/ +def runWithEffectOfCommands + (input : String) (fileName : String) (opts : Options := {}) (cnt? : Option Nat) + (action : Context → State → State → ConstantInfo → IO (Option α)) : IO (Array α) := do + let inputCtx := Parser.mkInputContext input fileName + let (header, parserState, messages) ← Parser.parseHeader inputCtx + let (env, messages) ← processHeader header opts messages inputCtx + let commandState := Command.mkState env messages opts + (runWithEffectOfCommandsCore cnt? action { inputCtx }).run' + { commandState := commandState, parserState := parserState, cmdPos := parserState.pos } + +open Elab Tactic in +/-- + Note: Use `initSrcSearchPath` to get SearchPath of Lean4's builtin source files +-/ +def runTacticAtConstantDeclaration + (name : Name) (searchPath : SearchPath) + (tactic : ConstantInfo → TacticM Unit) : CoreM Result := do + let .some modName ← Lean.findModuleOf? name + | throwError "{decl_name%} :: Cannot find constant {name}" + let .some uri ← Server.documentUriFromModule searchPath modName + | throwError "{decl_name%} :: Cannot find module {modName}" + let .some path := System.Uri.fileUriToPath? uri + | throwError "{decl_name%} :: URI {uri} of {modName} is not a file" + let path := path.normalize + let inputHandle ← IO.FS.Handle.mk path .read + let input ← inputHandle.readToEnd + let results ← runWithEffectOfCommands input path.toString {} (.some 1) (fun ctx st₁ st₂ ci => + let metaAction : MetaM (Option Result) := do + if ci.name != name then + return .none + let .mvar mid ← Meta.mkFreshExprMVar ci.type + | throwError "{decl_name%} :: Unexpected error" + let result : List MVarId ⊕ Exception ← + tryCatchRuntimeEx + (do let goals ← Term.TermElabM.run' (Tactic.run mid (tactic ci)) {}; return .inl goals) + (fun e => return .inr e) + match result with + | .inl goals => + if goals.length >= 1 then + return .some .subGoals + let proof ← instantiateMVars (.mvar mid) + match Kernel.check (← getEnv) {} proof with + | Except.ok autoProofType => + match Kernel.isDefEq (← getEnv) {} autoProofType ci.type with + | Except.ok true => return .some .success + | _ => return .some .typeUnequal + | Except.error _ => return .some .typeCheckFail + | .inr e => return .some (.exception e) + let coreAction : CoreM (Option Result) := metaAction.run' + let ioAction : IO (Option Result × _) := coreAction.toIO {fileName := path.toString, fileMap := FileMap.ofString input } { env := st₁.commandState.env } + do + return (← ioAction).fst) + let #[result] := results + | throwError "{decl_name%} :: Unexpected error" + return result + +end EvalAuto diff --git a/Auto/EvaluateAuto/ConstAnalysis.lean b/Auto/EvaluateAuto/ConstAnalysis.lean index b9ed36c..c732453 100644 --- a/Auto/EvaluateAuto/ConstAnalysis.lean +++ b/Auto/EvaluateAuto/ConstAnalysis.lean @@ -50,6 +50,17 @@ def allHumanTheorems : CoreM (Array Name) := do let allHumanTheorems ← allConsts.filterM Name.isHumanTheorem return Array.mk allHumanTheorems +def Name.isFromPackage (name : Name) (pkgPrefix : String) : CoreM Bool := do + let .some mod ← Lean.findModuleOf? name + | throwError "{decl_name%} :: Cannot find {name}" + return mod.components[0]? == .some (.str .anonymous pkgPrefix) + +def allHumanTheoremsFromPackage (pkgPrefix : String) : CoreM (Array Name) := do + let allConsts := (← getEnv).constants.toList.map Prod.fst + let allHumanTheoremsFromPackage ← allConsts.filterM (fun n => + return (← Name.isHumanTheorem n) && (← Name.isFromPackage n pkgPrefix)) + return Array.mk allHumanTheoremsFromPackage + /-- Return the theorems that occurs in an expression -/ def Expr.getUsedTheorems (e : Expr) : CoreM (Array Name) := e.getUsedConstants.filterM Name.isTheorem diff --git a/Auto/EvaluateAuto/EnvAnalysis.lean b/Auto/EvaluateAuto/EnvAnalysis.lean index d16437e..b1e5ad0 100644 --- a/Auto/EvaluateAuto/EnvAnalysis.lean +++ b/Auto/EvaluateAuto/EnvAnalysis.lean @@ -4,6 +4,15 @@ open Lean namespace EvalAuto +/-- + Suppose `env₂` is the environment after running several non-import + commands starting from `env₁`, then `Environment.newLocalConstants env₁ env₂` + returns the new `ConstantInfo`s added by these commands +-/ +def Environment.newLocalConstants (env₁ env₂ : Environment) := + env₂.constants.map₂.toArray.filterMap (fun (name, ci) => + if !env₁.constants.map₂.contains name then .some ci else .none) + def mathlibModules : CoreM (Array Name) := do let u := (← getEnv).header.moduleNames return u.filter (fun name => name.components[0]? == .some `Mathlib) diff --git a/Auto/EvaluateAuto/Result.lean b/Auto/EvaluateAuto/Result.lean new file mode 100644 index 0000000..126fbd9 --- /dev/null +++ b/Auto/EvaluateAuto/Result.lean @@ -0,0 +1,32 @@ +import Lean +open Lean + +namespace EvalAuto + +inductive Result + | success + | nonProp + | typeCheckFail + | typeUnequal + -- `auto` does not produce subgoals, but other tactics we test might (such as `simp`) + | subGoals + | exception (e : Exception) + +instance : ToMessageData Result where + toMessageData : Result → MessageData + | .success => "Result.success" + | .nonProp => "Result.nonProp" + | .typeCheckFail => "Result.typeCheckFail" + | .typeUnequal => "Result.typeUnequal" + | .subGoals => "Result.subGoals" + | .exception e => m!"Result.exception ::\n{e.toMessageData}" + +def Result.concise : Result → String +| .success => "S" +| .nonProp => "N" +| .typeCheckFail => "F" +| .typeUnequal => "U" +| .subGoals => "G" +| .exception _ => "E" + +end EvalAuto diff --git a/Auto/EvaluateAuto/TestCode.lean b/Auto/EvaluateAuto/TestCode.lean index 64c7801..6028c90 100644 --- a/Auto/EvaluateAuto/TestCode.lean +++ b/Auto/EvaluateAuto/TestCode.lean @@ -1,7 +1,9 @@ import Lean +import Auto.EvaluateAuto.Result import Auto.EvaluateAuto.ConstAnalysis import Auto.EvaluateAuto.EnvAnalysis import Auto.EvaluateAuto.NameArr +import Auto.EvaluateAuto.CommandAnalysis import Auto.Tactic open Lean Auto @@ -13,28 +15,6 @@ initialize namespace EvalAuto -inductive Result - | success - | nonProp - | typeCheckFail - | typeUnequal - | autoException (e : Exception) - -instance : ToMessageData Result where - toMessageData : Result → MessageData - | .success => "Result.success" - | .nonProp => "Result.nonProp" - | .typeCheckFail => "Result.typeCheckFail" - | .typeUnequal => "Result.typeUnequal" - | .autoException e => m!"Result.autoException ::\n{e.toMessageData}" - -def Result.concise : Result → String -| .success => "S" -| .nonProp => "N" -| .typeCheckFail => "F" -| .typeUnequal => "U" -| .autoException _ => "E" - inductive SolverConfig where | native | leanSmt @@ -102,7 +82,7 @@ private def runAutoOnAutoLemma (declName? : Option Name) (lem : Auto.Lemma) : Co | Except.ok true => return .success | _ => return .typeUnequal | Except.error _ => return .typeCheckFail - | .inr e => return .autoException e + | .inr e => return .exception e /-- Run `Lean-auto` on the type of ``name``, using premises collected From 77e3ee7c1c26192bb33096baacc3984c24df5198 Mon Sep 17 00:00:00 2001 From: PratherConid Date: Wed, 1 Jan 2025 00:43:50 +0800 Subject: [PATCH 2/4] align with tactic elaboration --- Auto/EvaluateAuto/TestCode.lean | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/Auto/EvaluateAuto/TestCode.lean b/Auto/EvaluateAuto/TestCode.lean index 6028c90..e5ec990 100644 --- a/Auto/EvaluateAuto/TestCode.lean +++ b/Auto/EvaluateAuto/TestCode.lean @@ -70,9 +70,11 @@ private def runAutoOnAutoLemma (declName? : Option Name) (lem : Auto.Lemma) : Co Meta.mkLambdaFVars #[negGoalFVar] proofOfFalse let goal := mkApp2 (.const ``Classical.byContradiction []) body negGoalImpFalse Meta.mkLambdaFVars bs goal + -- Align with tactic elaboration (see `Lean.Elab.Term.TermElabM.run`) + let metaContext : Meta.Context := { config := Elab.Term.setElabConfig {} } let result : Expr ⊕ Exception ← Lean.Core.tryCatchRuntimeEx - (do let autoProof ← Meta.MetaM.run' autoProofFn; return .inl autoProof) + (do let autoProof ← Meta.MetaM.run' autoProofFn (ctx := metaContext); return .inl autoProof) (fun e => return .inr e) match result with | .inl autoProof => From aefb5d1c50fcfc82821737815382f0e0f8171254 Mon Sep 17 00:00:00 2001 From: PratherConid Date: Wed, 1 Jan 2025 10:11:24 +0800 Subject: [PATCH 3/4] add type reduction feature --- Auto/Lib/MetaExtra.lean | 19 +++++++++++++++++++ Auto/Translation/LamReif.lean | 2 +- Auto/Translation/Monomorphization.lean | 13 +------------ Auto/Translation/Reduction.lean | 16 ++++++++++++++++ 4 files changed, 37 insertions(+), 13 deletions(-) diff --git a/Auto/Lib/MetaExtra.lean b/Auto/Lib/MetaExtra.lean index 149feb2..c0d5893 100644 --- a/Auto/Lib/MetaExtra.lean +++ b/Auto/Lib/MetaExtra.lean @@ -9,6 +9,25 @@ namespace Auto def Meta.isDefEqD (t s : Expr) : MetaM Bool := Meta.withDefault <| Meta.isDefEq t s +def Meta.whnfNondependentForall (e : Expr) : MetaM Expr := do + let e' ← Meta.whnf e + match e' with + | .forallE _ _ body _ => + if body.hasLooseBVar 0 then + return e + else + return e' + | _ => return e + +partial def Meta.normalizeNondependentForall (e : Expr) : MetaM Expr := do + let e' ← whnfNondependentForall e + match e' with + | .forallE name ty body bi => + let ty' ← normalizeNondependentForall ty + let body' ← normalizeNondependentForall body + return .forallE name ty' body' bi + | _ => return e + def Meta.withoutMVarAssignments (m : MetaM α) : MetaM α := do let mctx ← getMCtx Meta.withMCtx {mctx with eAssignment := {}, lAssignment := {}} m diff --git a/Auto/Translation/LamReif.lean b/Auto/Translation/LamReif.lean index f7ded10..6f71693 100644 --- a/Auto/Translation/LamReif.lean +++ b/Auto/Translation/LamReif.lean @@ -1011,7 +1011,7 @@ private def reifTypeAux : Expr → ReifM LamSort | e => processTypeExpr e def reifType (e : Expr) : ReifM LamSort := do - let e ← prepReduceExpr e + let e ← prepReduceTypeForall e reifTypeAux e def newTermExpr (e : Expr) : ReifM LamTerm := do diff --git a/Auto/Translation/Monomorphization.lean b/Auto/Translation/Monomorphization.lean index 9efed32..0b7b434 100644 --- a/Auto/Translation/Monomorphization.lean +++ b/Auto/Translation/Monomorphization.lean @@ -57,16 +57,6 @@ register_option auto.mono.termLikeDefEq.maxHeartbeats : Nat := { descr := "Heartbeats allocated to each unification of term-like expression" } -register_option auto.mono.tyRed.mode : Meta.TransparencyMode := { - defValue := .reducible - descr := "Transparency level used when reducing types" -} - -register_option auto.mono.tyDefEq.mode : Meta.TransparencyMode := { - defValue := .default - descr := "Transparency level used when testing definitional equality of types" -} - namespace Auto inductive MonoMode where @@ -842,8 +832,7 @@ namespace FVarRep /-- Return : (reduce(e), whether reduce(e) contain bfvars) -/ def processType (e : Expr) : FVarRepM (Expr × Bool) := do - let mode := auto.mono.tyRed.mode.get (← getOptions) - let e ← MetaState.runMetaM <| prepReduceExprWithMode e mode + let e ← MetaState.runMetaM <| prepReduceTypeForall e let bfvarSet ← getBfvarSet -- If `e` contains no bound variables if !e.hasAnyFVar bfvarSet.contains then diff --git a/Auto/Translation/Reduction.lean b/Auto/Translation/Reduction.lean index 7a0f3c0..2707a46 100644 --- a/Auto/Translation/Reduction.lean +++ b/Auto/Translation/Reduction.lean @@ -1,5 +1,6 @@ import Lean import Auto.Lib.ExprExtra +import Auto.Lib.MetaExtra open Lean Meta private instance : ToString TransparencyMode where @@ -23,6 +24,16 @@ register_option auto.redMode : TransparencyMode := { descr := "TransparencyMode used when reducing collected facts" } +register_option auto.mono.tyRed.mode : Meta.TransparencyMode := { + defValue := .reducible + descr := "Transparency level used when reducing types. The default mode `reducible` does nothing." +} + +register_option auto.mono.tyDefEq.mode : Meta.TransparencyMode := { + defValue := .default + descr := "Transparency level used when testing definitional equality of types" +} + namespace Auto def unfoldProj (e : Expr) : MetaM Expr := @@ -79,4 +90,9 @@ def prepReduceDefeq (type : Expr) : MetaM (Option Expr) := do let eq' := Lean.mkApp3 (.const ``Eq lvls) ty lhs rhs return .some (← mkForallFVars xs eq') +def prepReduceTypeForall (e : Expr) : MetaM Expr := do + let e ← prepReduceExpr e + let mode := auto.mono.tyRed.mode.get (← getOptions) + Meta.withTransparency mode <| Meta.normalizeNondependentForall e + end Auto From 21e487c185e44bf30205f6995ac5462d40139f8d Mon Sep 17 00:00:00 2001 From: PratherConid Date: Wed, 1 Jan 2025 10:34:21 +0800 Subject: [PATCH 4/4] add initialize check --- Auto/EvaluateAuto/CommandAnalysis.lean | 2 ++ 1 file changed, 2 insertions(+) diff --git a/Auto/EvaluateAuto/CommandAnalysis.lean b/Auto/EvaluateAuto/CommandAnalysis.lean index 01c0d2c..019fd79 100644 --- a/Auto/EvaluateAuto/CommandAnalysis.lean +++ b/Auto/EvaluateAuto/CommandAnalysis.lean @@ -54,6 +54,8 @@ open Elab Tactic in def runTacticAtConstantDeclaration (name : Name) (searchPath : SearchPath) (tactic : ConstantInfo → TacticM Unit) : CoreM Result := do + if ← isInitializerExecutionEnabled then + throwError "{decl_name%} :: Running this function with execution of `initialize` code enabled is unsafe" let .some modName ← Lean.findModuleOf? name | throwError "{decl_name%} :: Cannot find constant {name}" let .some uri ← Server.documentUriFromModule searchPath modName