Dev

Duper/ClauseStreamHeap.lean

@@ -138,9 +138,9 @@ def ProverM.postProcessInferenceResult (cp : ClauseProof) : ProverM Unit := do
   let allClauses ← getAllClauses
   let parentClauseInfoOpts ← proof.parents.mapM
     (fun p =>
-      match allClauses.find? p.clause with
+      match allClauses.get? p.clause with
       | some pi => pure pi
-      | none => throwError "ProverM.postProcessInferenceResult: Unable to find parent clause {p.clause}")
+      | none => throwError "ProverM.postProcessInferenceResult: Unable to find parent clause {p.clause.toForallExpr}")
   -- c's generation number is one greater than the sum of its parents generation numbers
   let generationNumber := parentClauseInfoOpts.foldl (fun acc parentInfo => acc + parentInfo.generationNumber) 1
   -- c's goalDistance is at most maxGoalDistance and is otherwise one greater than the distance of the parent closest to the goal

Duper/ProverM.lean

@@ -98,9 +98,6 @@ instance : AddMessageContext ProverM where
 @[inline] def ProverM.run' (x : ProverM α) (ctx : Context := {}) (s : State := {}) : MetaM α :=
   Prod.fst <$> x.run ctx s
 
-instance [MetaEval α] : MetaEval (ProverM α) :=
-  ⟨fun env opts x _ => MetaEval.eval env opts x.run' true⟩
-
 initialize
   registerTraceClass `duper.prover.saturate
   registerTraceClass `duper.createdClauses

Duper/Selection.lean

@@ -131,7 +131,7 @@ def selectMaxLitComplex (c : MClause) (alreadyReduced : Bool) : RuleM (List Nat)
     selectMaxLitComplex but uses the number of positive literals with a shared predicate symbol as a tiebreaker (preferring
     to select literals that share a predicate symbol with as few positive literals as possible). For this, specification, I
     am defining a predicate symbol as the top symbol for the lhs of a literal of the form `e = True` or `e = False`.
-    
+
     Note: According to "Extending a Brainiac Prover to Lambda-Free Higher-Order Logic", SelectMaxLComplexAvoidPosPred
     (aka SelectMLCAPP) should be have very similarly to E's SelectMLCAPPPreferAppVar and SelectMLCAPPAvoidAppVar. So
     it should be unnecessary to separately implement those two selection functions. -/
@@ -204,7 +204,7 @@ def selectMaxLitComplexAvoidPosPred (c : MClause) (alreadyReduced : Bool) : Rule
     literal of the form `e = True` or `e = False`). If there are multiple negative literals with the same largest predicate, then
     the size difference between the lit's lhs and rhs will be the tiebreaker (with larger size differences being preferred). -/
 def selectCQIPrecWNTNp (c : MClause) (alreadyReduced : Bool) : RuleM (List Nat) := do
-  let idxLitPairs := c.lits.mapIdx (fun idx l => (idx.1, l))
+  let idxLitPairs := c.lits.mapIdx (fun idx l => (idx, l))
   let idxPredPairs := idxLitPairs.filterMap
     (fun (idx, l) =>
       -- Since we only select negative literals, and since we need a predicate, the only form we allow `l` to have is `e = False`
@@ -217,10 +217,10 @@ def selectCQIPrecWNTNp (c : MClause) (alreadyReduced : Bool) : RuleM (List Nat)
     )
   let symbolPrecMap ← getSymbolPrecMap -- Recall that low values in symbolPrecMap correspond to high precedence
   let idxPredPairsSorted := idxPredPairs.qsort -- Sorting so that highest precedence symbols will be first in idxPredPairsSorted
-    (fun (idx1, pred1Opt) (idx2, pred2Opt) =>
+    (fun (_idx1, pred1Opt) (_idx2, pred2Opt) =>
       match pred1Opt, pred2Opt with
       | some pred1, some pred2 =>
-        match symbolPrecMap.find? pred1, symbolPrecMap.find? pred2 with
+        match symbolPrecMap.get? pred1, symbolPrecMap.get? pred2 with
         | none, _ => false -- Never sort symbol not found in symbolPrecMap before anything else
         | some _, none => true -- Symbols found in symbolPrecMap are sorted before symbols found in symbolPrecMap
         | some prec1, some prec2 => prec1 < prec2 -- Low values in symbolPrecMap correspond to higher precedence
@@ -287,12 +287,12 @@ def litSelected (c : MClause) (i : Nat) (alreadyReduced : Bool) : RuleM Bool :=
   return sel.contains i
 
 /-- Data type to capture whether a literal in a clause is eligible.
-If it is not eligible, we distinguish the cases where there might 
+If it is not eligible, we distinguish the cases where there might
 be substitutions that make the literal eligble (`potentiallyEligible`)
 or not (`notEligible`).-/
-inductive Eligibility 
-  | eligible 
-  | potentiallyEligible 
+inductive Eligibility
+  | eligible
+  | potentiallyEligible
   | notEligible
 deriving Inhabited, BEq, Repr, Hashable
 
@@ -343,4 +343,4 @@ def eligibilityPostUnificationCheck (c : MClause) (alreadyReduced := false) (i :
   else if preUnificationResult == Eligibility.notEligible then return false
   else c.isMaximalLit (← getOrder) alreadyReduced i (strict := strict)
 
-end Duper
+end Duper

Duper/Tactic.lean

@@ -3,6 +3,8 @@ import Duper.Interface
 
 open Lean Meta Duper ProverM Parser Elab Tactic
 
+initialize Lean.registerTraceClass `duper.ignoredUnusableFacts
+
 namespace Duper
 
 register_option duper.printTimeInformation : Bool := {
@@ -22,12 +24,12 @@ def getPrintTimeInformationM : CoreM Bool := do
   let opts ← getOptions
   return getPrintTimeInformation opts
 
-def getIgnoreUsableFacts (opts : Options) : Bool :=
+def getIgnoreUnusableFacts (opts : Options) : Bool :=
   duper.ignoreUnusableFacts.get opts
 
-def getIgnoreUsableFactsM : CoreM Bool := do
+def getIgnoreUnusableFactsM : CoreM Bool := do
   let opts ← getOptions
-  return getIgnoreUsableFacts opts
+  return getIgnoreUnusableFacts opts
 
 /-- Produces definional equations for a recursor `recVal` such as
 
@@ -37,8 +39,8 @@ def getIgnoreUsableFactsM : CoreM Bool := do
   for each constructor, a proof of the equation, and the contained level
   parameters. -/
 def addRecAsFact (recVal : RecursorVal): TacticM (List (Expr × Expr × Array Name)) := do
-  let some (.inductInfo indVal) := (← getEnv).find? recVal.getInduct
-    | throwError "Expected inductive datatype: {recVal.getInduct}"
+  let some (.inductInfo indVal) := (← getEnv).find? recVal.getMajorInduct
+    | throwError "Expected inductive datatype: {recVal.getMajorInduct}"
   let expr := mkConst recVal.name (recVal.levelParams.map Level.param)
   let res ← forallBoundedTelescope (← inferType expr) recVal.getMajorIdx fun xs _ => do
     let expr := mkAppN expr xs
@@ -67,8 +69,11 @@ def elabFact (stx : Term) : TacticM (Array (Expr × Expr × Array Name)) := do
   match stx with
   | `($id:ident) =>
     let some expr ← Term.resolveId? id
-      | if ← getIgnoreUsableFactsM then return #[]
-        else throwError "Unknown identifier {id}"
+      | if ← getIgnoreUnusableFactsM then
+          trace[duper.ignoredUnusableFacts] "Ignored {id} because it was unknown"
+          return #[]
+        else
+          throwError "Unknown identifier {id}"
     match expr with
     | .const exprConstName _ =>
       match (← getEnv).find? exprConstName with
@@ -91,33 +96,61 @@ def elabFact (stx : Term) : TacticM (Array (Expr × Expr × Array Name)) := do
           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 (.axiomInfo _)  =>
+        let ret ← elabFactAux stx
+        trace[duper.elabFact.debug] "Adding axiom {stx} as the following fact: {ret.1}"
+        return #[ret]
+      | some (.thmInfo _)    =>
+        let ret ← elabFactAux stx
+        trace[duper.elabFact.debug] "Adding theorem {stx} as the following fact: {ret.1}"
+        return #[ret]
       | some (.opaqueInfo _) =>
-        if ← getIgnoreUsableFactsM then return #[]
-        else throwError "Opaque constants cannot be provided as facts"
+        if ← getIgnoreUnusableFactsM then
+          trace[duper.ignoredUnusableFacts] "Ignored {expr} ({id}) because it is an opaque constant"
+          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"
+        if ← getIgnoreUnusableFactsM then
+          trace[duper.ignoredUnusableFacts] "Ignored {expr} ({id}) because it is a quotient constant"
+          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"
+        if ← getIgnoreUnusableFactsM then
+          trace[duper.ignoredUnusableFacts] "Ignored {expr} ({id}) because it is an inductive type"
+          return #[]
+        else
+          throwError "Inductive types cannot be provided as facts"
       | some (.ctorInfo _)   =>
-        if ← getIgnoreUsableFactsM then return #[]
-        else throwError "Constructors cannot be provided as facts"
+        if ← getIgnoreUnusableFactsM then
+          trace[duper.ignoredUnusableFacts] "Ignored {expr} ({id}) because it is a constructor"
+          return #[]
+        else
+          throwError "Constructors cannot be provided as facts"
       | none                 =>
-        if ← getIgnoreUsableFactsM then return #[]
-        else throwError "Unknown constant {id}"
+        if ← getIgnoreUnusableFactsM then
+          trace[duper.ignoredUnusableFacts] "Ignored {expr} ({id}) because it is an unknown constant"
+          return #[]
+        else
+          throwError "Unknown constant {id}"
     | .fvar exprFVarId =>
       match (← getLCtx).find? exprFVarId with
-      | some _ => return #[← elabFactAux stx]
+      | some _ =>
+        let ret ← elabFactAux stx
+        trace[duper.elabFact.debug] "Adding fvar {stx} as the following fact: {ret.1}"
+        return #[ret]
       | none => throwError "Unknown fvar {id}"
     | _ => throwError "Unknown identifier {id}"
-  | _ => return #[← elabFactAux stx]
+  | _ =>
+    let ret ← elabFactAux stx
+    trace[duper.elabFact.debug] "Adding {stx} as the following fact: {ret.1}"
+    return #[ret]
 where elabFactAux (stx : Term) : TacticM (Expr × Expr × Array Name) :=
   -- elaborate term as much as possible and abstract any remaining mvars:
   Term.withoutModifyingElabMetaStateWithInfo <| withRef stx <| Term.withoutErrToSorry do
-    let e ← Term.elabTerm stx none
+    let stxWithAt ← `(term| @$stx)
+    let e ← Term.elabTerm stxWithAt none (implicitLambda := false)
     Term.synthesizeSyntheticMVars (postpone := .no) (ignoreStuckTC := true)
     let e ← instantiateMVars e
     let abstres ← Duper.abstractMVars e
@@ -152,7 +185,15 @@ 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
+      else if ← isDefEq (← inferType fact) (.sort 0) then
+        /- This check can succeed where the previous failed in instances where `fact`'s type is
+           a sort with an undetermined universe level. We try the previous check first to avoid
+           unnecessarily assigning metavariables in `fact`'s type (which the above `isDefEq` check
+           can do)-/
+        let fact ← preprocessFact (← instantiateMVars fact)
+        formulas := (fact, ← mkAppM ``eq_true #[proof], params, false, some factStx) :: formulas
+      else if ← getIgnoreUnusableFactsM then
+        trace[duper.ignoredUnusableFacts] "Ignored {fact} ({factStx}) because it is not a Prop"
         continue
       else
         throwError "Invalid fact {factStx} for duper. Proposition expected"

lake-manifest.json

@@ -1,25 +1,25 @@
 {"version": "1.1.0",
  "packagesDir": ".lake/packages",
  "packages":
- [{"url": "https://github.com/leanprover-community/lean-auto.git",
+ [{"url": "https://github.com/leanprover-community/batteries",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "915802517242f70b284fbcd5eac55bdaae29535e",
-   "name": "auto",
+   "rev": "8d6c853f11a5172efa0e96b9f2be1a83d861cdd9",
+   "name": "batteries",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "915802517242f70b284fbcd5eac55bdaae29535e",
+   "inputRev": "v4.14.0",
    "inherited": false,
-   "configFile": "lakefile.lean"},
-  {"url": "https://github.com/leanprover-community/batteries",
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/lean-auto.git",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "31a10a332858d6981dbcf55d54ee51680dd75f18",
-   "name": "batteries",
+   "rev": "4d73b99262f1ce80a33ac832bef26549cf3c2034",
+   "name": "auto",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.13.0",
+   "inputRev": "4d73b99262f1ce80a33ac832bef26549cf3c2034",
    "inherited": false,
-   "configFile": "lakefile.toml"}],
+   "configFile": "lakefile.lean"}],
  "name": "Duper",
  "lakeDir": ".lake"}

lakefile.lean

@@ -2,8 +2,8 @@ import Lake
 
 open Lake DSL
 
-require auto from git "https://github.com/leanprover-community/lean-auto.git"@"915802517242f70b284fbcd5eac55bdaae29535e"
-require batteries from git "https://github.com/leanprover-community/batteries" @ "v4.13.0"
+require auto from git "https://github.com/leanprover-community/lean-auto.git"@"4d73b99262f1ce80a33ac832bef26549cf3c2034"
+require batteries from git "https://github.com/leanprover-community/batteries" @ "v4.14.0"
 
 package Duper {
   precompileModules := true

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.13.0
+leanprover/lean4:v4.14.0