Preprocessing options now include full, none, and monomorphization only

Duper/Rules/FalseElim.lean

@@ -81,4 +81,4 @@ def falseElim (given : Clause) (c : MClause) (cNum : Nat) : RuleM (Array ClauseS
       streams := streams.append str
   return streams
 
-end Duper
+end Duper

Duper/Tactic.lean

@@ -158,7 +158,7 @@ def parseConfigOptions (configOptionsStx : TSyntaxArray `Duper.configOption) : T
   let mut portfolioModeOpt : Option Bool := none
   let mut portfolioInstanceOpt : Option Nat := none
   let mut inhabitationReasoningOpt : Option Bool := none
-  let mut monomorphizationOpt : Option Bool := none
+  let mut preprocessingOpt : Option PreprocessingOption := none
   let mut includeExpensiveRulesOpt : Option Bool := none
   let mut selFunctionOpt : Option Nat := none
   for configOptionStx in configOptionsStx do
@@ -182,11 +182,11 @@ def parseConfigOptions (configOptionsStx : TSyntaxArray `Duper.configOption) : T
         throwError "Erroneous invocation of duper: The inhabitation reasoning option has been specified multiple times"
       let inhabitationReasoning ← elabBoolLit inhabitationReasoningStx
       inhabitationReasoningOpt := some inhabitationReasoning
-    | `(configOption| monomorphization := $monomorphizationStx:Duper.bool_lit) =>
-      if monomorphizationOpt.isSome then
-        throwError "Erroneous invocation of duper: The monomorphization option has been specified multiple times"
-      let monomorphization ← elabBoolLit monomorphizationStx
-      monomorphizationOpt := some monomorphization
+    | `(configOption| preprocessing := $preprocessingStx:Duper.preprocessing_option) =>
+      if preprocessingOpt.isSome then
+        throwError "Erroneous invocation of duper: The preprocessing option has been specified multiple times"
+      let preprocessing ← elabPreprocessingOption preprocessingStx
+      preprocessingOpt := some preprocessing
     | `(configOption| includeExpensiveRules := $includeExpensiveRulesStx:Duper.bool_lit) =>
       if includeExpensiveRulesOpt.isSome then
         throwError "Erroneous invocation of duper: The includeExpensiveRules option has been specified multiple times"
@@ -212,13 +212,13 @@ def parseConfigOptions (configOptionsStx : TSyntaxArray `Duper.configOption) : T
       if portfolioMode then none -- If portfolio mode is enabled then no portfolio instance should be specified
       else some 0 -- If portfolio mode was explicitly disabled and no portfolio instance was specified, choose instance 0 by default
   if portfolioInstance != none && portfolioInstance != some 0 then
-    if inhabitationReasoningOpt.isSome || monomorphizationOpt.isSome || includeExpensiveRulesOpt.isSome then
+    if inhabitationReasoningOpt.isSome || preprocessingOpt.isSome || includeExpensiveRulesOpt.isSome then
       IO.println s!"Warning: The specified portfolio instance {portfolioInstance.get!} will override all additional configuration options"
   return {
     portfolioMode := portfolioMode,
     portfolioInstance := portfolioInstance,
     inhabitationReasoning := inhabitationReasoningOpt,
-    monomorphization := monomorphizationOpt,
+    preprocessing := preprocessingOpt,
     includeExpensiveRules := includeExpensiveRulesOpt,
     selFunction := selFunctionOpt
   }
@@ -253,8 +253,9 @@ def evalDuper : Tactic
     let lctxAfterIntros ← getLCtx
     let goalDecls := getGoalDecls lctxBeforeIntros lctxAfterIntros
     let formulas ← collectAssumptions facts factsContainsDuperStar goalDecls
+    let declName? ← Elab.Term.getDeclName? -- Needed for `Auto.monoPrepInterface`
     if configOptions.portfolioMode then
-      let proof ← runDuperPortfolioMode formulas configOptions none
+      let proof ← runDuperPortfolioMode formulas declName? configOptions none
       Lean.MVarId.assign (← getMainGoal) proof -- Apply the discovered proof to the main goal
       IO.println s!"Constructed proof. Time: {(← IO.monoMsNow) - startTime}ms"
     else
@@ -265,24 +266,32 @@ def evalDuper : Tactic
       let proof ←
         match portfolioInstance with
         | 0 =>
-          runDuperInstance0 formulas 0 configOptions.inhabitationReasoning configOptions.monomorphization
+          runDuperInstance0 formulas declName? 0 configOptions.inhabitationReasoning configOptions.preprocessing
             configOptions.includeExpensiveRules configOptions.selFunction
-        | 1 => runDuperInstance1 formulas 0
-        | 2 => runDuperInstance2 formulas 0
-        | 3 => runDuperInstance3 formulas 0
-        | 4 => runDuperInstance4 formulas 0
-        | 5 => runDuperInstance5 formulas 0
-        | 6 => runDuperInstance6 formulas 0
-        | 7 => runDuperInstance7 formulas 0
-        | 8 => runDuperInstance8 formulas 0
-        | 9 => runDuperInstance9 formulas 0
-        | 10 => runDuperInstance10 formulas 0
-        | 11 => runDuperInstance11 formulas 0
-        | 12 => runDuperInstance12 formulas 0
-        | 13 => runDuperInstance13 formulas 0
-        | 14 => runDuperInstance14 formulas 0
-        | 15 => runDuperInstance15 formulas 0
-        | 16 => runDuperInstance16 formulas 0
+        | 1 => runDuperInstance1 formulas declName? 0
+        | 2 => runDuperInstance2 formulas declName? 0
+        | 3 => runDuperInstance3 formulas declName? 0
+        | 4 => runDuperInstance4 formulas declName? 0
+        | 5 => runDuperInstance5 formulas declName? 0
+        | 6 => runDuperInstance6 formulas declName? 0
+        | 7 => runDuperInstance7 formulas declName? 0
+        | 8 => runDuperInstance8 formulas declName? 0
+        | 9 => runDuperInstance9 formulas declName? 0
+        | 10 => runDuperInstance10 formulas declName? 0
+        | 11 => runDuperInstance11 formulas declName? 0
+        | 12 => runDuperInstance12 formulas declName? 0
+        | 13 => runDuperInstance13 formulas declName? 0
+        | 14 => runDuperInstance14 formulas declName? 0
+        | 15 => runDuperInstance15 formulas declName? 0
+        | 16 => runDuperInstance16 formulas declName? 0
+        | 17 => runDuperInstance17 formulas declName? 0
+        | 18 => runDuperInstance18 formulas declName? 0
+        | 19 => runDuperInstance19 formulas declName? 0
+        | 20 => runDuperInstance20 formulas declName? 0
+        | 21 => runDuperInstance21 formulas declName? 0
+        | 22 => runDuperInstance22 formulas declName? 0
+        | 23 => runDuperInstance23 formulas declName? 0
+        | 24 => runDuperInstance24 formulas declName? 0
         | _ => throwError "Portfolio instance {portfolioInstance} not currently defined"
       Lean.MVarId.assign (← getMainGoal) proof -- Apply the discovered proof to the main goal
       IO.println s!"Constructed proof. Time: {(← IO.monoMsNow) - startTime}ms"
@@ -300,8 +309,9 @@ def evalDuperTrace : Tactic
     let lctxAfterIntros ← withMainContext getLCtx
     let goalDecls := getGoalDecls lctxBeforeIntros lctxAfterIntros
     let formulas ← collectAssumptions facts factsContainsDuperStar goalDecls
+    let declName? ← Elab.Term.getDeclName? -- Needed for `Auto.monoPrepInterface`
     if configOptions.portfolioMode then
-      let proof ← runDuperPortfolioMode formulas configOptions (some (duperStxRef, ← getRef, facts, factsContainsDuperStar))
+      let proof ← runDuperPortfolioMode formulas declName? configOptions (some (duperStxRef, ← getRef, facts, factsContainsDuperStar))
       Lean.MVarId.assign (← getMainGoal) proof -- Apply the discovered proof to the main goal
       IO.println s!"Constructed proof. Time: {(← IO.monoMsNow) - startTime}ms"
     else
@@ -312,19 +322,36 @@ def evalDuperTrace : Tactic
       let proof ←
         match portfolioInstance with
         | 0 =>
-          runDuperInstance0 formulas 0 configOptions.inhabitationReasoning configOptions.monomorphization
+          runDuperInstance0 formulas declName? 0 configOptions.inhabitationReasoning configOptions.preprocessing
             configOptions.includeExpensiveRules configOptions.selFunction
-        | 1 => runDuperInstance1 formulas 0
-        | 2 => runDuperInstance2 formulas 0
-        | 3 => runDuperInstance3 formulas 0
-        | 4 => runDuperInstance4 formulas 0
-        | 5 => runDuperInstance5 formulas 0
-        | 6 => runDuperInstance6 formulas 0
-        | 7 => runDuperInstance7 formulas 0
+        | 1 => runDuperInstance1 formulas declName? 0
+        | 2 => runDuperInstance2 formulas declName? 0
+        | 3 => runDuperInstance3 formulas declName? 0
+        | 4 => runDuperInstance4 formulas declName? 0
+        | 5 => runDuperInstance5 formulas declName? 0
+        | 6 => runDuperInstance6 formulas declName? 0
+        | 7 => runDuperInstance7 formulas declName? 0
+        | 8 => runDuperInstance8 formulas declName? 0
+        | 9 => runDuperInstance9 formulas declName? 0
+        | 10 => runDuperInstance10 formulas declName? 0
+        | 11 => runDuperInstance11 formulas declName? 0
+        | 12 => runDuperInstance12 formulas declName? 0
+        | 13 => runDuperInstance13 formulas declName? 0
+        | 14 => runDuperInstance14 formulas declName? 0
+        | 15 => runDuperInstance15 formulas declName? 0
+        | 16 => runDuperInstance16 formulas declName? 0
+        | 17 => runDuperInstance17 formulas declName? 0
+        | 18 => runDuperInstance18 formulas declName? 0
+        | 19 => runDuperInstance19 formulas declName? 0
+        | 20 => runDuperInstance20 formulas declName? 0
+        | 21 => runDuperInstance21 formulas declName? 0
+        | 22 => runDuperInstance22 formulas declName? 0
+        | 23 => runDuperInstance23 formulas declName? 0
+        | 24 => runDuperInstance24 formulas declName? 0
         | _ => throwError "Portfolio instance {portfolioInstance} not currently defined"
       Lean.MVarId.assign (← getMainGoal) proof -- Apply the discovered proof to the main goal
       mkDuperCallSuggestion duperStxRef (← getRef) facts factsContainsDuperStar portfolioInstance configOptions.inhabitationReasoning
-        configOptions.monomorphization configOptions.includeExpensiveRules configOptions.selFunction
+        configOptions.preprocessing configOptions.includeExpensiveRules configOptions.selFunction
       IO.println s!"Constructed proof. Time: {(← IO.monoMsNow) - startTime}ms"
 | _ => throwUnsupportedSyntax
 

DuperOnMathlib/DuperOnMathlib/DuperInterface.lean

@@ -11,11 +11,11 @@ def Auto.duperRaw (lemmas : Array Lemma) : MetaM Expr := do
 def Auto.duperPort (lemmas : Array Lemma) : MetaM Expr := do
   let lemmas : Array (Expr × Expr × Array Name) ← lemmas.mapM
     (fun ⟨proof, ty, _⟩ => do return (ty, ← Meta.mkAppM ``eq_true #[proof], #[]))
-  runDuperPortfolioMode lemmas.data
+  runDuperPortfolioMode lemmas.data .none
     { portfolioMode := true,
       portfolioInstance := none,
       inhabitationReasoning := none,
-      monomorphization := false, -- It would be redundant to enable monomorphization for Auto
+      preprocessing := PreprocessingOption.NoPreprocessing, -- It would be redundant to enable Auto's preprocessing for Auto calls
       includeExpensiveRules := none,
       selFunction := none
     }

DuperOnMathlib/DuperOnMathlib/Function.lean

@@ -44,23 +44,26 @@ example : f '' s ⊆ v ↔ s ⊆ f ⁻¹' v := by
 
 -- Zipperposition (non-portfolio): 541 iterations and 1.345s
 example : f '' s ⊆ v ↔ s ⊆ f ⁻¹' v := by
-  auto [subset_def, mem_image, mem_preimage] -- Universe polymorphic skolem issue?
+  duper [subset_def, mem_image, mem_preimage]
 
 example (h : Injective f) : f ⁻¹' (f '' s) ⊆ s := by
   rintro x ⟨y, ys, fxeq⟩
   rw [← h fxeq]
   exact ys
 
 example (h : Injective f) : f ⁻¹' (f '' s) ⊆ s := by
-  auto [subset_def, mem_preimage, Injective.mem_set_image, h]
+  duper [subset_def, mem_preimage, Injective.mem_set_image, h]
 
 example : f '' (f ⁻¹' u) ⊆ u := by
   rintro y ⟨x, xmem, rfl⟩
   exact xmem
 
 -- Zipperposition (non-portfolio): 27 iterations in 0.083s
+-- TODO: Figure out why auto can solve this with maxHeartbeats 1000000 and kStep 100 but duper can't
+set_option maxHeartbeats 1000000 in
+set_option kStep 100 in
 example : f '' (f ⁻¹' u) ⊆ u := by
-  auto [subset_def, mem_image, mem_preimage] -- Universe polymorphic skolem issue?
+  auto [subset_def, mem_image, mem_preimage]
 
 example (h : Surjective f) : u ⊆ f '' (f ⁻¹' u) := by
   intro y yu
@@ -74,26 +77,26 @@ example (h : Surjective f) : u ⊆ f '' (f ⁻¹' u) := by
 
 -- Zipperposition (non-portfolio): ResourceOut
 example (h : Surjective f) : u ⊆ f '' (f ⁻¹' u) := by
-  auto [subset_def, mem_image, mem_preimage, h]
+  duper [subset_def, mem_image, mem_preimage, h]
 
 example (h : s ⊆ t) : f '' s ⊆ f '' t := by
   rintro y ⟨x, xs, fxeq⟩
   use x, h xs
 
 -- Zipperposition (non-portfolio): 73 iterations in 0.138s
 example (h : s ⊆ t) : f '' s ⊆ f '' t := by
-  auto [subset_def, mem_image, h] -- Universe polymorphic skolem issue?
+  duper [subset_def, mem_image, h]
 
 example (h : u ⊆ v) : f ⁻¹' u ⊆ f ⁻¹' v := by
   intro x; apply h
 
 example (h : u ⊆ v) : f ⁻¹' u ⊆ f ⁻¹' v := by
-  auto [subset_def, mem_preimage, h]
+  duper [subset_def, mem_preimage, h]
 
 example : f ⁻¹' (u ∪ v) = f ⁻¹' u ∪ f ⁻¹' v := rfl
 
 example : f ⁻¹' (u ∪ v) = f ⁻¹' u ∪ f ⁻¹' v := by
-  ext x; auto [mem_union, mem_preimage]
+  ext x; duper [mem_union, mem_preimage]
 
 example : f '' (s ∩ t) ⊆ f '' s ∩ f '' t := by
   rintro y ⟨x, ⟨xs, xt⟩, rfl⟩
@@ -103,7 +106,7 @@ example : f '' (s ∩ t) ⊆ f '' s ∩ f '' t := by
 
 -- Zipperposition (non-portfolio): ResourceOut
 example : f '' (s ∩ t) ⊆ f '' s ∩ f '' t := by
-  auto [mem_inter_iff, subset_def, mem_image]
+  duper [mem_inter_iff, subset_def, mem_image]
 
 example (h : Injective f) : f '' s ∩ f '' t ⊆ f '' (s ∩ t) := by
   rintro y ⟨⟨x₁, x₁s, rfl⟩, ⟨x₂, x₂t, fx₂eq⟩⟩
@@ -116,13 +119,13 @@ example (h : Injective f) : f '' s ∩ f '' t ⊆ f '' (s ∩ t) := by
 
 -- Zipperposition (non-portfolio): ResourceOut
 example : f '' s \ f '' t ⊆ f '' (s \ t) := by
-  intro x; auto [mem_image, mem_diff]
+  intro x; duper [mem_image, mem_diff]
 
 example : f ⁻¹' u \ f ⁻¹' v ⊆ f ⁻¹' (u \ v) :=
   fun x ↦ id
 
 example : f ⁻¹' u \ f ⁻¹' v ⊆ f ⁻¹' (u \ v) := by
-  intro x; auto [mem_preimage, mem_diff]
+  intro x; duper [mem_preimage, mem_diff]
 
 example : f '' s ∩ v = f '' (s ∩ f ⁻¹' v) := by
   ext y; constructor
@@ -133,21 +136,22 @@ example : f '' s ∩ v = f '' (s ∩ f ⁻¹' v) := by
 
 -- Zipperposition (non-portfolio): ResourceOut
 example : f '' s ∩ v = f '' (s ∩ f ⁻¹' v) := by
-  ext y; auto [mem_inter_iff, mem_image, mem_preimage]
+  ext y; duper [mem_inter_iff, mem_image, mem_preimage]
 
 example : f '' (s ∩ f ⁻¹' u) ⊆ f '' s ∩ u := by
   rintro y ⟨x, ⟨xs, fxu⟩, rfl⟩
   exact ⟨⟨x, xs, rfl⟩, fxu⟩
 
 -- Zipperposition (non-portfolio): ResourceOut
 example : f '' (s ∩ f ⁻¹' u) ⊆ f '' s ∩ u := by
-  intro x; auto [mem_inter_iff, mem_image, mem_preimage]
+  intro x; duper [mem_inter_iff, mem_image, mem_preimage]
 
 example : s ∩ f ⁻¹' u ⊆ f ⁻¹' (f '' s ∩ u) := by
   rintro x ⟨xs, fxu⟩
   exact ⟨⟨x, xs, rfl⟩, fxu⟩
 
 -- Zipperposition (non-portfolio): 870 iterations in 1.644s
+-- TODO: Figure out why auto can solve this with maxHeartbeats 800000 but Duper can't
 set_option maxHeartbeats 800000 in -- Corresponds to 200000 heartbeats if portfolio mode were disabled
 example : s ∩ f ⁻¹' u ⊆ f ⁻¹' (f '' s ∩ u) := by
   intro x; auto [mem_inter_iff, mem_image, mem_preimage]
@@ -159,6 +163,7 @@ example : s ∪ f ⁻¹' u ⊆ f ⁻¹' (f '' s ∪ u) := by
   right; exact fxu
 
 -- Zipperposition (non-portfolio): 387 iterations in 0.638s
+-- TODO: Figure out why auto can solve this with maxHeartbeats 800000 but Duper can't
 set_option maxHeartbeats 800000 in -- Corresponds to 200000 heartbeats if portfolio mode were disabled
 example : s ∪ f ⁻¹' u ⊆ f ⁻¹' (f '' s ∪ u) := by
   intro x; auto [mem_union, mem_image, mem_preimage]
@@ -174,7 +179,7 @@ example : (f '' ⋃ i, A i) = ⋃ i, f '' A i := by
   exact ⟨x, ⟨i, xAi⟩, fxeq⟩
 
 example : (f '' ⋃ i, A i) = ⋃ i, f '' A i := by
-  ext y; simp; apply Iff.intro <;> auto
+  ext y; simp; apply Iff.intro <;> duper
 
 example : (f '' ⋂ i, A i) ⊆ ⋂ i, f '' A i := by
   intro y; simp
@@ -183,7 +188,7 @@ example : (f '' ⋂ i, A i) ⊆ ⋂ i, f '' A i := by
   exact ⟨h i, fxeq⟩
 
 example : (f '' ⋂ i, A i) ⊆ ⋂ i, f '' A i := by
-  intro y; simp; auto
+  intro y; simp; duper
 
 example (i : I) (injf : Injective f) : (⋂ i, f '' A i) ⊆ f '' ⋂ i, A i := by
   intro y; simp
@@ -199,7 +204,7 @@ example (i : I) (injf : Injective f) : (⋂ i, f '' A i) ⊆ f '' ⋂ i, A i :=
   exact fxeq
 
 example (i : I) (injf : Injective f) : (⋂ i, f '' A i) ⊆ f '' ⋂ i, A i := by
-  intro y; simp; auto [injf] d[Injective]
+  intro y; simp; duper [injf, Injective]
 
 example : (f ⁻¹' ⋃ i, B i) = ⋃ i, f ⁻¹' B i := by
   ext x
@@ -235,15 +240,15 @@ example : Injective f ↔ LeftInverse (inverse f) f :=
 -- Encounters a proof reconstruction error when monomorphization is enabled
 example : Injective f ↔ LeftInverse (inverse f) f := by
   dsimp [Injective, LeftInverse]
-  duper [inverse_spec] {monomorphization := false}
+  duper [inverse_spec] {preprocessing := no_preprocessing}
 
 example : Surjective f ↔ RightInverse (inverse f) f :=
   ⟨fun h y ↦ inverse_spec _ (h _), fun h y ↦ ⟨inverse f y, h _⟩⟩
 
 -- Zipperposition (non-portfolio): ResourceOut
 example : Surjective f ↔ RightInverse (inverse f) f := by
   dsimp [Surjective, Function.RightInverse, LeftInverse]
-  auto [inverse_spec]
+  duper [inverse_spec]
 
 end
 
@@ -267,6 +272,6 @@ theorem Cantor' : ∀ f : α → Set α, ¬Surjective f := by
   intro f surjf
   let S := { i | i ∉ f i }
   have s_spec : ∀ i, i ∈ S ↔ i ∉ f i := by intros; rfl
-  auto [surjf S, s_spec]
+  duper [surjf S, s_spec]
 
 end

DuperOnMathlib/DuperOnMathlib/Prime.lean

@@ -10,7 +10,7 @@ set_option auto.tptp.solver.name "zipperposition"
 
 theorem prime_def_lt_DUPER {p : ℕ} : Prime p ↔ 2 ≤ p ∧ ∀ m < p, m ∣ p → m = 1 := by
   have : 2 ≤ p → 0 < p := by intro; linarith
-  duper [*, Nat.prime_def_lt'', Nat.le_of_dvd, Nat.lt_of_le_of_ne, Nat.lt_irrefl]
+  duper [*, Nat.prime_def_lt'', Nat.le_of_dvd, Nat.lt_of_le_of_ne, Nat.lt_irrefl] {portfolioInstance := 1}
 
 #check Nat.prime_def_lt' -- Reproving this theorem using duper:
 
@@ -33,7 +33,6 @@ theorem prime_def_le_sqrt_DUPER' {p : ℕ} : Prime p ↔ 2 ≤ p ∧ ∀ m, 2 
     rw [prime_def_lt']
     refine ⟨h.1, ?_⟩
     have h₂ : ∀ m, 2 ≤ m → m < p → m ∣ p → 2 ≤ (p / m) := by
-      duper [*, Nat.lt_irrefl, Nat.dvd_iff_div_mul_eq, Nat.mul_zero, Nat.one_mul, two_le_iff] {portfolioInstance := 0}
-    duper
-      [*, Nat.div_dvd_of_dvd, Nat.dvd_iff_div_mul_eq, le_sqrt, Nat.mul_le_mul_right, Nat.mul_le_mul_left, mul_comm, Nat.le_total]
-      {portfolioInstance := 0}
+      duper [*, Nat.lt_irrefl, Nat.dvd_iff_div_mul_eq, Nat.mul_zero, Nat.one_mul, two_le_iff] {portfolioInstance := 1}
+    duper [*, Nat.div_dvd_of_dvd, Nat.dvd_iff_div_mul_eq, le_sqrt, Nat.mul_le_mul_right,
+      Nat.mul_le_mul_left, mul_comm, Nat.le_total] {portfolioInstance := 1}

DuperOnMathlib/DuperOnMathlib/Prime2.lean

@@ -1,7 +1,7 @@
 import Duper.Tactic
 import Mathlib.Data.Nat.Prime
 
-set_option includeHoistRules false
+set_option includeExpensiveRules false
 
 /- Duper can solve this theorem when `preprocessFact` in Util.Reduction.lean is disabled (set to the identity function).
    When `preprocessFact` runs as it usually does, Duper times out when attempting to solve this theorem. Previously,