From eed2d390e27f9aeb5f18ecb19f23ccd11a8a1e1e Mon Sep 17 00:00:00 2001
From: JOSHCLUNE <josh.seth.clune@gmail.com>
Date: Sun, 13 Oct 2024 22:06:50 -0400
Subject: [PATCH 1/6] Update lean-auto

---
 Duper/Tests/temp.lean | 1 +
 lake-manifest.json    | 4 ++--
 lakefile.lean         | 2 +-
 3 files changed, 4 insertions(+), 3 deletions(-)

diff --git a/Duper/Tests/temp.lean b/Duper/Tests/temp.lean
index bd2be0a..6d97f20 100644
--- a/Duper/Tests/temp.lean
+++ b/Duper/Tests/temp.lean
@@ -13,6 +13,7 @@ open Lean Auto
 @[rebind Auto.Native.solverFunc]
 def Auto.duperPort (lemmas : Array Lemma) : MetaM Expr := do
   let formulas ← Duper.autoLemmasToFormulas lemmas
+  let formulas := formulas.map (fun f => (f.1, f.2.1, f.2.2.1, f.2.2.2, none))
   Duper.runDuperPortfolioMode formulas .none
     { portfolioMode := true,
       portfolioInstance := none,
diff --git a/lake-manifest.json b/lake-manifest.json
index 2931a0e..b5554af 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -5,10 +5,10 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "2b6ed7d9f86d558d94b8d9036a637395163c4fa6",
+   "rev": "6cd81c96800dc2d2741499e931f350f069ca74c7",
    "name": "auto",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "2b6ed7d9f86d558d94b8d9036a637395163c4fa6",
+   "inputRev": "6cd81c96800dc2d2741499e931f350f069ca74c7",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/batteries",
diff --git a/lakefile.lean b/lakefile.lean
index 12b68d4..5a6007e 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -2,7 +2,7 @@ import Lake
 
 open Lake DSL
 
-require auto from git "https://github.com/leanprover-community/lean-auto.git"@"2b6ed7d9f86d558d94b8d9036a637395163c4fa6"
+require auto from git "https://github.com/leanprover-community/lean-auto.git"@"6cd81c96800dc2d2741499e931f350f069ca74c7"
 require batteries from git "https://github.com/leanprover-community/batteries" @ "v4.11.0"
 
 package Duper {

From a0afb1ecb87048bce820dde4e572e423ac3eb09f Mon Sep 17 00:00:00 2001
From: JOSHCLUNE <josh.seth.clune@gmail.com>
Date: Mon, 14 Oct 2024 21:37:10 -0400
Subject: [PATCH 2/6] Add ignoreUnusableFact option

---
 Duper/Tactic.lean | 34 +++++++++++++++++++++++++++++-----
 1 file changed, 29 insertions(+), 5 deletions(-)

diff --git a/Duper/Tactic.lean b/Duper/Tactic.lean
index 50da552..bdb7ec0 100644
--- a/Duper/Tactic.lean
+++ b/Duper/Tactic.lean
@@ -10,6 +10,11 @@ register_option duper.printTimeInformation : Bool := {
   descr := "Whether to print the total time it took for Duper to construct a proof"
 }
 
+register_option duper.ignoreUnusableFacts : Bool := {
+  defValue := false
+  descr := "If true, suppresses the error that Duper would throw if given a fact it would not ordinarily accept (e.g. a constructor or opaque constant)"
+}
+
 def getPrintTimeInformation (opts : Options) : Bool :=
   duper.printTimeInformation.get opts
 
@@ -17,6 +22,13 @@ def getPrintTimeInformationM : CoreM Bool := do
   let opts ← getOptions
   return getPrintTimeInformation opts
 
+def getIgnoreUsableFacts (opts : Options) : Bool :=
+  duper.ignoreUnusableFacts.get opts
+
+def getIgnoreUsableFactsM : CoreM Bool := do
+  let opts ← getOptions
+  return getIgnoreUsableFacts opts
+
 /-- Produces definional equations for a recursor `recVal` such as
 
   `@Nat.rec m z s (Nat.succ n) = s n (@Nat.rec m z s n)`
@@ -80,11 +92,21 @@ def elabFact (stx : Term) : TacticM (Array (Expr × Expr × Array Name)) := do
         return ret
       | some (.axiomInfo _)  => return #[← elabFactAux stx]
       | some (.thmInfo _)    => return #[← elabFactAux stx]
-      | some (.opaqueInfo _) => throwError "Opaque constants cannot be provided as facts"
-      | some (.quotInfo _)   => throwError "Quotient constants cannot be provided as facts"
-      | some (.inductInfo _) => throwError "Inductive types cannot be provided as facts"
-      | some (.ctorInfo _)   => throwError "Constructors cannot be provided as facts"
-      | none                 => throwError "Unknown constant {id}"
+      | some (.opaqueInfo _) =>
+        if ← getIgnoreUsableFactsM then return #[]
+        else throwError "Opaque constants cannot be provided as facts"
+      | some (.quotInfo _)   =>
+        if ← getIgnoreUsableFactsM then return #[]
+        else throwError "Quotient constants cannot be provided as facts"
+      | some (.inductInfo _) =>
+        if ← getIgnoreUsableFactsM then return #[]
+        else throwError "Inductive types cannot be provided as facts"
+      | some (.ctorInfo _)   =>
+        if ← getIgnoreUsableFactsM then return #[]
+        else throwError "Constructors cannot be provided as facts"
+      | none                 =>
+        if ← getIgnoreUsableFactsM then return #[]
+        else throwError "Unknown constant {id}"
     | .fvar exprFVarId =>
       match (← getLCtx).find? exprFVarId with
       | some _ => return #[← elabFactAux stx]
@@ -129,6 +151,8 @@ def collectAssumptions (facts : Array Term) (withAllLCtx : Bool) (goalDecls : Ar
       if ← isProp fact then
         let fact ← preprocessFact (← instantiateMVars fact)
         formulas := (fact, ← mkAppM ``eq_true #[proof], params, false, some factStx) :: formulas
+      else if ← getIgnoreUsableFactsM then
+        continue
       else
         throwError "Invalid fact {factStx} for duper. Proposition expected"
   return formulas

From e68416d3af6385760265c2fa13ee58b9b2b13972 Mon Sep 17 00:00:00 2001
From: JOSHCLUNE <josh.seth.clune@gmail.com>
Date: Mon, 14 Oct 2024 21:52:29 -0400
Subject: [PATCH 3/6] ignoreUsableFacts option bug fix

---
 Duper/Tactic.lean | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/Duper/Tactic.lean b/Duper/Tactic.lean
index bdb7ec0..8d47837 100644
--- a/Duper/Tactic.lean
+++ b/Duper/Tactic.lean
@@ -67,7 +67,8 @@ def elabFact (stx : Term) : TacticM (Array (Expr × Expr × Array Name)) := do
   match stx with
   | `($id:ident) =>
     let some expr ← Term.resolveId? id
-      | throwError "Unknown identifier {id}"
+      | if ← getIgnoreUsableFactsM then return #[]
+        else throwError "Unknown identifier {id}"
     match expr with
     | .const exprConstName _ =>
       match (← getEnv).find? exprConstName with

From fdb2ab35ea29a08d07e71b1be8f910f2a68686da Mon Sep 17 00:00:00 2001
From: JOSHCLUNE <josh.seth.clune@gmail.com>
Date: Sun, 20 Oct 2024 21:54:36 -0400
Subject: [PATCH 4/6] Update lean-auto

---
 Duper/Interface.lean | 8 ++++----
 lake-manifest.json   | 4 ++--
 lakefile.lean        | 2 +-
 3 files changed, 7 insertions(+), 7 deletions(-)

diff --git a/Duper/Interface.lean b/Duper/Interface.lean
index c08dbe8..51f7f52 100644
--- a/Duper/Interface.lean
+++ b/Duper/Interface.lean
@@ -454,8 +454,8 @@ def runDuperInstanceWithMonomorphization (formulas : List (Expr × Expr × Array
   -- Calling Auto.unfoldConstAndPreprocessLemma is an essential step for the monomorphization procedure
   let lemmas ← lemmas.mapM (m:=MetaM) (Auto.unfoldConstAndPreprocessLemma #[])
   let inhFacts ← Auto.Inhabitation.getInhFactsFromLCtx
-  let prover : Array Auto.Lemma → MetaM Expr :=
-    fun lemmas => do
+  let prover : Array Auto.Lemma → Array Auto.Lemma → MetaM Expr :=
+    fun lemmas inhLemmas => do
       let monomorphizedFormulas ← autoLemmasToFormulas lemmas
       trace[duper.monomorphization.debug] "Original formulas: {formulas.map (fun f => (f.1, f.2.2.2))}"
       trace[duper.monomorphization.debug] "Auto lemmas: {lemmas.map (fun l => (l.type, l.proof, l.deriv))}"
@@ -471,8 +471,8 @@ def runDuperInstanceWithFullPreprocessing (formulas : List (Expr × Expr × Arra
   -- Calling Auto.unfoldConstAndPreprocessLemma is an essential step for the monomorphization procedure
   let lemmas ← lemmas.mapM (m:=MetaM) (Auto.unfoldConstAndPreprocessLemma #[])
   let inhFacts ← Auto.Inhabitation.getInhFactsFromLCtx
-  let prover : Array Auto.Lemma → MetaM Expr :=
-    fun lemmas => do
+  let prover : Array Auto.Lemma → Array Auto.Lemma → MetaM Expr :=
+    fun lemmas inhLemmas => do
       let monomorphizedFormulas ← autoLemmasToFormulas lemmas
       trace[duper.monomorphization.debug] "Original formulas: {formulas.map (fun f => (f.1, f.2.2.2))}"
       trace[duper.monomorphization.debug] "Auto lemmas: {lemmas.map (fun l => (l.type, l.proof, l.deriv))}"
diff --git a/lake-manifest.json b/lake-manifest.json
index b5554af..36f26d3 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -5,10 +5,10 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "6cd81c96800dc2d2741499e931f350f069ca74c7",
+   "rev": "5149acf1aaa07a62a53a7e0979ff79d85812287d",
    "name": "auto",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "6cd81c96800dc2d2741499e931f350f069ca74c7",
+   "inputRev": "5149acf1aaa07a62a53a7e0979ff79d85812287d",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/batteries",
diff --git a/lakefile.lean b/lakefile.lean
index 5a6007e..2b75ff5 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -2,7 +2,7 @@ import Lake
 
 open Lake DSL
 
-require auto from git "https://github.com/leanprover-community/lean-auto.git"@"6cd81c96800dc2d2741499e931f350f069ca74c7"
+require auto from git "https://github.com/leanprover-community/lean-auto.git"@"5149acf1aaa07a62a53a7e0979ff79d85812287d"
 require batteries from git "https://github.com/leanprover-community/batteries" @ "v4.11.0"
 
 package Duper {

From 25c3ea88da2505158998eea07f40b07c0cdfe5ba Mon Sep 17 00:00:00 2001
From: JOSHCLUNE <josh.seth.clune@gmail.com>
Date: Thu, 24 Oct 2024 00:40:44 -0400
Subject: [PATCH 5/6] Update to lean v4.12.0

---
 Duper/Fingerprint.lean                       | 2 +-
 Duper/Rules/SyntacticTautologyDeletion3.lean | 6 +++---
 Duper/Tactic.lean                            | 2 +-
 lake-manifest.json                           | 8 ++++----
 lakefile.lean                                | 4 ++--
 lean-toolchain                               | 2 +-
 6 files changed, 12 insertions(+), 12 deletions(-)

diff --git a/Duper/Fingerprint.lean b/Duper/Fingerprint.lean
index 9838178..c8cf282 100644
--- a/Duper/Fingerprint.lean
+++ b/Duper/Fingerprint.lean
@@ -113,7 +113,7 @@ def emptyCFP : ClauseFingerprintTrie := mkEmptyWithDepth numFingerprintFeatures
    I could be quite off-base on that. -/
 structure RootCFPTrie where
   root : ClauseFingerprintTrie := emptyCFP
-  filterSet : HashSet Clause := {} -- Keeps track of the set of clauses that should be filtered out (i.e. "removed" clauses)
+  filterSet : Std.HashSet Clause := {} -- Keeps track of the set of clauses that should be filtered out (i.e. "removed" clauses)
 deriving Inhabited
 
 namespace RootCFPTrie
diff --git a/Duper/Rules/SyntacticTautologyDeletion3.lean b/Duper/Rules/SyntacticTautologyDeletion3.lean
index 1e09121..bf366aa 100644
--- a/Duper/Rules/SyntacticTautologyDeletion3.lean
+++ b/Duper/Rules/SyntacticTautologyDeletion3.lean
@@ -10,8 +10,8 @@ open SimpResult
     duper often gets cluttered with clauses of the form "x = True ∨ x = False". Neither syntacticTautologyDeletion1 nor
     syntacticTautologyDeletion2 remove clauses of this form, so that is what syntacticTautologyDeletion3 targets. -/
 def syntacticTautologyDeletion3 : MSimpRule := fun c => do
-  let mut eqTrueSet : HashSet Lean.Expr := mkHashSet -- Stores Lean expressions equated to True in c
-  let mut eqFalseSet : HashSet Lean.Expr := mkHashSet -- Stores Lean expressions equated to False in c
+  let mut eqTrueSet : Std.HashSet Lean.Expr := Std.HashSet.empty -- Stores Lean expressions equated to True in c
+  let mut eqFalseSet : Std.HashSet Lean.Expr := Std.HashSet.empty -- Stores Lean expressions equated to False in c
   for lit in c.lits do
     if lit.sign then
       if lit.rhs == mkConst ``True then
@@ -41,4 +41,4 @@ def syntacticTautologyDeletion3 : MSimpRule := fun c => do
         else eqTrueSet := eqTrueSet.insert lit.rhs
   return none
 
-end Duper
\ No newline at end of file
+end Duper
diff --git a/Duper/Tactic.lean b/Duper/Tactic.lean
index 8d47837..71d74bb 100644
--- a/Duper/Tactic.lean
+++ b/Duper/Tactic.lean
@@ -87,7 +87,7 @@ def elabFact (stx : Term) : TacticM (Array (Expr × Expr × Array Name)) := do
         if sort.isProp then
           ret := ret.push (← elabFactAux stx)
         -- Generate definitional equation for the fact
-        if let some eqns ← getEqnsFor? exprConstName (nonRec := true) then
+        if let some eqns ← getEqnsFor? exprConstName then
           ret := ret.append (← eqns.mapM fun eq => do elabFactAux (← `($(mkIdent eq))))
         trace[duper.elabFact.debug] "Adding definition {expr} as the following facts: {ret.map (fun x => x.1)}"
         return ret
diff --git a/lake-manifest.json b/lake-manifest.json
index 36f26d3..3a19deb 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -5,20 +5,20 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "5149acf1aaa07a62a53a7e0979ff79d85812287d",
+   "rev": "680d6d58ce2bb65d15e5711d93111b2e5b22cb1a",
    "name": "auto",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "5149acf1aaa07a62a53a7e0979ff79d85812287d",
+   "inputRev": "680d6d58ce2bb65d15e5711d93111b2e5b22cb1a",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/batteries",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "9c6c2d647e57b2b7a0b42dd8080c698bd33a1b6f",
+   "rev": "4756e0fc48acce0cc808df0ad149de5973240df6",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.11.0",
+   "inputRev": "v4.12.0",
    "inherited": false,
    "configFile": "lakefile.lean"}],
  "name": "Duper",
diff --git a/lakefile.lean b/lakefile.lean
index 2b75ff5..9416246 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -2,8 +2,8 @@ import Lake
 
 open Lake DSL
 
-require auto from git "https://github.com/leanprover-community/lean-auto.git"@"5149acf1aaa07a62a53a7e0979ff79d85812287d"
-require batteries from git "https://github.com/leanprover-community/batteries" @ "v4.11.0"
+require auto from git "https://github.com/leanprover-community/lean-auto.git"@"680d6d58ce2bb65d15e5711d93111b2e5b22cb1a"
+require batteries from git "https://github.com/leanprover-community/batteries" @ "v4.12.0"
 
 package Duper {
   precompileModules := true
diff --git a/lean-toolchain b/lean-toolchain
index 5a9c76d..8998520 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.11.0
+leanprover/lean4:v4.12.0

From a500ea7a5b9eca0ecaa7b4a229786a61b2707d30 Mon Sep 17 00:00:00 2001
From: JOSHCLUNE <josh.seth.clune@gmail.com>
Date: Thu, 31 Oct 2024 00:44:36 -0400
Subject: [PATCH 6/6] Update lean-auto

---
 Duper/Tests/temp.lean  | 2 +-
 Duper/Tests/temp2.lean | 2 +-
 lake-manifest.json     | 4 ++--
 lakefile.lean          | 2 +-
 4 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/Duper/Tests/temp.lean b/Duper/Tests/temp.lean
index 6d97f20..d08366c 100644
--- a/Duper/Tests/temp.lean
+++ b/Duper/Tests/temp.lean
@@ -11,7 +11,7 @@ set_option auto.native true
 open Lean Auto
 
 @[rebind Auto.Native.solverFunc]
-def Auto.duperPort (lemmas : Array Lemma) : MetaM Expr := do
+def Auto.duperPort (lemmas inhLemmas : Array Lemma) : MetaM Expr := do
   let formulas ← Duper.autoLemmasToFormulas lemmas
   let formulas := formulas.map (fun f => (f.1, f.2.1, f.2.2.1, f.2.2.2, none))
   Duper.runDuperPortfolioMode formulas .none
diff --git a/Duper/Tests/temp2.lean b/Duper/Tests/temp2.lean
index 88c52f7..f00a418 100644
--- a/Duper/Tests/temp2.lean
+++ b/Duper/Tests/temp2.lean
@@ -11,7 +11,7 @@ set_option auto.native true
 open Lean Auto
 
 @[rebind Auto.Native.solverFunc]
-def Auto.duperPort (lemmas : Array Lemma) : MetaM Expr := do
+def Auto.duperPort (lemmas inhLemmas : Array Lemma) : MetaM Expr := do
   let formulas ← Duper.autoLemmasToFormulas lemmas
   let formulas := formulas.map (fun f => (f.1, f.2.1, f.2.2.1, f.2.2.2, none))
   Duper.runDuperPortfolioMode formulas .none
diff --git a/lake-manifest.json b/lake-manifest.json
index 3a19deb..585682b 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -5,10 +5,10 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "680d6d58ce2bb65d15e5711d93111b2e5b22cb1a",
+   "rev": "0728f384d78982e6fb0f1cdf263e172d3135e0be",
    "name": "auto",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "680d6d58ce2bb65d15e5711d93111b2e5b22cb1a",
+   "inputRev": "0728f384d78982e6fb0f1cdf263e172d3135e0be",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/batteries",
diff --git a/lakefile.lean b/lakefile.lean
index 9416246..3cd8544 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -2,7 +2,7 @@ import Lake
 
 open Lake DSL
 
-require auto from git "https://github.com/leanprover-community/lean-auto.git"@"680d6d58ce2bb65d15e5711d93111b2e5b22cb1a"
+require auto from git "https://github.com/leanprover-community/lean-auto.git"@"0728f384d78982e6fb0f1cdf263e172d3135e0be"
 require batteries from git "https://github.com/leanprover-community/batteries" @ "v4.12.0"
 
 package Duper {