Simultaneous superposition bug fix and oracleInst modification

I'm confident that the change made to the simultaneous superposition
code is a strict improvement. Currently at least, it is possible for
Expr.replaceGreenWithPos to miss occurrences of sidePremiseLhs which
can cause a unification problem to succeed without a rewrite occurring
at mainPremisePos. This commit's simultaneous superposition change
ensures that even if occurrences of sidePremiseLhs can be missed
elsewhere in the main clause, superposition will always rewrite at
mainPremisePos.

However, the change to oracleInst this commit makes is much more
suspect. I made the change because with the previous oracleInst code
(and this commit's simultaneous superposition bug fix), the following
problem would fail due to an application type mismatch exception:

theorem proj_test (h1 : ∀ x : Nat, x > 0 → ∃ y : Fin x, y.1 = 0)
  (h2 : 3 > 0) : ∃ z : Fin 3, z.1 = 0 := by
  duper [h1, h2] {portfolioInstance := 7}

With this commit's change to oracleInst, this problem no longer results
in an error. However, tests poly₃, poly₄, and poly₅ in DReflTests.lean
now fail even though they previously succeeded.

Duper/DUnif/Oracles.lean

@@ -38,7 +38,29 @@ def oracleInst (p : UnifProblem) (eq : UnifEq) : MetaM (Option UnifProblem) := d
   --   does not consider metavariables in the type of metavariables
   if (← mustNotOccursCheck mvarId eq.rhs) then
     mvarId.assign eq.rhs
-    return some {(← p.pushParentRuleIfDbgOn (.OracleInst eq)) with checked := false, mctx := ← getMCtx}
+    /- It's not sufficient to just assigned mvarId to eq.rhs in all cases. If mvarId's type is more specific
+       than eq.rhs's type (e.g. if mvarId's type is `Fin 3` and eq.rhs's type is `Fin ?m`), then it is necessary
+       to additionally unify the types of mvarId and eq.rhs. -/
+    let mvarIdType ← Meta.inferType (.mvar mvarId)
+    let rhsType ← Meta.inferType eq.rhs
+    if mvarIdType != rhsType then
+      -- This code is loosely adapted from DUnif.imitation
+      trace[DUnif.oracles] "oracleInst: {mvarIdType} needs to be unified with {rhsType}"
+      trace[DUnif.oracles] "Before forallTelescope:"
+      trace[DUnif.oracles] "rhs: {eq.rhs} (type: {rhsType})"
+      trace[DUnif.oracles] "mvar: {mvarId} (type: {mvarIdType})"
+      Meta.forallTelescopeReducing mvarIdType fun xs β => do
+        let β ← Meta.mkLambdaFVars xs β
+        let (ys, _, _) ← Meta.forallMetaTelescopeReducing rhsType
+        let β' ← Meta.instantiateForall rhsType ys
+        let β' ← Meta.mkLambdaFVars xs β'
+        trace[DUnif.oracles] "After forallTelescope:"
+        trace[DUnif.oracles] "oracleInst: rhsType (β'): {β'}"
+        trace[DUnif.oracles] "oracleInst: mvarIdType (β): {β}"
+        let p := p.pushPrioritized (UnifEq.fromExprPair β β')
+        return some {(← p.pushParentRuleIfDbgOn (.OracleInst eq)) with checked := false, mctx := ← getMCtx}
+    else
+      return some {(← p.pushParentRuleIfDbgOn (.OracleInst eq)) with checked := false, mctx := ← getMCtx}
   else
     return none
 
@@ -65,4 +87,4 @@ def oracleOccurs (p : UnifProblem) (eq : UnifEq) : MetaM Bool := do
     if let .mvar id := eq.lhs.eta then
       mustOccursCheck id eq.rhs
     else
-      return false
+      return false

Duper/Rules/Superposition.lean

@@ -248,9 +248,15 @@ def superpositionAtLitWithPartner (mainPremise : MClause) (mainPremiseNum : Nat)
       let mut mainPremiseReplaced : MClause := Inhabited.default
       let mut poses : Array ClausePos := #[]
       if simultaneousSuperposition then
+        let mainPremise ← mainPremise.replaceAtPos! mainPremisePos sidePremiseRhs
+        /- In addition to performing the replacement at the intended location, the simultaneous superposition option indicates
+           that Duper should attempt to replace sidePremiseLhs with sidePremiseRhs wherever it is found in the mainPremise -/
         let mainPremise ← mainPremise.mapM (fun e => betaEtaReduceInstMVars e)
         (mainPremiseReplaced, poses) ← mainPremise.mapMWithPos <|
           Expr.replaceGreenWithPos sidePremiseLhs sidePremiseRhs
+        /- In addition to all of the additional positions found by Expr.replaceGreenWithPos, we also need to note the position
+           of the original rewrite -/
+        poses := poses.push mainPremisePos
       else
         mainPremiseReplaced ← mainPremise.replaceAtPos! mainPremisePos sidePremiseRhs
 

Duper/Tests/DReflTests.lean

@@ -62,8 +62,8 @@ namespace ChNum
 
 def pellEquation₁ (done : Prop) (q : ChNat → (Nat → Nat) → (Nat → Nat) → Nat)
                   -- ?m = 2, ?n = 1
-                  (h : ∀ (m n : ChNat), 
-                  q (chmul (chadd n c2) (chadd n c2)) (idtest m)   (idtest n) = 
+                  (h : ∀ (m n : ChNat),
+                  q (chmul (chadd n c2) (chadd n c2)) (idtest m)   (idtest n) =
                   q (chadd (chmul (chmul c2 m) m) c1) (fun z => z) (fun z => z)  → done)
                   : done := by
   apply h;
@@ -73,8 +73,8 @@ def pellEquation₁ (done : Prop) (q : ChNat → (Nat → Nat) → (Nat → Nat)
 
 def pellEquation₂ (done : Prop) (q : ChNat → (Nat → Nat) → (Nat → Nat) → Nat)
                   -- ?m = 3, ?n = 6
-                  (h : ∀ (m n : ChNat), 
-                  q (chmul (chadd n c2) (chadd n c2)) (idtest m)   (idtest n) = 
+                  (h : ∀ (m n : ChNat),
+                  q (chmul (chadd n c2) (chadd n c2)) (idtest m)   (idtest n) =
                   q (chadd (chmul (chmul c7 m) m) c1) (fun z => z) (fun z => z)→ done)
                   : done := by
   apply h;
@@ -85,7 +85,7 @@ def pellEquation₂ (done : Prop) (q : ChNat → (Nat → Nat) → (Nat → Nat)
 def pythagoreanTriple₁ (done : Prop) (q : ChNat → (Nat → Nat) → (Nat → Nat) → (Nat → Nat) → Nat)
                        (h : ∀ (x y z : ChNat),
                        -- 3² + 4² = 5²
-                       q (chadd (chmul (chadd x c1) (chadd x c1))  (chmul (chadd y c1) (chadd y c1)))  (idtest x)   (idtest y)   (idtest z) = 
+                       q (chadd (chmul (chadd x c1) (chadd x c1))  (chmul (chadd y c1) (chadd y c1)))  (idtest x)   (idtest y)   (idtest z) =
                        q (chmul (chadd z c2) (chadd z c2)) (fun z => z) (fun z => z) (fun z => z) → done):
                        done := by
   apply h;
@@ -169,23 +169,27 @@ def letrefl₁  (done : Prop)
 def ora₁ (done : Prop) (inh : α → β → Nat)
   (h : ∀ (a b : α → β → Nat), (fun x y => a y x) = (fun x y => b y x) → done) : done := by
   apply h
-  drefl attempt 3 unifier 0 contains 0
+  drefl attempt 30 unifier 0 contains 0
   exact inh
 
 def ora₂ (done : Prop) (inh : ∀ (α β : Type) (x : α) (y : β), α → β)
   (h : ∀ (a b : ∀ (α β : Type) (x : α) (y : β), α → β),
     (fun β y α x => a α β x y) = (fun β y α x => b α β x y) → done) : done := by
   apply h
-  drefl attempt 3 unifier 0 contains 0
+  drefl attempt 30 unifier 0 contains 0
   exact inh
 
 def ora₃ (done : Prop) (inh : ∀ (α β : Type) (x : α) (y : β), α → β)
   (h : ∀ (a b : ∀ (α β : Type) (x : α) (y : β), α → β),
     (fun β α y x => a α β x y) = (fun β α y x => b α β x y) → done) : done := by
   apply h
-  drefl attempt 3 unifier 0 contains 0
+  drefl attempt 30 unifier 0 contains 0
   exact inh
 
+def ora₄ (done : Prop) (sk : ∀ (α : Type), α)
+  (h : ∀ (a : Fin 3) (x : Nat), (↑a : Nat) = ↑(sk (Fin x)) → done) : done := by
+  apply h
+  drefl attempt 30 unifier 0 contains 0
 
 -- Polymorphism
 
@@ -199,14 +203,15 @@ def poly₂ (done : Prop) (f : ∀ (α : Type), α)
   apply h
   drefl attempt 20 unifier 0 contains 0
 
+set_option trace.DUnif.oracles true in
 def poly₃
   (done : Prop)
   (skS : ∀ {_ : Nat} {α : Type}, α)
   (α β : Type) (p : α → β → Prop) (f : α → β) (x : α)
   (h : ∀ a b c d, p a (@skS (nat_lit 1) (α → β → β) a b) = p (@skS (nat_lit 0) ((α → β) → α → α) c d) (c (@skS (nat_lit 0) ((α → β) → α → α) c d)) → done) :
   done := by
   apply h
-  drefl attempt 30 unifier 0 contains 0
+  drefl attempt 60 unifier 0 contains 0
   exact f; exact x
 
 def poly₄
@@ -216,9 +221,20 @@ def poly₄
   (h : ∀ a b c d e, p a (@skS (nat_lit 1) (α → β → β → β) a b e) = p (@skS (nat_lit 0) ((α → β) → α → α) c d) (c (@skS (nat_lit 0) ((α → β) → α → α) c d)) → done) :
   done := by
   apply h
-  drefl attempt 37 unifier 0 contains 0
+  drefl attempt 60 unifier 0 contains 0
   exact f; exact f; exact x
 
+set_option drefl.reduce true in
+def poly₅
+  (done : Prop)
+  (skS : {p : Type 1} → Nat → {α : Type} → α)
+  (h : ∀ (q b : Fin 3), q.1 = (@skS Type 0 ((x_0 : Nat) → Fin x_0 → Fin x_0) 3 b).1 → done) :
+  done := by
+  apply h
+  case a =>
+    drefl attempt 10000 unifier 0 contains 0
+    case b => exact Inhabited.default
+
 -- Negative tests
 set_option trace.DUnif.debug true in
 def neg₁ (done : Prop) (f : Nat → Nat)

Duper/Tests/test_inhabitationReasoning.lean

@@ -3,6 +3,7 @@ import Duper.TPTP
 
 set_option inhabitationReasoning true
 set_option trace.typeInhabitationReasoning.debug true
+set_option throwPortfolioErrors true
 
 theorem optionTest1 (t : Type) (f : Option t) : ∃ x : Option t, True := by duper
 
@@ -15,12 +16,16 @@ theorem finTest (x : Nat) (f : Fin x → Fin x)
   (h : ∃ y : Fin x, ∀ z : Fin x, (f y ≠ y) ∧ (f z = y)) : False := by duper [h]
 
 -- Needs to synthesize Inhabited (Fin default)
+set_option trace.Saturate.debug true in
 theorem finTest2
-  (h : ∀ x : Nat, ∃ f : Fin x → Fin x, ∃ y : Fin x, ∀ z : Fin x, (f y ≠ y) ∧ (f z = y)) : False := by duper [h]
+  (h : ∀ x : Nat, ∃ f : Fin x → Fin x, ∃ y : Fin x, ∀ z : Fin x, (f y ≠ y) ∧ (f z = y)) : False := by
+  duper [h] {portfolioInstance := 7}
 
 -- Needs to synthesize Inhabited (Fin [anonymous]) (pretty sure [anonymous] is a skolem var)
+set_option trace.Saturate.debug true in
 theorem finTest3 (mult_Nats : ∃ y : Nat, y ≠ 0)
-  (h : ∀ x : Nat, x ≠ 0 → ∃ f : Fin x → Fin x, ∃ y : Fin x, ∀ z : Fin x, (f y ≠ y) ∧ (f z = y)) : False := by duper [h]
+  (h : ∀ x : Nat, x ≠ 0 → ∃ f : Fin x → Fin x, ∃ y : Fin x, ∀ z : Fin x, (f y ≠ y) ∧ (f z = y)) : False := by
+  duper [h]
 
 -- Needs to synthesize Inhabited person
 set_option trace.ProofReconstruction true in