DecElim no longer eliminates decidably true clauses

Duper/Rules/DecElim.lean

@@ -10,18 +10,15 @@ open Meta
 
 initialize Lean.registerTraceClass `duper.rule.decElim
 
-/-- Checks whether a literal is decidable, and if it is, uses mkDecide to return whether the literal is
-    decidably true or false. If the literal is not decidable, returns none. -/
-def decideLiteral (lit : Lit) : MetaM (Option Bool) := do
+/-- Checks whether a literal is decidably false. Returns true if the literal is decidably false and false otherwise. -/
+def isDecidablyFalse (lit : Lit) : MetaM Bool := do
   try
     let d ← mkDecide lit.toExpr
     let d ← instantiateMVars d
     let r ← withDefault <| whnf d
-    if r.isConstOf ``false then return some false
-    else if r.isConstOf ``true then return some true
-    else return none
+    return r.isConstOf ``false
   catch _ =>
-    return none
+    return false
 
 def mkDecElimProof (refs : List (Option Nat)) (premises : List Expr) (parents : List ProofParent)
   (transferExprs : Array Expr) (c : Clause) : MetaM Expr :=
@@ -77,12 +74,9 @@ def decElim : MSimpRule := fun c => do
   let mut newLits : List Lit := []
   let mut refs : List (Option Nat) := []
   for lit in c.lits do
-    match ← decideLiteral lit with
-    | some true => -- Remove the entire clause because it is decidably true
-      return some #[]
-    | some false => -- Remove the decidably false literal from the clause
+    if ← isDecidablyFalse lit then -- Remove the decidably false literal from the clause
       refs := none :: refs
-    | none =>
+    else
       refs := (some newLits.length) :: refs
       newLits := lit :: newLits
   -- To achieve the desired spec for newLits and refs, I must reverse them

Duper/Saturate.lean

@@ -66,7 +66,9 @@ def forwardSimpRules : ProverM (Array SimpRule) := do
       elimDupLit.toSimpRule,
       elimResolvedLit.toSimpRule,
       destructiveEqualityResolution.toSimpRule,
-      decElim.toSimpRule, -- decElim subsumes identPropFalseElim and identBoolFalseElim
+      identPropFalseElim.toSimpRule,
+      identBoolFalseElim.toSimpRule,
+      decElim.toSimpRule,
       (forwardDemodulation (← getDemodSidePremiseIdx)).toSimpRule,
       (forwardClauseSubsumption subsumptionTrie).toSimpRule,
       (forwardEqualitySubsumption subsumptionTrie).toSimpRule,

README.md

@@ -63,8 +63,10 @@ If Duper times out, the following trace options are available:
 - Using `set_option trace.duper.timeout.debug.fullActiveSet true` will cause Duper to print the full active set (i.e. all clauses that Duper has fully processed, not just those that can be expressed with a single equality or inequality). Note that for some problems, enabling this option can cause VSCode to crash (because it struggles to handle the amount of trace output).
 - Using `set_option trace.duper.timeout.debug.fullPassiveSet true` will cause Duper to print the full passive set (i.e. all clauses that Duper has proven but not yet fully processed). Note that for some problems, enabling this option can cause VSCode to crash (because it struggles to handle the amount of trace output).
 
-If Duper saturates, meaning Duper fully processed all clauses and was unable to generate more, then `set_option duper.saturate.debug true` will cause Duper to print:
+If Duper saturates, meaning Duper fully processed all clauses and was unable to generate more, then `set_option trace.duper.saturate.debug true` will cause Duper to print:
 - The final active set (i.e. all clauses that Duper generated and fully processed)
 - Information about types that have been identified in the problem and whether they are provably inhabited by typeclass reasoning, provably nonempty from assumptions given to duper, or potentially uninhabited
 
+If Duper successfully proves the goal and you want to obtain additional information about the proof Duper found, then `set_option trace.duper.printProof true` will show the clauses used in the final proof and `set_option trace.duper.proofReconstruction true` will show information about the proofs of said clauses and the final proof that was used to resolve the goal.
+
 In our experience, we have generally found attempting to debug problems that Duper saturates on to be more fruitful than problems that Duper timed out on (because there is typically a smaller volume of clauses to look at). This is most helpful when Duper is capable of solving a problem in principle but needs to be provided some additional fact that it is not natively aware of. Additionally, we have generally found trace output to be more readable when preprocessing is disabled, since the current preprocessing procedure transforms input lemmas into facts with uninformative names. If you need to look at Duper's trace output even with preprocessing enabled, then `set_option trace.duper.monomorphization.debug true` will cause Duper to print its input facts before and after the monomorphization procedure. This can help in understanding how the monomorphized constants that appear in Duper's clauses correspond to constants in the original problem.