Duper no longer reads whole lctx by default

To call duper with all facts from the local context, duper can now be
called via duper[*, externalLemmas...]. Additionally, duper can now be called
with specific fvars from the local context, and these fvars can be mixed with
external lemmas. So duper [fvarFromLocalContext, externalLemma] is now
a valid invocation of duper.

Duper/Tests/bugs.lean

@@ -33,11 +33,11 @@ end Color2
 set_option inhabitationReasoning true in
 set_option trace.typeInhabitationReasoning.debug true in
 tptp ITP023_3 "../TPTP-v8.0.0/Problems/ITP/ITP023_3.p"
-  by duper -- Fails due to error: unknown free variable '_uniq.6173142'
+  by duper [*] -- Fails due to error: unknown free variable '_uniq.6173142'
 
 set_option inhabitationReasoning false in
 tptp ITP023_3' "../TPTP-v8.0.0/Problems/ITP/ITP023_3.p"
-  by duper -- Det timeout
+  by duper [*] -- Det timeout
 
 -- Diagnosis of the above test
 /-
@@ -61,22 +61,6 @@ example : ((∃ (A B : Type) (f : B → A) (x : B), f x = f x) = True) :=
 This might be a more viable example to investigate because of how much shorter it is
 -/
 
--- Bug 6
-set_option inhabitationReasoning true in
-example : ((∃ (A B : Type) (f : B → A) (x : B), f x = f x) = True) :=
-  by duper -- Fails because we currently do not infer that A is nonempty from the fact that B and B → A are nonempty
-
-set_option inhabitationReasoning true in
-example : ∃ (A : Type) (B : A → Type) (f : ∀ (a : A), B a) (x : A), (f x = f x) = True :=
-  by duper
-
--- Diagnosis of the above two examples
-/-
-This isn't so much a bug as it is a limitation in the current approach to inhabitation reasoning. The extent of reasoning Duper
-currently performs in attempting to determine whether a type is inhabited is limited. The two above examples provide somewhat
-more complicated cases in which Duper is not able to infer that a particular type is inhabited
--/
-
 -- Bug 7
 example (a : α) (as : List α) : [] ≠ a :: as :=
   by duper [List.rec] -- Error: AppBuilder for 'mkAppOptM', result contains metavariables @List.nil

Duper/Tests/fail_group.lean

@@ -15,4 +15,4 @@ theorem cubeisom
   (cube_injective : ∀ x y, cube x = cube y → x = y)
   (cube_surjective : ∀ x, ∃ y, x = cube y)
   (cube_homomorphism : ∀ x y, cube (mult x y) = mult (cube x) (cube y))
-  : ∀ x y, mult x y = mult y x := by duper
+  : ∀ x y, mult x y = mult y x := by duper [*]

Duper/Tests/fail_lattice.lean

@@ -22,4 +22,4 @@ theorem mod_lattice1
   (ModLatA : ∀ a x b, U (A a b) (A x b) = A (U (A a b) x) b)
   (a b c : L)
   (Hyp : A a (U b c) = U (A a b) (A a c))
-  : U a (A b c) = A (U a b) (U a c) := by duper
+  : U a (A b c) = A (U a b) (U a c) := by duper [*]

Duper/Tests/fail_tests.lean

@@ -24,7 +24,7 @@ f (f (f a)) = d ∨ f (f b) = d ∨ f c = d)
 (h2 : f (f (f (f a1))) ≠ d)
 (h2 : f (f (f a)) ≠ d)
 (h3 : f (f b) ≠ d)
-: False := by duper
+: False := by duper [*]
 
 -- Tests where duper should time out
 -- This example is intended to test duper's ability of

Duper/Tests/ffffa.lean

@@ -15,4 +15,4 @@ a
 ))))))))))
 ))))))))))
 )))))))))) = a
- := by duper
+ := by duper [h]

Duper/Tests/fluidSupTests.lean

@@ -1,6 +1,5 @@
 import Duper.Tactic
 import Duper.TPTP
-import Duper.DUnif.DApply
 
 set_option trace.Saturate.debug true
 set_option trace.Rule.fluidSup true
@@ -9,14 +8,14 @@ set_option trace.Rule.fluidSup true
 
 theorem supWithLambdasEx13 (a b c : t) (f g : t → t) (h : t → t → t)
   (eq1 : f a = c) (eq2 : ∀ y : t → t, h (y b) (y a) ≠ h (g (f b)) (g c)) : False :=
-  by duper
+  by duper [*] {portfolioInstance := 0}
 
 theorem supWithLambdasEx14 (a b c d : t) (f g : t → t)
   (eq1 : f a = c) (eq2 : f b = d) (eq3 : ∀ y : t → t, g c ≠ y a ∨ g d ≠ y b) : False :=
-  by duper
+  by duper [*]
 
 -- Note: Since the original example was untyped, it's possible that the types I chose for this don't work. So I don't
 -- put too much stock in it if this continues to fail. But I do think that supWithLambda13 should be solvable
 theorem supWithLambdaEx15 (a c : t) (f g : t → t) (h : t → ((t → t) → t → t) → t)
   (eq1 : f a = c) (eq2 : ∀ y : (t → t) → t → t, h (y (fun x => g (f x)) a) y ≠ h (g c) (fun w x => w x)) :
-  False := by duper
+  False := by duper [*]

Duper/Tests/group.lean

@@ -13,25 +13,25 @@ axiom exists_left_inv : ∀ (x : G), ∃ (y : G), x ⬝ y = e
 noncomputable instance : Inhabited G := ⟨e⟩
 
 theorem e_mul : e ⬝ x = x :=
-by duper [mul_assoc, mul_e, exists_left_inv]
+by duper [mul_assoc, mul_e, exists_left_inv] {portfolioInstance := 0}
 
 theorem exists_right_inv (x : G) : ∃ (y : G), y ⬝ x = e :=
-by duper [mul_assoc, mul_e, exists_left_inv]
+by duper [mul_assoc, mul_e, exists_left_inv] {portfolioInstance := 0}
 
 theorem left_neutral_unique (x : G) : (∀ y, x ⬝ y = y) → x = e :=
-by duper [mul_assoc, mul_e, exists_left_inv]
+by duper [mul_assoc, mul_e, exists_left_inv] {portfolioInstance := 0}
 
 theorem right_neutral_unique (x : G) : (∀ y, y ⬝ x = y) → x = e :=
-by duper [mul_assoc, mul_e, exists_left_inv]
+by duper [mul_assoc, mul_e, exists_left_inv] {portfolioInstance := 0}
 
 theorem right_inv_unique (x y z : G) (h : x ⬝ y = e) (h : x ⬝ z = e) : y = z :=
-by duper [mul_assoc, mul_e, exists_left_inv]
+by duper [*, mul_assoc, mul_e, exists_left_inv] {portfolioInstance := 0}
 
 theorem left_inv_unique (x y z : G) (h : y ⬝ x = e) (h : z ⬝ x = e) : y = z :=
-by duper [mul_assoc, mul_e, exists_left_inv]
+by duper [*, mul_assoc, mul_e, exists_left_inv] {portfolioInstance := 0}
 
 noncomputable def sq (x : G) := x ⬝ x
 
 theorem sq_mul_sq_eq_e (x y : G) (h_comm : ∀ a b, a ⬝ b = b ⬝ a) (h : x ⬝ y = e) :
   sq x ⬝ sq y = e :=
-by duper [sq, mul_assoc, mul_e]
+by duper [h_comm, h, sq, mul_assoc, mul_e] {portfolioInstance := 0}

Duper/Tests/group2.lean

@@ -1,6 +1,6 @@
 import Duper.Tactic
 
-class Group (G : Type) where 
+class Group (G : Type) where
 (one : G)
 (inv : G → G)
 (mul : G → G → G)
@@ -19,25 +19,30 @@ noncomputable instance : Inhabited G := ⟨one⟩
 theorem test : x ⬝ one = x :=
 by duper [Group.mul_one]
 
+/- Note: Currently, includeHoist must be disabled in order for duper to solve these problems. In the future,
+   portfolio mode should be enhanced so that at least one portfolio instance enables hoist rules and most
+   portfolio instances disable hoist rules. -/
+set_option includeHoistRules false
+
 theorem exists_right_inv (x : G) : inv x ⬝ x = one :=
-by duper [Group.mul_assoc, Group.mul_one, Group.mul_inv]
+by duper [Group.mul_assoc, Group.mul_one, Group.mul_inv] {portfolioInstance := 0}
 
 theorem left_neutral_unique (x : G) : (∀ y, x ⬝ y = y) → x = one :=
-by duper [Group.mul_assoc, Group.mul_one, Group.mul_inv]
+by duper [Group.mul_assoc, Group.mul_one, Group.mul_inv] {portfolioInstance := 0}
 
 theorem right_neutral_unique (x : G) : (∀ y, y ⬝ x = y) → x = one :=
-by duper [Group.mul_assoc, Group.mul_one, Group.mul_inv]
+by duper [Group.mul_assoc, Group.mul_one, Group.mul_inv] {portfolioInstance := 0}
 
 theorem right_inv_unique (x y z : G) (h : x ⬝ y = one) (h : x ⬝ z = one) : y = z :=
-by duper [Group.mul_assoc, Group.mul_one, Group.mul_inv]
+by duper [*, Group.mul_assoc, Group.mul_one, Group.mul_inv] {portfolioInstance := 0}
 
 theorem left_inv_unique (x y z : G) (h : y ⬝ x = one) (h : z ⬝ x = one) : y = z :=
-by duper [Group.mul_assoc, Group.mul_one, Group.mul_inv]
+by duper [*, Group.mul_assoc, Group.mul_one, Group.mul_inv] {portfolioInstance := 0}
 
 noncomputable def sq := x ⬝ x
 
 theorem sq_mul_sq_eq_e (h_comm : ∀ (a b : G), a ⬝ b = b ⬝ a) (h : x ⬝ y = one) :
   sq x ⬝ sq y = one :=
-by duper [sq, Group.mul_assoc, Group.mul_one, Group.mul_inv]
+by duper [h, h_comm, sq, Group.mul_assoc, Group.mul_one, Group.mul_inv] {portfolioInstance := 0}
 
-end Group
+end Group

Duper/Tests/lastAsylum.lean

@@ -37,14 +37,14 @@ example
 theorem asylum_one
   (h1 : Sane Jones ↔ Doctor Smith)
   (h2 : Sane Smith ↔ ¬ Doctor Jones)
-  : ∃ x : Inhab, (¬ Sane (x) ∧ Doctor (x)) ∨ (Sane (x) ∧ ¬ Doctor (x)) := by duper
+  : ∃ x : Inhab, (¬ Sane (x) ∧ Doctor (x)) ∨ (Sane (x) ∧ ¬ Doctor (x)) := by duper [h1, h2]
 
 #print axioms asylum_one
 
 theorem asylum_seven
   (h1 : Sane A ↔ ¬ Sane B)
   (h2 : Sane B ↔ Doctor A)
-  : (¬ Sane A ∧ Doctor A) ∨ (Sane A ∧ ¬ Doctor A) := by duper
+  : (¬ Sane A ∧ Doctor A) ∨ (Sane A ∧ ¬ Doctor A) := by duper [*]
 
 #print axioms asylum_seven
 
@@ -57,7 +57,7 @@ theorem asylum_nine
   (h4 : A ≠ B ∧ A ≠ C ∧ A ≠ D ∧ B ≠ C ∧ B ≠ D ∧ C ≠ D) :
   (∃ x : Inhab, Sane x ∧ ¬ Doctor x) ∨
   (∃ x : Inhab, ∃ y : Inhab, x ≠ y ∧ (¬ Sane x) ∧ Doctor x ∧ (¬ Sane y) ∧ Doctor y) :=
-  by duper
+  by duper [*]
 
 #print axioms asylum_nine
-#print asylum_nine
+#print asylum_nine