Merge pull request #39 from leanprover-community/main

Update duper2 to match main
leanprover-community · Dec 29, 2024 · b63cdd0 · b63cdd0
2 parents 4d73b99 + d627c4c
commit b63cdd0
Show file tree

Hide file tree

Showing 9 changed files with 279 additions and 123 deletions.
diff --git a/Auto/EvaluateAuto/TestCode.lean b/Auto/EvaluateAuto/TestCode.lean
@@ -28,6 +28,13 @@ instance : ToMessageData Result where
   | .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
@@ -123,6 +130,7 @@ def runAutoOnConsts (config : EvalConfig) (names : Array Name) : CoreM Unit := d
   if let .some fhandle := logFileHandle then
     fhandle.putStrLn s!"Config = {config}"
   let startTime ← IO.monoMsNow
+  let mut results := #[]
   for name in names do
     let ci ← Name.getCi name decl_name%
     trace[auto.eval.printProblem] m!"Testing || {name} : {ci.type}"
@@ -164,11 +172,15 @@ def runAutoOnConsts (config : EvalConfig) (names : Array Name) : CoreM Unit := d
             | .vampire        => auto.tptp.vampire.path.set o path) <|
               runAutoOnConst name
     trace[auto.eval.printResult] m!"{result}"
+    results := results.push result
     if let .some fhandle := logFileHandle then
       fhandle.putStrLn (toString (← MessageData.format m!"{result}"))
   if let .some fhandle := logFileHandle then
     fhandle.putStrLn ""
     fhandle.putStrLn s!"Elapsed time: {(← IO.monoMsNow) - startTime} ms"
+    fhandle.putStrLn s!"\nSummary:\n"
+    for ((name, result), idx) in (names.zip results).zipWithIndex do
+      fhandle.putStrLn s!"{idx} {result.concise} {name}"
 
 def namesFileEval (cfg : EvalConfig) (fname : String) : CoreM Unit := do
   let names ← NameArray.load fname

diff --git a/Auto/Lib/ExprExtra.lean b/Auto/Lib/ExprExtra.lean
@@ -231,29 +231,33 @@ def Expr.whnfIfNotForall (e : Expr) : MetaM Expr := do
     return (← Meta.whnf e)
 
 /--
-  Given expression `e₁, e₂`, attempt to find variables `x₁, ⋯, xₗ`,
-  terms `t₁, ⋯, tₖ` and a `m ≤ l` such that `∀ x₁ ⋯ xₗ. e₁ x₁ ⋯ xₘ = e₂ t₁ ⋯ tₖ`
+  Given expression `e₁, e₂` where `e₁` have universe level parameters
+  `params`, attempt to find variables `x₁, ⋯, xₗ`,
+  terms `t₁, ⋯, tₖ` and a `m ≤ l` such that `∀ x₁ ⋯ xₗ. e₁ t₁ ⋯ tₖ = e₂ x₁ ⋯ xₘ`
   Note that universe polymorphism is not supported
 
   If successful, return
-    `(fun x₁ ⋯ xₗ => Eq.refl (e₁ x₁ ⋯ xₘ), ∀ x₁ ⋯ xₗ. e₁ x₁ ⋯ xₘ = e₂ t₁ ⋯ tₖ)`\
+    `(fun x₁ ⋯ xₗ => Eq.refl (e₂ x₁ ⋯ xₘ), ∀ x₁ ⋯ xₗ. e₁ t₁ ⋯ tₖ = e₂ x₁ ⋯ xₘ)`\
   Otherwise, return `.none`
 -/
-def Expr.instanceOf? (e₁ e₂ : Expr) : MetaM (Option (Expr × Expr)) := do
+def Expr.instanceOf? (e₁ : Expr) (params : Array Name) (e₂ : Expr) : MetaM (Option (Expr × Expr × Array Name)) := do
+  let e₁ := e₁.instantiateLevelParamsArray params (← params.mapM (fun _ => Meta.mkFreshLevelMVar))
   let ty₁ ← Meta.inferType e₁
   let ty₂ ← Meta.inferType e₂
-  Meta.forallTelescope ty₁ fun xs _ => do
-    let (ms, _, _) ← Meta.forallMetaTelescope ty₂
-    let e₁app := mkAppN e₁ xs
-    let e₂app := mkAppN e₂ ms
+  Meta.forallTelescope ty₂ fun xs _ => do
+    let (ms, _, _) ← Meta.forallMetaTelescope ty₁
+    let e₁app := mkAppN e₁ ms
+    let e₂app := mkAppN e₂ xs
+    if !(← Meta.isDefEq (← Meta.inferType e₁app) (← Meta.inferType e₂app)) then
+      return .none
     if ← Meta.isDefEq e₁app e₂app then
-      let e₂app ← instantiateMVars e₂app
-      let (e₂app, s) := AbstractMVars.abstractExprMVars e₂app { mctx := (← getMCtx), lctx := (← getLCtx), ngen := (← getNGen)}
+      let e₁app ← instantiateMVars e₁app
+      let (e₁app, s) := AbstractMVars.abstractExprMVars e₁app { mctx := (← getMCtx), lctx := (← getLCtx), ngen := (← getNGen)}
       setNGen s.ngen; setMCtx s.mctx
       Meta.withLCtx s.lctx (← Meta.getLocalInstances) <| do
-        let proof ← Meta.mkLambdaFVars (xs ++ s.fvars) (← Meta.mkAppM ``Eq.refl #[e₁app])
+        let proof ← Meta.mkLambdaFVars (xs ++ s.fvars) (← Meta.mkAppM ``Eq.refl #[e₂app])
         let eq ← Meta.mkForallFVars (xs ++ s.fvars) (← Meta.mkAppM ``Eq #[e₁app, e₂app])
-        return (proof, eq)
+        return (proof, eq, s.paramNames)
     else
       return .none
 

diff --git a/Auto/Lib/MetaExtra.lean b/Auto/Lib/MetaExtra.lean
@@ -103,4 +103,24 @@ def Meta.isTypeCorrectCore (e : Expr) : MetaM Bool := do
   let type? ← Meta.coreCheck e
   return type?.isSome
 
+def Meta.withMaxHeartbeats [Monad m] [MonadLiftT BaseIO m]
+    [MonadWithReaderOf Core.Context m] (n : Nat) (x : m α) : m α := do
+  let numHeartbeats ← IO.getNumHeartbeats
+  let f s := {
+    s with
+    initHeartbeats := numHeartbeats
+    maxHeartbeats := n * 1000
+  }
+  withReader f x
+
+def Meta.exToExcept (x : MetaM α) : MetaM (Except Exception α) :=
+  try
+    let v ← x
+    return .ok v
+  catch e =>
+    return .error e
+
+def Meta.runtimeExToExcept (x : MetaM α) : MetaM (Except Exception α) :=
+  tryCatchRuntimeEx (do let v ← x; return .ok v) (fun e => return .error e)
+
 end Auto
diff --git a/Auto/Lib/MetaState.lean b/Auto/Lib/MetaState.lean
@@ -105,6 +105,9 @@ def isDefEq (t s : Expr) : MetaStateM Bool := runMetaM (Meta.isDefEq t s)
 
 def isDefEqRigid (t s : Expr) : MetaStateM Bool := runMetaM (Meta.withNewMCtxDepth (Meta.isDefEq s t))
 
+def isDefEqRigidWith (t s : Expr) (mode : Meta.TransparencyMode) : MetaStateM Bool :=
+  runMetaM (Meta.withTransparency mode <| Meta.withNewMCtxDepth (Meta.isDefEq s t))
+
 def isLevelDefEq (u v : Level) : MetaStateM Bool := runMetaM (Meta.isLevelDefEq u v)
 
 def isLevelDefEqRigid (u v : Level) : MetaStateM Bool := runMetaM (Meta.withNewMCtxDepth (Meta.isLevelDefEq u v))

diff --git a/Auto/Tactic.lean b/Auto/Tactic.lean
@@ -658,56 +658,57 @@ def queryNative
   Run `auto`'s monomorphization and preprocessing, then send the problem to different solvers
 -/
 def runAuto
-  (declName? : Option Name) (lemmas : Array Lemma) (inhFacts : Array Lemma) : MetaM Expr := do
-  traceLemmas `auto.runAuto.printLemmas s!"All lemmas received by {decl_name%}:" lemmas
-  -- Simplify `ite`
-  let ite_simp_lem ← Lemma.ofConst ``Auto.Bool.ite_simp (.leaf "hw Auto.Bool.ite_simp")
-  let lemmas ← lemmas.mapM (fun lem => Lemma.rewriteUPolyRigid lem ite_simp_lem)
-  -- Simplify `cond`
-  let cond_simp_lem ← Lemma.ofConst ``Auto.Bool.cond_simp (.leaf "hw Auto.Bool.cond_simp")
-  let lemmas ← lemmas.mapM (fun lem => Lemma.rewriteUPolyRigid lem cond_simp_lem)
-  -- Simplify `decide`
-  let decide_simp_lem ← Lemma.ofConst ``Auto.Bool.decide_simp (.leaf "hw Auto.Bool.decide_simp")
-  let lemmas ← lemmas.mapM (fun lem => Lemma.rewriteUPolyRigid lem decide_simp_lem)
-  let afterReify (uvalids : Array UMonoFact) (uinhs : Array UMonoFact) (minds : Array (Array SimpleIndVal)) : LamReif.ReifM Expr := (do
-    let exportFacts ← LamReif.reifFacts uvalids
-    let mut exportFacts := exportFacts.map (Embedding.Lam.REntry.valid [])
-    let _ ← LamReif.reifInhabitations uinhs
-    let exportInhs := (← LamReif.getRst).nonemptyMap.toArray.map
-      (fun (s, _) => Embedding.Lam.REntry.nonempty s)
-    let exportInds ← LamReif.reifMutInds minds
-    LamReif.printValuation
-    -- **Preprocessing in Verified Checker**
-    let (exportFacts', exportInds) ← LamReif.preprocess exportFacts exportInds
-    exportFacts := exportFacts'
-    -- **TPTP invocation and Premise Selection**
-    if auto.tptp.get (← getOptions) then
-      let (proof, unsatCore) ← queryTPTP exportFacts
-      if let .some proof := proof then
-        return proof
-      let premiseSel? := auto.tptp.premiseSelection.get (← getOptions)
-      if premiseSel? then
-        if let .some unsatCore := unsatCore then
-          exportFacts := unsatCore
-    -- **SMT**
-    if auto.smt.get (← getOptions) then
-      let (proof, _) ← querySMT exportFacts exportInds
-      if let .some proof := proof then
-        return proof
-    -- **Native Prover**
-    exportFacts := exportFacts.append (← LamReif.auxLemmas exportFacts)
-    if auto.native.get (← getOptions) then
-      if let .some proof ← queryNative declName? exportFacts exportInhs then
-        return proof
-    throwError "Auto failed to find proof"
-    )
-  let (proof, _) ← Monomorphization.monomorphize lemmas inhFacts (@id (Reif.ReifM Expr) do
-    let s ← get
-    let u ← computeMaxLevel s.facts
-    (afterReify s.facts s.inhTys s.inds).run' {u := u})
-  trace[auto.tactic] "Auto found proof of {← Meta.inferType proof}"
-  trace[auto.tactic.printProof] "{proof}"
-  return proof
+  (declName? : Option Name) (lemmas : Array Lemma) (inhFacts : Array Lemma) : MetaM Expr :=
+  Meta.withDefault do
+    traceLemmas `auto.runAuto.printLemmas s!"All lemmas received by {decl_name%}:" lemmas
+    -- Simplify `ite`
+    let ite_simp_lem ← Lemma.ofConst ``Auto.Bool.ite_simp (.leaf "hw Auto.Bool.ite_simp")
+    let lemmas ← lemmas.mapM (fun lem => Lemma.rewriteUPolyRigid lem ite_simp_lem)
+    -- Simplify `cond`
+    let cond_simp_lem ← Lemma.ofConst ``Auto.Bool.cond_simp (.leaf "hw Auto.Bool.cond_simp")
+    let lemmas ← lemmas.mapM (fun lem => Lemma.rewriteUPolyRigid lem cond_simp_lem)
+    -- Simplify `decide`
+    let decide_simp_lem ← Lemma.ofConst ``Auto.Bool.decide_simp (.leaf "hw Auto.Bool.decide_simp")
+    let lemmas ← lemmas.mapM (fun lem => Lemma.rewriteUPolyRigid lem decide_simp_lem)
+    let afterReify (uvalids : Array UMonoFact) (uinhs : Array UMonoFact) (minds : Array (Array SimpleIndVal)) : LamReif.ReifM Expr := (do
+      let exportFacts ← LamReif.reifFacts uvalids
+      let mut exportFacts := exportFacts.map (Embedding.Lam.REntry.valid [])
+      let _ ← LamReif.reifInhabitations uinhs
+      let exportInhs := (← LamReif.getRst).nonemptyMap.toArray.map
+        (fun (s, _) => Embedding.Lam.REntry.nonempty s)
+      let exportInds ← LamReif.reifMutInds minds
+      LamReif.printValuation
+      -- **Preprocessing in Verified Checker**
+      let (exportFacts', exportInds) ← LamReif.preprocess exportFacts exportInds
+      exportFacts := exportFacts'
+      -- **TPTP invocation and Premise Selection**
+      if auto.tptp.get (← getOptions) then
+        let (proof, unsatCore) ← queryTPTP exportFacts
+        if let .some proof := proof then
+          return proof
+        let premiseSel? := auto.tptp.premiseSelection.get (← getOptions)
+        if premiseSel? then
+          if let .some unsatCore := unsatCore then
+            exportFacts := unsatCore
+      -- **SMT**
+      if auto.smt.get (← getOptions) then
+        let (proof, _) ← querySMT exportFacts exportInds
+        if let .some proof := proof then
+          return proof
+      -- **Native Prover**
+      exportFacts := exportFacts.append (← LamReif.auxLemmas exportFacts)
+      if auto.native.get (← getOptions) then
+        if let .some proof ← queryNative declName? exportFacts exportInhs then
+          return proof
+      throwError "Auto failed to find proof"
+      )
+    let (proof, _) ← Monomorphization.monomorphize lemmas inhFacts (@id (Reif.ReifM Expr) do
+      let s ← get
+      let u ← computeMaxLevel s.facts
+      (afterReify s.facts s.inhTys s.inds).run' {u := u})
+    trace[auto.tactic] "Auto found proof of {← Meta.inferType proof}"
+    trace[auto.tactic.printProof] "{proof}"
+    return proof
 
 @[tactic auto]
 def evalAuto : Tactic