Working on adding monomorphization to Duper

Duper/Interface.lean

@@ -1,5 +1,6 @@
 import Std.Lean.CoreM
 import Duper.ProofReconstruction
+import Auto.Tactic
 
 open Lean
 open Lean.Meta
@@ -167,6 +168,22 @@ def runDuper (formulas : List (Expr × Expr × Array Name)) (instanceMaxHeartbea
        determine whether Duper threw an error due to an actual problem or due to a timeout -/
     throwError "Prover was terminated."
 
+/- Note for converting between Duper's formulas format and Auto's lemmas format. If `hp : p`, then Duper stores the formula
+   `(p, eq_true hp, #[])` whereas Auto stores the lemma `⟨hp, p, #[]⟩`. Importantly, Duper stores the proof of `p = True` and
+   Auto stores the proof of `p`, so this must be accounted for in the conversion (maybe later, it will be good to refactor Duper
+   to be in alignment with how Auto stores lemmas to avoid the unnecessary cost of this conversion, but for now, it suffices to
+   add or remove `eq_true` as needed) -/
+
+/-- Converts formulas/lemmas from the format used by Duper to the format used by Auto. -/
+def formulasToAutoLemmas (formulas : List (Expr × Expr × Array Name)) : MetaM (Array Auto.Lemma) :=
+  formulas.toArray.mapM
+    (fun (fact, proof, params) =>
+      return {proof := ← Meta.mkAppM ``of_eq_true #[proof], type := fact, params := params})
+
+/-- Converts formulas/lemmas from the format used by Auto to the format used by Duper. -/
+def autoLemmasToFormulas (lemmas : Array Auto.Lemma) : MetaM (List (Expr × Expr × Array Name)) :=
+  lemmas.toList.mapM (fun lem => return (lem.type, ← Meta.mkAppM ``eq_true #[lem.proof], lem.params))
+
 /-- Default duper instance (does not modify any options except inhabitationReasoning if specified) -/
 def runDuperInstance0 (formulas : List (Expr × Expr × Array Name)) (inhabitationReasoning : Option Bool) (instanceMaxHeartbeats : Nat) : MetaM Expr :=
   match inhabitationReasoning with
@@ -203,6 +220,20 @@ def runDuperInstance5 (formulas : List (Expr × Expr × Array Name)) (inhabitati
   | none => withOptions (fun o => o.set `selFunction 1) $ runDuper formulas instanceMaxHeartbeats
   | some b => withOptions (fun o => (o.set `selFunction 1).set `inhabitationReasoning b) $ runDuper formulas instanceMaxHeartbeats
 
+/-- Default duper instance with monomorphization enabled. -/
+def runDuperInstance6 (formulas : List (Expr × Expr × Array Name)) (inhabitationReasoning : Option Bool) (instanceMaxHeartbeats : Nat) : MetaM Expr := do
+  let lemmas ← formulasToAutoLemmas formulas
+  -- 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 monomorphizedFormulas ← autoLemmasToFormulas lemmas
+      match inhabitationReasoning with
+      | none => runDuper monomorphizedFormulas instanceMaxHeartbeats
+      | some b => withOptions (fun o => o.set `inhabitationReasoning b) $ runDuper monomorphizedFormulas instanceMaxHeartbeats
+  Auto.monoInterface lemmas inhFacts prover
+
 declare_syntax_cat Duper.bool_lit (behavior := symbol)
 
 syntax "true" : Duper.bool_lit
@@ -245,6 +276,7 @@ def portfolioInstanceToConfigOptionStx [Monad m] [MonadError m] [MonadQuotation
   | 3 => `(configOption| portfolioInstance := 3)
   | 4 => `(configOption| portfolioInstance := 4)
   | 5 => `(configOption| portfolioInstance := 5)
+  | 6 => `(configOption| portfolioInstance := 6)
   | _ => throwError "Invalid Duper instance {n}"
 
 /-- Constructs and suggests the syntax for a duper call, for use with `duper?` -/

Duper/Tactic.lean

@@ -237,6 +237,8 @@ def evalDuper : Tactic
         | 2 => runDuperInstance2 formulas configOptions.inhabitationReasoning 0
         | 3 => runDuperInstance3 formulas configOptions.inhabitationReasoning 0
         | 4 => runDuperInstance4 formulas configOptions.inhabitationReasoning 0
+        | 5 => runDuperInstance5 formulas configOptions.inhabitationReasoning 0
+        | 6 => runDuperInstance6 formulas configOptions.inhabitationReasoning 0
         | _ => throwError "Portfolio instance {portfolioInstance} not currently defined. Please choose instance 0-4"
       Lean.MVarId.assign (← getMainGoal) proof -- Apply the discovered proof to the main goal
       IO.println s!"Constructed proof. Time: {(← IO.monoMsNow) - startTime}ms"
@@ -270,6 +272,8 @@ def evalDuperTrace : Tactic
         | 2 => runDuperInstance2 formulas configOptions.inhabitationReasoning 0
         | 3 => runDuperInstance3 formulas configOptions.inhabitationReasoning 0
         | 4 => runDuperInstance4 formulas configOptions.inhabitationReasoning 0
+        | 5 => runDuperInstance5 formulas configOptions.inhabitationReasoning 0
+        | 6 => runDuperInstance6 formulas configOptions.inhabitationReasoning 0
         | _ => throwError "Portfolio instance {portfolioInstance} not currently defined. Please choose instance 0-4"
       Lean.MVarId.assign (← getMainGoal) proof -- Apply the discovered proof to the main goal
       mkDuperCallSuggestion duperStxRef (← getRef) facts factsContainsDuperStar portfolioInstance configOptions.inhabitationReasoning

Duper/Tests/monobugs.lean

@@ -0,0 +1,73 @@
+import Duper.Tactic
+import Duper.TPTP
+import Auto.Tactic
+
+-- This file is for documenting bugs in Duper's current invocation of the monomorphization procedure.
+
+-- Note: This example fails if inhabitation reasoning is enabled (see bug 5 in bugs.lean) or if monomorphization is enabled
+example : ((∃ (A B : Type) (f : B → A) (x : B), f x = f x) = True) :=
+  by duper {portfolioInstance := 6, inhabitationReasoning := false}
+
+example : ((∃ (A B : Type) (f : B → A) (x : B), f x = f x) = True) :=
+  by duper {portfolioInstance := 1, inhabitationReasoning := false}
+
+-- allNative_direct :: Cannot find external proof of nonempty #0
+tptp SEU123 "../TPTP-v8.0.0/Problems/SEU/SEU123+1.p"
+  by duper [*] {portfolioInstance := 6}
+
+tptp SEU123_new "../TPTP-v8.0.0/Problems/SEU/SEU123+1.p"
+  by duper [*] {portfolioInstance := 1}
+
+-- unexpected bound variable #0
+theorem boolSimpRule27TestDep₁ (a b c y z r : Prop) (f : a ∧ b ∧ c → Prop) (h : ((x : a ∧ b ∧ c) → (y ∨ f x ∨ c ∨ z)) = r) : r :=
+  by duper [*] {portfolioInstance := 6}
+
+theorem boolSimpRule27TestDep₁_new (a b c y z r : Prop) (f : a ∧ b ∧ c → Prop) (h : ((x : a ∧ b ∧ c) → (y ∨ f x ∨ c ∨ z)) = r) : r :=
+  by duper [*] {portfolioInstance := 1}
+
+namespace NegativeBoolSimpTests
+
+axiom f.{u} : Sort u → Nat
+
+-- reifTermCheckType :: LamTerm (¬ ((!0 (∀ x0 : Nat, !1)) = (!0 (∀ x0 : Nat, !1)))) is not type correct
+def neg₁ : (f (Nat → Nat) = f (Nat → Nat)) := by duper {portfolioInstance := 6}
+
+def neg₁_new : (f (Nat → Nat) = f (Nat → Nat)) := by duper {portfolioInstance := 1}
+
+end NegativeBoolSimpTests
+
+axiom f.{u} : Type u → Prop
+
+axiom ftrue.{u} : f.{u} (Sort u)
+
+-- prover saturated
+def unitst₁ : f.{max u v} (Sort (max u v)) ∧ f.{v} (Sort v) := by
+  duper [ftrue] {portfolioInstance := 6}
+
+def unitst₁_new : f.{max u v} (Sort (max u v)) ∧ f.{v} (Sort v) := by
+  duper [ftrue] {portfolioInstance := 1}
+
+axiom fmoretrue.{u} : ∀ (x : Type u), f x
+
+-- prover saturated
+def unitst₂ : ∀ (x : Type v), f x := by
+  duper [fmoretrue] {portfolioInstance := 6}
+
+def unitst₂_new : ∀ (x : Type v), f x := by
+  duper [fmoretrue] {portfolioInstance := 1}
+
+axiom exftrue.{u} : ∃ (x : Type u), f x
+
+-- prover saturated
+def skuniverse.{u} : ∃ (x : Type u), f x := by
+  duper [exftrue] {portfolioInstance := 6}
+
+def skuniverse_new.{u} : ∃ (x : Type u), f x := by
+  duper [exftrue] {portfolioInstance := 1}
+
+-- prover saturated (presumably because monomorphization procedure doesn't use nonempty lemmas in the same way duper does)
+example (h : Nonempty (α → β)) : (∀ n : Nat, ∀ a : α, ∃ b : β, True) = True :=
+  by duper [h] {portfolioInstance := 6}
+
+example (h : Nonempty (α → β)) : (∀ n : Nat, ∀ a : α, ∃ b : β, True) = True :=
+  by duper [h] {portfolioInstance := 1}

Duper/Tests/test_regression.lean

@@ -465,16 +465,13 @@ example (f g : Nat → Nat) (h : ∀ a, ∃ d, f a = d) :
 set_option trace.Meta.debug true in
 example : ((∀ (f : Nat → Nat) (x : Nat), f x = f x) = True) := by duper
 
--- Duper cannot yet solve this example with inhabitation reasoning enabled because this example requires
--- inferring that type A is inhabited from the fact that type B is inhabited and there exists a function from B to A
-set_option inhabitationReasoning false in
+-- Note: This example fails if inhabitation reasoning is enabled (bug 5) or if monomorphization is enabled
 example : ((∃ (A B : Type) (f : B → A) (x : B), f x = f x) = True) :=
-  by duper
+  by duper {portfolioInstance := 1, inhabitationReasoning := false}
 
--- Duper cannot yet solve this example with inhabitation reasoning enabled for the same sort of reason as the above example
-set_option inhabitationReasoning false in
+-- Note: This example saturates if inhabitation reasoning is enabled, not sure why
 example : ∃ (A : Type) (B : A → Type) (f : ∀ (a : A), B a) (x : A), (f x = f x) = True :=
-  by duper
+  by duper {portfolioInstance := 1, inhabitationReasoning := false}
 
 example (A : Type) (x : A) : (∃ x : A, x = x) := by duper
 
@@ -640,10 +637,10 @@ instance : Add (Int → Int) := (⟨fun f g x => f x + g x⟩ : Add (Int → Int
 instance : Add (Nat → Nat) := (⟨fun f g x => f x + g x⟩ : Add (Nat → Nat))
 
 example (f : Int → Int) (hf : ∀ x, f (-x) = f x) : even_int_fun f := by -- The goal is the same as hf
-  duper [hf, even_int_fun]
+  duper [hf, even_int_fun] {portfolioInstance := 0} -- Times out in portfolio mode
 
 example (f : Nat → Nat) (hf : ∀ x, f (-x) = f x) : even_nat_fun f := by -- The goal is the same as hf
-  duper [hf, even_nat_fun]
+  duper [hf, even_nat_fun] {portfolioInstance := 6} -- Times out in portfolio mode, times out without monomorphization
 --###############################################################################################################################
 -- Tests duper's ability to derive that types are nonempty