Dev

Duper/TPTPParser/PrattParser.lean

@@ -43,7 +43,7 @@ def tokenPrefixes : Std.HashSet String :=
   Std.HashSet.emptyWithCapacity.insertMany $ tokens.flatMap (fun t => Id.run do
     let mut res := []
     let mut pref := ""
-    for c in t.data do
+    for c in t.toList do
       pref := pref.push c
       res := pref :: res
     return res
@@ -88,7 +88,7 @@ def finalizeToken : TokenizerM Unit := do
     setStatus .default
 
 def tokenizeAux (str : String) : TokenizerM Unit := do
-  for char in str.data do
+  for char in str.toList do
     match ← getStatus with
     | .default =>
       if char.isWhitespace then
@@ -105,7 +105,7 @@ def tokenizeAux (str : String) : TokenizerM Unit := do
         setStatus .comment
       else if tokenPrefixes.contains ((← getCurrToken).push char) then
         addToCurrToken char
-      else if tokenPrefixes.contains ([char].asString) then
+      else if tokenPrefixes.contains (String.ofList [char]) then
         finalizeToken
         addToCurrToken char
       else throw $ IO.userError s!"Invalid token: {char}"
@@ -493,7 +493,7 @@ partial def collectConstantsOfCmd (topLevel : Bool) (acc : Std.HashMap String Ex
   match t with
   | ⟨.ident n, as⟩ => do
     let acc ← as.foldlM (collectConstantsOfCmd false) acc
-    if n.data[0]!.isLower && n.data[0]! != '$' && !acc.contains n
+    if n.toList[0]!.isLower && n.toList[0]! != '$' && !acc.contains n
     then
       let ty ← as.foldlM
         (fun acc _ => mkArrow (mkConst `Iota) acc)

Duper/Tests/temp2.lean

@@ -10,6 +10,7 @@ set_option auto.native true
 
 open Lean Auto
 
+/-
 @[rebind Auto.Native.solverFunc]
 def Auto.duperPort (lemmas inhLemmas : Array Lemma) : MetaM Expr := do
   let formulas ← Duper.autoLemmasToFormulas lemmas
@@ -23,6 +24,7 @@ def Auto.duperPort (lemmas inhLemmas : Array Lemma) : MetaM Expr := do
       selFunction := none
     }
     .none
+-/
 
 inductive myType
 | const1 : myType
@@ -115,3 +117,21 @@ theorem exists₂_comm
     {ι₁ ι₂ : Sort} {κ₁ : ι₁ → Sort} {κ₂ : ι₂ → Sort} {p : ∀ i₁, κ₁ i₁ → ∀ i₂, κ₂ i₂ → Prop} :
     (∃ i₁ j₁ i₂ j₂, p i₁ j₁ i₂ j₂) ↔ ∃ i₂ j₂ i₁ j₁, p i₁ j₁ i₂ j₂ := by
   duper [*] {preprocessing := no_preprocessing}
+
+--------------------------------------------------------------------
+
+set_option trace.duper.printProof true in
+set_option trace.duper.proofReconstruction true in
+set_option trace.duper.saturate.debug true in
+set_option trace.duper.rule.superposition true in
+-- set_option trace.duper.prover.saturate true in
+set_option enableSuperpositionWatchClauses true in
+set_option superpositionWatchClause1 4 in
+set_option superpositionWatchClause2 5 in
+example (f : Nat → Prop) (h1 : ∀ x : Nat, f (x + x)) (h2 : ¬ f (1 + 1)) : False := by
+  duper [*] {portfolioInstance := 1} -- {preprocessing := no_preprocessing} works
+
+-- In the above example, Duper fails to perform an inference that it ought to be able to perform
+-- First reason: superposition inference is not performed due to condition 7
+-- Second reason: After disabling the above check, Duper never reaches "Inside yC for..." line. This seems like a bug to me, but will
+-- require more investigation.

README.md

@@ -7,7 +7,7 @@ Duper is an automatic proof-producing theorem prover broadly similar to Isabelle
 To use Duper in an existing Lean 4 project, first add this package as a dependency. In your lakefile.lean, add:
 
 ```lean
-require Duper from git "https://github.com/leanprover-community/duper.git" @ "v4.25.2"
+require Duper from git "https://github.com/leanprover-community/duper.git" @ "v4.26.0"
 ```
 
 Then, make sure that your `lean-toolchain` file contains the same version of Lean 4 as Duper and that if your project imports [batteries](https://github.com/leanprover-community/batteries), then it uses the same version of batteries as Duper. This step is necessary because Duper depends on batteries, so errors can arise if your project attempts to import a version of batteries different from the one imported by Duper.

lake-manifest.json

@@ -5,20 +5,20 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "ffad3f5b7ebe1ac3e09779ec8a863a5138c1246c",
+   "rev": "24241822ef9d3e7f6a3bcc53ad136e12663db8f3",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.25.1",
+   "inputRev": "v4.26.0",
    "inherited": false,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/lean-auto.git",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "e1ef2099e666103b85cd099a1ab5086ede15e7c0",
+   "rev": "6e66058117f0d073914c2c1f674b880537d9eb2e",
    "name": "auto",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.25.2-hammer",
+   "inputRev": "v4.26.0-hammer",
    "inherited": false,
    "configFile": "lakefile.lean"}],
  "name": "Duper",

lakefile.lean

@@ -2,8 +2,8 @@ import Lake
 
 open Lake DSL
 
-require auto from git "https://github.com/leanprover-community/lean-auto.git"@"v4.25.2-hammer"
-require batteries from git "https://github.com/leanprover-community/batteries" @ "v4.25.1"
+require auto from git "https://github.com/leanprover-community/lean-auto.git"@"v4.26.0-hammer"
+require batteries from git "https://github.com/leanprover-community/batteries" @ "v4.26.0"
 
 package Duper {
   precompileModules := true

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.25.2
+leanprover/lean4:v4.26.0