Merge pull request #24 from leanprover-community/dev

Dev

Duper/Clause.lean

@@ -158,7 +158,7 @@ def replaceAtPos! [Monad m] [MonadLiftT MetaM m] [MonadError m] (l : Lit) (pos :
   | LitSide.lhs => return {l with lhs := ← l.lhs.replaceAtPos! pos.pos replacement}
   | LitSide.rhs => return {l with rhs := ← l.rhs.replaceAtPos! pos.pos replacement}
 
--- Note : This function will throw error if ``pos`` is not a valid ``pos`` for `l`
+/-- Note : This function will throw error if ``pos`` is not a valid ``pos`` for `l` -/
 def replaceAtPosUpdateType? (l : Lit) (pos : LitPos) (replacement : Expr) : MetaM (Option Lit) := do
   let repPos ← replaceAtPos! l pos replacement
   try

Duper/Rules/BoolHoist.lean

@@ -37,7 +37,9 @@ def boolHoistAtExpr (e : Expr) (pos : ClausePos) (given : Clause) (c : MClause)
         return none
       -- All side conditions have been met. Yield the appropriate clause
       let cErased := c.eraseLit pos.lit
-      let newClause := cErased.appendLits #[← lit.replaceAtPos! ⟨pos.side, pos.pos⟩ (mkConst ``False), Lit.fromSingleExpr e true]
+      let some newLit ← lit.replaceAtPosUpdateType? ⟨pos.side, pos.pos⟩ (mkConst ``False)
+        | return none -- If `lit` can't be safely changed at position `p`, then don't apply `boolHoist` at `p`
+      let newClause := cErased.appendLits #[newLit, Lit.fromSingleExpr e true]
       trace[duper.rule.boolHoist] "Created {newClause.lits} from {c.lits}"
       yieldClause newClause "boolHoist" $ some (mkBoolHoistProof pos false)
     return #[ClauseStream.mk ug given yC "boolHoist"]

Duper/Rules/Demodulation.lean

@@ -80,7 +80,8 @@ def forwardDemodulationWithPartner (mainPremise : MClause) (mainPremiseMVarIds :
     return none -- Cannot perform demodulation because we could not match sidePremiseLit.lhs to mainPremiseSubterm
   if (← compare sidePremiseLit.lhs sidePremiseLit.rhs false) != Comparison.GreaterThan then
     return none -- Cannot perform demodulation because side condition 2 listed above is not met
-  let mainPremiseReplaced ← mainPremise.replaceAtPos! mainPremisePos sidePremiseLit.rhs
+  let some mainPremiseReplaced ← mainPremise.replaceAtPosUpdateType? mainPremisePos sidePremiseLit.rhs
+    | return none -- If `mainPremise` cannot be safely changed at `mainPremisePos`, then don't apply demodulation
   return some (mainPremiseReplaced, (some $ mkDemodulationProof sidePremiseLhs mainPremisePos true))
 
 def forwardDemodulationAtExpr (e : Expr) (pos : ClausePos) (sideIdx : RootCFPTrie) (givenMainClause : MClause)
@@ -147,7 +148,8 @@ def backwardDemodulationWithPartner (mainPremise : MClause) (mainPremiseMVarIds
     return none -- Cannot perform demodulation because we could not match sidePremiseLit.lhs to mainPremiseSubterm
   if (← compare sidePremiseLit.lhs sidePremiseLit.rhs false) != Comparison.GreaterThan then
     return none -- Cannot perform demodulation because side condition 2 listed above is not met
-  let mainPremiseReplaced ← mainPremise.replaceAtPos! mainPremisePos sidePremiseLit.rhs
+  let some mainPremiseReplaced ← mainPremise.replaceAtPosUpdateType? mainPremisePos sidePremiseLit.rhs
+    | return none -- If `mainPremise` cannot be safely changed at `mainPremisePos`, then don't apply demodulation
   trace[duper.rule.demodulation] "(Backward) Main mclause (after matching): {mainPremise.lits}"
   trace[duper.rule.demodulation] "(Backward) Side clause (after matching): {sidePremise.lits}"
   trace[duper.rule.demodulation] "(Backward) Result: {mainPremiseReplaced.lits}"

Duper/Rules/EqHoist.lean

@@ -86,7 +86,9 @@ def eqHoistAtExpr (e : Expr) (pos : ClausePos) (given : Clause) (c : MClause) :
         return none
       -- All side conditions have been met. Yield the appropriate clause
       let cErased := c.eraseLit pos.lit
-      let newClause := cErased.appendLits #[← lit.replaceAtPos! ⟨pos.side, pos.pos⟩ (mkConst ``False), Lit.fromExpr freshVarEquality]
+      let some newLit ← lit.replaceAtPosUpdateType? ⟨pos.side, pos.pos⟩ (mkConst ``False)
+        | return none -- If `lit` can't be safely changed at position `pos`, then don't apply `eqHoist` at `pos`
+      let newClause := cErased.appendLits #[newLit, Lit.fromExpr freshVarEquality]
       trace[duper.rule.eqHoist] "Created {newClause.lits} from {c.lits}"
       let mkProof := mkEqHoistProof pos
       yieldClause newClause "eqHoist" mkProof (transferExprs := #[freshVar1, freshVar2])

Duper/Rules/FluidBoolHoist.lean

@@ -101,7 +101,9 @@ def fluidBoolHoistAtExpr (e : Expr) (pos : ClausePos) (given : Clause) (c : MCla
       -- All side conditions for fluidBoolHoist have been met
       let cErased := c.eraseLit pos.lit
       let litOriginal := c.lits[pos.lit]! -- No lhs/rhs swap
-      let newClause := cErased.appendLits #[← litOriginal.replaceAtPos! ⟨pos.side, pos.pos⟩ freshFunctionGivenFalse, Lit.fromSingleExpr freshPropVar true]
+      let some newLit ← litOriginal.replaceAtPosUpdateType? ⟨pos.side, pos.pos⟩ freshFunctionGivenFalse
+        | return none -- If `litOriginal` can't be safely changed at position `pos`, then don't apply fluidBoolHoist at `pos`
+      let newClause := cErased.appendLits #[newLit, Lit.fromSingleExpr freshPropVar true]
       trace[duper.rule.fluidBoolHoist] "Created {newClause.lits} from {c.lits}"
       let mkProof := mkFluidBoolHoistProof pos false -- Is fluidBoolHoist not fluidLoobHoist
       yieldClause newClause "fluidBoolHoist" mkProof (transferExprs := #[freshFunctionOutputType, freshFunction, freshPropVar])
@@ -125,7 +127,9 @@ def fluidBoolHoistAtExpr (e : Expr) (pos : ClausePos) (given : Clause) (c : MCla
       -- All side conditions for fluidLoobHoist have been met
       let cErased := c.eraseLit pos.lit
       let litOriginal := c.lits[pos.lit]! -- No lhs/rhs swap
-      let newClause := cErased.appendLits #[← litOriginal.replaceAtPos! ⟨pos.side, pos.pos⟩ freshFunctionGivenTrue, Lit.fromSingleExpr freshPropVar false]
+      let some newLit ← litOriginal.replaceAtPosUpdateType? ⟨pos.side, pos.pos⟩ freshFunctionGivenTrue
+        | return none -- If `litOriginal` can't be safely changed at position `pos`, then don't apply fluidBoolHoist at `pos`
+      let newClause := cErased.appendLits #[newLit, Lit.fromSingleExpr freshPropVar false]
       trace[duper.rule.fluidLoobHoist] "Created {newClause.lits} from {c.lits}"
       let mkProof := mkFluidBoolHoistProof pos true -- True because this is fluidLoobHoist
       yieldClause newClause "fluidLoobHoist" mkProof (transferExprs := #[freshFunctionOutputType, freshFunction, freshPropVar])

Duper/Rules/FluidSup.lean

@@ -127,7 +127,8 @@ def fluidSupWithPartner (mainPremise : MClause) (mainPremiseNum : Nat) (mainPrem
       let freshFunctionWithRhs ← Core.betaReduce freshFunctionWithRhs
       if (freshFunctionWithLhs == freshFunctionWithRhs) then return none
 
-      let mainPremiseReplaced ← mainPremise.replaceAtPos! mainPremisePos freshFunctionWithRhs
+      let some mainPremiseReplaced ← mainPremise.replaceAtPosUpdateType? mainPremisePos freshFunctionWithRhs
+        | return none -- If `mainPremise` can't be safely changed at `mainPremisePos` then don't apply `fluidSup` at `mainPremisePos`
       if mainPremiseReplaced.isTrivial then
         trace[duper.rule.fluidSup] "trivial: {mainPremiseReplaced.lits}"
         return none

Duper/Rules/IdentBoolHoist.lean

@@ -84,13 +84,15 @@ def identBoolHoistAtExpr (e : Expr) (pos : ClausePos) (c : MClause) : RuleM (Opt
       else
         trace[duper.rule.identBoolHoist] m!"BoolHoist at literal {l}, side {s}, position {p} in clause {c.lits.map Lit.toExpr}"
         let litl := c.lits[l]!
+        let some litl1 ← litl.replaceAtPosUpdateType? ⟨s, p⟩ (mkConst ``True)
+          | return none -- If `litl` can't be safely changed at position `p`, then don't apply `identBoolHoist` at `p`
+        let some litl2 ← litl.replaceAtPosUpdateType? ⟨s, p⟩ (mkConst ``False)
+          | return none -- If `litl` can't be safely changed at position `p`, then don't apply `identBoolHoist` at `p`
         let c_erased := c.eraseLit l
-        let nc := c_erased.appendLits
-          #[← litl.replaceAtPos! ⟨s, p⟩ (mkConst ``True), Lit.fromSingleExpr e false]
+        let nc := c_erased.appendLits #[litl1, Lit.fromSingleExpr e false]
         trace[duper.rule.identBoolHoist] s!"New Clause: {nc.lits.map Lit.toExpr}"
         let cp1 ← yieldClause nc "identity loobHoist" (some (mkBoolHoistProof pos true))
-        let nc := c_erased.appendLits
-          #[← litl.replaceAtPos! ⟨s, p⟩ (mkConst ``False), Lit.fromSingleExpr e true]
+        let nc := c_erased.appendLits #[litl2, Lit.fromSingleExpr e true]
         trace[duper.rule.identBoolHoist] s!"New Clause: {nc.lits.map Lit.toExpr}"
         let cp2 ← yieldClause nc "identity boolHoist" (some (mkBoolHoistProof pos false))
         return some #[cp1, cp2]

Duper/Rules/NeHoist.lean

@@ -86,7 +86,9 @@ def neHoistAtExpr (e : Expr) (pos : ClausePos) (given : Clause) (c : MClause) :
         return none
       -- All side conditions have been met. Yield the appropriate clause
       let cErased := c.eraseLit pos.lit
-      let newClause := cErased.appendLits #[← lit.replaceAtPos! ⟨pos.side, pos.pos⟩ (mkConst ``True), Lit.fromExpr freshVarEquality]
+      let some newLit ← lit.replaceAtPosUpdateType? ⟨pos.side, pos.pos⟩ (mkConst ``True)
+        | return none -- If `lit` can't be safely changed at position `pos`, then don't apply `neHoist` at `pos`
+      let newClause := cErased.appendLits #[newLit, Lit.fromExpr freshVarEquality]
       trace[duper.rule.neHoist] "Created {newClause.lits} from {c.lits}"
       let mkProof := mkNeHoistProof pos
       yieldClause newClause "neHoist" mkProof (transferExprs := #[freshVar1, freshVar2])

Duper/Rules/Superposition.lean

@@ -248,7 +248,8 @@ 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
+        let some mainPremise ← mainPremise.replaceAtPosUpdateType? mainPremisePos sidePremiseRhs
+          | return none -- If `mainPremise` can't be safely changed at `mainPremisePos`, then don't apply `superposition` at `mainPremisePos`
         /- 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)
@@ -258,7 +259,9 @@ def superpositionAtLitWithPartner (mainPremise : MClause) (mainPremiseNum : Nat)
            of the original rewrite -/
         poses := poses.push mainPremisePos
       else
-        mainPremiseReplaced ← mainPremise.replaceAtPos! mainPremisePos sidePremiseRhs
+        match ← mainPremise.replaceAtPosUpdateType? mainPremisePos sidePremiseRhs with
+        | some updatedMainPremise => mainPremiseReplaced := updatedMainPremise
+        | none => return none -- If `mainPremise` can't be safely changed at `mainPremisePos`, then don't apply `superposition` at `mainPremisePos`
 
       if mainPremiseReplaced.isTrivial then
         if (enableWCTrace && ((mainPremiseNum == wc1 && sidePremiseNum == wc2) || (mainPremiseNum == wc2 && sidePremiseNum == wc1))) then

README.md

@@ -36,6 +36,8 @@ Duper is a terminal tactic that will look at the current main goal and either so
 The `facts` supplied to Duper are separated by commas and can include:
 - Hypotheses (of type `Prop`) from the local context
 - External lemmas
+- Definitions (which will prompt Duper to use the defining equations for each provided definition)
+- Recursors (which will prompt Duper to produce definitional equations for each provided recursor)
 - The symbol `*` to indicate that Duper should consider all proofs in the current local context
 
 If the `[facts]` argument are omitted from the Duper call, then Duper will only reason about the goal, meaning `by duper` is equivalent to `by duper []`. Duper performs best when it is given a minimal set of facts that can be used to prove the goal, and it also performs better when more specific lemmas are used (e.g. Duper will generally perform better if given `Nat.mul_one` rather than `mul_one`, though it is capable of working with either). We do not yet have Duper connected to a relevance filter so for now it is necessary to manually provide Duper all of the lemmas it needs, though we hope to improve this state of affairs in the future.

lake-manifest.json

@@ -4,10 +4,10 @@
  [{"url": "https://github.com/leanprover-community/lean-auto.git",
    "type": "git",
    "subDir": null,
-   "rev": "bfb20f93b4e67029b977f218c67d8ca87ca09c9a",
+   "rev": "1ba441f1d385cc2a7eebd927a5d2aa71b40fbd7a",
    "name": "auto",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "bfb20f93b4e67029b977f218c67d8ca87ca09c9a",
+   "inputRev": "1ba441f1d385cc2a7eebd927a5d2aa71b40fbd7a",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/batteries",

lakefile.lean

@@ -2,7 +2,7 @@ import Lake
 
 open Lake DSL
 
-require auto from git "https://github.com/leanprover-community/lean-auto.git"@"bfb20f93b4e67029b977f218c67d8ca87ca09c9a"
+require auto from git "https://github.com/leanprover-community/lean-auto.git"@"1ba441f1d385cc2a7eebd927a5d2aa71b40fbd7a"
 require batteries from git "https://github.com/leanprover-community/batteries" @ "v4.9.1"
 
 package Duper {