From 88204f71f5e2bb8bf39be6a6eb52c77087cfed21 Mon Sep 17 00:00:00 2001 From: JOSHCLUNE Date: Tue, 14 Nov 2023 00:00:32 -0500 Subject: [PATCH] Updating clause selection strategy There is still more work to be done on the clause selection strategy (some of which is documented at the stop of StrategyHeap.lean), but this commit already makes Duper able to solve one of the problems in DuperOnMathlib/Function.lean that it couldn't before. --- Duper/ClauseStreamHeap.lean | 12 ++++- Duper/ProverM.lean | 27 ++++++---- Duper/Simp.lean | 17 +++--- Duper/Tests/test_regression.lean | 1 + Duper/Util/StrategyHeap.lean | 59 +++++++++++++++------ Duper/Util/TypeInhabitationReasoning.lean | 59 +++++++++++++-------- DuperOnMathlib/DuperOnMathlib/Function.lean | 13 ++--- DuperOnMathlib/DuperOnMathlib/Prime.lean | 2 +- 8 files changed, 126 insertions(+), 64 deletions(-) diff --git a/Duper/ClauseStreamHeap.lean b/Duper/ClauseStreamHeap.lean index e6026c4..0f65e1b 100644 --- a/Duper/ClauseStreamHeap.lean +++ b/Duper/ClauseStreamHeap.lean @@ -136,15 +136,23 @@ def ClauseStreamHeap.fairProbe {σ} [OptionMStream ProverM σ ClauseProof] -- Note: This function is responsible for adding results of inference rules to the passive set. def ProverM.postProcessInferenceResult (cp : ClauseProof) : ProverM Unit := do let (given, c, proof) := cp + let allClauses ← getAllClauses + let parentClauseInfoOpts ← proof.parents.mapM + (fun p => + match allClauses.find? p.clause with + | some pi => pure pi + | none => throwError "ProverM.postProcessInferenceResult: Unable to find parent clause {p.clause}") + -- 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 match ← immediateSimplification given c with | some subsumingClause => -- subsumingClause subsumes c so we can remove c and only need to add subsumingClause removeClause given [subsumingClause] if c == subsumingClause then - addNewToPassive c proof (proof.parents.map (fun p => p.clause)) + addNewToPassive c proof generationNumber (proof.parents.map (fun p => p.clause)) else throwError "Unable to find {subsumingClause} in resultClauses" | none => -- No result clause subsumes c, so add each result clause to the passive set - addNewToPassive c proof (proof.parents.map (fun p => p.clause)) + addNewToPassive c proof generationNumber (proof.parents.map (fun p => p.clause)) def ProverM.performInferences (rules : List (Clause → MClause → Nat → RuleM (Array ClauseStream))) (given : Clause) : ProverM Unit := do trace[Prover.saturate] "perform inference with given clause {given}" diff --git a/Duper/ProverM.lean b/Duper/ProverM.lean index 39c8806..37446a3 100644 --- a/Duper/ProverM.lean +++ b/Duper/ProverM.lean @@ -33,6 +33,7 @@ open Result structure ClauseInfo where (number : Nat) +(generationNumber : Nat) -- The total number of inference (not simplification) rules that were used to create this clause (proof : Proof) (generatingAncestors : Array Clause) (descendants : List Clause) @@ -45,7 +46,7 @@ abbrev FairAgeClauseHeap := StrategyHeap Clause (β:=Nat) abbrev abstractedMVarList := List Meta.AbstractMVarsResult abbrev abstractedMVarAndClauseList := List (Meta.AbstractMVarsResult × Clause) -instance : ToMessageData Result := +instance : ToMessageData Result := ⟨fun r => match r with | unknown => "unknown" | saturated => "saturated" @@ -103,6 +104,7 @@ instance [MetaEval α] : MetaEval (ProverM α) := initialize registerTraceClass `Prover registerTraceClass `Prover.saturate + registerTraceClass `Prover.createdClauses def getInstanceMaxHeartbeats : ProverM Nat := return (← get).instanceMaxHeartbeats @@ -259,7 +261,7 @@ def markAsDescendantToGeneratingAncestors (c : Clause) (generatingAncestors : Ar /-- Registers a new clause, but does not add it to active or passive set. Typically, you'll want to use `addNewToPassive` instead. -/ -def addNewClause (c : Clause) (proof : Proof) (generatingAncestors : Array Clause) : ProverM ClauseInfo := do +def addNewClause (c : Clause) (proof : Proof) (generationNumber : Nat) (generatingAncestors : Array Clause) : ProverM ClauseInfo := do markAsDescendantToGeneratingAncestors c generatingAncestors let allClauses ← getAllClauses let ci ← (do @@ -274,6 +276,7 @@ def addNewClause (c : Clause) (proof : Proof) (generatingAncestors : Array Claus | none => let ci : ClauseInfo := { number := allClauses.size + generationNumber := generationNumber proof := proof generatingAncestors := generatingAncestors descendants := [] @@ -282,7 +285,7 @@ def addNewClause (c : Clause) (proof : Proof) (generatingAncestors : Array Claus } setAllClauses (allClauses.insert c ci) if ← getInhabitationReasoningM then - if c.lits.size == 0 && c.bVarTypes.size == 0 then + if c.lits.size == 0 && c.bVarTypes.size == 0 then setEmptyClause c throwEmptyClauseException return ci @@ -295,11 +298,15 @@ def addNewClause (c : Clause) (proof : Proof) (generatingAncestors : Array Claus let parentInfos := proof.parents.map (fun p => allClauses.find! p.clause) m!"New clause #{ci.number} by {proof.ruleName} on {parentInfos.map (fun i => i.number)}: {c}" ) + trace[Prover.createdClauses] ( + let parentInfos := proof.parents.map (fun p => allClauses.find! p.clause) + m!"New clause #{ci.number} by {proof.ruleName} on {parentInfos.map (fun i => i.number)}: {c}" + ) return ci /-- Registers a new clause and adds it to the passive set. The `generatingAncestors` argument contains the list of clauses that were used to generate `c` (or `c`'s ancestor which generated `c` by a modifying inference). See page 8 of "E – A Brainiac Theorem Prover" -/ -def addNewToPassive (c : Clause) (proof : Proof) (generatingAncestors : Array Clause) : ProverM Unit := do +def addNewToPassive (c : Clause) (proof : Proof) (generationNumber : Nat) (generatingAncestors : Array Clause) : ProverM Unit := do match (← getAllClauses).find? c with | some ci => if (ci.wasSimplified) then pure () -- No need to add c to the passive set because it would just be simplified away later @@ -309,17 +316,17 @@ def addNewToPassive (c : Clause) (proof : Proof) (generatingAncestors : Array Cl let ci := {ci with generatingAncestors := generatingAncestors, isOrphan := false} setAllClauses ((← getAllClauses).insert c ci) markAsDescendantToGeneratingAncestors c generatingAncestors -- For each generating ancestor of c, add c as a descendant of said ancestor - setPassiveSet $ (← getPassiveSet).insert c c.weight ci.number + setPassiveSet $ (← getPassiveSet).insert c c.weight (ci.generationNumber, ci.number) else pure () -- c exists in allClauses and is not an orphan, so it has already been produced and can safely be ignored | none => - let ci ← addNewClause c proof generatingAncestors - setPassiveSet $ (← getPassiveSet).insert c c.weight ci.number + let ci ← addNewClause c proof generationNumber generatingAncestors + setPassiveSet $ (← getPassiveSet).insert c c.weight (ci.generationNumber, ci.number) /-- Takes a clause that was generated by preprocessing clausification and re-adds it to the passive set and its associated heaps -/ def addClausifiedToPassive (c : Clause) : ProverM Unit := do match (← getAllClauses).find? c with | some ci => - setPassiveSet $ (← getPassiveSet).insert c c.weight ci.number + setPassiveSet $ (← getPassiveSet).insert c c.weight (ci.generationNumber, ci.number) | none => throwError "Unable to find information for clausified clause {c}" def ProverM.runWithExprs (x : ProverM α) (es : List (Expr × Expr × Array Name)) (ctx : Context) (s : State) : MetaM (α × State) := do @@ -327,7 +334,7 @@ def ProverM.runWithExprs (x : ProverM α) (es : List (Expr × Expr × Array Name for (e, proof, paramNames) in es do let c := Clause.fromSingleExpr paramNames e let mkProof := fun _ _ _ _ => pure proof - addNewToPassive c {parents := #[], ruleName := "assumption", mkProof := mkProof} #[] + addNewToPassive c {parents := #[], ruleName := "assumption", mkProof := mkProof} 0 #[] x @[inline] def runRuleM (x : RuleM α) : ProverM.ProverM α := do @@ -541,4 +548,4 @@ def immediateSimplification (givenClause : Clause) (resultClause : Clause) : return none end ProverM -end Duper \ No newline at end of file +end Duper diff --git a/Duper/Simp.lean b/Duper/Simp.lean index b86af16..988dde0 100644 --- a/Duper/Simp.lean +++ b/Duper/Simp.lean @@ -52,7 +52,7 @@ abbrev BackwardSimpRule := Clause → ProverM Unit def MSimpRule.toSimpRule (rule : MSimpRule) : SimpRule := fun givenClause => do let res ← runRuleM (rule givenClause) match res with - | none => + | none => return Unapplicable | some cs => do trace[Simplification.debug] "About to remove {givenClause} because it was simplified away to produce {cs.map (fun x => x.1)}" @@ -64,10 +64,12 @@ def MSimpRule.toSimpRule (rule : MSimpRule) : SimpRule := fun givenClause => do | some givenClauseInfo => -- For forward simplification rules, each result clause has the same set of generating ancestors as givenClause let generatingAncestors := givenClauseInfo.generatingAncestors + -- For forward simplification rules, each result clause has the same generation number as givenClause + let generationNumber := givenClauseInfo.generationNumber -- Register and return first result clause without adding it to the active or passive set. Add other result clauses to passive set - let ci ← addNewClause c proof generatingAncestors + let ci ← addNewClause c proof generationNumber generatingAncestors for (c, proof) in restCs do - addNewToPassive c proof generatingAncestors + addNewToPassive c proof generationNumber generatingAncestors if ci.wasSimplified then return Removed -- No need to continue working on c because we've already seen previously that it will be simplified away return Applied c | none => throwError "givenClause {givenClause} was not found" @@ -77,16 +79,17 @@ def BackwardMSimpRule.toBackwardSimpRule (rule : BackwardMSimpRule) : BackwardSi let backwardSimpRes ← runRuleM do withoutModifyingMCtx do rule givenClause - let mut generatingAncestorsArray : Array (Array Clause) := #[] + let mut generatingNumberAndAncestorsArray : Array (Nat × Array Clause) := #[] -- It is important that we remove each clause in clausesToRemove before reading the newly generated clauses for (c, _) in backwardSimpRes do trace[Simplification.debug] "About to remove {c} because it was simplified away" removeClause c [givenClause] -- givenClause must be protected when we remove c and its descendants because givenClause was used to eliminate c match (← getAllClauses).find? c with - | some ci => generatingAncestorsArray := generatingAncestorsArray.push ci.generatingAncestors + | some ci => + generatingNumberAndAncestorsArray := generatingNumberAndAncestorsArray.push (ci.generationNumber, ci.generatingAncestors) | none => throwError "Could not find {c} in all clauses" - for (generatingAncestors, _, ocp) in generatingAncestorsArray.zip backwardSimpRes do + for ((generationNumber, generatingAncestors), _, ocp) in generatingNumberAndAncestorsArray.zip backwardSimpRes do if let some (c, proof) := ocp then - addNewToPassive c proof generatingAncestors + addNewToPassive c proof generationNumber generatingAncestors end Duper diff --git a/Duper/Tests/test_regression.lean b/Duper/Tests/test_regression.lean index 8ec2c1e..0028e95 100644 --- a/Duper/Tests/test_regression.lean +++ b/Duper/Tests/test_regression.lean @@ -540,6 +540,7 @@ def neg3 : g (True → True) (fun _ => True.intro) = g (True → True) (fun _ => end NegativeBoolSimpTests /- ClauseStreamHeap tests -/ +set_option maxHeartbeats 250000 in tptp MGT008 "../TPTP-v8.0.0/Problems/MGT/MGT008+1.p" by duper [*] {portfolioInstance := 3} -- Runs out of time if run in portfolio mode diff --git a/Duper/Util/StrategyHeap.lean b/Duper/Util/StrategyHeap.lean index dd622d6..b8515db 100644 --- a/Duper/Util/StrategyHeap.lean +++ b/Duper/Util/StrategyHeap.lean @@ -6,11 +6,30 @@ open Std namespace Duper +/-- The age of each clause will be treated as a tuple of Nats. The first Nat in the tuple will be the + number of inference (not simplification) rules that have been used to generate the clause. The second + Nat in the tuple will be the clause id (lower ids are created before greater ids). This method is + used rather than just using the clause id (which would be a fair measure of Age) because empirically, + having generation number (the number of inference rules used to generate a clause) be a consideration in + clause selection helps problems where there are large facts that aren't clausified all at once (e.g. if + a clause has lit `p ↔ q`, then two clauses will be generated via clausification, and it can take a very + long time for the second one to be selected). + + Note: This current strategy does not guarantee total fairness in the presence of inference rules that can + generate infinitely many children. + + TODO: Rather than make the generation number the first Nat in an age heap, just add an additional generation + heap to be used in addition to the weight and age heaps. The age heap would then guarantee fairness and the + generation heap would hopefully confer the same empirical benefits that this strategy has over just using + clause id for fairness. -/ +def Age := Nat × Nat +def Age.le (x y : Age) : Bool := x.1 < y.1 || (x.1 = y.1 && x.2 ≤ y.2) + -- `StrategyHeap` models GivenClause Selection structure StrategyHeap (α : Type u) {β : Type} [BEq α] [Hashable α] where set : HashSet α := HashSet.empty -- Set of elements of `α` weightheap : BinomialHeap (Nat × α) fun c d => c.1 ≤ d.1 := BinomialHeap.empty - ageheap : BinomialHeap (Nat × α) fun c d => c.1 ≤ d.1 := BinomialHeap.empty + ageheap : BinomialHeap (Age × α) (fun c d => Age.le c.1 d.1) := BinomialHeap.empty status : β strategy : β → Bool × β deriving Inhabited @@ -28,7 +47,7 @@ def StrategyHeap.toList [BEq α] [Hashable α] (sh : StrategyHeap α (β:=β)) := sh.set.toList @[inline] def StrategyHeap.insert [BEq α] [Hashable α] - (sh : StrategyHeap α (β:=β)) (x : α) (weight age : Nat) : StrategyHeap α (β:=β) := + (sh : StrategyHeap α (β:=β)) (x : α) (weight : Nat) (age : Age) : StrategyHeap α (β:=β) := {sh with set := sh.set.insert x, ageheap := sh.ageheap.insert (age, x), weightheap := sh.weightheap.insert (weight, x)} @@ -40,31 +59,41 @@ def StrategyHeap.toList [BEq α] [Hashable α] @[inline] partial def StrategyHeap.pop? [BEq α] [Hashable α] (sh : StrategyHeap α (β:=β)) : Option (α × StrategyHeap α (β:=β)) := Id.run <| do let (hid, status') := sh.strategy sh.status - let mut heap := if hid then sh.weightheap else sh.ageheap - while true do - if let some (x, h') := heap.deleteMin then - let x := x.2 - if sh.set.contains x then - if hid then + if hid then + let mut heap := sh.weightheap + while true do + if let some (x, h') := heap.deleteMin then + let x := x.2 + if sh.set.contains x then return (x, {sh with set := sh.set.erase x, weightheap := heap, status := status'}) else + heap := h' + else + break + return none + else + let mut heap := sh.ageheap + while true do + if let some (x, h') := heap.deleteMin then + let x := x.2 + if sh.set.contains x then return (x, {sh with set := sh.set.erase x, ageheap := heap, status := status'}) + else + heap := h' else - heap := h' - else - break - return none + break + return none -- The clause heap, for givenClause selection -- The size of `heaps` should be 2. The first heap is the -- weight heap and the second heap is the age heap abbrev FairAgeHeap (α : Type u) [BEq α] [Hashable α] := StrategyHeap α (β:=Nat) - + abbrev FairAgeHeap.empty (α : Type u) [BEq α] [Hashable α] (fN : Nat) : FairAgeHeap α := -- status : fairnessCounter -- true : weight heap @@ -75,7 +104,7 @@ abbrev FairAgeHeap.empty (α : Type u) [BEq α] [Hashable α] (fN : Nat) : FairA private def heap₁ := Id.run <| do let mut fah := FairAgeHeap.empty Nat 3 for i in List.range 40 do - fah := fah.insert i (2 * i) (100 - (i - 20) * (i - 20)) + fah := fah.insert i (2 * i) (0, 100 - (i - 20) * (i - 20)) return fah private def testheap₁ : IO Unit := do @@ -87,4 +116,4 @@ private def testheap₁ : IO Unit := do else println! "No" -#eval testheap₁ \ No newline at end of file +#eval testheap₁ diff --git a/Duper/Util/TypeInhabitationReasoning.lean b/Duper/Util/TypeInhabitationReasoning.lean index 5e90c76..8c7763d 100644 --- a/Duper/Util/TypeInhabitationReasoning.lean +++ b/Duper/Util/TypeInhabitationReasoning.lean @@ -42,7 +42,7 @@ def mkRemoveVanishedVarsProof (premises : List Expr) (parents : List ProofParent /-- mkDeriveNewNonemptyTypeProof1 expects to receive one parent of the form `Nonempty (t1 → t2) = True` where `t1` is a type in verifiedInhabitedTypes (and is therefore a type whose inhabitation status can be confirmed by Lean.Meta.findInstance). - + Note: Right now, mkDeriveNewNonemptyTypeProof1 does not support lemmas of the form `True = Nonempty t`, and I think this is fine because Duper should never generate clauses of that form. However, if for some reason this ever becomes a problem, it should be straightforward to extend mkDeriveNewNonemptyTypeProof1 to support that case. -/ @@ -63,7 +63,7 @@ def mkDeriveNewNonemptyTypeProof1 (premises : List Expr) (parents : List ProofPa /-- mkDeriveNewNonemptyTypeProof2 expects to receive two parents, first a clause that says `Nonempty (t1 → t2) = True` and second a clause that says `Nonempty t1 = True`. - + Note: Right now, mkDeriveNewNonemptyTypeProof2 does not support lemmas of the form `True = Nonempty t`, and I think this is fine because Duper should never generate clauses of that form. However, if for some reason this ever becomes a problem, it should be straightforward to extend mkDeriveNewNonemptyTypeProof2 to support that case. -/ @@ -117,7 +117,7 @@ def mkDeriveNewNonemptyTypeProof2 (premises : List Expr) (parents : List ProofPa /-- mkDeriveNewNonemptyTypeProof3 expects to receive one parent of the form `Nonempty (t1 × t2) = True` and yields a proof of `Nonempty t1 = True`. - + Note: Right now, mkDeriveNewNonemptyTypeProof3 does not support lemmas of the form `True = Nonempty t`, and I think this is fine because Duper should never generate clauses of that form. However, if for some reason this ever becomes a problem, it should be straightforward to extend mkDeriveNewNonemptyTypeProof2 to support that case. -/ @@ -135,7 +135,7 @@ def mkDeriveNewNonemptyTypeProof3 (premises : List Expr) (parents : List ProofPa /-- mkDeriveNewNonemptyTypeProof4 expects to receive one parent of the form `Nonempty (t1 × t2) = True` and yields a proof of `Nonempty t2 = True`. - + Note: Right now, mkDeriveNewNonemptyTypeProof4 does not support lemmas of the form `True = Nonempty t`, and I think this is fine because Duper should never generate clauses of that form. However, if for some reason this ever becomes a problem, it should be straightforward to extend mkDeriveNewNonemptyTypeProof2 to support that case. -/ @@ -153,7 +153,7 @@ def mkDeriveNewNonemptyTypeProof4 (premises : List Expr) (parents : List ProofPa /-- mkDeriveNewNonemptyTypeProof5 expects to receive one parent of the form `Nonempty (PProd t1 t2) = True` and yields a proof of `Nonempty t1 = True`. - + Note: Right now, mkDeriveNewNonemptyTypeProof5 does not support lemmas of the form `True = Nonempty t`, and I think this is fine because Duper should never generate clauses of that form. However, if for some reason this ever becomes a problem, it should be straightforward to extend mkDeriveNewNonemptyTypeProof2 to support that case. -/ @@ -171,7 +171,7 @@ def mkDeriveNewNonemptyTypeProof5 (premises : List Expr) (parents : List ProofPa /-- mkDeriveNewNonemptyTypeProof6 expects to receive one parent of the form `Nonempty (PProd t1 t2) = True` and yields a proof of `Nonempty t2 = True`. - + Note: Right now, mkDeriveNewNonemptyTypeProof6 does not support lemmas of the form `True = Nonempty t`, and I think this is fine because Duper should never generate clauses of that form. However, if for some reason this ever becomes a problem, it should be straightforward to extend mkDeriveNewNonemptyTypeProof2 to support that case. -/ @@ -189,7 +189,7 @@ def mkDeriveNewNonemptyTypeProof6 (premises : List Expr) (parents : List ProofPa /-- mkDeriveNewNonemptyTypeProof7 expects to receive one parent of the form `Nonempty p = True` where `p : Prop`. mkDeriveNewNonemptyTypeProof6 yields a proof that `p = True`. - + Note: Right now, mkDeriveNewNonemptyTypeProof7 does not support lemmas of the form `True = Nonempty t`, and I think this is fine because Duper should never generate clauses of that form. However, if for some reason this ever becomes a problem, it should be straightforward to extend mkDeriveNewNonemptyTypeProof2 to support that case. -/ @@ -290,7 +290,7 @@ def removeVanishedVarsHelper (c : Clause) (verifiedInhabitedTypes : abstractedMV that the clause should not be used to simplify away any other clauses. Otherwise, `removeVanishedVars` returns the updated clause and true. The only case where `removeVanishedVars` will return none is if it generates a clause that has already been simplified away (and therefore does not need to be re-evaluated). - + Note: removeVanishedVars is not written as a forward simplification rule (even though it functions similarly) because it uniquely interacts with ProverM's verifiedInhabitedTypes and potentiallyUninhabitedTypes. -/ def removeVanishedVars (givenClause : Clause) : ProverM (Option (Clause × Bool)) := do @@ -306,7 +306,8 @@ def removeVanishedVars (givenClause : Clause) : ProverM (Option (Clause × Bool) match (← getAllClauses).find? givenClause with | some givenClauseInfo => let generatingAncestors := givenClauseInfo.generatingAncestors - let ci ← addNewClause c cProof generatingAncestors + let generationNumber := givenClauseInfo.generationNumber + let ci ← addNewClause c cProof generationNumber generatingAncestors if ci.wasSimplified then return none -- No need to continue working on c because we've already seen previously that it will be simplified away return some (c, false) | none => throwError "givenClause {givenClause} was not found" @@ -315,7 +316,8 @@ def removeVanishedVars (givenClause : Clause) : ProverM (Option (Clause × Bool) match (← getAllClauses).find? givenClause with | some givenClauseInfo => let generatingAncestors := givenClauseInfo.generatingAncestors - let ci ← addNewClause c cProof generatingAncestors + let generationNumber := givenClauseInfo.generationNumber + let ci ← addNewClause c cProof generationNumber generatingAncestors if ci.wasSimplified then return none -- No need to continue working on c because we've already seen previously that it will be simplified away return some (c, true) | none => throwError "givenClause {givenClause} was not found" @@ -367,7 +369,8 @@ def deriveNewNonemptyTypesHelper (abstractedT : AbstractMVarsResult) (givenClaus match (← getAllClauses).find? c with | some cInfo => let generatingAncestors := cInfo.generatingAncestors ++ givenClauseInfo.generatingAncestors - addNewToPassive t2NonemptyClause t2NonemptyProof generatingAncestors + let generationNumber := givenClauseInfo.generationNumber + addNewToPassive t2NonemptyClause t2NonemptyProof generationNumber generatingAncestors | none => throwError "{c} from verifiedNonemptyTypes was not found" | none => throwError "givenClause {givenClause} was not found" | _ => throwError "Inconsistency between original and abstracted type" @@ -378,7 +381,7 @@ def deriveNewNonemptyTypesHelper (abstractedT : AbstractMVarsResult) (givenClaus - If `abstracted.expr` has the form `t1 × t2` (where `×` denotes either `Prod` or `PProd`) then derive `Nonempty t1` and `Nonempty t2` - If `abstractedT.expr` has the form `t1 → t2` and `t1` is Inhabited or Nonempty, then derive `Nonempty t2` - If any type in verifiedNonemptyTypes has the form `t1 → t2` and `abstractedT` matches `t1`, then derive `Nonempty t2` - + Jointly, these rules keep verifiedNonemptyTypes saturated with respect to application in the long run. Temporarily, verifiedNonemptyTypes can have a state where `α` `α → β` are both in verifiedNonemptyTypes but `β` is not, but this will only occur after `deriveNewNonemptyTypes` returns if either `Nonempty α` or `Nonempty (α → β)` was generated by @@ -406,7 +409,8 @@ def deriveNewNonemptyTypes (abstractedT : AbstractMVarsResult) (givenClause : Cl match (← getAllClauses).find? givenClause with | some givenClauseInfo => let generatingAncestors := givenClauseInfo.generatingAncestors - addNewToPassive t2NonemptyClause t2NonemptyProof generatingAncestors + let generationNumber := givenClauseInfo.generationNumber + addNewToPassive t2NonemptyClause t2NonemptyProof generationNumber generatingAncestors | none => throwError "givenClause {givenClause} was not found" else match ← deriveNonempty t1' verifiedNonemptyTypes with @@ -423,7 +427,8 @@ def deriveNewNonemptyTypes (abstractedT : AbstractMVarsResult) (givenClause : Cl match (← getAllClauses).find? givenClause with | some givenClauseInfo => let generatingAncestors := givenClauseInfo.generatingAncestors - addNewToPassive t2NonemptyClause t2NonemptyProof generatingAncestors + let generationNumber := givenClauseInfo.generationNumber + addNewToPassive t2NonemptyClause t2NonemptyProof generationNumber generatingAncestors | none => throwError "givenClause {givenClause} was not found" | none => if potentinallyUninhabitedTypes.contains t1' then pure () @@ -442,7 +447,8 @@ def deriveNewNonemptyTypes (abstractedT : AbstractMVarsResult) (givenClause : Cl match (← getAllClauses).find? givenClause with | some givenClauseInfo => let generatingAncestors := givenClauseInfo.generatingAncestors - addNewToPassive t2NonemptyClause t2NonemptyProof generatingAncestors + let generationNumber := givenClauseInfo.generationNumber + addNewToPassive t2NonemptyClause t2NonemptyProof generationNumber generatingAncestors | none => throwError "givenClause {givenClause} was not found" | none => -- We learned that Meta.findInstance can't find an instance for t1 so we update potentinallyUninhabitedTypes setPotentiallyUninhabitedTypes (t1' :: potentinallyUninhabitedTypes) @@ -458,7 +464,8 @@ def deriveNewNonemptyTypes (abstractedT : AbstractMVarsResult) (givenClause : Cl match (← getAllClauses).find? givenClause with | some givenClauseInfo => let generatingAncestors := givenClauseInfo.generatingAncestors - addNewToPassive t1NonemptyClause t1NonemptyProof generatingAncestors + let generationNumber := givenClauseInfo.generationNumber + addNewToPassive t1NonemptyClause t1NonemptyProof generationNumber generatingAncestors | none => throwError "givenClause {givenClause} was not found" let t2' ← abstractMVars t2 if !(verifiedInhabitedTypes.contains t2') && !(verifiedNonemptyTypes.any (fun (t, _) => t == t2')) then @@ -470,7 +477,8 @@ def deriveNewNonemptyTypes (abstractedT : AbstractMVarsResult) (givenClause : Cl match (← getAllClauses).find? givenClause with | some givenClauseInfo => let generatingAncestors := givenClauseInfo.generatingAncestors - addNewToPassive t2NonemptyClause t2NonemptyProof generatingAncestors + let generationNumber := givenClauseInfo.generationNumber + addNewToPassive t2NonemptyClause t2NonemptyProof generationNumber generatingAncestors | none => throwError "givenClause {givenClause} was not found" deriveNewNonemptyTypesHelper abstractedT givenClause | Expr.app (Expr.app (Expr.const ``PProd lvls) t1) t2 => @@ -484,7 +492,8 @@ def deriveNewNonemptyTypes (abstractedT : AbstractMVarsResult) (givenClause : Cl match (← getAllClauses).find? givenClause with | some givenClauseInfo => let generatingAncestors := givenClauseInfo.generatingAncestors - addNewToPassive t1NonemptyClause t1NonemptyProof generatingAncestors + let generationNumber := givenClauseInfo.generationNumber + addNewToPassive t1NonemptyClause t1NonemptyProof generationNumber generatingAncestors | none => throwError "givenClause {givenClause} was not found" let t2' ← abstractMVars t2 if !(verifiedInhabitedTypes.contains t2') && !(verifiedNonemptyTypes.any (fun (t, _) => t == t2')) then @@ -496,7 +505,8 @@ def deriveNewNonemptyTypes (abstractedT : AbstractMVarsResult) (givenClause : Cl match (← getAllClauses).find? givenClause with | some givenClauseInfo => let generatingAncestors := givenClauseInfo.generatingAncestors - addNewToPassive t2NonemptyClause t2NonemptyProof generatingAncestors + let generationNumber := givenClauseInfo.generationNumber + addNewToPassive t2NonemptyClause t2NonemptyProof generationNumber generatingAncestors | none => throwError "givenClause {givenClause} was not found" deriveNewNonemptyTypesHelper abstractedT givenClause | _ => @@ -509,7 +519,8 @@ def deriveNewNonemptyTypes (abstractedT : AbstractMVarsResult) (givenClause : Cl match (← getAllClauses).find? givenClause with | some givenClauseInfo => let generatingAncestors := givenClauseInfo.generatingAncestors - addNewToPassive originalTEqTrueClause originalTEqTrueProof generatingAncestors + let generationNumber := givenClauseInfo.generationNumber + addNewToPassive originalTEqTrueClause originalTEqTrueProof generationNumber generatingAncestors | none => throwError "givenClause {givenClause} was not found" deriveNewNonemptyTypesHelper abstractedT givenClause @@ -548,13 +559,15 @@ def registerNewNonemptyTypes (givenClause : Clause) : ProverM Unit := do match (← getAllClauses).find? c with | some givenClauseInfo => let generatingAncestors := givenClauseInfo.generatingAncestors - addNewToPassive newC newCProof generatingAncestors + let generationNumber := givenClauseInfo.generationNumber + addNewToPassive newC newCProof generationNumber generatingAncestors | none => throwError "givenClause {givenClause} was not found" | NotVacuous (newC, newCProof) => -- Running removeVanishedVarsHelper generated a new clause that can directly be added to the passive set removeClause c -- We remove c and its descendants before readding newC to the passiveSet because newC makes c redundant match (← getAllClauses).find? c with | some givenClauseInfo => let generatingAncestors := givenClauseInfo.generatingAncestors - addNewToPassive newC newCProof generatingAncestors + let generationNumber := givenClauseInfo.generationNumber + addNewToPassive newC newCProof generationNumber generatingAncestors | none => throwError "givenClause {givenClause} was not found" - setPotentiallyVacuousClauses potentiallyVacuousClauses \ No newline at end of file + setPotentiallyVacuousClauses potentiallyVacuousClauses diff --git a/DuperOnMathlib/DuperOnMathlib/Function.lean b/DuperOnMathlib/DuperOnMathlib/Function.lean index fa3570a..a92dfd1 100644 --- a/DuperOnMathlib/DuperOnMathlib/Function.lean +++ b/DuperOnMathlib/DuperOnMathlib/Function.lean @@ -59,11 +59,8 @@ example : f '' (f ⁻¹' u) ⊆ u := by exact xmem -- Zipperposition (non-portfolio): 27 iterations in 0.083s --- TODO: Figure out why auto can solve this with maxHeartbeats 1000000 and kStep 100 but duper can't -set_option maxHeartbeats 1000000 in -set_option kStep 100 in example : f '' (f ⁻¹' u) ⊆ u := by - auto [subset_def, mem_image, mem_preimage] + duper [subset_def, mem_image, mem_preimage] {portfolioInstance := 2} example (h : Surjective f) : u ⊆ f '' (f ⁻¹' u) := by intro y yu @@ -151,7 +148,9 @@ example : s ∩ f ⁻¹' u ⊆ f ⁻¹' (f '' s ∩ u) := by exact ⟨⟨x, xs, rfl⟩, fxu⟩ -- Zipperposition (non-portfolio): 870 iterations in 1.644s --- TODO: Figure out why auto can solve this with maxHeartbeats 800000 but Duper can't +/- Currently, auto will solve this but duper won't. This could be for a number of reasons, but the most + likely one is that auto's premise selection (which only sends duper the facts that Zipperposition used + in its proof) is critically helpful for this problem. -/ set_option maxHeartbeats 800000 in -- Corresponds to 200000 heartbeats if portfolio mode were disabled example : s ∩ f ⁻¹' u ⊆ f ⁻¹' (f '' s ∩ u) := by intro x; auto [mem_inter_iff, mem_image, mem_preimage] @@ -163,7 +162,9 @@ example : s ∪ f ⁻¹' u ⊆ f ⁻¹' (f '' s ∪ u) := by right; exact fxu -- Zipperposition (non-portfolio): 387 iterations in 0.638s --- TODO: Figure out why auto can solve this with maxHeartbeats 800000 but Duper can't +/- Currently, auto will solve this but duper won't. This could be for a number of reasons, but the most + likely one is that auto's premise selection (which only sends duper the facts that Zipperposition used + in its proof) is critically helpful for this problem. -/ set_option maxHeartbeats 800000 in -- Corresponds to 200000 heartbeats if portfolio mode were disabled example : s ∪ f ⁻¹' u ⊆ f ⁻¹' (f '' s ∪ u) := by intro x; auto [mem_union, mem_image, mem_preimage] diff --git a/DuperOnMathlib/DuperOnMathlib/Prime.lean b/DuperOnMathlib/DuperOnMathlib/Prime.lean index 57fdb6e..f15ae33 100644 --- a/DuperOnMathlib/DuperOnMathlib/Prime.lean +++ b/DuperOnMathlib/DuperOnMathlib/Prime.lean @@ -10,7 +10,7 @@ set_option auto.tptp.solver.name "zipperposition" theorem prime_def_lt_DUPER {p : ℕ} : Prime p ↔ 2 ≤ p ∧ ∀ m < p, m ∣ p → m = 1 := by have : 2 ≤ p → 0 < p := by intro; linarith - duper [*, Nat.prime_def_lt'', Nat.le_of_dvd, Nat.lt_of_le_of_ne, Nat.lt_irrefl] {portfolioInstance := 1} + duper [*, Nat.prime_def_lt'', Nat.le_of_dvd, Nat.lt_of_le_of_ne, Nat.lt_irrefl] {portfolioInstance := 9} #check Nat.prime_def_lt' -- Reproving this theorem using duper: