Merge pull request #40 from leanprover-community/main

Update duper2 branch to match main branch

Auto/EvaluateAuto/CommandAnalysis.lean

@@ -0,0 +1,98 @@
+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
+  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
+    | 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

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

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)

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

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
@@ -90,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 =>
@@ -102,7 +84,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

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

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

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
@@ -844,8 +834,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

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