From 4007a2788d000c6c2e9fcc6d7ae0a1709b65377b Mon Sep 17 00:00:00 2001 From: JOSHCLUNE Date: Fri, 29 Nov 2024 23:49:32 -0500 Subject: [PATCH 1/7] Added duper.ignoredUnusableFacts trace class --- Duper/Tactic.lean | 53 +++++++++++++++++++++++++++++++++-------------- 1 file changed, 37 insertions(+), 16 deletions(-) diff --git a/Duper/Tactic.lean b/Duper/Tactic.lean index 71d74bb..58fa78b 100644 --- a/Duper/Tactic.lean +++ b/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 @@ -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 @@ -94,20 +99,35 @@ def elabFact (stx : Term) : TacticM (Array (Expr × Expr × Array Name)) := do | some (.axiomInfo _) => return #[← elabFactAux stx] | some (.thmInfo _) => return #[← elabFactAux stx] | some (.opaqueInfo _) => - if ← getIgnoreUsableFactsM then return #[] - else throwError "Opaque constants cannot be provided as facts" + if ← getIgnoreUnusableFactsM then + trace[duper.ignoredUnusableFacts] "Ignored {expr} 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} 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} 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} 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} because it is an unknown constant" + return #[] + else + throwError "Unknown constant {id}" | .fvar exprFVarId => match (← getLCtx).find? exprFVarId with | some _ => return #[← elabFactAux stx] @@ -152,7 +172,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 + else if ← getIgnoreUnusableFactsM then + trace[duper.ignoredUnusableFacts] "Ignored {fact} because it is not a Prop" continue else throwError "Invalid fact {factStx} for duper. Proposition expected" From 4c83d7c7cbc56a50ac50f2b7d100b263de3ad33f Mon Sep 17 00:00:00 2001 From: JOSHCLUNE Date: Sat, 30 Nov 2024 16:13:43 -0500 Subject: [PATCH 2/7] Update duper.ignordUnusableFacts trace messages --- Duper/Tactic.lean | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/Duper/Tactic.lean b/Duper/Tactic.lean index 58fa78b..744e236 100644 --- a/Duper/Tactic.lean +++ b/Duper/Tactic.lean @@ -100,31 +100,31 @@ def elabFact (stx : Term) : TacticM (Array (Expr × Expr × Array Name)) := do | some (.thmInfo _) => return #[← elabFactAux stx] | some (.opaqueInfo _) => if ← getIgnoreUnusableFactsM then - trace[duper.ignoredUnusableFacts] "Ignored {expr} because it is an opaque constant" + 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 ← getIgnoreUnusableFactsM then - trace[duper.ignoredUnusableFacts] "Ignored {expr} because it is a quotient constant" + 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 ← getIgnoreUnusableFactsM then - trace[duper.ignoredUnusableFacts] "Ignored {expr} because it is an inductive type" + 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 ← getIgnoreUnusableFactsM then - trace[duper.ignoredUnusableFacts] "Ignored {expr} because it is a constructor" + trace[duper.ignoredUnusableFacts] "Ignored {expr} ({id}) because it is a constructor" return #[] else throwError "Constructors cannot be provided as facts" | none => if ← getIgnoreUnusableFactsM then - trace[duper.ignoredUnusableFacts] "Ignored {expr} because it is an unknown constant" + trace[duper.ignoredUnusableFacts] "Ignored {expr} ({id}) because it is an unknown constant" return #[] else throwError "Unknown constant {id}" @@ -173,7 +173,7 @@ def collectAssumptions (facts : Array Term) (withAllLCtx : Bool) (goalDecls : Ar 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} because it is not a Prop" + trace[duper.ignoredUnusableFacts] "Ignored {fact} ({factStx}) because it is not a Prop" continue else throwError "Invalid fact {factStx} for duper. Proposition expected" From 530b94e022dca0c38b8331285ddd86bb2c788701 Mon Sep 17 00:00:00 2001 From: JOSHCLUNE Date: Sat, 30 Nov 2024 17:09:21 -0500 Subject: [PATCH 3/7] Added support for facts whose types are not Prop but can be made definitionally equal to Prop with metavariable assignment --- Duper/Tactic.lean | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/Duper/Tactic.lean b/Duper/Tactic.lean index 744e236..54e4b13 100644 --- a/Duper/Tactic.lean +++ b/Duper/Tactic.lean @@ -172,6 +172,13 @@ 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 ← 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 From 514dbba3ac811f7253b208d60f4965ec17bc6b48 Mon Sep 17 00:00:00 2001 From: JOSHCLUNE Date: Sat, 30 Nov 2024 17:31:08 -0500 Subject: [PATCH 4/7] Adding some duper.delabFact.debug trace messages --- Duper/Tactic.lean | 20 ++++++++++++++++---- 1 file changed, 16 insertions(+), 4 deletions(-) diff --git a/Duper/Tactic.lean b/Duper/Tactic.lean index 54e4b13..eca30e7 100644 --- a/Duper/Tactic.lean +++ b/Duper/Tactic.lean @@ -96,8 +96,14 @@ 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 ← getIgnoreUnusableFactsM then trace[duper.ignoredUnusableFacts] "Ignored {expr} ({id}) because it is an opaque constant" @@ -130,10 +136,16 @@ def elabFact (stx : Term) : TacticM (Array (Expr × Expr × Array Name)) := do 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 From 99dfe084040cd5e3d4924f7d70cb90cfb1633153 Mon Sep 17 00:00:00 2001 From: JOSHCLUNE Date: Sat, 30 Nov 2024 17:38:22 -0500 Subject: [PATCH 5/7] Set implicitLambda to false when elaborating terms passed into Duper --- Duper/Tactic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Duper/Tactic.lean b/Duper/Tactic.lean index eca30e7..968731a 100644 --- a/Duper/Tactic.lean +++ b/Duper/Tactic.lean @@ -149,7 +149,7 @@ def elabFact (stx : Term) : TacticM (Array (Expr × Expr × Array Name)) := do 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 e ← Term.elabTerm stx none (implicitLambda := false) Term.synthesizeSyntheticMVars (postpone := .no) (ignoreStuckTC := true) let e ← instantiateMVars e let abstres ← Duper.abstractMVars e From 2f5a1f6ed919a62c183bf07ff13f838baf7cc41d Mon Sep 17 00:00:00 2001 From: JOSHCLUNE Date: Sat, 30 Nov 2024 18:36:15 -0500 Subject: [PATCH 6/7] Adding @ before elaborating input fact syntax --- Duper/Tactic.lean | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/Duper/Tactic.lean b/Duper/Tactic.lean index 968731a..e027463 100644 --- a/Duper/Tactic.lean +++ b/Duper/Tactic.lean @@ -149,7 +149,8 @@ def elabFact (stx : Term) : TacticM (Array (Expr × Expr × Array Name)) := do 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 (implicitLambda := false) + 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 From 15bd942bfd58cc85cbce782cb80f86f1110acc61 Mon Sep 17 00:00:00 2001 From: JOSHCLUNE Date: Wed, 18 Dec 2024 00:01:30 -0500 Subject: [PATCH 7/7] Update to v4.14.0 --- Duper/ClauseStreamHeap.lean | 4 ++-- Duper/ProverM.lean | 3 --- Duper/Selection.lean | 18 +++++++++--------- Duper/Tactic.lean | 4 ++-- lake-manifest.json | 20 ++++++++++---------- lakefile.lean | 4 ++-- lean-toolchain | 2 +- 7 files changed, 26 insertions(+), 29 deletions(-) diff --git a/Duper/ClauseStreamHeap.lean b/Duper/ClauseStreamHeap.lean index ab57f1c..ebb0425 100644 --- a/Duper/ClauseStreamHeap.lean +++ b/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 diff --git a/Duper/ProverM.lean b/Duper/ProverM.lean index 9f98598..a2e5096 100644 --- a/Duper/ProverM.lean +++ b/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 diff --git a/Duper/Selection.lean b/Duper/Selection.lean index f9e0363..69c0b99 100644 --- a/Duper/Selection.lean +++ b/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 \ No newline at end of file +end Duper diff --git a/Duper/Tactic.lean b/Duper/Tactic.lean index e027463..bff210f 100644 --- a/Duper/Tactic.lean +++ b/Duper/Tactic.lean @@ -39,8 +39,8 @@ def getIgnoreUnusableFactsM : 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 diff --git a/lake-manifest.json b/lake-manifest.json index 11a2fd9..5e397fe 100644 --- a/lake-manifest.json +++ b/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"} diff --git a/lakefile.lean b/lakefile.lean index 98d1a82..93fcd38 100644 --- a/lakefile.lean +++ b/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 diff --git a/lean-toolchain b/lean-toolchain index 4f86f95..1e70935 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.13.0 +leanprover/lean4:v4.14.0