From 9e4bc73c0a484b21550615f99373f3624ad29628 Mon Sep 17 00:00:00 2001 From: JOSHCLUNE Date: Mon, 12 Feb 2024 13:47:41 -0500 Subject: [PATCH 1/5] unfoldDefinitions bug fix --- Duper/Interface.lean | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/Duper/Interface.lean b/Duper/Interface.lean index a467c92..6912e34 100644 --- a/Duper/Interface.lean +++ b/Duper/Interface.lean @@ -342,7 +342,8 @@ def unfoldDefinitions (formulas : List (Expr × Expr × Array Name × Bool)) : M let f := abstracted.instantiate1 rhs' let fproof ← withTransparency .default do mkAppOptM ``Eq.ndrec #[none, some lhs, - some $ mkLambda `x .default ty' (← Meta.mkAppM ``Eq #[abstracted, mkConst ``True]), + some (← Meta.withLocalDeclD `_ ty' fun fvar => do + Meta.mkLambdaFVars #[fvar] $ ← Meta.mkAppM ``Eq #[abstracted.instantiate1 fvar, mkConst ``True]), some fproof, rhs', proof'] From e753c62d9806402fb45a7463d9261cb6ece1f16e Mon Sep 17 00:00:00 2001 From: JOSHCLUNE Date: Sun, 18 Feb 2024 11:44:56 -0500 Subject: [PATCH 2/5] Tracking isFromGoal through unfoldDefinitions correctly --- Duper/Interface.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/Duper/Interface.lean b/Duper/Interface.lean index 6912e34..f48ee90 100644 --- a/Duper/Interface.lean +++ b/Duper/Interface.lean @@ -328,9 +328,9 @@ def unfoldDefinitions (formulas : List (Expr × Expr × Array Name × Bool)) : M for (e, proof, paramNames, isFromGoal) in formulas do let update (ty lhs rhs : Expr) newFormulas (containedIn : Expr → Bool) : MetaM _ := do if containedIn rhs then pure newFormulas else - newFormulas.mapM fun (f, fproof, fparamNames) => do + newFormulas.mapM fun (f, fproof, fparamNames, fIsFromGoal) => do if !containedIn f then - return (f, fproof, fparamNames) + return (f, fproof, fparamNames, fIsFromGoal) else let us ← paramNames.mapM fun _ => mkFreshLevelMVar let lhs' := lhs.instantiateLevelParamsArray paramNames us @@ -347,7 +347,7 @@ def unfoldDefinitions (formulas : List (Expr × Expr × Array Name × Bool)) : M some fproof, rhs', proof'] - return (f, ← instantiateMVars $ fproof, fparamNames) + return (f, ← instantiateMVars $ fproof, fparamNames, isFromGoal || fIsFromGoal) match e with | .app ( .app ( .app (.const ``Eq _) ty) (.fvar fid)) rhs => let containedIn := fun e => (e.find? (· == .fvar fid)).isSome From 5181e3b19e1cbf5c8d73eee1520aad5f9ea8f5b2 Mon Sep 17 00:00:00 2001 From: JOSHCLUNE Date: Tue, 20 Feb 2024 17:50:06 -0500 Subject: [PATCH 3/5] Tracking isFromGoal through monomorphization procedure --- Duper/Interface.lean | 26 +++++++++++++++++++------- lake-manifest.json | 8 ++++---- lakefile.lean | 2 +- 3 files changed, 24 insertions(+), 12 deletions(-) diff --git a/Duper/Interface.lean b/Duper/Interface.lean index f48ee90..b64e83c 100644 --- a/Duper/Interface.lean +++ b/Duper/Interface.lean @@ -410,18 +410,30 @@ def runDuper (formulas : List (Expr × Expr × Array Name × Bool)) (instanceMax to be in alignment with how Auto stores lemmas to avoid the unnecessary cost of this conversion, but for now, it suffices to add or remove `eq_true` as needed) -/ -/-- Converts formulas/lemmas from the format used by Duper to the format used by Auto. -/ +partial def getLeavesFromDTr (t : Auto.DTr) : Array String := + match t with + | Auto.DTr.node _ subTrees => (subTrees.map getLeavesFromDTr).flatten + | Auto.DTr.leaf s => #[s] + +/-- Converts formulas/lemmas from the format used by Duper to the format used by Auto. Duper uses Auto's deriv DTr to keep + track of `isFromGoal` information through the monomorphization procedure. -/ def formulasToAutoLemmas (formulas : List (Expr × Expr × Array Name × Bool)) : MetaM (Array Auto.Lemma) := formulas.toArray.mapM (fun (fact, proof, params, isFromGoal) => -- For now, isFromGoal is ignored - return {proof := ← Meta.mkAppM ``of_eq_true #[proof], type := fact, params := params, deriv := (.leaf s!"❰{fact}❱")}) + return {proof := ← Meta.mkAppM ``of_eq_true #[proof], type := fact, params := params, deriv := (.leaf s!"{isFromGoal}")}) /-- Converts formulas/lemmas from the format used by Auto to the format used by Duper. -/ def autoLemmasToFormulas (lemmas : Array Auto.Lemma) : MetaM (List (Expr × Expr × Array Name × Bool)) := /- Currently, we don't have any means of determining which lemmas are originally from the goal, so for now, we are indicating that all lemmas don't come from the goal. This behavior should be updated once we get a means of tracking that information through the monomorphization procedure. -/ - lemmas.toList.mapM (fun lem => return (lem.type, ← Meta.mkAppM ``eq_true #[lem.proof], lem.params, false)) + lemmas.toList.mapM + (fun lem => do + let derivLeaves := getLeavesFromDTr lem.deriv + let isFromGoal := derivLeaves.contains "true" + trace[duper.monomorphization.debug] "deriv for {lem.type}: {lem.deriv}" + trace[duper.monomorphization.debug] "derivLeaves for {lem.type}: {derivLeaves}" + return (lem.type, ← Meta.mkAppM ``eq_true #[lem.proof], lem.params, isFromGoal)) /-- Given `formulas`, `instanceMaxHeartbeats`, and an instance of Duper `inst`, runs `inst` with monomorphization preprocessing. -/ def runDuperInstanceWithMonomorphization (formulas : List (Expr × Expr × Array Name × Bool)) (instanceMaxHeartbeats : Nat) @@ -433,8 +445,8 @@ def runDuperInstanceWithMonomorphization (formulas : List (Expr × Expr × Array let prover : Array Auto.Lemma → MetaM Expr := fun lemmas => do let monomorphizedFormulas ← autoLemmasToFormulas lemmas - trace[duper.monomorphization.debug] "Original formulas: {formulas.map (fun f => f.1)}" - trace[duper.monomorphization.debug] "Monomorphized formulas: {monomorphizedFormulas.map (fun f => f.1)}" + trace[duper.monomorphization.debug] "Original formulas: {formulas.map (fun f => (f.1, f.2.2.2))}" + trace[duper.monomorphization.debug] "Monomorphized formulas: {monomorphizedFormulas.map (fun f => (f.1, f.2.2.2))}" inst monomorphizedFormulas instanceMaxHeartbeats Auto.monoInterface lemmas inhFacts prover @@ -449,8 +461,8 @@ def runDuperInstanceWithFullPreprocessing (formulas : List (Expr × Expr × Arra let prover : Array Auto.Lemma → MetaM Expr := fun lemmas => do let monomorphizedFormulas ← autoLemmasToFormulas lemmas - trace[duper.monomorphization.debug] "Original formulas: {formulas.map (fun f => f.1)}" - trace[duper.monomorphization.debug] "Monomorphized formulas: {monomorphizedFormulas.map (fun f => f.1)}" + trace[duper.monomorphization.debug] "Original formulas: {formulas.map (fun f => (f.1, f.2.2.2))}" + trace[duper.monomorphization.debug] "Monomorphized formulas: {monomorphizedFormulas.map (fun f => (f.1, f.2.2.2))}" inst monomorphizedFormulas instanceMaxHeartbeats Auto.runNativeProverWithAuto declName? prover lemmas inhFacts diff --git a/lake-manifest.json b/lake-manifest.json index 11bc98d..6ffaef6 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -4,19 +4,19 @@ [{"url": "https://github.com/leanprover/std4.git", "type": "git", "subDir": null, - "rev": "276953b13323ca151939eafaaec9129bf7970306", + "rev": "f697bda1b4764a571042fed030690220c66ac4b2", "name": "std", "manifestFile": "lake-manifest.json", - "inputRev": "v4.6.0-rc1", + "inputRev": "main", "inherited": true, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/lean-auto.git", "type": "git", "subDir": null, - "rev": "b53593923a1423ae145c47c66306a68b6d0fbf44", + "rev": "9bfc3ca419307ff59a89823e0ad78d00c5487e06", "name": "auto", "manifestFile": "lake-manifest.json", - "inputRev": "v0.0.6", + "inputRev": "v0.0.7", "inherited": false, "configFile": "lakefile.lean"}], "name": "Duper", diff --git a/lakefile.lean b/lakefile.lean index d3f589b..8a29c16 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"@"v0.0.6" +require auto from git "https://github.com/leanprover-community/lean-auto.git"@"v0.0.7" package Duper { precompileModules := true From 667e860cb31a971898eda19b4e90ef034a168ce0 Mon Sep 17 00:00:00 2001 From: JOSHCLUNE Date: Thu, 14 Mar 2024 00:32:10 -0400 Subject: [PATCH 4/5] Update to lean4:v4.7.0-rc2 --- Duper/Interface.lean | 9 +++------ lake-manifest.json | 6 +++--- lakefile.lean | 2 +- lean-toolchain | 2 +- 4 files changed, 8 insertions(+), 11 deletions(-) diff --git a/Duper/Interface.lean b/Duper/Interface.lean index b64e83c..f166678 100644 --- a/Duper/Interface.lean +++ b/Duper/Interface.lean @@ -1,4 +1,3 @@ -import Std.Lean.CoreM import Duper.ProofReconstruction import Auto.Tactic @@ -251,13 +250,13 @@ def mkDuperCallSuggestion (duperStxRef : Syntax) (origSpan : Syntax) (facts : Sy let configOptionsStx : Syntax.TSepArray `Duper.configOption "," := {elemsAndSeps := configOptionsArr} if withDuperStar && facts.elemsAndSeps.isEmpty then let suggestion ←`(tactic| duper [*] {$configOptionsStx,*}) - Std.Tactic.TryThis.addSuggestion duperStxRef suggestion (origSpan? := origSpan) + Tactic.TryThis.addSuggestion duperStxRef suggestion (origSpan? := origSpan) else if withDuperStar then let suggestion ←`(tactic| duper [*, $facts,*] {$configOptionsStx,*}) - Std.Tactic.TryThis.addSuggestion duperStxRef suggestion (origSpan? := origSpan) + Tactic.TryThis.addSuggestion duperStxRef suggestion (origSpan? := origSpan) else let suggestion ←`(tactic| duper [$facts,*] {$configOptionsStx,*}) - Std.Tactic.TryThis.addSuggestion duperStxRef suggestion (origSpan? := origSpan) + Tactic.TryThis.addSuggestion duperStxRef suggestion (origSpan? := origSpan) /-- We save the `CoreM` state. This is because we will add a constant `skolemSorry` to the environment to support skolem constants with universe levels. We want to erase this constant after the saturation procedure ends -/ @@ -431,8 +430,6 @@ def autoLemmasToFormulas (lemmas : Array Auto.Lemma) : MetaM (List (Expr × Expr (fun lem => do let derivLeaves := getLeavesFromDTr lem.deriv let isFromGoal := derivLeaves.contains "true" - trace[duper.monomorphization.debug] "deriv for {lem.type}: {lem.deriv}" - trace[duper.monomorphization.debug] "derivLeaves for {lem.type}: {derivLeaves}" return (lem.type, ← Meta.mkAppM ``eq_true #[lem.proof], lem.params, isFromGoal)) /-- Given `formulas`, `instanceMaxHeartbeats`, and an instance of Duper `inst`, runs `inst` with monomorphization preprocessing. -/ diff --git a/lake-manifest.json b/lake-manifest.json index 6ffaef6..4777f8e 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -4,7 +4,7 @@ [{"url": "https://github.com/leanprover/std4.git", "type": "git", "subDir": null, - "rev": "f697bda1b4764a571042fed030690220c66ac4b2", + "rev": "6b203c31b414beb758ef9b7fdc71b01d144504ad", "name": "std", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -13,10 +13,10 @@ {"url": "https://github.com/leanprover-community/lean-auto.git", "type": "git", "subDir": null, - "rev": "9bfc3ca419307ff59a89823e0ad78d00c5487e06", + "rev": "1507142f79f05371e5eb25202eec6396bb940d72", "name": "auto", "manifestFile": "lake-manifest.json", - "inputRev": "v0.0.7", + "inputRev": "1507142f79f05371e5eb25202eec6396bb940d72", "inherited": false, "configFile": "lakefile.lean"}], "name": "Duper", diff --git a/lakefile.lean b/lakefile.lean index 8a29c16..c1b55c6 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"@"v0.0.7" +require auto from git "https://github.com/leanprover-community/lean-auto.git"@"1507142f79f05371e5eb25202eec6396bb940d72" package Duper { precompileModules := true diff --git a/lean-toolchain b/lean-toolchain index 8e2eb6d..e35881c 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.6.0-rc1 \ No newline at end of file +leanprover/lean4:v4.7.0-rc2 From 44ec745f02c7c01c66119a84e56c2e86affccbda Mon Sep 17 00:00:00 2001 From: JOSHCLUNE Date: Thu, 14 Mar 2024 00:51:00 -0400 Subject: [PATCH 5/5] Updating version on README --- README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/README.md b/README.md index f3bf8d9..9926177 100644 --- a/README.md +++ b/README.md @@ -7,7 +7,7 @@ Duper is an automatic proof-producing theorem prover broadly similar to Isabelle To use Duper in an existing Lean 4 project, first add this package as a dependency. In your lakefile.lean, add: ```lean -require Duper from git "https://github.com/leanprover-community/duper.git" @ "v0.0.8" +require Duper from git "https://github.com/leanprover-community/duper.git" @ "v0.0.10" ``` Then, make sure that your `lean-toolchain` file contains the same version of Lean 4 as Duper and that if your project imports [std4](https://github.com/leanprover/std4.git), then it uses the same version of std4 as the Duper branch of [Auto](https://github.com/leanprover-community/lean-auto.git). This step is necessary because Duper depends on Auto which depends on std4, so errors can arise if your project attempts to import a version of std4 different from the one imported by Duper.