Merge pull request #31 from leanprover-community/dev

Dev

Duper/Fingerprint.lean

@@ -113,7 +113,7 @@ def emptyCFP : ClauseFingerprintTrie := mkEmptyWithDepth numFingerprintFeatures
    I could be quite off-base on that. -/
 structure RootCFPTrie where
   root : ClauseFingerprintTrie := emptyCFP
-  filterSet : HashSet Clause := {} -- Keeps track of the set of clauses that should be filtered out (i.e. "removed" clauses)
+  filterSet : Std.HashSet Clause := {} -- Keeps track of the set of clauses that should be filtered out (i.e. "removed" clauses)
 deriving Inhabited
 
 namespace RootCFPTrie

Duper/Interface.lean

@@ -454,8 +454,8 @@ def runDuperInstanceWithMonomorphization (formulas : List (Expr × Expr × Array
   -- 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 prover : Array Auto.Lemma → Array Auto.Lemma → MetaM Expr :=
+    fun lemmas inhLemmas => do
       let monomorphizedFormulas ← autoLemmasToFormulas lemmas
       trace[duper.monomorphization.debug] "Original formulas: {formulas.map (fun f => (f.1, f.2.2.2))}"
       trace[duper.monomorphization.debug] "Auto lemmas: {lemmas.map (fun l => (l.type, l.proof, l.deriv))}"
@@ -471,8 +471,8 @@ def runDuperInstanceWithFullPreprocessing (formulas : List (Expr × Expr × Arra
   -- 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 prover : Array Auto.Lemma → Array Auto.Lemma → MetaM Expr :=
+    fun lemmas inhLemmas => do
       let monomorphizedFormulas ← autoLemmasToFormulas lemmas
       trace[duper.monomorphization.debug] "Original formulas: {formulas.map (fun f => (f.1, f.2.2.2))}"
       trace[duper.monomorphization.debug] "Auto lemmas: {lemmas.map (fun l => (l.type, l.proof, l.deriv))}"

Duper/Rules/SyntacticTautologyDeletion3.lean

@@ -10,8 +10,8 @@ open SimpResult
     duper often gets cluttered with clauses of the form "x = True ∨ x = False". Neither syntacticTautologyDeletion1 nor
     syntacticTautologyDeletion2 remove clauses of this form, so that is what syntacticTautologyDeletion3 targets. -/
 def syntacticTautologyDeletion3 : MSimpRule := fun c => do
-  let mut eqTrueSet : HashSet Lean.Expr := mkHashSet -- Stores Lean expressions equated to True in c
-  let mut eqFalseSet : HashSet Lean.Expr := mkHashSet -- Stores Lean expressions equated to False in c
+  let mut eqTrueSet : Std.HashSet Lean.Expr := Std.HashSet.empty -- Stores Lean expressions equated to True in c
+  let mut eqFalseSet : Std.HashSet Lean.Expr := Std.HashSet.empty -- Stores Lean expressions equated to False in c
   for lit in c.lits do
     if lit.sign then
       if lit.rhs == mkConst ``True then
@@ -41,4 +41,4 @@ def syntacticTautologyDeletion3 : MSimpRule := fun c => do
         else eqTrueSet := eqTrueSet.insert lit.rhs
   return none
 
-end Duper
+end Duper

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)`
@@ -55,7 +67,8 @@ def elabFact (stx : Term) : TacticM (Array (Expr × Expr × Array Name)) := do
   match stx with
   | `($id:ident) =>
     let some expr ← Term.resolveId? id
-      | throwError "Unknown identifier {id}"
+      | if ← getIgnoreUsableFactsM then return #[]
+        else throwError "Unknown identifier {id}"
     match expr with
     | .const exprConstName _ =>
       match (← getEnv).find? exprConstName with
@@ -74,17 +87,27 @@ def elabFact (stx : Term) : TacticM (Array (Expr × Expr × Array Name)) := do
         if sort.isProp then
           ret := ret.push (← elabFactAux stx)
         -- Generate definitional equation for the fact
-        if let some eqns ← getEqnsFor? exprConstName (nonRec := true) then
+        if let some eqns ← getEqnsFor? exprConstName then
           ret := ret.append (← eqns.mapM fun eq => do elabFactAux (← `($(mkIdent eq))))
         trace[duper.elabFact.debug] "Adding definition {expr} as the following facts: {ret.map (fun x => x.1)}"
         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 +152,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

Duper/Tests/temp.lean

@@ -11,8 +11,9 @@ set_option auto.native true
 open Lean Auto
 
 @[rebind Auto.Native.solverFunc]
-def Auto.duperPort (lemmas : Array Lemma) : MetaM Expr := do
+def Auto.duperPort (lemmas inhLemmas : Array Lemma) : MetaM Expr := do
   let formulas ← Duper.autoLemmasToFormulas lemmas
+  let formulas := formulas.map (fun f => (f.1, f.2.1, f.2.2.1, f.2.2.2, none))
   Duper.runDuperPortfolioMode formulas .none
     { portfolioMode := true,
       portfolioInstance := none,

Duper/Tests/temp2.lean

@@ -11,7 +11,7 @@ set_option auto.native true
 open Lean Auto
 
 @[rebind Auto.Native.solverFunc]
-def Auto.duperPort (lemmas : Array Lemma) : MetaM Expr := do
+def Auto.duperPort (lemmas inhLemmas : Array Lemma) : MetaM Expr := do
   let formulas ← Duper.autoLemmasToFormulas lemmas
   let formulas := formulas.map (fun f => (f.1, f.2.1, f.2.2.1, f.2.2.2, none))
   Duper.runDuperPortfolioMode formulas .none

lake-manifest.json

@@ -5,20 +5,20 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "2b6ed7d9f86d558d94b8d9036a637395163c4fa6",
+   "rev": "0728f384d78982e6fb0f1cdf263e172d3135e0be",
    "name": "auto",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "2b6ed7d9f86d558d94b8d9036a637395163c4fa6",
+   "inputRev": "0728f384d78982e6fb0f1cdf263e172d3135e0be",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/batteries",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "9c6c2d647e57b2b7a0b42dd8080c698bd33a1b6f",
+   "rev": "4756e0fc48acce0cc808df0ad149de5973240df6",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.11.0",
+   "inputRev": "v4.12.0",
    "inherited": false,
    "configFile": "lakefile.lean"}],
  "name": "Duper",

lakefile.lean

@@ -2,8 +2,8 @@ import Lake
 
 open Lake DSL
 
-require auto from git "https://github.com/leanprover-community/lean-auto.git"@"2b6ed7d9f86d558d94b8d9036a637395163c4fa6"
-require batteries from git "https://github.com/leanprover-community/batteries" @ "v4.11.0"
+require auto from git "https://github.com/leanprover-community/lean-auto.git"@"0728f384d78982e6fb0f1cdf263e172d3135e0be"
+require batteries from git "https://github.com/leanprover-community/batteries" @ "v4.12.0"
 
 package Duper {
   precompileModules := true

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.11.0
+leanprover/lean4:v4.12.0