From bc01394cd3c99e454304cd7d52f308c21d52e810 Mon Sep 17 00:00:00 2001 From: JOSHCLUNE Date: Sat, 27 Jul 2024 12:31:59 -0400 Subject: [PATCH 1/4] Update lean-auto --- lake-manifest.json | 4 ++-- lakefile.lean | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/lake-manifest.json b/lake-manifest.json index 8cf38cb..d2d3ce7 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -4,10 +4,10 @@ [{"url": "https://github.com/leanprover-community/lean-auto.git", "type": "git", "subDir": null, - "rev": "bfb20f93b4e67029b977f218c67d8ca87ca09c9a", + "rev": "320d2cdf10d8d9875b0533a61023ee589b8e08e5", "name": "auto", "manifestFile": "lake-manifest.json", - "inputRev": "bfb20f93b4e67029b977f218c67d8ca87ca09c9a", + "inputRev": "320d2cdf10d8d9875b0533a61023ee589b8e08e5", "inherited": false, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/batteries", diff --git a/lakefile.lean b/lakefile.lean index 18facb8..33767ef 100644 --- a/lakefile.lean +++ b/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"@"320d2cdf10d8d9875b0533a61023ee589b8e08e5" require batteries from git "https://github.com/leanprover-community/batteries" @ "v4.9.1" package Duper { From 0557795029bc82edd440ec8dfb726e17889241b8 Mon Sep 17 00:00:00 2001 From: JOSHCLUNE Date: Sat, 27 Jul 2024 12:52:50 -0400 Subject: [PATCH 2/4] Update lean-auto --- lake-manifest.json | 4 ++-- lakefile.lean | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/lake-manifest.json b/lake-manifest.json index d2d3ce7..0071614 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -4,10 +4,10 @@ [{"url": "https://github.com/leanprover-community/lean-auto.git", "type": "git", "subDir": null, - "rev": "320d2cdf10d8d9875b0533a61023ee589b8e08e5", + "rev": "1ba441f1d385cc2a7eebd927a5d2aa71b40fbd7a", "name": "auto", "manifestFile": "lake-manifest.json", - "inputRev": "320d2cdf10d8d9875b0533a61023ee589b8e08e5", + "inputRev": "1ba441f1d385cc2a7eebd927a5d2aa71b40fbd7a", "inherited": false, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/batteries", diff --git a/lakefile.lean b/lakefile.lean index 33767ef..e51f9b7 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -2,7 +2,7 @@ import Lake open Lake DSL -require auto from git "https://github.com/leanprover-community/lean-auto.git"@"320d2cdf10d8d9875b0533a61023ee589b8e08e5" +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 { From c2d45b0ba46e2317a45174e6f99772fd8cc28ea0 Mon Sep 17 00:00:00 2001 From: JOSHCLUNE Date: Sun, 28 Jul 2024 22:26:41 -0400 Subject: [PATCH 3/4] replaceAtPos! -> replaceAtPosUpdateType? We still call replaceAtPos! during proof reconstruction, but now, when generating inferences and applying simplification rules, we only use replaceAtPosUpdateType? to avoid inadvertently rewriting a term that other terms depend on --- Duper/Clause.lean | 2 +- Duper/Rules/BoolHoist.lean | 4 +++- Duper/Rules/Demodulation.lean | 6 ++++-- Duper/Rules/EqHoist.lean | 4 +++- Duper/Rules/FluidBoolHoist.lean | 8 ++++++-- Duper/Rules/FluidSup.lean | 3 ++- Duper/Rules/IdentBoolHoist.lean | 10 ++++++---- Duper/Rules/NeHoist.lean | 4 +++- Duper/Rules/Superposition.lean | 7 +++++-- 9 files changed, 33 insertions(+), 15 deletions(-) diff --git a/Duper/Clause.lean b/Duper/Clause.lean index 9747405..0c74449 100644 --- a/Duper/Clause.lean +++ b/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 diff --git a/Duper/Rules/BoolHoist.lean b/Duper/Rules/BoolHoist.lean index 1b895ff..6c627d9 100644 --- a/Duper/Rules/BoolHoist.lean +++ b/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"] diff --git a/Duper/Rules/Demodulation.lean b/Duper/Rules/Demodulation.lean index e7600fb..a15e999 100644 --- a/Duper/Rules/Demodulation.lean +++ b/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}" diff --git a/Duper/Rules/EqHoist.lean b/Duper/Rules/EqHoist.lean index 1e1ebff..7da9c7c 100644 --- a/Duper/Rules/EqHoist.lean +++ b/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]) diff --git a/Duper/Rules/FluidBoolHoist.lean b/Duper/Rules/FluidBoolHoist.lean index 80660e9..6e899c2 100644 --- a/Duper/Rules/FluidBoolHoist.lean +++ b/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]) diff --git a/Duper/Rules/FluidSup.lean b/Duper/Rules/FluidSup.lean index b98e57c..52548d1 100644 --- a/Duper/Rules/FluidSup.lean +++ b/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 diff --git a/Duper/Rules/IdentBoolHoist.lean b/Duper/Rules/IdentBoolHoist.lean index 4fbd8d0..3816341 100644 --- a/Duper/Rules/IdentBoolHoist.lean +++ b/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] diff --git a/Duper/Rules/NeHoist.lean b/Duper/Rules/NeHoist.lean index 8a7ca1b..32e0a3a 100644 --- a/Duper/Rules/NeHoist.lean +++ b/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]) diff --git a/Duper/Rules/Superposition.lean b/Duper/Rules/Superposition.lean index 2ca0719..4276f93 100644 --- a/Duper/Rules/Superposition.lean +++ b/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 From eadea024a7ce233792482f214377adb2ac627d34 Mon Sep 17 00:00:00 2001 From: JOSHCLUNE Date: Sun, 28 Jul 2024 23:54:25 -0400 Subject: [PATCH 4/4] Mention that Duper can take definitions and recurors in README --- README.md | 2 ++ 1 file changed, 2 insertions(+) diff --git a/README.md b/README.md index 85b6daf..324c867 100644 --- a/README.md +++ b/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.