Merge pull request #11 from leanprover-community/dev

Dev

Duper/Fingerprint.lean

@@ -157,7 +157,7 @@ def transformToUntypedFirstOrderTerm [Monad m] [MonadLiftT MetaM m] (e : Expr) :
      -/
     return .bvar bvarNum
   | Expr.mdata _ e => transformToUntypedFirstOrderTerm e
-  | Expr.letE _ _ _ _ _ => panic! "The letE expression {e} should have been removed by zeta reduction"
+  | Expr.letE _ _ _ _ _ => panic! s!"The letE expression {e} should have been removed by zeta reduction"
   -- Strip away levels
   | Expr.const name _ => return Expr.const name []
   | _ => return e -- Expr.fvar, Expr.mvar, Expr.lit, Expr.const, and Expr.sort cases

Duper/Util/Reduction.lean

@@ -44,11 +44,12 @@ partial def preprocessFact (fact : Expr) : MetaM Expr := do
     -- Restore ≠, i.e., ¬ a = b ⇒ a ≠ b
     -- If we don't do this, it seems that clausification will become more inefficient
     let fact ← Core.transform fact (pre := restoreNE)
+    let fact ← zetaReduce fact
     trace[duper.preprocessing.debug] "fact after preprocessing: {fact}"
     return fact
   else
-    trace[duper.preprocessing.debug] "Skipping preprocessing because reduceInstances option is set to false"
-    return fact
+    trace[duper.preprocessing.debug] "reduceInstances option is set to false, only applying zeta reduction"
+    zetaReduce fact
 
 /-- Eta-expand a beta-reduced expression. This function is currently unused -/
 partial def etaLong (e : Expr) : MetaM Expr := do
@@ -101,13 +102,13 @@ partial def etaReduce (e : Expr) : MetaM Expr := do
     | none => return .done e
   Meta.transform e (post := post) (usedLetOnly := true)
 
-/-- Instantiates mvars then applies beta, eta and zeta reduction exhaustively. -/
+/-- Instantiates mvars then applies beta and eta reduction exhaustively. -/
 def betaEtaReduceInstMVars (e : Expr) : MetaM Expr := do
   let e ← instantiateMVars e
   let e ← Core.betaReduce e
   etaReduce e
 
-/-- Applies beta, eta and zeta reduction exhaustively -/
+/-- Applies beta and eta reduction exhaustively -/
 def betaEtaReduce (e : Expr) : MetaM Expr := do
   let e ← Core.betaReduce e
   etaReduce e

lake-manifest.json

@@ -13,10 +13,10 @@
   {"url": "https://github.com/leanprover-community/lean-auto.git",
    "type": "git",
    "subDir": null,
-   "rev": "1507142f79f05371e5eb25202eec6396bb940d72",
+   "rev": "df285d9950123b2799ea71d9772d1a806f7d1e7a",
    "name": "auto",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "1507142f79f05371e5eb25202eec6396bb940d72",
+   "inputRev": "df285d9950123b2799ea71d9772d1a806f7d1e7a",
    "inherited": false,
    "configFile": "lakefile.lean"}],
  "name": "Duper",

lakefile.lean

@@ -2,7 +2,7 @@ import Lake
 
 open Lake DSL
 
-require auto from git "https://github.com/leanprover-community/lean-auto.git"@"1507142f79f05371e5eb25202eec6396bb940d72"
+require auto from git "https://github.com/leanprover-community/lean-auto.git"@"df285d9950123b2799ea71d9772d1a806f7d1e7a"
 
 package Duper {
   precompileModules := true