Add ignoreUnusableFact option

Duper/Tactic.lean

@@ -10,13 +10,25 @@ register_option duper.printTimeInformation : Bool := {
   descr := "Whether to print the total time it took for Duper to construct a proof"
 }
 
+register_option duper.ignoreUnusableFacts : Bool := {
+  defValue := false
+  descr := "If true, suppresses the error that Duper would throw if given a fact it would not ordinarily accept (e.g. a constructor or opaque constant)"
+}
+
 def getPrintTimeInformation (opts : Options) : Bool :=
   duper.printTimeInformation.get opts
 
 def getPrintTimeInformationM : CoreM Bool := do
   let opts ← getOptions
   return getPrintTimeInformation opts
 
+def getIgnoreUsableFacts (opts : Options) : Bool :=
+  duper.ignoreUnusableFacts.get opts
+
+def getIgnoreUsableFactsM : CoreM Bool := do
+  let opts ← getOptions
+  return getIgnoreUsableFacts opts
+
 /-- Produces definional equations for a recursor `recVal` such as
 
   `@Nat.rec m z s (Nat.succ n) = s n (@Nat.rec m z s n)`
@@ -80,11 +92,21 @@ def elabFact (stx : Term) : TacticM (Array (Expr × Expr × Array Name)) := do
         return ret
       | some (.axiomInfo _)  => return #[← elabFactAux stx]
       | some (.thmInfo _)    => return #[← elabFactAux stx]
-      | some (.opaqueInfo _) => throwError "Opaque constants cannot be provided as facts"
-      | some (.quotInfo _)   => throwError "Quotient constants cannot be provided as facts"
-      | some (.inductInfo _) => throwError "Inductive types cannot be provided as facts"
-      | some (.ctorInfo _)   => throwError "Constructors cannot be provided as facts"
-      | none                 => throwError "Unknown constant {id}"
+      | some (.opaqueInfo _) =>
+        if ← getIgnoreUsableFactsM then return #[]
+        else throwError "Opaque constants cannot be provided as facts"
+      | some (.quotInfo _)   =>
+        if ← getIgnoreUsableFactsM then return #[]
+        else throwError "Quotient constants cannot be provided as facts"
+      | some (.inductInfo _) =>
+        if ← getIgnoreUsableFactsM then return #[]
+        else throwError "Inductive types cannot be provided as facts"
+      | some (.ctorInfo _)   =>
+        if ← getIgnoreUsableFactsM then return #[]
+        else throwError "Constructors cannot be provided as facts"
+      | none                 =>
+        if ← getIgnoreUsableFactsM then return #[]
+        else throwError "Unknown constant {id}"
     | .fvar exprFVarId =>
       match (← getLCtx).find? exprFVarId with
       | some _ => return #[← elabFactAux stx]
@@ -129,6 +151,8 @@ def collectAssumptions (facts : Array Term) (withAllLCtx : Bool) (goalDecls : Ar
       if ← isProp fact then
         let fact ← preprocessFact (← instantiateMVars fact)
         formulas := (fact, ← mkAppM ``eq_true #[proof], params, false, some factStx) :: formulas
+      else if ← getIgnoreUsableFactsM then
+        continue
       else
         throwError "Invalid fact {factStx} for duper. Proposition expected"
   return formulas