From 35dd67327af3c55abbf8bbe8cf0d83b15778101f Mon Sep 17 00:00:00 2001 From: Peiyang-Song Date: Tue, 12 Sep 2023 08:56:28 -0700 Subject: [PATCH 01/31] Finish a RuleTac and a RuleBuilder to run neural network under the hood, along with up/downstream parts --- .gitignore | 2 ++ Aesop/Builder.lean | 1 + Aesop/Builder/Neural.lean | 61 ++++++++++++++++++++++++++++++++++++ Aesop/Frontend/RuleExpr.lean | 19 +++++++++++ Aesop/Rule/Name.lean | 2 ++ Aesop/RuleTac.lean | 2 ++ Aesop/RuleTac/Basic.lean | 2 ++ Aesop/RuleTac/Neural.lean | 39 +++++++++++++++++++++++ AesopTest/NeuralProver.lean | 17 ++++++++++ lake-manifest.json | 10 +++++- lakefile.lean | 2 ++ 11 files changed, 156 insertions(+), 1 deletion(-) create mode 100644 Aesop/Builder/Neural.lean create mode 100644 Aesop/RuleTac/Neural.lean create mode 100644 AesopTest/NeuralProver.lean diff --git a/.gitignore b/.gitignore index 44c8e983..80f90be6 100644 --- a/.gitignore +++ b/.gitignore @@ -1,3 +1,5 @@ /build/ /tests/*.produced /lake-packages + +onnx-leandojo-lean4-tacgen-byt5-small/ \ No newline at end of file diff --git a/Aesop/Builder.lean b/Aesop/Builder.lean index 69404f69..bc5a8f8e 100644 --- a/Aesop/Builder.lean +++ b/Aesop/Builder.lean @@ -13,3 +13,4 @@ import Aesop.Builder.Forward import Aesop.Builder.NormSimp import Aesop.Builder.Tactic import Aesop.Builder.Unfold +import Aesop.Builder.Neural diff --git a/Aesop/Builder/Neural.lean b/Aesop/Builder/Neural.lean new file mode 100644 index 00000000..67e15d25 --- /dev/null +++ b/Aesop/Builder/Neural.lean @@ -0,0 +1,61 @@ +import Aesop.Builder.Basic + +open Lean +open Lean.Meta + +namespace Aesop + +structure NeuralBuilderOptions extends RegularBuilderOptions where + /-- The transparency used by the rule tactic. -/ + transparency : TransparencyMode + /-- The transparency used to index the rule. The rule is not indexed unless + this is `.reducible`. -/ + indexTransparency : TransparencyMode + neuralProver : String + numReturnSequences : UInt64 + maxLength : UInt64 + temperature : Float + numBeams : UInt64 + + +instance : Inhabited NeuralBuilderOptions where + default := { + toRegularBuilderOptions := default + transparency := .default + indexTransparency := .reducible + neuralProver := "onnx-leandojo-lean4-tacgen-byt5-small" + numReturnSequences := 32 + maxLength := 256 + temperature := 1.0 + numBeams := 1 + } + +def RuleBuilder.neural (opts : NeuralBuilderOptions) : RuleBuilder := λ input => + match input.kind with + | RuleBuilderKind.global _ => do + -- let tac := .neuralProvers opts.neuralProver opts.numReturnSequences + -- opts.maxLength opts.temperature opts.numBeams + let tac := .neuralProvers opts.neuralProver + -- let type := (← getConstInfo decl).type + RuleBuilderOutput.global <$> mkResult tac + | RuleBuilderKind.local _ _ => + throwError "neural rule builder does not support local hypotheses" + -- goal.withContext do + -- let tac := RuleTacDescr.applyFVar fvarUserName opts.transparency + -- let type ← instantiateMVars (← getLocalDeclFromUserName fvarUserName).type + -- let result ← mkResult tac + -- return RuleBuilderOutput.local goal result + where + mkResult (tac : RuleTacDescr) : MetaM RuleBuilderResult := + return RuleBuilderResult.regular { + builder := BuilderName.neural + tac := tac + -- indexingMode := ← opts.getIndexingModeM do + -- if opts.indexTransparency != .reducible then + -- return .unindexed + -- else + -- IndexingMode.targetMatchingConclusion type + indexingMode := ← opts.getIndexingModeM $ pure IndexingMode.unindexed + } + +end Aesop diff --git a/Aesop/Frontend/RuleExpr.lean b/Aesop/Frontend/RuleExpr.lean index 638f973a..9c4844e7 100644 --- a/Aesop/Frontend/RuleExpr.lean +++ b/Aesop/Frontend/RuleExpr.lean @@ -119,6 +119,7 @@ syntax "forward" : Aesop.builder_name syntax "destruct" : Aesop.builder_name syntax "cases" : Aesop.builder_name syntax "default" : Aesop.builder_name +syntax "neural" : Aesop.builder_name end Parser @@ -140,6 +141,7 @@ def «elab» (stx : Syntax) : ElabM DBuilderName := | `(builder_name| forward) => return regular .forward | `(builder_name| destruct) => return regular .destruct | `(builder_name| cases) => return regular .cases + | `(builder_name| neural) => return regular .neural | `(builder_name| default) => return «default» | _ => throwUnsupportedSyntax @@ -369,6 +371,19 @@ def constructors : BuilderOptions ConstructorsBuilderOptions where some opts | _, _ => none +def neural : BuilderOptions NeuralBuilderOptions where + builderName := .regular .neural + init := default + add + | opts, .index indexingMode? => some { opts with indexingMode? } + | opts, .transparency transparency alsoForIndex => + let opts := { opts with transparency } + if alsoForIndex then + some { opts with indexTransparency := transparency } + else + some opts + | _, _ => none + end BuilderOptions @@ -389,6 +404,7 @@ inductive Builder | constructors (opts : ConstructorsBuilderOptions) | forward (opts : ForwardBuilderOptions) | cases (opts : CasesBuilderOptions) + | neural (opts: NeuralBuilderOptions) | «default» deriving Inhabited @@ -404,6 +420,7 @@ def elabOptions (b : DBuilderName) (opts : Syntax) : ElabM Builder := do | .regular .forward => forward <$> BuilderOptions.forward.elab opts | .regular .destruct => forward <$> BuilderOptions.destruct.elab opts | .regular .cases => «cases» <$> BuilderOptions.cases.elab opts + | .regular .neural => neural <$> BuilderOptions.neural.elab opts | .default => checkNoOptions; return default where checkNoOptions := BuilderOptions.none b |>.«elab» opts @@ -425,6 +442,7 @@ def toRuleBuilder : Builder → RuleBuilder | constructors opts => RuleBuilder.constructors opts | forward opts => RuleBuilder.forward opts | cases opts => RuleBuilder.cases opts + | neural opts => RuleBuilder.neural opts | «default» => RuleBuilder.default open DBuilderName in @@ -436,6 +454,7 @@ def toDBuilderName : Builder → DBuilderName | constructors .. => regular .constructors | forward .. => regular .forward | cases .. => regular .cases + | neural .. => regular .neural | .«default» => .default end Builder diff --git a/Aesop/Rule/Name.lean b/Aesop/Rule/Name.lean index cd79bc73..6a0b098a 100644 --- a/Aesop/Rule/Name.lean +++ b/Aesop/Rule/Name.lean @@ -59,6 +59,7 @@ inductive BuilderName | constructors | destruct | forward + | neural | simp | tactic | unfold @@ -78,6 +79,7 @@ instance : ToString BuilderName where | constructors => "constructors" | destruct => "destruct" | forward => "forward" + | neural => "neural" | simp => "simp" | tactic => "tactic" | unfold => "unfold" diff --git a/Aesop/RuleTac.lean b/Aesop/RuleTac.lean index c3954f53..8c158574 100644 --- a/Aesop/RuleTac.lean +++ b/Aesop/RuleTac.lean @@ -11,6 +11,7 @@ import Aesop.RuleTac.Forward import Aesop.RuleTac.Preprocess import Aesop.RuleTac.RuleApplicationWithMVarInfo import Aesop.RuleTac.Tactic +import Aesop.RuleTac.Neural open Lean @@ -20,6 +21,7 @@ protected def run : RuleTacDescr → RuleTacInput → MetaM RuleTacOutput | applyConst decl md => RuleTac.applyConst decl md | applyFVar userName md => RuleTac.applyFVar userName md | constructors cs md => RuleTac.applyConsts cs md + | neuralProvers nps => RuleTac.applyNeural nps | forwardConst decl immediate clear md => RuleTac.forwardConst decl immediate clear md | forwardFVar userName immediate clear md => diff --git a/Aesop/RuleTac/Basic.lean b/Aesop/RuleTac/Basic.lean index 44328f06..8aba2ba7 100644 --- a/Aesop/RuleTac/Basic.lean +++ b/Aesop/RuleTac/Basic.lean @@ -106,6 +106,7 @@ inductive RuleTacDescr | applyConst (decl : Name) (md : TransparencyMode) | applyFVar (userName : Name) (md : TransparencyMode) | constructors (constructorNames : Array Name) (md : TransparencyMode) + | neuralProvers (neuralProverName : String) | forwardConst (decl : Name) (immediate : UnorderedArraySet Nat) (clear : Bool) (md : TransparencyMode) | forwardFVar (userName : Name) (immediate : UnorderedArraySet Nat) @@ -124,6 +125,7 @@ def isGlobal : RuleTacDescr → Bool | applyConst .. => true | applyFVar .. => false | constructors .. => true + | neuralProvers .. => true | forwardConst .. => true | forwardFVar .. => false | cases .. => true diff --git a/Aesop/RuleTac/Neural.lean b/Aesop/RuleTac/Neural.lean new file mode 100644 index 00000000..36368b10 --- /dev/null +++ b/Aesop/RuleTac/Neural.lean @@ -0,0 +1,39 @@ +import LeanInfer + +import Aesop.RuleTac.Basic + +open Lean Lean.Meta Lean.Elab Lean.Elab.Command Lean.Elab.Tactic + +namespace Aesop.RuleTac + +-- Tries to apply each tactic suggested by a neural network. For each one that +-- applies, a rule application is returned. If none applies, the tactic fails. +def applyNeural (model: String) : RuleTac := λ input => do + let initialState ← saveState + -- let generateScript := input.options.generateScript + if model == "onnx-leandojo-lean4-tacgen-byt5-small" then + let iptGoal ← LeanInfer.ppTacticState [input.goal] + let optSuggestions ← LeanInfer.generate iptGoal + let suggestions := optSuggestions.map (·.1) + let apps ← suggestions.filterMapM λ tacticStr => do + match Parser.runParserCategory (← getEnv) `tactic tacticStr (fileName := "") with + | .error _ => return none + | .ok stx => + initialState.restore + let tac := evalTactic stx + let goals ← run input.goal tac |>.run' + let postState ← saveState + let thisApp : RuleApplication := { + postState := postState + goals := goals.toArray + scriptBuilder? := none + } + return thisApp + restoreState initialState + if apps.isEmpty then throwError + "failed to apply any tactics generated by {model}" + return ⟨apps⟩ + else + throwError "unknown neural network model: {model}" + +end RuleTac diff --git a/AesopTest/NeuralProver.lean b/AesopTest/NeuralProver.lean new file mode 100644 index 00000000..8494feba --- /dev/null +++ b/AesopTest/NeuralProver.lean @@ -0,0 +1,17 @@ +import Aesop +-- import LeanInfer +-- When we can use LeanInfer without importing it, this means the +-- LeanInfer module successfully got integrated into the aesop dependency graph. + +set_option aesop.check.all true + +open Lean Lean.Meta Lean.Elab.Tactic + +section simpleTest + +theorem foo (a: Nat) : a + 1 = Nat.succ a := by + aesop + -- aesop (rule_sets [-default, -builtin]) + -- suggest_tactics + -- rfl + -- sorry \ No newline at end of file diff --git a/lake-manifest.json b/lake-manifest.json index 71e52539..e0fa113d 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -2,9 +2,17 @@ "packagesDir": "lake-packages", "packages": [{"git": + {"url": "https://github.com/lean-dojo/LeanInfer.git", + "subDir?": null, + "rev": "c59fe2bd0e8aedbbdcfbef11295fdb8ee64acc88", + "opts": {}, + "name": "LeanInfer", + "inputRev?": "c59fe2bd0e8aedbbdcfbef11295fdb8ee64acc88", + "inherited": false}}, + {"git": {"url": "https://github.com/leanprover/std4", "subDir?": null, - "rev": "28459f72f3190b0f540b49ab769745819eeb1c5e", + "rev": "ba5e5e3af519b4fc5221ad0fa4b2c87276f1d323", "opts": {}, "name": "std", "inputRev?": "main", diff --git a/lakefile.lean b/lakefile.lean index 267a075d..393a613a 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -4,6 +4,7 @@ open Lake DSL package aesop { precompileModules := false -- breaks mathlib cache + moreLinkArgs := #["-lonnxruntime", "-lstdc++"] -- added for LeanInfer } @[default_target] @@ -14,3 +15,4 @@ lean_lib AesopTest { } require std from git "https://github.com/leanprover/std4" @ "main" +require LeanInfer from git "https://github.com/lean-dojo/LeanInfer.git" @ "c59fe2bd0e8aedbbdcfbef11295fdb8ee64acc88" \ No newline at end of file From 5919da49d0a926f095984664fba222ebb385b648 Mon Sep 17 00:00:00 2001 From: Peiyang-Song Date: Wed, 13 Sep 2023 08:19:03 -0700 Subject: [PATCH 02/31] Bump to LeanInfer 2.0.0, simplify additional installation steps --- Aesop/Builder/Neural.lean | 11 ----------- AesopTest/NeuralProver.lean | 18 ++++++++++++++---- lake-manifest.json | 4 ++-- lakefile.lean | 3 +-- 4 files changed, 17 insertions(+), 19 deletions(-) diff --git a/Aesop/Builder/Neural.lean b/Aesop/Builder/Neural.lean index 67e15d25..8475da78 100644 --- a/Aesop/Builder/Neural.lean +++ b/Aesop/Builder/Neural.lean @@ -36,25 +36,14 @@ def RuleBuilder.neural (opts : NeuralBuilderOptions) : RuleBuilder := λ input = -- let tac := .neuralProvers opts.neuralProver opts.numReturnSequences -- opts.maxLength opts.temperature opts.numBeams let tac := .neuralProvers opts.neuralProver - -- let type := (← getConstInfo decl).type RuleBuilderOutput.global <$> mkResult tac | RuleBuilderKind.local _ _ => throwError "neural rule builder does not support local hypotheses" - -- goal.withContext do - -- let tac := RuleTacDescr.applyFVar fvarUserName opts.transparency - -- let type ← instantiateMVars (← getLocalDeclFromUserName fvarUserName).type - -- let result ← mkResult tac - -- return RuleBuilderOutput.local goal result where mkResult (tac : RuleTacDescr) : MetaM RuleBuilderResult := return RuleBuilderResult.regular { builder := BuilderName.neural tac := tac - -- indexingMode := ← opts.getIndexingModeM do - -- if opts.indexTransparency != .reducible then - -- return .unindexed - -- else - -- IndexingMode.targetMatchingConclusion type indexingMode := ← opts.getIndexingModeM $ pure IndexingMode.unindexed } diff --git a/AesopTest/NeuralProver.lean b/AesopTest/NeuralProver.lean index 8494feba..0d6b2a84 100644 --- a/AesopTest/NeuralProver.lean +++ b/AesopTest/NeuralProver.lean @@ -9,9 +9,19 @@ open Lean Lean.Meta Lean.Elab.Tactic section simpleTest +structure neuralConfig where + model_name : String + +@[aesop unsafe neural] +def conf : neuralConfig := { model_name := "onnx-leandojo-lean4-tacgen-byt5-small" } + theorem foo (a: Nat) : a + 1 = Nat.succ a := by - aesop - -- aesop (rule_sets [-default, -builtin]) - -- suggest_tactics + aesop + -- aesop alone should be able to prove this simple theorem. + + -- suggest_tactics + -- aesop should also be able to call LeanInfer to suggest tactics as LeanInfer is already added into the loop. + -- rfl - -- sorry \ No newline at end of file + -- sorry + -- both closes the proof each in a safe/unsafe way. \ No newline at end of file diff --git a/lake-manifest.json b/lake-manifest.json index e0fa113d..8bc91453 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -4,10 +4,10 @@ [{"git": {"url": "https://github.com/lean-dojo/LeanInfer.git", "subDir?": null, - "rev": "c59fe2bd0e8aedbbdcfbef11295fdb8ee64acc88", + "rev": "a93e2f0baf25ddea2477535dcf4c78eed6a6fdd1", "opts": {}, "name": "LeanInfer", - "inputRev?": "c59fe2bd0e8aedbbdcfbef11295fdb8ee64acc88", + "inputRev?": "v0.0.2", "inherited": false}}, {"git": {"url": "https://github.com/leanprover/std4", diff --git a/lakefile.lean b/lakefile.lean index 393a613a..9ff950c9 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -4,7 +4,6 @@ open Lake DSL package aesop { precompileModules := false -- breaks mathlib cache - moreLinkArgs := #["-lonnxruntime", "-lstdc++"] -- added for LeanInfer } @[default_target] @@ -15,4 +14,4 @@ lean_lib AesopTest { } require std from git "https://github.com/leanprover/std4" @ "main" -require LeanInfer from git "https://github.com/lean-dojo/LeanInfer.git" @ "c59fe2bd0e8aedbbdcfbef11295fdb8ee64acc88" \ No newline at end of file +require LeanInfer from git "https://github.com/lean-dojo/LeanInfer.git" @ "v0.0.2" \ No newline at end of file From 03fd2aa2247fa3e043602eae775100e50c282607 Mon Sep 17 00:00:00 2001 From: Peiyang-Song Date: Thu, 14 Sep 2023 00:49:53 -0700 Subject: [PATCH 03/31] Bump to LeanInfer v0.0.4 --- AesopTest/NeuralProver.lean | 4 ++-- lake-manifest.json | 6 +++--- lakefile.lean | 2 +- 3 files changed, 6 insertions(+), 6 deletions(-) diff --git a/AesopTest/NeuralProver.lean b/AesopTest/NeuralProver.lean index 0d6b2a84..83667731 100644 --- a/AesopTest/NeuralProver.lean +++ b/AesopTest/NeuralProver.lean @@ -16,10 +16,10 @@ structure neuralConfig where def conf : neuralConfig := { model_name := "onnx-leandojo-lean4-tacgen-byt5-small" } theorem foo (a: Nat) : a + 1 = Nat.succ a := by - aesop + aesop -- aesop alone should be able to prove this simple theorem. - -- suggest_tactics + -- suggest_tactics -- aesop should also be able to call LeanInfer to suggest tactics as LeanInfer is already added into the loop. -- rfl diff --git a/lake-manifest.json b/lake-manifest.json index 8bc91453..894e72b8 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -4,15 +4,15 @@ [{"git": {"url": "https://github.com/lean-dojo/LeanInfer.git", "subDir?": null, - "rev": "a93e2f0baf25ddea2477535dcf4c78eed6a6fdd1", + "rev": "ef15c38f05db7e4de200f8b46db63276e02072d1", "opts": {}, "name": "LeanInfer", - "inputRev?": "v0.0.2", + "inputRev?": "v0.0.4", "inherited": false}}, {"git": {"url": "https://github.com/leanprover/std4", "subDir?": null, - "rev": "ba5e5e3af519b4fc5221ad0fa4b2c87276f1d323", + "rev": "efcb1a6fe69b57b16d370ffe36551c3d21b5a53e", "opts": {}, "name": "std", "inputRev?": "main", diff --git a/lakefile.lean b/lakefile.lean index 9ff950c9..544d7cef 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -14,4 +14,4 @@ lean_lib AesopTest { } require std from git "https://github.com/leanprover/std4" @ "main" -require LeanInfer from git "https://github.com/lean-dojo/LeanInfer.git" @ "v0.0.2" \ No newline at end of file +require LeanInfer from git "https://github.com/lean-dojo/LeanInfer.git" @ "v0.0.4" \ No newline at end of file From 8d1adba61d017b732505268f653245e0dff005b1 Mon Sep 17 00:00:00 2001 From: Peiyang-Song Date: Tue, 19 Sep 2023 21:32:32 -0700 Subject: [PATCH 04/31] Add script builder for neural --- Aesop/Builder/Neural.lean | 4 ++-- Aesop/RuleTac.lean | 2 +- Aesop/RuleTac/Basic.lean | 2 +- Aesop/RuleTac/Neural.lean | 11 ++++++++--- AesopTest/NeuralProver.lean | 9 +++++++-- 5 files changed, 19 insertions(+), 9 deletions(-) diff --git a/Aesop/Builder/Neural.lean b/Aesop/Builder/Neural.lean index 8475da78..3881029c 100644 --- a/Aesop/Builder/Neural.lean +++ b/Aesop/Builder/Neural.lean @@ -24,7 +24,7 @@ instance : Inhabited NeuralBuilderOptions where transparency := .default indexTransparency := .reducible neuralProver := "onnx-leandojo-lean4-tacgen-byt5-small" - numReturnSequences := 32 + numReturnSequences := 64 maxLength := 256 temperature := 1.0 numBeams := 1 @@ -35,7 +35,7 @@ def RuleBuilder.neural (opts : NeuralBuilderOptions) : RuleBuilder := λ input = | RuleBuilderKind.global _ => do -- let tac := .neuralProvers opts.neuralProver opts.numReturnSequences -- opts.maxLength opts.temperature opts.numBeams - let tac := .neuralProvers opts.neuralProver + let tac := .neuralProvers opts.neuralProver opts.transparency RuleBuilderOutput.global <$> mkResult tac | RuleBuilderKind.local _ _ => throwError "neural rule builder does not support local hypotheses" diff --git a/Aesop/RuleTac.lean b/Aesop/RuleTac.lean index 8c158574..8d84c7a6 100644 --- a/Aesop/RuleTac.lean +++ b/Aesop/RuleTac.lean @@ -21,7 +21,7 @@ protected def run : RuleTacDescr → RuleTacInput → MetaM RuleTacOutput | applyConst decl md => RuleTac.applyConst decl md | applyFVar userName md => RuleTac.applyFVar userName md | constructors cs md => RuleTac.applyConsts cs md - | neuralProvers nps => RuleTac.applyNeural nps + | neuralProvers nps md => RuleTac.applyNeural nps md | forwardConst decl immediate clear md => RuleTac.forwardConst decl immediate clear md | forwardFVar userName immediate clear md => diff --git a/Aesop/RuleTac/Basic.lean b/Aesop/RuleTac/Basic.lean index 8aba2ba7..95b56168 100644 --- a/Aesop/RuleTac/Basic.lean +++ b/Aesop/RuleTac/Basic.lean @@ -106,7 +106,7 @@ inductive RuleTacDescr | applyConst (decl : Name) (md : TransparencyMode) | applyFVar (userName : Name) (md : TransparencyMode) | constructors (constructorNames : Array Name) (md : TransparencyMode) - | neuralProvers (neuralProverName : String) + | neuralProvers (neuralProverName : String) (md : TransparencyMode) | forwardConst (decl : Name) (immediate : UnorderedArraySet Nat) (clear : Bool) (md : TransparencyMode) | forwardFVar (userName : Name) (immediate : UnorderedArraySet Nat) diff --git a/Aesop/RuleTac/Neural.lean b/Aesop/RuleTac/Neural.lean index 36368b10..0bcb985d 100644 --- a/Aesop/RuleTac/Neural.lean +++ b/Aesop/RuleTac/Neural.lean @@ -8,9 +8,9 @@ namespace Aesop.RuleTac -- Tries to apply each tactic suggested by a neural network. For each one that -- applies, a rule application is returned. If none applies, the tactic fails. -def applyNeural (model: String) : RuleTac := λ input => do +def applyNeural (model: String) (md : TransparencyMode) : RuleTac := λ input => do let initialState ← saveState - -- let generateScript := input.options.generateScript + let generateScript := input.options.generateScript if model == "onnx-leandojo-lean4-tacgen-byt5-small" then let iptGoal ← LeanInfer.ppTacticState [input.goal] let optSuggestions ← LeanInfer.generate iptGoal @@ -21,12 +21,17 @@ def applyNeural (model: String) : RuleTac := λ input => do | .ok stx => initialState.restore let tac := evalTactic stx + let tstx : TSyntax `tactic := {raw := stx} let goals ← run input.goal tac |>.run' + let scriptBuilder? := + mkScriptBuilder? generateScript $ + .ofTactic goals.toArray.size do + withAllTransparencySyntax md tstx let postState ← saveState let thisApp : RuleApplication := { postState := postState goals := goals.toArray - scriptBuilder? := none + scriptBuilder? := scriptBuilder? } return thisApp restoreState initialState diff --git a/AesopTest/NeuralProver.lean b/AesopTest/NeuralProver.lean index 83667731..6277d60d 100644 --- a/AesopTest/NeuralProver.lean +++ b/AesopTest/NeuralProver.lean @@ -19,9 +19,14 @@ theorem foo (a: Nat) : a + 1 = Nat.succ a := by aesop -- aesop alone should be able to prove this simple theorem. + -- aesop? + -- aesop? should be able to suggest tactics to the user, + -- displayed in the InfoView as LeanInfer does. + -- suggest_tactics - -- aesop should also be able to call LeanInfer to suggest tactics as LeanInfer is already added into the loop. + -- aesop should also be able to call LeanInfer to suggest tactics + -- as LeanInfer is already added into the loop. -- rfl -- sorry - -- both closes the proof each in a safe/unsafe way. \ No newline at end of file + -- both closes the proof either in a safe/unsafe way. \ No newline at end of file From e34adc488c74408a02b7be79429b86f21f32295f Mon Sep 17 00:00:00 2001 From: Peiyang-Song Date: Wed, 20 Sep 2023 07:08:03 -0700 Subject: [PATCH 05/31] Bump to LeanInfer v0.0.7 --- lake-manifest.json | 4 ++-- lakefile.lean | 3 ++- 2 files changed, 4 insertions(+), 3 deletions(-) diff --git a/lake-manifest.json b/lake-manifest.json index 894e72b8..10ba4aa0 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -4,10 +4,10 @@ [{"git": {"url": "https://github.com/lean-dojo/LeanInfer.git", "subDir?": null, - "rev": "ef15c38f05db7e4de200f8b46db63276e02072d1", + "rev": "6b4211f30e0bdcd070fd6ca3d0c163693aeca909", "opts": {}, "name": "LeanInfer", - "inputRev?": "v0.0.4", + "inputRev?": "v0.0.7", "inherited": false}}, {"git": {"url": "https://github.com/leanprover/std4", diff --git a/lakefile.lean b/lakefile.lean index 544d7cef..d7a3df8d 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -4,6 +4,7 @@ open Lake DSL package aesop { precompileModules := false -- breaks mathlib cache + moreLinkArgs := #["-L./lake-packages/LeanInfer/build/lib", "-lonnxruntime", "-lstdc++"] } @[default_target] @@ -14,4 +15,4 @@ lean_lib AesopTest { } require std from git "https://github.com/leanprover/std4" @ "main" -require LeanInfer from git "https://github.com/lean-dojo/LeanInfer.git" @ "v0.0.4" \ No newline at end of file +require LeanInfer from git "https://github.com/lean-dojo/LeanInfer.git" @ "v0.0.7" \ No newline at end of file From 3bc83506b9fc91ad1802eddca35f4651ef16cc83 Mon Sep 17 00:00:00 2001 From: Peiyang Song Date: Sat, 23 Sep 2023 14:12:47 -0700 Subject: [PATCH 06/31] Add Aesop-LeanInfer readme --- README.md | 45 ++++++++++++++++++++++++++++++++++++++++++++- 1 file changed, 44 insertions(+), 1 deletion(-) diff --git a/README.md b/README.md index b5bf1342..bb40f077 100644 --- a/README.md +++ b/README.md @@ -1,4 +1,47 @@ -# Aesop +# Aesop-LeanInfer + +Aesop-LeanInfer is an enhanced version of [Aesop](https://github.com/JLimperg/aesop) (Automated Extensible Search for Obvious Proofs), a proof search tactic for Lean 4 similar to Isabelle's `auto`. In addition to the original Aesop, this version adds a new `RuleBuilder` and its corresponding `RuleTac`, which together enable fast plugin of machine learning models to assist with the proof search process, by seamlessly incorporating [LeanInfer](https://github.com/lean-dojo/LeanInfer)'s tactic suggestion feature into Aesop's workflow. + +This tool is in its alpha stage and we are actively working to further enhance it. It is based on an early version of LeanInfer, which will be enriched in the near future. We aim to always keep this tool updated with the latest LeanInfer and have it support more variations in machine learning models of choice and accompanying features. + +## Requirements + +* Supported platforms: Linux and macOS (:warning: maybe also Windows WSL, but untested) +* [elan](https://github.com/leanprover/elan) +* [Git LFS](https://git-lfs.com/) + +## Building + +A direct `lake build` in this directory should suffice. + +To quickly test its success, write a simple theorem and try to prove it `by aesop`. If the goal is closed (i.e., `No goals` displayed in the InfoView), `aesop` is likely to have been properly built. Then replace `by aesop` with `by suggest_tactics`. If a list of tactics is shown under `Tactic suggestions` in the InfoView while the goal is not closed, the LeanInfer part is successfully built as well. For the first time, should it ask you to download the model by running `suggest_tactics!`, following it will automatically download the model to `~/.cache/lean_infer/` by default, with the path overridable by setting the `LEAN_INFER_CACHE_DIR` environment variable. A simple guide of this testing process is available [here](./AesopTest/NeuralProver.lean) as well. + +## Usage + +Users can opt to add a new rule that calls a pre-trained machine learning model under the hood, by simply defining a structure consisting of a model name and a set of hyperparameters (all optional, if any of them is not specified by the users, built-in default settings automatically apply), and then annotating it with our new rule builder `neural`. See [here](./AesopTest/NeuralProver.lean) for a quick example where the model is specified by the user while hyperparameters are not (thus inheriting the default settings). + +Note that we always allow the users to choose using the machine learning power or not, as it can be easily turned on/off by adding such a new rule or sticking to the raw Aesop. + +## Questions and Bugs + +* For general questions and discussions, please use [GitHub Discussions](https://github.com/Peiyang-Song/aesop/discussions). +* To report a potential bug, please open an issue. In the issue, please include your OS information and the exact steps to reproduce the error. The more details you provide, the better we will be able to help you. + +## Related Links + +* [LeanDojo Website](https://leandojo.org/) +* [LeanInfer](https://github.com/lean-dojo/LeanInfer) +* [LeanDojo](https://github.com/lean-dojo/LeanDojo) +* [ReProver](https://github.com/lean-dojo/ReProver) +* [Aesop](https://github.com/JLimperg/aesop) + +## Acknowledgements + +* We thank [Jannis Limperg](https://limperg.de/) for help and insights regarding the integration of Aesop and LeanInfer. + + + +# Aesop (original) Aesop (Automated Extensible Search for Obvious Proofs) is a proof search tactic for Lean 4. It is broadly similar to Isabelle's `auto`. In essence, Aesop works From ad2b3e8fe15fa143d328678cc98ac34635421e7a Mon Sep 17 00:00:00 2001 From: Peiyang Song Date: Sat, 23 Sep 2023 14:16:43 -0700 Subject: [PATCH 07/31] Separate Aesop-LeanInfer readme from original Aesop --- README.md | 949 +----------------------------------------------------- 1 file changed, 1 insertion(+), 948 deletions(-) diff --git a/README.md b/README.md index bb40f077..a642328e 100644 --- a/README.md +++ b/README.md @@ -37,951 +37,4 @@ Note that we always allow the users to choose using the machine learning power o ## Acknowledgements -* We thank [Jannis Limperg](https://limperg.de/) for help and insights regarding the integration of Aesop and LeanInfer. - - - -# Aesop (original) - -Aesop (Automated Extensible Search for Obvious Proofs) is a proof search tactic -for Lean 4. It is broadly similar to Isabelle's `auto`. In essence, Aesop works -like this: - -- As with `simp`, you tag a (large) collection of definitions with the - `@[aesop]` attribute, registering them as Aesop _rules_. Rules can be - arbitrary tactics. We provide convenient ways to create common types of rules, - e.g. rules which apply a lemma. -- Aesop takes these rules and tries to apply each of them to the initial goal. - If a rule succeeds and generates subgoals, Aesop recursively applies the rules - to these subgoals, building a _search tree_. -- The search tree is explored in a _best-first_ manner. You can mark rules as - more or less likely to be useful. Based on this information, Aesop prioritises - the goals in the search tree, visiting more promising goals before less - promising ones. -- Before any rules are applied to a goal, it is _normalised_, using a special - (customisable) set of _normalisation rules_. An important built-in - normalisation rule runs `simp_all`, so your `@[simp]` lemmas are taken into - account by Aesop. -- Rules can be marked as _safe_ to optimise Aesop's performance. A safe rule is - applied eagerly and is never backtracked. For example, Aesop's built-in rules - safely split a goal `P ∧ Q` into goals for `P` and `Q`. After this split, the - original goal `P ∧ Q` is never revisited. -- Aesop provides a set of built-in rules which perform logical operations (e.g. - case-split on hypotheses `P ∨ Q`) and some other straightforward deductions. -- Aesop uses indexing methods similar to those of `simp` and other Lean tactics. - This means it should remain reasonably fast even with a large rule set. -- When called as `aesop?`, Aesop prints a tactic script that proves the goal, - similar to `simp?`. This way you can avoid the performance penalty of running - Aesop all the time. However, the script generation is currently not fully - reliable, so you may have to adjust the generated script. - -Aesop should be suitable for two main use cases: - -- General-purpose automation, where Aesop is used to dispatch 'trivial' goals. - Once mathlib is ported to Lean 4 and we have registered many lemmas as Aesop - rules, Aesop will hopefully serve as a much more powerful `simp`. -- Special-purpose automation, where specific Aesop rule sets are built to - address a certain class of goals. Tactics such as `measurability`, - `continuity` or `tidy`, which perform some sort of recursive search, can - hopefully be replaced by Aesop rule sets. - -I only occasionally update this README, so details may be out of date. If you -have questions, please create an issue or ping me (Jannis Limperg) on the [Lean -Zulip](https://leanprover.zulipchat.com). Pull requests are very welcome! - -There's also [a paper about Aesop](https://zenodo.org/record/7430233) which -covers many of the topics discussed here, sometimes in more detail. - -## Building - -With [elan](https://github.com/leanprover/elan) installed, `lake build` -should suffice. - -## Adding Aesop to Your Project - -To use Aesop in a Lean 4 project, first add this package as a dependency. In -your `lakefile.lean`, add - -```lean -require aesop from git "https://github.com/JLimperg/aesop" -``` - -You also need to make sure that your `lean-toolchain` file contains the same -version of Lean 4 as Aesop's, and that your versions of Aesop's dependencies -(currently only `std4`) match. We unfortunately can't support version ranges at -the moment. - -Now the following test file should compile: - -```lean -import Aesop - -example : α → α := - by aesop -``` - -## Quickstart - -To get you started, I'll explain Aesop's major concepts with a series of -examples. A more thorough, reference-style discussion follows in the next -section. - -We first define our own version of lists (so as not to clash with the standard -library) and an `append` function: - -``` lean -inductive MyList (α : Type _) - | nil - | cons (hd : α) (tl : MyList α) - -namespace MyList - -protected def append : (_ _ : MyList α) → MyList α - | nil, ys => ys - | cons x xs, ys => cons x (MyList.append xs ys) - -instance : Append (MyList α) := - ⟨MyList.append⟩ -``` - -We also tell `simp` to unfold applications of `append`: - -```lean -@[simp] -theorem nil_append : nil ++ xs = xs := rfl - -@[simp] -theorem cons_append : cons x xs ++ ys = cons x (xs ++ ys) := rfl -``` - -When Aesop first encounters a goal, it normalises it by running a customisable -set of normalisation rules. One such normalisation rule effectively runs -`simp_all`, so Aesop automatically takes `simp` lemmas into account. - -Now we define the `NonEmpty` predicate on `MyList`: - -``` lean -@[aesop safe [constructors, cases]] -inductive NonEmpty : MyList α → Prop - | cons : NonEmpty (cons x xs) -``` - -Here we see the first proper Aesop feature: we use the **`@[aesop]`** attribute -to construct two Aesop rules related to the `NonEmpty` type. These rules are -added to a global rule set. When Aesop searches for a proof, it systematically -applies each available rule, then recursively searches for proofs of the -subgoals generated by the rule, and so on, building a search tree. A goal is -proved when Aesop applies a rule that generates no subgoals. - -In general, rules can be arbitrary tactics. But since you probably don't want to -write a tactic for every rule, the `aesop` attribute provides several **rule -builders** which construct common sorts of rules. In our example, we construct: - -- A **`constructors`** rule. This rule tries to apply each constructor of - `NonEmpty` whenever a goal has target `NonEmpty _`. -- A **`cases`** rule. This rule searches for hypotheses `h : NonEmpty _` and - performs case analysis on them (like the `cases` tactic). - -Both rules above are added as **safe** rules. When a safe rule succeeds on a -goal encountered during the proof search, it is applied and the goal is never -visited again. In other words, the search does not backtrack safe rules. We will -later see **unsafe** rules, which can backtrack. - -With these rules, we can prove a theorem about `NonEmpty` and `append`: - -``` lean -@[aesop unsafe 50% apply] -theorem nonEmpty_append₁ {xs : MyList α} ys : - NonEmpty xs → NonEmpty (xs ++ ys) := by - aesop -``` - -Aesop finds this proof in four steps: - -- A built-in rule introduces the hypothesis `h : NonEmpty xs`. By default, - Aesop's rule set contains a number of straightforward rules for handling the - logical connectives `→`, `∧`, `∨` and `¬` as well as the quantifiers `∀` and - `∃` and some other basic types. -- The `cases` rule for `NonEmpty` performs case analysis on `h`. -- The `simp` rule `cons_append`, which we added earlier, unfolds the `++` - operation. -- The `constructor` rule for `NonEmpty` applies `NonEmpty.cons`. - -If you want to see how Aesop proves your goal (or why it doesn't prove your -goal, or why it takes too long to prove your goal), you can enable tracing: - -``` lean -set_option trace.aesop true -``` - -This makes Aesop print out the steps it takes while searching for a proof. You -can also look at the search tree Aesop constructed by enabling the -`trace.aesop.finalTree` option. For more tracing options, type `set_option -trace.aesop` and see what auto-completion suggests. - -If, in the example above, you call `aesop?` instead, then Aesop prints a proof -script. At time of writing, it looks like this: - -``` lean -intro a -unhygienic aesop_cases a -simp_all only [cons_append] -apply MyList.NonEmpty.cons -``` - -With a bit of post-processing, you can use this script instead of the Aesop -call. This way you avoid the performance penalty of making Aesop search for a -proof over and over again. The proof script generation currently has some known -bugs, but it produces usable scripts most of the time. - -The `@[aesop]` attribute on `nonEmpty_append₁` adds this lemma as an **unsafe** -rule to the default rule set. For this rule we use the **`apply`** rule builder, -which generates a rule that tries to apply `nonEmpty_append₁` whenever the -target is of the form `NonEmpty (_ ++ _)`. - -Unsafe rules are rules which can backtrack, so after they have been applied to a -goal, Aesop may still try other rules to solve the same goal. This makes sense -for `nonEmpty_append₁`: if we have a goal `NonEmpty (xs ++ ys)`, we may prove it -either by showing `NonEmpty xs` (i.e., by applying `nonEmpty_append₁`) or by -showing `NonEmpty ys`. If `nonEmpty_append₁` were registered as a safe rule, we -would always choose `NonEmpty xs` and never investigate `NonEmpty ys`. - -Each unsafe rule is annotated with a **success probability**, here 50%. This is -a very rough estimate of how likely it is that the rule will to lead to a -successful proof. It is used to prioritise goals: the initial goal starts with a -priority of 100% and whenever we apply an unsafe rule, the priority of its -subgoals is the priority of its parent goal multiplied with the success -probability of the applied rule. So applying `nonEmpty_append₁` repeatedly would -give us goals with priority 50%, 25%, etc. Aesop always considers the -highest-priority unsolved goal first, so it prefers proof attempts involving few -and high-probability rules. Additionally, when Aesop has a choice between -multiple unsafe rules, it prefers the one with the highest success probability. -(Ties are broken arbitrarily but deterministically.) - -After adding `nonEmpty_append`, Aesop can prove some consequences of this -lemma: - -``` lean -example {α : Type u} {xs : MyList α} ys zs : - NonEmpty xs → NonEmpty (xs ++ ys ++ zs) := by - aesop -``` - -Next, we prove another simple theorem about `NonEmpty`: - -``` lean -theorem nil_not_nonEmpty (xs : MyList α) : xs = nil → ¬ NonEmpty xs := by - aesop (add 10% cases MyList, norm simp Not) -``` - -Here we add two rules in an **`add`** clause. These rules are not part of a -rule set but are added for this Aesop call only. - -The first rule is an unsafe `cases` rule for `MyList`. (As you can see, you can -leave out the `unsafe` keyword and specify only a success probability.) This -rule is dangerous: when we apply it to a hypothesis `xs : MyList α`, we get `x : -α` and `ys : MyList α`, so we can apply the `cases` rule again to `ys`, and so -on. We therefore give this rule a very low success probability, to make sure -that Aesop applies other rules if possible. - -We also add a **norm** or **normalisation** rule. As mentioned above, these -rules are used to normalise the goal before any other rules are applied. As part -of this normalisation process, we run a variant of `simp_all` with the global -`simp` set plus Aesop-specific `simp` lemmas. The **`simp`** builder adds such -an Aesop-specific `simp` lemma which unfolds the `Not` definition. (There is -also a built-in rule which performs the same unfolding, so this rule is -redundant.) - -Here are some other examples where normalisation comes in handy: - -``` lean -@[simp] -theorem append_nil {xs : MyList α} : - xs ++ nil = xs := by - induction xs <;> aesop - -theorem append_assoc {xs ys zs : MyList α} : - (xs ++ ys) ++ zs = xs ++ (ys ++ zs) := by - induction xs <;> aesop -``` - -Since we previously added unfolding lemmas for `append` to the global `simp` -set, Aesop can prove theorems about this function more or less by itself (though -in fact `simp_all` would already suffice.) However, we still need to perform -induction explicitly. This is a deliberate design choice: techniques for -automating induction exist, but they are complex, somewhat slow and not entirely -reliable, so we prefer to do it manually. - -Many more examples can be found in the `tests` folder of this repository. In -particular, the file `tests/run/List.lean` contains an Aesop-ified port of 200 -basic list lemmas from the Lean 3 version of mathlib. The file -`tests/run/SeqCalcProver.lean` shows how Aesop can help with the formalisation -of a simple sequent calculus prover. - -## Reference - -This section contains a systematic and fairly comprehensive account of how Aesop -operates. - -### Rules - -A rule is a tactic plus some associated metadata. Rules come in three flavours: - -- **Normalisation rules** (keyword `norm`) must generate zero or one subgoal. - (Zero means that the rule closed the goal). Each normalisation rule is - associated with an integer **penalty** (default 1). Normalisation rules are - applied in a fixpoint loop in order of penalty, lowest first. For rules with - equal penalties, the order is unspecified. See below for details on - the normalisation algorithm. - - Normalisation rules can also be simp lemmas. These are constructed with the - `simp` builder. They are used by a special `simp` call during - the normalisation process. - -- **Safe rules** (keyword `safe`) are applied after normalisation but before any - unsafe rules. When a safe rule is successfully applied to a goal, the goal - becomes *inactive*, meaning no other rules are considered for it. Like - normalisation rules, safe rules are associated with a penalty (default 1) - which determines the order in which the rules are tried. - - Safe rules should be provability-preserving, meaning that if a goal is - provable and we apply a safe rule to it, the generated subgoals should still - be provable. This is a less precise notion than it may appear since - what is provable depends on the entire Aesop rule set. - -- **Unsafe rules** (keyword `unsafe`) are tried only if all available safe rules - have failed on a goal. When an unsafe rule is applied to a goal, the goal is - not marked as inactive, so other (unsafe) rules may be applied to it. These - rule applications are considered independently until one of them proves the - goal (or until we've exhausted all available rules and determine that the goal - is not provable with the current rule set). - - Each unsafe rule has a **success probability** between 0% and 100%. These - probabilities are used to determine the priority of a goal. The initial goal - has priority 100% and whenever we apply an unsafe rule, the priorities of its - subgoals are the priority of the rule's parent goal times the rule's success - probability. Safe rules are treated as having 100% success probability. - -Rules can also be **multi-rules**. These are rules which add multiple rule -applications to a goal. For example, registering the constructors of the `Or` -type will generate a multi-rule that, given a goal with target `A ∨ B`, -generates one rule application with goal `A` and one with goal `B`. This is -equivalent to registering one rule for each constructor, but multi-rules can be -both slightly more efficient and slightly more natural. - -### Search Tree - -Aesop's central data structure is a search tree. This tree alternates between -two kinds of nodes: - -- **Goal nodes**: these nodes store a goal, plus metadata relevant to the - search. The parent and children of a goal node are rule application nodes. In - particular, each goal node has a **priority** between 0% and 100%. -- **Rule application ('rapp') nodes**: these goals store a rule (plus metadata). - The parent and children of a rapp node are goal nodes. When the search tree - contains a rapp node with rule `r`, parent `p` and children `c₁, ..., cₙ`, - this means that the tactic of rule `r` was applied to the goal of `p`, - generating the subgoals of the `cᵢ`. - -When a goal node has multiple child rapp nodes, we have a choice of how to solve -the goals. This makes the tree an AND-OR tree: to prove a rapp, *all* its child -goals must be proved; to prove a goal, *any* of its child rapps must be proved. - -### Search - -We start with a search tree containing a single goal node. This node's goal is -the goal which Aesop is supposed to solve. Then we perform the following steps -in a loop, stopping if (a) the root goal has been proved; (b) the root goal -becomes unprovable; or (c) one of Aesop's rule limits has been reached. (There -are configurable limits on, e.g., the total number of rules applied or the -search depth.) - -- Pick the highest-priority active goal node `G`. Roughly speaking, a goal node - is active if it is not proved and we haven't yet applied all possible rules to - it. -- If the goal of `G` has not been normalised yet, normalise it. That means we - run the following normalisation loop: - - Run the normalisation rules with negative penalty (lowest penalty first). If - any of these rules is successful, restart the normalisation loop with the - goal produced by the rule. - - Run `simp` on all hypotheses and the target, using the global simp set (i.e. - lemmas tagged `@[simp]`) plus Aesop's `simp` rules. - - Run the normalisation rules with positive penalty (lowest penalty first). - If any of these rules is successful, restart the normalisation loop. - - The loop ends when all normalisation rules fail. It destructively updates - the goal of `G` (and may prove it outright). -- If we haven't tried to apply the safe rules to the goal of `G` yet, try to - apply each safe rule (lowest penalty first). As soon as a rule succeeds, add - the corresponding rapp and child goals to the tree and mark `G` as inactive. - The child goals receive the same priority as `G`. -- Otherwise there is at least one unsafe rule that hasn't been tried on `G` yet - (or else `G` would have been inactive). Try the unsafe rule with the highest - success probability and if it succeeds, add the corresponding rapp and child - goals to the tree. The child goals receive the priority of `G` times the - success probability of the applied rule. - -A goal is **unprovable** if we have applied all possible rules to it and all -resulting child rapps are unprovable. A rapp is unprovable if any of its -subgoals is unprovable. - -During the search, a goal or rapp can also become **irrelevant**. This means -that we don't have to visit it again. Informally, goals and rapps are irrelevant -if they are part of a branch of the search tree which has either successfully -proved its goal already or which can never prove its goal. More formally: - -- A goal is irrelevant if its parent rapp is unprovable. (This means that a - sibling of the goal is already unprovable, in which case we know that the - parent rapp will never be proved.) -- A rapp is irrelevant if its parent goal is proved. (This means that a sibling - of the rapp is already proved, and we only need one proof.) -- A goal or rapp is irrelevant if any of its ancestors is irrelevant. - -### Rule Builders - -A **rule builder** is a metaprogram that turns a declaration or hypothesis into -an Aesop rule. Currently available builders are: - -- **`apply`**: generates a rule which tries to apply the given declaration or - hypothesis `x` to the target. The rule acts like the tactic `apply x`. -- **`forward`**: when applied to a declaration or hypothesis of type `A₁ → ... - Aₙ → B`, generates a rule which looks for hypotheses `h₁ : A₁`, ..., `hₙ : Aₙ` - in the goal and, if they are found, adds a new hypothesis `h : B`. As an - example, consider the lemma `even_or_odd`: - - ```lean - even_or_odd : ∀ (n : Nat), Even n ∨ Odd n - ``` - - Registering this as a forward rule will cause the goal - - ```lean - n : Nat - m : Nat - ⊢ T - ``` - - to be transformed into this: - - ```lean - n : Nat - hn : Even n ∨ Odd n - m : Nat - hm : Even m ∨ Odd m - ⊢ T - ``` - - The forward builder may also be given a list of *immediate names*: - - ``` - (forward (immediate := [n])) even_or_odd - ``` - - The immediate names, here `n`, refer to the arguments of `even_or_odd`. When - Aesop applies a forward rule with explicit immediate names, it only matches - the corresponding arguments to hypotheses. (Here, `even_or_odd` has only one - argument, so there is no difference.) - - When no immediate names are given, Aesop considers every argument immediate, - except for instance arguments and dependent arguments (i.e. those that can be - inferred from the types of later arguments). - - When a forward rule is successful, Aesop remembers the type of the hypothesis - added by the rule, say `T`. If a forward rule (possibly the same one) is - subsequently applied to a subgoal and wants to add another hypothesis of type - `T`, this is forbidden and the rule fails. Without this restriction, forward - rules would in many cases be applied infinitely often. However, note that the - rule is still executed on its own subgoals (and their subgoals, etc.), which - can become a performance issue. You should therefore prefer `destruct` rules - where possible. -- **`destruct`**: works like `forward`, but after the rule has been applied, - hypotheses that were used as immediate arguments are cleared. This is useful - when you want to eliminate a hypothesis. E.g. the rule - ``` - @[aesop norm destruct] - theorem and_elim_right : α ∧ β → α := ... - ``` - will cause the goal - ``` - h₁ : (α ∧ β) ∧ γ - h₂ : δ ∧ ε - ``` - to be transformed into - ``` - h₁ : α - h₂ : δ - ``` - - Unlike with `forward` rules, when an `destruct` rule is successfully applied, - it may be applied again to the resulting subgoals (and their subgoals, etc.). - There is less danger of infinite cycles because the original hypothesis is - cleared. - - However, if the hypothesis or hypotheses to which the `destruct` rule is - applied have dependencies, they are not cleared. In this case, you'll probably - get an infinite cycle. (TODO fix this.) -- **`constructors`**: when applied to an inductive type or structure `T`, - generates a rule which tries to apply each constructor of `T` to the target. - This is a multi-rule, so if multiple constructors apply, they are considered - in parallel. If you use this constructor to build an unsafe rule, each - constructor application receives the same success probability; if this is not - what you want, add separate `apply` rules for the constructors. -- **`cases`**: when applied to an inductive type or structure `T`, generates a - rule that performs case analysis on every hypothesis `h : T` in the context. - The rule recurses into subgoals, so `cases Or` will generate 6 goals when - applied to a goal with hypotheses `h₁ : A ∨ B ∨ C` and `h₂ : D ∨ E`. However, - if `T` is a recursive type (e.g. `List`), we only perform case analysis once - on each hypothesis. Otherwise we would loop infinitely. - - The `patterns` option can be used to apply the rule only on hypotheses of a - certain shape. E.g. the rule `(cases (patterns := [Fin 0])) Fin` will perform - case analysis only on hypotheses of type `Fin 0`. Patterns can contain - underscores, e.g. `0 ≤ _`. Multiple patterns can be given (separated by - commas); the rule is then applied whenever at least one of the patterns - matches a hypothesis. -- **`simp`**: when applied to an equation `eq : A₁ → ... Aₙ → x = y`, registers - `eq` as a simp lemma for the built-in simp pass during normalisation. As such, - this builder can only build normalisation rules. -- **`unfold`**: when applied to a definition or `let` hypothesis `f`, registers - `f` to be unfolded (i.e. replaced with its definition) during normalisation. - As such, this builder can only build normalisation rules. The unfolding - happens in a separate `simp` pass. - - The `simp` builder can also be used to unfold definitions. The difference is - that `simp` rules perform smart unfolding (like the `simp` tactic) and - `unfold` rules perform non-smart unfolding (like the `unfold` tactic). - Non-smart unfolding unfolds functions even when none of their equations - match, so `unfold` rules for recursive functions generally lead to looping. -- **`tactic`**: takes a tactic and directly turns it into a rule. The given - declaration (the builder does not work for hypotheses) must have type `TacticM - Unit`, `Aesop.SimpleRuleTac` or `Aesop.RuleTac`. The latter are Aesop data - types which associate a tactic with additional metadata; using them may allow - the rule to operate somewhat more efficiently. - - The builder may be given an option `uses_branch_state := ` (default - true). This indicates whether the given tactic uses the branch state; see - below. - - Rule tactics should not be 'no-ops': if a rule tactic is not applicable to a - goal, it should fail rather than return the goal unchanged. All no-op rules - waste time and no-op `norm` rules will send normalisation into an infinite - loop. - - Normalisation rules may not assign metavariables (other than the goal - metavariable) or introduce new metavariables (other than the new goal - metavariable). This can be a problem because some Lean tactics, e.g. `cases`, - do so even in cases where you probably would not expect them to. I'm afraid - there is currently no good solution for this. -- **`default`**: The default builder. This is the builder used when you - register a rule without specifying a builder, but you can also use it - explicitly. Depending on the rule's phase, the default builder tries - different builders, using the first one that works. These builders are: - - For `safe` and `unsafe` rules: `constructors`, `tactic`, `apply`. - - For `norm` rules: `constructors`, `tactic`, `simp`, `apply`. - -#### Transparency Options - -The rule builders `apply`, `forward`, `destruct`, `constructors` and `cases` -each have a `transparency` option. This option controls the transparency at -which the rule is executed. For example, registering a rule with the builder -`(apply (transparency := reducible))` makes the rule act like the tactic -`with_reducible apply`. - -However, even if you change the transparency of a rule, it is still indexed at -`reducible` transparency (since the data structure we use for indexing only -supports `reducible` transparency). So suppose you register an `apply` rule with -`default` transparency. Further suppose the rule concludes `A ∧ B` and your -target is `T` with `def T := A ∧ B`. Then the rule could apply to the target -since it can unfold `T` at `default` transparency to discover `A ∧ B`. However, -the rule is never applied because the indexing procedure sees only `T` and does -not consider the rule potentially applicable. - -To override this behaviour, you can write `(apply (transparency! := default))` -(note the bang). This disables indexing, so the rule is tried on every goal. - -### Rule Sets - -Rule sets are declared with the command - -``` lean -declare_aesop_rule_sets [r₁, ..., rₙ] -``` - -where the `rᵢ` are arbitrary names. To avoid clashes, pick names in the -namespace of your package. - -Within a rule set, rules are identified by their name, builder and phase -(safe/unsafe/norm). This means you can add the same declaration as multiple -rules with different builders or in different phases, but not with different -priorities or different builder options (if the rule's builder has any options). - -Rules can appear in multiple rule sets, but in this case you should make sure -that they have the same priority and use the same builder options. Otherwise, -Aesop will consider these rules the same and arbitrarily pick one. - -By default, the `aesop` tactic uses the `builtin` and `default` rule sets. The -`builtin` set contains built-in rules for handling various constructions (see -below). The `default` set contains rules which were added by Aesop users without -specifying a rule set. - -### The `@[aesop]` Attribute - -Declarations can be added to rule sets by annotating them with the `@[aesop]` -attribute. - -#### Single Rule - -In most cases, you'll want to add one rule for the declaration. The syntax for -this is - -``` lean -@[aesop ? ? ? ?] -``` - -where - -- `` is `safe`, `norm` or `unsafe`. Cannot be omitted except under the - conditions in the next bullets. - -- `` is: - - For `simp` rules, a natural number. This is used as the priority of the - `simp` generated `simp` lemmas, so registering a `simp` rule with priority - `n` is roughly equivalent to the attribute `@[simp n]`. If omitted, defaults - to Lean's default `simp` priority. - - For `safe` and `norm` rules (except `simp` rules), an integer penalty. If - omitted, defaults to 1. - - For `unsafe` rules, a percentage between 0% and 100%. Cannot be omitted. - You may omit the `unsafe` phase specification when giving a percentage. - - For `unfold` rules, a penalty can be given, but it is currently ignored. - -- `` is one of the builders given above. If you want to pass options to - a builder, write it like this (with mandatory parentheses): - - ```text - (tactic (uses_branch_state := true)) - ``` - - If no builder is specified, the default builder for the given phase is used. - Since the `simp` builder generates only normalisation rules, the `norm` phase - may be omitted. - -- `` is a clause of the form - - ```text - (rule_sets [r₁, ..., rₙ]) - ``` - - where the `rᵢ` are declared rule sets. (Parentheses are mandatory.) The rule - is added exactly to the specified rule sets. If this clause is omitted, it - defaults to `(rule_sets [default])`. - -#### Multiple Rules - -It is occasionally useful to add multiple rules for a single declaration, e.g. -a `cases` and a `constructors` rule for the same inductive type. In this case, -you can write for example - -``` lean -@[aesop unsafe [constructors 75%, cases 90%]] -inductive T ... - -@[aesop apply [safe (rule_sets [A]), 70% (rule_sets [B])]] -def foo ... - -@[aesop [80% apply, safe 5 (forward (immediate := x))]] -def bar (x : T) ... -``` - -In the first example, two unsafe rules for `T` are registered, one with success -probability 75% and one with 90%. - -In the second example, two rules are registered for `foo`. Both use the `apply` -builder. The first, a `safe` rule with default penalty, is added to rule set -`A`. The second, an `unsafe` rule with 70% success probability, is added to -rule set `B`. - -In the third example, two rules are registered for `bar`: an `unsafe` rule with -80% success probability using the `apply` builder and a `safe` rule with penalty -5 using the `forward` builder. - -In general, the grammar for the `@[aesop]` attribute is - -``` lean -attr ::= @[aesop ] - | @[aesop []] - -rule_expr ::= feature - | feature - | feature [] -``` - -where `feature` is a phase, priority, builder or `rule_sets` clause. This -grammar yields one or more trees of features and each branch of these trees -specifies one rule. (A branch is a list of features.) - -### Adding External Rules - -You can use the `attribute` command to add rules for constants which were -declared previously, either in your own development or in a package you import: - -``` -attribute [aesop norm unfold] List.all -- List.all is from Init -``` - -### Erasing Rules - -There are two ways to erase rules. Usually it suffices to remove the `@[aesop]` -attribute: - -``` lean -attribute [-aesop] foo -``` - -This will remove all rules associated with the declaration `foo` from all rule -sets. However, this erasing is not persistent, so the rule will reappear at the -end of the file. This is a fundamental limitation of Lean's attribute system: -once a declaration is tagged with an attribute, it cannot be permanently -untagged. - -If you want to remove only certain rules, you can use the `erase_aesop_rules` -command: - -``` lean -erase_aesop_rules [safe apply foo, bar (rule_sets [A])] -``` - -This will remove: - -- all safe rules for `foo` with the `apply` builder from all rule sets (but not -other, for example, unsafe rules or `forward` rules); -- all rules for `bar` from rule set `A`. - -In general, the syntax is - -``` lean -erase_aesop_rules [] -``` - -i.e. rules are specified in the same way as for the `@[aesop]` attribute. -However, each rule must also specify the name of the declaration whose rules -should be erased. The `rule_expr` grammar is therefore extended such that a -`feature` can also be the name of a declaration. - -Note that a rule added with one of the default builders (`safe_default`, -`norm_default`, `unsafe_default`) will be registered under the name of the -builder that is ultimately used, e.g. `apply` or `simp`. So if you want to erase -such a rule, you may have to specify that builder instead of the default -builder. - -### The `aesop` Tactic - -In its most basic form, you can call the Aesop tactic just by writing - -``` lean -example : α → α := by - aesop -``` - -This will use the rules in the `default` rule set (i.e. those added via the -attribute with no explicit rule set specified) and the rules in the `builtin` -rule set (i.e. those provided by Aesop itself). - -The tactic's behaviour can also be customised with various options. A more -involved Aesop call might look like this: - -``` text -aesop - (add safe foo, 10% cases Or, safe cases Empty) - (erase A, baz) - (rule_sets [A, B]) - (options := { maxRuleApplicationDepth := 10 }) -``` - -Here we add some rules with an `add` clause, erase other rules with an `erase` -clause, limit the used rule sets and set some options. Each of these clauses -is discussed in more detail below. - -#### Adding Rules to an Aesop Call - -Rules can be added to an Aesop call with an `add` clause. This won't affect any -declared rule sets. The syntax of the `add` clause is - -``` text -(add ) -``` - -i.e. rules can be specified in the same way as for the `@[aesop]` attribute. -As with the `erase_aesop_rules` command, each rule must specify the name of -declaration from which the rule should be built; for example - -``` text -(add safe [foo 1, bar 5]) -``` - -will add the declaration `foo` as a safe rule with penalty 1 and `bar` as a safe -rule with penalty 5. - -The rule names can also refer to hypotheses in the goal context, but not all -builders support this. - -#### Erasing Rules From an Aesop Call - -Rules can be removed from an Aesop call with an `erase` clause. Again, this -affects only the current Aesop call and not the declared rule sets. The syntax -of the `erase` clause is - -``` text -(erase ) -``` - -and it works exactly like the `erase_aesop_rules` command. To erase all rules -associated with `x` and `y`, write - -``` lean -(erase x, y) -``` - -#### Selecting Rule Sets - -By default, Aesop uses the `default` and `builtin` rule sets. A `rule_sets` -clause can be given to include additional rule sets, e.g. - -``` text -(rule_sets [A, B]) -``` - -This will use rule sets `A`, `B`, `default` and `builtin`. Rule sets can also -be disabled with `rule_sets [-default, -builtin]`. - -#### Setting Options - -Various options can be set with an `options` clause, whose syntax is: - -``` text -(options := ) -``` - -The term is an arbitrary Lean expression of type `Aesop.Options`; see there for -details. A notable option is `strategy`, which is one of `.bestFirst`, -`.depthFirst` and `.breadthFirst` and instructs Aesop to use the corresponding -search strategy. Best-first is the default. - -Similarly, options for the built-in norm simp call can be set with - -``` text -(simp_options := ) -``` - -The term has type `Aesop.SimpConfig`; see there for details. The `useHyps` -option may be particularly useful: when `true` (the default), norm simp behaves -like the `simp_all` tactic; when `false`, norm simp behaves like `simp at *`. - -### Built-In Rules - -The set of built-in rules (those in the `builtin` rule set) is currently quite -unstable, so for now I won't document them in detail. See -`Aesop/BuiltinRules.lean` and `Aesop/BuiltinRules/*.lean` - -### Proof Scripts - -By calling `aesop?` instead of `aesop`, you can instruct Aesop to generate a -tactic script which proves the goal (if Aesop succeeds). The script is printed -as a `Try this:` suggestion, similar to `simp?`. - -The scripts generated by Aesop are currently a bit idiosyncratic. For example, -they may contain the `aesop_cases` tactic, which is a slight variation of the -standard `cases`. Additionally, Aesop occasionally generates buggy scripts which -do not solve the goal. We hope to eventually fix these issues; until then, you -may have to lightly adjust the proof scripts by hand. - -### Tracing - -To see how Aesop proves a goal -- or why it doesn't prove a goal, or why it's -slow to prove a goal -- it is useful to see what it's doing. To that end, you -can enable various tracing options. These use the usual syntax, e.g. - -``` lean -set_option trace.aesop true -``` - -The main options are: - -- `trace.aesop`: print a step-by-step log of which goals Aesop tried to - solve, which rules it tried to apply (successfully or unsuccessfully), etc. -- `trace.aesop.ruleSet`: print the rule set used for an Aesop call. -- `trace.aesop.proof`: if Aesop is successful, print the proof that was - generated (as a Lean term). You should be able to copy-and-paste this proof - to replace Aesop. - -### Profiling - -To get an idea of where Aesop spends its time, use - -``` lean -set_option trace.aesop.profile true -``` - -Aesop then prints a summary of how much time its various tasks took. - -To get a more fine-grained picture, enable the `trace.aesop` and `profiler` -options. The trace is then augmented with information about how much time each -step took. Note that only the timing information pertaining to goal expansions -and rule applications is relevant. Other timings, such as those attached to new -rapps and goals, are just artefacts of the Lean tracing API. - -### Checking Internal Invariants - -If you encounter behaviour that looks like an internal error in Aesop, it may -help to set the option `aesop.check.all` (or the more fine-grained -`aesop.check.*` options). This makes Aesop check various invariants while the -tactic is running. These checks are somewhat expensive, so remember to unset the -option after you've reported the bug. - -### Handling Metavariables - -Rules which create metavariables must be handled specially by Aesop. For -example, suppose we register transitivity of `<` as an Aesop rule. Then we may -get a goal state of this form: - -``` lean -n k : Nat -⊢ n < ?m - -n k : Nat -⊢ ?m < k -``` - -We may now solve the first goal by applying different rules. We could, for -example, apply the theorem `∀ n, n < n + 1`. We could also use an assumption `n -< a`. Both proofs close the first goal, but crucially, they modify the second -goal: in the first case, it becomes `n + 1 < k`; in the second case, `a < k`. -And of course one of these could be provable while the other is not. In other -words, the second subgoal now depends on the *proof* of the first subgoal -(whereas usually we don't care *how* a goal was proven, only *that* it was -proven). Aesop could also decide to work on the second subgoal first, in which -case the situation is symmetric. - -Due to this dependency, Aesop in effect treats the instantiations of the second -subgoal as *additional goals*. Thus, when we apply the theorem `∀ n, n < n + 1`, -which closes the first goal, Aesop realises that because this theorem was -applied, we must now prove `n + 1 < k` as well. So it adds this goal as an -additional subgoal of the rule application `∀ n, n < n + 1` (which otherwise -would not have any subgoals). Similarly, when the assumption `n < a` is applied, -its rule application gains an additional subgoal `a < k`. - -This mechanism makes sure that we consider all potential proofs. The downside is -that it's quite explosive: when there are multiple metavariables in multiple -goals, which Aesop may visit in any order, Aesop may spend a lot of time copying -goals with shared metavariables. It may even try to prove the same goal more -than once since different rules may yield the same metavariable instantiations. -For these reasons, rules which create metavariables are best kept out of the -global rule set and added to individual Aesop calls on an ad-hoc basis. - -It is also worth noting that when a safe rule assigns a metavariable, it is -treated as an unsafe rule (with success probability 90%). This is because -assigning metavariables is almost never safe, for the same reason as above: the -usually perfectly safe rule `∀ n, n < n + 1` would, if treated as safe, force us -to commit to one particular instantiation of the metavariable `?m`. - -For more details on the handling of metavariables, see the [Aesop -paper](https://zenodo.org/record/7430233). +* We thank [Jannis Limperg](https://limperg.de/) for insightful discussions regarding the integration of Aesop and LeanInfer. From 9d410b5a5bde1e81e938ed3c2f6cd53935a72b84 Mon Sep 17 00:00:00 2001 From: Peiyang Song Date: Sat, 23 Sep 2023 14:17:52 -0700 Subject: [PATCH 08/31] Create Aesop-README.md --- Aesop-README.md | 944 ++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 944 insertions(+) create mode 100644 Aesop-README.md diff --git a/Aesop-README.md b/Aesop-README.md new file mode 100644 index 00000000..5dcad4d6 --- /dev/null +++ b/Aesop-README.md @@ -0,0 +1,944 @@ +# Aesop (original) + +Aesop (Automated Extensible Search for Obvious Proofs) is a proof search tactic +for Lean 4. It is broadly similar to Isabelle's `auto`. In essence, Aesop works +like this: + +- As with `simp`, you tag a (large) collection of definitions with the + `@[aesop]` attribute, registering them as Aesop _rules_. Rules can be + arbitrary tactics. We provide convenient ways to create common types of rules, + e.g. rules which apply a lemma. +- Aesop takes these rules and tries to apply each of them to the initial goal. + If a rule succeeds and generates subgoals, Aesop recursively applies the rules + to these subgoals, building a _search tree_. +- The search tree is explored in a _best-first_ manner. You can mark rules as + more or less likely to be useful. Based on this information, Aesop prioritises + the goals in the search tree, visiting more promising goals before less + promising ones. +- Before any rules are applied to a goal, it is _normalised_, using a special + (customisable) set of _normalisation rules_. An important built-in + normalisation rule runs `simp_all`, so your `@[simp]` lemmas are taken into + account by Aesop. +- Rules can be marked as _safe_ to optimise Aesop's performance. A safe rule is + applied eagerly and is never backtracked. For example, Aesop's built-in rules + safely split a goal `P ∧ Q` into goals for `P` and `Q`. After this split, the + original goal `P ∧ Q` is never revisited. +- Aesop provides a set of built-in rules which perform logical operations (e.g. + case-split on hypotheses `P ∨ Q`) and some other straightforward deductions. +- Aesop uses indexing methods similar to those of `simp` and other Lean tactics. + This means it should remain reasonably fast even with a large rule set. +- When called as `aesop?`, Aesop prints a tactic script that proves the goal, + similar to `simp?`. This way you can avoid the performance penalty of running + Aesop all the time. However, the script generation is currently not fully + reliable, so you may have to adjust the generated script. + +Aesop should be suitable for two main use cases: + +- General-purpose automation, where Aesop is used to dispatch 'trivial' goals. + Once mathlib is ported to Lean 4 and we have registered many lemmas as Aesop + rules, Aesop will hopefully serve as a much more powerful `simp`. +- Special-purpose automation, where specific Aesop rule sets are built to + address a certain class of goals. Tactics such as `measurability`, + `continuity` or `tidy`, which perform some sort of recursive search, can + hopefully be replaced by Aesop rule sets. + +I only occasionally update this README, so details may be out of date. If you +have questions, please create an issue or ping me (Jannis Limperg) on the [Lean +Zulip](https://leanprover.zulipchat.com). Pull requests are very welcome! + +There's also [a paper about Aesop](https://zenodo.org/record/7430233) which +covers many of the topics discussed here, sometimes in more detail. + +## Building + +With [elan](https://github.com/leanprover/elan) installed, `lake build` +should suffice. + +## Adding Aesop to Your Project + +To use Aesop in a Lean 4 project, first add this package as a dependency. In +your `lakefile.lean`, add + +```lean +require aesop from git "https://github.com/JLimperg/aesop" +``` + +You also need to make sure that your `lean-toolchain` file contains the same +version of Lean 4 as Aesop's, and that your versions of Aesop's dependencies +(currently only `std4`) match. We unfortunately can't support version ranges at +the moment. + +Now the following test file should compile: + +```lean +import Aesop + +example : α → α := + by aesop +``` + +## Quickstart + +To get you started, I'll explain Aesop's major concepts with a series of +examples. A more thorough, reference-style discussion follows in the next +section. + +We first define our own version of lists (so as not to clash with the standard +library) and an `append` function: + +``` lean +inductive MyList (α : Type _) + | nil + | cons (hd : α) (tl : MyList α) + +namespace MyList + +protected def append : (_ _ : MyList α) → MyList α + | nil, ys => ys + | cons x xs, ys => cons x (MyList.append xs ys) + +instance : Append (MyList α) := + ⟨MyList.append⟩ +``` + +We also tell `simp` to unfold applications of `append`: + +```lean +@[simp] +theorem nil_append : nil ++ xs = xs := rfl + +@[simp] +theorem cons_append : cons x xs ++ ys = cons x (xs ++ ys) := rfl +``` + +When Aesop first encounters a goal, it normalises it by running a customisable +set of normalisation rules. One such normalisation rule effectively runs +`simp_all`, so Aesop automatically takes `simp` lemmas into account. + +Now we define the `NonEmpty` predicate on `MyList`: + +``` lean +@[aesop safe [constructors, cases]] +inductive NonEmpty : MyList α → Prop + | cons : NonEmpty (cons x xs) +``` + +Here we see the first proper Aesop feature: we use the **`@[aesop]`** attribute +to construct two Aesop rules related to the `NonEmpty` type. These rules are +added to a global rule set. When Aesop searches for a proof, it systematically +applies each available rule, then recursively searches for proofs of the +subgoals generated by the rule, and so on, building a search tree. A goal is +proved when Aesop applies a rule that generates no subgoals. + +In general, rules can be arbitrary tactics. But since you probably don't want to +write a tactic for every rule, the `aesop` attribute provides several **rule +builders** which construct common sorts of rules. In our example, we construct: + +- A **`constructors`** rule. This rule tries to apply each constructor of + `NonEmpty` whenever a goal has target `NonEmpty _`. +- A **`cases`** rule. This rule searches for hypotheses `h : NonEmpty _` and + performs case analysis on them (like the `cases` tactic). + +Both rules above are added as **safe** rules. When a safe rule succeeds on a +goal encountered during the proof search, it is applied and the goal is never +visited again. In other words, the search does not backtrack safe rules. We will +later see **unsafe** rules, which can backtrack. + +With these rules, we can prove a theorem about `NonEmpty` and `append`: + +``` lean +@[aesop unsafe 50% apply] +theorem nonEmpty_append₁ {xs : MyList α} ys : + NonEmpty xs → NonEmpty (xs ++ ys) := by + aesop +``` + +Aesop finds this proof in four steps: + +- A built-in rule introduces the hypothesis `h : NonEmpty xs`. By default, + Aesop's rule set contains a number of straightforward rules for handling the + logical connectives `→`, `∧`, `∨` and `¬` as well as the quantifiers `∀` and + `∃` and some other basic types. +- The `cases` rule for `NonEmpty` performs case analysis on `h`. +- The `simp` rule `cons_append`, which we added earlier, unfolds the `++` + operation. +- The `constructor` rule for `NonEmpty` applies `NonEmpty.cons`. + +If you want to see how Aesop proves your goal (or why it doesn't prove your +goal, or why it takes too long to prove your goal), you can enable tracing: + +``` lean +set_option trace.aesop true +``` + +This makes Aesop print out the steps it takes while searching for a proof. You +can also look at the search tree Aesop constructed by enabling the +`trace.aesop.finalTree` option. For more tracing options, type `set_option +trace.aesop` and see what auto-completion suggests. + +If, in the example above, you call `aesop?` instead, then Aesop prints a proof +script. At time of writing, it looks like this: + +``` lean +intro a +unhygienic aesop_cases a +simp_all only [cons_append] +apply MyList.NonEmpty.cons +``` + +With a bit of post-processing, you can use this script instead of the Aesop +call. This way you avoid the performance penalty of making Aesop search for a +proof over and over again. The proof script generation currently has some known +bugs, but it produces usable scripts most of the time. + +The `@[aesop]` attribute on `nonEmpty_append₁` adds this lemma as an **unsafe** +rule to the default rule set. For this rule we use the **`apply`** rule builder, +which generates a rule that tries to apply `nonEmpty_append₁` whenever the +target is of the form `NonEmpty (_ ++ _)`. + +Unsafe rules are rules which can backtrack, so after they have been applied to a +goal, Aesop may still try other rules to solve the same goal. This makes sense +for `nonEmpty_append₁`: if we have a goal `NonEmpty (xs ++ ys)`, we may prove it +either by showing `NonEmpty xs` (i.e., by applying `nonEmpty_append₁`) or by +showing `NonEmpty ys`. If `nonEmpty_append₁` were registered as a safe rule, we +would always choose `NonEmpty xs` and never investigate `NonEmpty ys`. + +Each unsafe rule is annotated with a **success probability**, here 50%. This is +a very rough estimate of how likely it is that the rule will to lead to a +successful proof. It is used to prioritise goals: the initial goal starts with a +priority of 100% and whenever we apply an unsafe rule, the priority of its +subgoals is the priority of its parent goal multiplied with the success +probability of the applied rule. So applying `nonEmpty_append₁` repeatedly would +give us goals with priority 50%, 25%, etc. Aesop always considers the +highest-priority unsolved goal first, so it prefers proof attempts involving few +and high-probability rules. Additionally, when Aesop has a choice between +multiple unsafe rules, it prefers the one with the highest success probability. +(Ties are broken arbitrarily but deterministically.) + +After adding `nonEmpty_append`, Aesop can prove some consequences of this +lemma: + +``` lean +example {α : Type u} {xs : MyList α} ys zs : + NonEmpty xs → NonEmpty (xs ++ ys ++ zs) := by + aesop +``` + +Next, we prove another simple theorem about `NonEmpty`: + +``` lean +theorem nil_not_nonEmpty (xs : MyList α) : xs = nil → ¬ NonEmpty xs := by + aesop (add 10% cases MyList, norm simp Not) +``` + +Here we add two rules in an **`add`** clause. These rules are not part of a +rule set but are added for this Aesop call only. + +The first rule is an unsafe `cases` rule for `MyList`. (As you can see, you can +leave out the `unsafe` keyword and specify only a success probability.) This +rule is dangerous: when we apply it to a hypothesis `xs : MyList α`, we get `x : +α` and `ys : MyList α`, so we can apply the `cases` rule again to `ys`, and so +on. We therefore give this rule a very low success probability, to make sure +that Aesop applies other rules if possible. + +We also add a **norm** or **normalisation** rule. As mentioned above, these +rules are used to normalise the goal before any other rules are applied. As part +of this normalisation process, we run a variant of `simp_all` with the global +`simp` set plus Aesop-specific `simp` lemmas. The **`simp`** builder adds such +an Aesop-specific `simp` lemma which unfolds the `Not` definition. (There is +also a built-in rule which performs the same unfolding, so this rule is +redundant.) + +Here are some other examples where normalisation comes in handy: + +``` lean +@[simp] +theorem append_nil {xs : MyList α} : + xs ++ nil = xs := by + induction xs <;> aesop + +theorem append_assoc {xs ys zs : MyList α} : + (xs ++ ys) ++ zs = xs ++ (ys ++ zs) := by + induction xs <;> aesop +``` + +Since we previously added unfolding lemmas for `append` to the global `simp` +set, Aesop can prove theorems about this function more or less by itself (though +in fact `simp_all` would already suffice.) However, we still need to perform +induction explicitly. This is a deliberate design choice: techniques for +automating induction exist, but they are complex, somewhat slow and not entirely +reliable, so we prefer to do it manually. + +Many more examples can be found in the `tests` folder of this repository. In +particular, the file `tests/run/List.lean` contains an Aesop-ified port of 200 +basic list lemmas from the Lean 3 version of mathlib. The file +`tests/run/SeqCalcProver.lean` shows how Aesop can help with the formalisation +of a simple sequent calculus prover. + +## Reference + +This section contains a systematic and fairly comprehensive account of how Aesop +operates. + +### Rules + +A rule is a tactic plus some associated metadata. Rules come in three flavours: + +- **Normalisation rules** (keyword `norm`) must generate zero or one subgoal. + (Zero means that the rule closed the goal). Each normalisation rule is + associated with an integer **penalty** (default 1). Normalisation rules are + applied in a fixpoint loop in order of penalty, lowest first. For rules with + equal penalties, the order is unspecified. See below for details on + the normalisation algorithm. + + Normalisation rules can also be simp lemmas. These are constructed with the + `simp` builder. They are used by a special `simp` call during + the normalisation process. + +- **Safe rules** (keyword `safe`) are applied after normalisation but before any + unsafe rules. When a safe rule is successfully applied to a goal, the goal + becomes *inactive*, meaning no other rules are considered for it. Like + normalisation rules, safe rules are associated with a penalty (default 1) + which determines the order in which the rules are tried. + + Safe rules should be provability-preserving, meaning that if a goal is + provable and we apply a safe rule to it, the generated subgoals should still + be provable. This is a less precise notion than it may appear since + what is provable depends on the entire Aesop rule set. + +- **Unsafe rules** (keyword `unsafe`) are tried only if all available safe rules + have failed on a goal. When an unsafe rule is applied to a goal, the goal is + not marked as inactive, so other (unsafe) rules may be applied to it. These + rule applications are considered independently until one of them proves the + goal (or until we've exhausted all available rules and determine that the goal + is not provable with the current rule set). + + Each unsafe rule has a **success probability** between 0% and 100%. These + probabilities are used to determine the priority of a goal. The initial goal + has priority 100% and whenever we apply an unsafe rule, the priorities of its + subgoals are the priority of the rule's parent goal times the rule's success + probability. Safe rules are treated as having 100% success probability. + +Rules can also be **multi-rules**. These are rules which add multiple rule +applications to a goal. For example, registering the constructors of the `Or` +type will generate a multi-rule that, given a goal with target `A ∨ B`, +generates one rule application with goal `A` and one with goal `B`. This is +equivalent to registering one rule for each constructor, but multi-rules can be +both slightly more efficient and slightly more natural. + +### Search Tree + +Aesop's central data structure is a search tree. This tree alternates between +two kinds of nodes: + +- **Goal nodes**: these nodes store a goal, plus metadata relevant to the + search. The parent and children of a goal node are rule application nodes. In + particular, each goal node has a **priority** between 0% and 100%. +- **Rule application ('rapp') nodes**: these goals store a rule (plus metadata). + The parent and children of a rapp node are goal nodes. When the search tree + contains a rapp node with rule `r`, parent `p` and children `c₁, ..., cₙ`, + this means that the tactic of rule `r` was applied to the goal of `p`, + generating the subgoals of the `cᵢ`. + +When a goal node has multiple child rapp nodes, we have a choice of how to solve +the goals. This makes the tree an AND-OR tree: to prove a rapp, *all* its child +goals must be proved; to prove a goal, *any* of its child rapps must be proved. + +### Search + +We start with a search tree containing a single goal node. This node's goal is +the goal which Aesop is supposed to solve. Then we perform the following steps +in a loop, stopping if (a) the root goal has been proved; (b) the root goal +becomes unprovable; or (c) one of Aesop's rule limits has been reached. (There +are configurable limits on, e.g., the total number of rules applied or the +search depth.) + +- Pick the highest-priority active goal node `G`. Roughly speaking, a goal node + is active if it is not proved and we haven't yet applied all possible rules to + it. +- If the goal of `G` has not been normalised yet, normalise it. That means we + run the following normalisation loop: + - Run the normalisation rules with negative penalty (lowest penalty first). If + any of these rules is successful, restart the normalisation loop with the + goal produced by the rule. + - Run `simp` on all hypotheses and the target, using the global simp set (i.e. + lemmas tagged `@[simp]`) plus Aesop's `simp` rules. + - Run the normalisation rules with positive penalty (lowest penalty first). + If any of these rules is successful, restart the normalisation loop. + + The loop ends when all normalisation rules fail. It destructively updates + the goal of `G` (and may prove it outright). +- If we haven't tried to apply the safe rules to the goal of `G` yet, try to + apply each safe rule (lowest penalty first). As soon as a rule succeeds, add + the corresponding rapp and child goals to the tree and mark `G` as inactive. + The child goals receive the same priority as `G`. +- Otherwise there is at least one unsafe rule that hasn't been tried on `G` yet + (or else `G` would have been inactive). Try the unsafe rule with the highest + success probability and if it succeeds, add the corresponding rapp and child + goals to the tree. The child goals receive the priority of `G` times the + success probability of the applied rule. + +A goal is **unprovable** if we have applied all possible rules to it and all +resulting child rapps are unprovable. A rapp is unprovable if any of its +subgoals is unprovable. + +During the search, a goal or rapp can also become **irrelevant**. This means +that we don't have to visit it again. Informally, goals and rapps are irrelevant +if they are part of a branch of the search tree which has either successfully +proved its goal already or which can never prove its goal. More formally: + +- A goal is irrelevant if its parent rapp is unprovable. (This means that a + sibling of the goal is already unprovable, in which case we know that the + parent rapp will never be proved.) +- A rapp is irrelevant if its parent goal is proved. (This means that a sibling + of the rapp is already proved, and we only need one proof.) +- A goal or rapp is irrelevant if any of its ancestors is irrelevant. + +### Rule Builders + +A **rule builder** is a metaprogram that turns a declaration or hypothesis into +an Aesop rule. Currently available builders are: + +- **`apply`**: generates a rule which tries to apply the given declaration or + hypothesis `x` to the target. The rule acts like the tactic `apply x`. +- **`forward`**: when applied to a declaration or hypothesis of type `A₁ → ... + Aₙ → B`, generates a rule which looks for hypotheses `h₁ : A₁`, ..., `hₙ : Aₙ` + in the goal and, if they are found, adds a new hypothesis `h : B`. As an + example, consider the lemma `even_or_odd`: + + ```lean + even_or_odd : ∀ (n : Nat), Even n ∨ Odd n + ``` + + Registering this as a forward rule will cause the goal + + ```lean + n : Nat + m : Nat + ⊢ T + ``` + + to be transformed into this: + + ```lean + n : Nat + hn : Even n ∨ Odd n + m : Nat + hm : Even m ∨ Odd m + ⊢ T + ``` + + The forward builder may also be given a list of *immediate names*: + + ``` + (forward (immediate := [n])) even_or_odd + ``` + + The immediate names, here `n`, refer to the arguments of `even_or_odd`. When + Aesop applies a forward rule with explicit immediate names, it only matches + the corresponding arguments to hypotheses. (Here, `even_or_odd` has only one + argument, so there is no difference.) + + When no immediate names are given, Aesop considers every argument immediate, + except for instance arguments and dependent arguments (i.e. those that can be + inferred from the types of later arguments). + + When a forward rule is successful, Aesop remembers the type of the hypothesis + added by the rule, say `T`. If a forward rule (possibly the same one) is + subsequently applied to a subgoal and wants to add another hypothesis of type + `T`, this is forbidden and the rule fails. Without this restriction, forward + rules would in many cases be applied infinitely often. However, note that the + rule is still executed on its own subgoals (and their subgoals, etc.), which + can become a performance issue. You should therefore prefer `destruct` rules + where possible. +- **`destruct`**: works like `forward`, but after the rule has been applied, + hypotheses that were used as immediate arguments are cleared. This is useful + when you want to eliminate a hypothesis. E.g. the rule + ``` + @[aesop norm destruct] + theorem and_elim_right : α ∧ β → α := ... + ``` + will cause the goal + ``` + h₁ : (α ∧ β) ∧ γ + h₂ : δ ∧ ε + ``` + to be transformed into + ``` + h₁ : α + h₂ : δ + ``` + + Unlike with `forward` rules, when an `destruct` rule is successfully applied, + it may be applied again to the resulting subgoals (and their subgoals, etc.). + There is less danger of infinite cycles because the original hypothesis is + cleared. + + However, if the hypothesis or hypotheses to which the `destruct` rule is + applied have dependencies, they are not cleared. In this case, you'll probably + get an infinite cycle. (TODO fix this.) +- **`constructors`**: when applied to an inductive type or structure `T`, + generates a rule which tries to apply each constructor of `T` to the target. + This is a multi-rule, so if multiple constructors apply, they are considered + in parallel. If you use this constructor to build an unsafe rule, each + constructor application receives the same success probability; if this is not + what you want, add separate `apply` rules for the constructors. +- **`cases`**: when applied to an inductive type or structure `T`, generates a + rule that performs case analysis on every hypothesis `h : T` in the context. + The rule recurses into subgoals, so `cases Or` will generate 6 goals when + applied to a goal with hypotheses `h₁ : A ∨ B ∨ C` and `h₂ : D ∨ E`. However, + if `T` is a recursive type (e.g. `List`), we only perform case analysis once + on each hypothesis. Otherwise we would loop infinitely. + + The `patterns` option can be used to apply the rule only on hypotheses of a + certain shape. E.g. the rule `(cases (patterns := [Fin 0])) Fin` will perform + case analysis only on hypotheses of type `Fin 0`. Patterns can contain + underscores, e.g. `0 ≤ _`. Multiple patterns can be given (separated by + commas); the rule is then applied whenever at least one of the patterns + matches a hypothesis. +- **`simp`**: when applied to an equation `eq : A₁ → ... Aₙ → x = y`, registers + `eq` as a simp lemma for the built-in simp pass during normalisation. As such, + this builder can only build normalisation rules. +- **`unfold`**: when applied to a definition or `let` hypothesis `f`, registers + `f` to be unfolded (i.e. replaced with its definition) during normalisation. + As such, this builder can only build normalisation rules. The unfolding + happens in a separate `simp` pass. + + The `simp` builder can also be used to unfold definitions. The difference is + that `simp` rules perform smart unfolding (like the `simp` tactic) and + `unfold` rules perform non-smart unfolding (like the `unfold` tactic). + Non-smart unfolding unfolds functions even when none of their equations + match, so `unfold` rules for recursive functions generally lead to looping. +- **`tactic`**: takes a tactic and directly turns it into a rule. The given + declaration (the builder does not work for hypotheses) must have type `TacticM + Unit`, `Aesop.SimpleRuleTac` or `Aesop.RuleTac`. The latter are Aesop data + types which associate a tactic with additional metadata; using them may allow + the rule to operate somewhat more efficiently. + + The builder may be given an option `uses_branch_state := ` (default + true). This indicates whether the given tactic uses the branch state; see + below. + + Rule tactics should not be 'no-ops': if a rule tactic is not applicable to a + goal, it should fail rather than return the goal unchanged. All no-op rules + waste time and no-op `norm` rules will send normalisation into an infinite + loop. + + Normalisation rules may not assign metavariables (other than the goal + metavariable) or introduce new metavariables (other than the new goal + metavariable). This can be a problem because some Lean tactics, e.g. `cases`, + do so even in cases where you probably would not expect them to. I'm afraid + there is currently no good solution for this. +- **`default`**: The default builder. This is the builder used when you + register a rule without specifying a builder, but you can also use it + explicitly. Depending on the rule's phase, the default builder tries + different builders, using the first one that works. These builders are: + - For `safe` and `unsafe` rules: `constructors`, `tactic`, `apply`. + - For `norm` rules: `constructors`, `tactic`, `simp`, `apply`. + +#### Transparency Options + +The rule builders `apply`, `forward`, `destruct`, `constructors` and `cases` +each have a `transparency` option. This option controls the transparency at +which the rule is executed. For example, registering a rule with the builder +`(apply (transparency := reducible))` makes the rule act like the tactic +`with_reducible apply`. + +However, even if you change the transparency of a rule, it is still indexed at +`reducible` transparency (since the data structure we use for indexing only +supports `reducible` transparency). So suppose you register an `apply` rule with +`default` transparency. Further suppose the rule concludes `A ∧ B` and your +target is `T` with `def T := A ∧ B`. Then the rule could apply to the target +since it can unfold `T` at `default` transparency to discover `A ∧ B`. However, +the rule is never applied because the indexing procedure sees only `T` and does +not consider the rule potentially applicable. + +To override this behaviour, you can write `(apply (transparency! := default))` +(note the bang). This disables indexing, so the rule is tried on every goal. + +### Rule Sets + +Rule sets are declared with the command + +``` lean +declare_aesop_rule_sets [r₁, ..., rₙ] +``` + +where the `rᵢ` are arbitrary names. To avoid clashes, pick names in the +namespace of your package. + +Within a rule set, rules are identified by their name, builder and phase +(safe/unsafe/norm). This means you can add the same declaration as multiple +rules with different builders or in different phases, but not with different +priorities or different builder options (if the rule's builder has any options). + +Rules can appear in multiple rule sets, but in this case you should make sure +that they have the same priority and use the same builder options. Otherwise, +Aesop will consider these rules the same and arbitrarily pick one. + +By default, the `aesop` tactic uses the `builtin` and `default` rule sets. The +`builtin` set contains built-in rules for handling various constructions (see +below). The `default` set contains rules which were added by Aesop users without +specifying a rule set. + +### The `@[aesop]` Attribute + +Declarations can be added to rule sets by annotating them with the `@[aesop]` +attribute. + +#### Single Rule + +In most cases, you'll want to add one rule for the declaration. The syntax for +this is + +``` lean +@[aesop ? ? ? ?] +``` + +where + +- `` is `safe`, `norm` or `unsafe`. Cannot be omitted except under the + conditions in the next bullets. + +- `` is: + - For `simp` rules, a natural number. This is used as the priority of the + `simp` generated `simp` lemmas, so registering a `simp` rule with priority + `n` is roughly equivalent to the attribute `@[simp n]`. If omitted, defaults + to Lean's default `simp` priority. + - For `safe` and `norm` rules (except `simp` rules), an integer penalty. If + omitted, defaults to 1. + - For `unsafe` rules, a percentage between 0% and 100%. Cannot be omitted. + You may omit the `unsafe` phase specification when giving a percentage. + - For `unfold` rules, a penalty can be given, but it is currently ignored. + +- `` is one of the builders given above. If you want to pass options to + a builder, write it like this (with mandatory parentheses): + + ```text + (tactic (uses_branch_state := true)) + ``` + + If no builder is specified, the default builder for the given phase is used. + Since the `simp` builder generates only normalisation rules, the `norm` phase + may be omitted. + +- `` is a clause of the form + + ```text + (rule_sets [r₁, ..., rₙ]) + ``` + + where the `rᵢ` are declared rule sets. (Parentheses are mandatory.) The rule + is added exactly to the specified rule sets. If this clause is omitted, it + defaults to `(rule_sets [default])`. + +#### Multiple Rules + +It is occasionally useful to add multiple rules for a single declaration, e.g. +a `cases` and a `constructors` rule for the same inductive type. In this case, +you can write for example + +``` lean +@[aesop unsafe [constructors 75%, cases 90%]] +inductive T ... + +@[aesop apply [safe (rule_sets [A]), 70% (rule_sets [B])]] +def foo ... + +@[aesop [80% apply, safe 5 (forward (immediate := x))]] +def bar (x : T) ... +``` + +In the first example, two unsafe rules for `T` are registered, one with success +probability 75% and one with 90%. + +In the second example, two rules are registered for `foo`. Both use the `apply` +builder. The first, a `safe` rule with default penalty, is added to rule set +`A`. The second, an `unsafe` rule with 70% success probability, is added to +rule set `B`. + +In the third example, two rules are registered for `bar`: an `unsafe` rule with +80% success probability using the `apply` builder and a `safe` rule with penalty +5 using the `forward` builder. + +In general, the grammar for the `@[aesop]` attribute is + +``` lean +attr ::= @[aesop ] + | @[aesop []] + +rule_expr ::= feature + | feature + | feature [] +``` + +where `feature` is a phase, priority, builder or `rule_sets` clause. This +grammar yields one or more trees of features and each branch of these trees +specifies one rule. (A branch is a list of features.) + +### Adding External Rules + +You can use the `attribute` command to add rules for constants which were +declared previously, either in your own development or in a package you import: + +``` +attribute [aesop norm unfold] List.all -- List.all is from Init +``` + +### Erasing Rules + +There are two ways to erase rules. Usually it suffices to remove the `@[aesop]` +attribute: + +``` lean +attribute [-aesop] foo +``` + +This will remove all rules associated with the declaration `foo` from all rule +sets. However, this erasing is not persistent, so the rule will reappear at the +end of the file. This is a fundamental limitation of Lean's attribute system: +once a declaration is tagged with an attribute, it cannot be permanently +untagged. + +If you want to remove only certain rules, you can use the `erase_aesop_rules` +command: + +``` lean +erase_aesop_rules [safe apply foo, bar (rule_sets [A])] +``` + +This will remove: + +- all safe rules for `foo` with the `apply` builder from all rule sets (but not +other, for example, unsafe rules or `forward` rules); +- all rules for `bar` from rule set `A`. + +In general, the syntax is + +``` lean +erase_aesop_rules [] +``` + +i.e. rules are specified in the same way as for the `@[aesop]` attribute. +However, each rule must also specify the name of the declaration whose rules +should be erased. The `rule_expr` grammar is therefore extended such that a +`feature` can also be the name of a declaration. + +Note that a rule added with one of the default builders (`safe_default`, +`norm_default`, `unsafe_default`) will be registered under the name of the +builder that is ultimately used, e.g. `apply` or `simp`. So if you want to erase +such a rule, you may have to specify that builder instead of the default +builder. + +### The `aesop` Tactic + +In its most basic form, you can call the Aesop tactic just by writing + +``` lean +example : α → α := by + aesop +``` + +This will use the rules in the `default` rule set (i.e. those added via the +attribute with no explicit rule set specified) and the rules in the `builtin` +rule set (i.e. those provided by Aesop itself). + +The tactic's behaviour can also be customised with various options. A more +involved Aesop call might look like this: + +``` text +aesop + (add safe foo, 10% cases Or, safe cases Empty) + (erase A, baz) + (rule_sets [A, B]) + (options := { maxRuleApplicationDepth := 10 }) +``` + +Here we add some rules with an `add` clause, erase other rules with an `erase` +clause, limit the used rule sets and set some options. Each of these clauses +is discussed in more detail below. + +#### Adding Rules to an Aesop Call + +Rules can be added to an Aesop call with an `add` clause. This won't affect any +declared rule sets. The syntax of the `add` clause is + +``` text +(add ) +``` + +i.e. rules can be specified in the same way as for the `@[aesop]` attribute. +As with the `erase_aesop_rules` command, each rule must specify the name of +declaration from which the rule should be built; for example + +``` text +(add safe [foo 1, bar 5]) +``` + +will add the declaration `foo` as a safe rule with penalty 1 and `bar` as a safe +rule with penalty 5. + +The rule names can also refer to hypotheses in the goal context, but not all +builders support this. + +#### Erasing Rules From an Aesop Call + +Rules can be removed from an Aesop call with an `erase` clause. Again, this +affects only the current Aesop call and not the declared rule sets. The syntax +of the `erase` clause is + +``` text +(erase ) +``` + +and it works exactly like the `erase_aesop_rules` command. To erase all rules +associated with `x` and `y`, write + +``` lean +(erase x, y) +``` + +#### Selecting Rule Sets + +By default, Aesop uses the `default` and `builtin` rule sets. A `rule_sets` +clause can be given to include additional rule sets, e.g. + +``` text +(rule_sets [A, B]) +``` + +This will use rule sets `A`, `B`, `default` and `builtin`. Rule sets can also +be disabled with `rule_sets [-default, -builtin]`. + +#### Setting Options + +Various options can be set with an `options` clause, whose syntax is: + +``` text +(options := ) +``` + +The term is an arbitrary Lean expression of type `Aesop.Options`; see there for +details. A notable option is `strategy`, which is one of `.bestFirst`, +`.depthFirst` and `.breadthFirst` and instructs Aesop to use the corresponding +search strategy. Best-first is the default. + +Similarly, options for the built-in norm simp call can be set with + +``` text +(simp_options := ) +``` + +The term has type `Aesop.SimpConfig`; see there for details. The `useHyps` +option may be particularly useful: when `true` (the default), norm simp behaves +like the `simp_all` tactic; when `false`, norm simp behaves like `simp at *`. + +### Built-In Rules + +The set of built-in rules (those in the `builtin` rule set) is currently quite +unstable, so for now I won't document them in detail. See +`Aesop/BuiltinRules.lean` and `Aesop/BuiltinRules/*.lean` + +### Proof Scripts + +By calling `aesop?` instead of `aesop`, you can instruct Aesop to generate a +tactic script which proves the goal (if Aesop succeeds). The script is printed +as a `Try this:` suggestion, similar to `simp?`. + +The scripts generated by Aesop are currently a bit idiosyncratic. For example, +they may contain the `aesop_cases` tactic, which is a slight variation of the +standard `cases`. Additionally, Aesop occasionally generates buggy scripts which +do not solve the goal. We hope to eventually fix these issues; until then, you +may have to lightly adjust the proof scripts by hand. + +### Tracing + +To see how Aesop proves a goal -- or why it doesn't prove a goal, or why it's +slow to prove a goal -- it is useful to see what it's doing. To that end, you +can enable various tracing options. These use the usual syntax, e.g. + +``` lean +set_option trace.aesop true +``` + +The main options are: + +- `trace.aesop`: print a step-by-step log of which goals Aesop tried to + solve, which rules it tried to apply (successfully or unsuccessfully), etc. +- `trace.aesop.ruleSet`: print the rule set used for an Aesop call. +- `trace.aesop.proof`: if Aesop is successful, print the proof that was + generated (as a Lean term). You should be able to copy-and-paste this proof + to replace Aesop. + +### Profiling + +To get an idea of where Aesop spends its time, use + +``` lean +set_option trace.aesop.profile true +``` + +Aesop then prints a summary of how much time its various tasks took. + +To get a more fine-grained picture, enable the `trace.aesop` and `profiler` +options. The trace is then augmented with information about how much time each +step took. Note that only the timing information pertaining to goal expansions +and rule applications is relevant. Other timings, such as those attached to new +rapps and goals, are just artefacts of the Lean tracing API. + +### Checking Internal Invariants + +If you encounter behaviour that looks like an internal error in Aesop, it may +help to set the option `aesop.check.all` (or the more fine-grained +`aesop.check.*` options). This makes Aesop check various invariants while the +tactic is running. These checks are somewhat expensive, so remember to unset the +option after you've reported the bug. + +### Handling Metavariables + +Rules which create metavariables must be handled specially by Aesop. For +example, suppose we register transitivity of `<` as an Aesop rule. Then we may +get a goal state of this form: + +``` lean +n k : Nat +⊢ n < ?m + +n k : Nat +⊢ ?m < k +``` + +We may now solve the first goal by applying different rules. We could, for +example, apply the theorem `∀ n, n < n + 1`. We could also use an assumption `n +< a`. Both proofs close the first goal, but crucially, they modify the second +goal: in the first case, it becomes `n + 1 < k`; in the second case, `a < k`. +And of course one of these could be provable while the other is not. In other +words, the second subgoal now depends on the *proof* of the first subgoal +(whereas usually we don't care *how* a goal was proven, only *that* it was +proven). Aesop could also decide to work on the second subgoal first, in which +case the situation is symmetric. + +Due to this dependency, Aesop in effect treats the instantiations of the second +subgoal as *additional goals*. Thus, when we apply the theorem `∀ n, n < n + 1`, +which closes the first goal, Aesop realises that because this theorem was +applied, we must now prove `n + 1 < k` as well. So it adds this goal as an +additional subgoal of the rule application `∀ n, n < n + 1` (which otherwise +would not have any subgoals). Similarly, when the assumption `n < a` is applied, +its rule application gains an additional subgoal `a < k`. + +This mechanism makes sure that we consider all potential proofs. The downside is +that it's quite explosive: when there are multiple metavariables in multiple +goals, which Aesop may visit in any order, Aesop may spend a lot of time copying +goals with shared metavariables. It may even try to prove the same goal more +than once since different rules may yield the same metavariable instantiations. +For these reasons, rules which create metavariables are best kept out of the +global rule set and added to individual Aesop calls on an ad-hoc basis. + +It is also worth noting that when a safe rule assigns a metavariable, it is +treated as an unsafe rule (with success probability 90%). This is because +assigning metavariables is almost never safe, for the same reason as above: the +usually perfectly safe rule `∀ n, n < n + 1` would, if treated as safe, force us +to commit to one particular instantiation of the metavariable `?m`. + +For more details on the handling of metavariables, see the [Aesop +paper](https://zenodo.org/record/7430233). From 2cdbed4a375b93d8f0087b681b847d9186f6d3f3 Mon Sep 17 00:00:00 2001 From: Peiyang-Song Date: Sat, 23 Sep 2023 15:30:41 -0700 Subject: [PATCH 09/31] Add build check example --- .gitignore | 4 +--- Aesop/Builder/Neural.lean | 2 -- AesopTest/NeuralCheck.lean | 29 +++++++++++++++++++++++++++++ AesopTest/NeuralProver.lean | 24 ++++-------------------- 4 files changed, 34 insertions(+), 25 deletions(-) create mode 100644 AesopTest/NeuralCheck.lean diff --git a/.gitignore b/.gitignore index 80f90be6..44229892 100644 --- a/.gitignore +++ b/.gitignore @@ -1,5 +1,3 @@ /build/ /tests/*.produced -/lake-packages - -onnx-leandojo-lean4-tacgen-byt5-small/ \ No newline at end of file +/lake-packages \ No newline at end of file diff --git a/Aesop/Builder/Neural.lean b/Aesop/Builder/Neural.lean index 3881029c..dcf9f488 100644 --- a/Aesop/Builder/Neural.lean +++ b/Aesop/Builder/Neural.lean @@ -33,8 +33,6 @@ instance : Inhabited NeuralBuilderOptions where def RuleBuilder.neural (opts : NeuralBuilderOptions) : RuleBuilder := λ input => match input.kind with | RuleBuilderKind.global _ => do - -- let tac := .neuralProvers opts.neuralProver opts.numReturnSequences - -- opts.maxLength opts.temperature opts.numBeams let tac := .neuralProvers opts.neuralProver opts.transparency RuleBuilderOutput.global <$> mkResult tac | RuleBuilderKind.local _ _ => diff --git a/AesopTest/NeuralCheck.lean b/AesopTest/NeuralCheck.lean new file mode 100644 index 00000000..5f21d056 --- /dev/null +++ b/AesopTest/NeuralCheck.lean @@ -0,0 +1,29 @@ +import Aesop + +set_option aesop.check.all true + +section buildCheck + +/- [1/2] Check aesop. + Write a simple theorem and try to prove it `by aesop`. + If the goal is closed (i.e., No goals displayed in the InfoView), + aesop is likely to have been properly built. + Additionally, you may try to type `aesop?` to see scripts suggested by aesop. +-/ +theorem foo1 (a : Nat) : a + 1 = Nat.succ a := by + aesop + -- aesop? + +/- [2/2] Check LeanInfer. + Write a simple theorem and try to prove it `by LeanInfer`. + If a list of tactics is shown under `Tactic suggestions` in the InfoView + while the goal is not closed, the LeanInfer part is successfully built as well. + For the first time, should it ask you to download the model by running `suggest_tactics!`, + following it will automatically download the model to `~/.cache/lean_infer/` by default, + with the path overridable by setting the `LEAN_INFER_CACHE_DIR` environment variable. +-/ +theorem foo2 (a b c : Nat) : a + b + c = a + c + b := by + suggest_tactics + -- suggest_tactics! + +end buildCheck diff --git a/AesopTest/NeuralProver.lean b/AesopTest/NeuralProver.lean index 6277d60d..a419e70b 100644 --- a/AesopTest/NeuralProver.lean +++ b/AesopTest/NeuralProver.lean @@ -1,32 +1,16 @@ import Aesop --- import LeanInfer --- When we can use LeanInfer without importing it, this means the --- LeanInfer module successfully got integrated into the aesop dependency graph. set_option aesop.check.all true -open Lean Lean.Meta Lean.Elab.Tactic - section simpleTest structure neuralConfig where - model_name : String + neuralProver : String -@[aesop unsafe neural] -def conf : neuralConfig := { model_name := "onnx-leandojo-lean4-tacgen-byt5-small" } +@[aesop unsafe 50% neural] +def conf : neuralConfig := { neuralProver := "onnx-leandojo-lean4-tacgen-byt5-small" } theorem foo (a: Nat) : a + 1 = Nat.succ a := by aesop - -- aesop alone should be able to prove this simple theorem. - - -- aesop? - -- aesop? should be able to suggest tactics to the user, - -- displayed in the InfoView as LeanInfer does. - -- suggest_tactics - -- aesop should also be able to call LeanInfer to suggest tactics - -- as LeanInfer is already added into the loop. - - -- rfl - -- sorry - -- both closes the proof either in a safe/unsafe way. \ No newline at end of file +end simpleTest From 1804f211fb9c635a41cdc99feed37da0d7966dda Mon Sep 17 00:00:00 2001 From: Peiyang Song Date: Mon, 25 Sep 2023 08:05:06 -0700 Subject: [PATCH 10/31] Link update --- README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/README.md b/README.md index a642328e..c4459d4d 100644 --- a/README.md +++ b/README.md @@ -14,7 +14,7 @@ This tool is in its alpha stage and we are actively working to further enhance i A direct `lake build` in this directory should suffice. -To quickly test its success, write a simple theorem and try to prove it `by aesop`. If the goal is closed (i.e., `No goals` displayed in the InfoView), `aesop` is likely to have been properly built. Then replace `by aesop` with `by suggest_tactics`. If a list of tactics is shown under `Tactic suggestions` in the InfoView while the goal is not closed, the LeanInfer part is successfully built as well. For the first time, should it ask you to download the model by running `suggest_tactics!`, following it will automatically download the model to `~/.cache/lean_infer/` by default, with the path overridable by setting the `LEAN_INFER_CACHE_DIR` environment variable. A simple guide of this testing process is available [here](./AesopTest/NeuralProver.lean) as well. +To quickly test its success, write a simple theorem and try to prove it `by aesop`. If the goal is closed (i.e., `No goals` displayed in the InfoView), `aesop` is likely to have been properly built. Then replace `by aesop` with `by suggest_tactics`. If a list of tactics is shown under `Tactic suggestions` in the InfoView while the goal is not closed, the LeanInfer part is successfully built as well. For the first time, should it ask you to download the model by running `suggest_tactics!`, following it will automatically download the model to `~/.cache/lean_infer/` by default, with the path overridable by setting the `LEAN_INFER_CACHE_DIR` environment variable. A simple guide of this testing process is available [here](./AesopTest/NeuralCheck.lean) as well. ## Usage From 2671f5e80d290f388843a7ed95c2a9fb5a41b226 Mon Sep 17 00:00:00 2001 From: Peiyang-Song Date: Wed, 27 Sep 2023 15:15:13 -0700 Subject: [PATCH 11/31] Add exception handling and fix specific-tactic bug --- Aesop/RuleTac/Neural.lean | 35 +++++++++++++++++++---------------- AesopTest/NeuralProver.lean | 24 ++++++++++++++++++++++-- 2 files changed, 41 insertions(+), 18 deletions(-) diff --git a/Aesop/RuleTac/Neural.lean b/Aesop/RuleTac/Neural.lean index 0bcb985d..e695bf25 100644 --- a/Aesop/RuleTac/Neural.lean +++ b/Aesop/RuleTac/Neural.lean @@ -10,7 +10,7 @@ namespace Aesop.RuleTac -- applies, a rule application is returned. If none applies, the tactic fails. def applyNeural (model: String) (md : TransparencyMode) : RuleTac := λ input => do let initialState ← saveState - let generateScript := input.options.generateScript + -- let generateScript := input.options.generateScript if model == "onnx-leandojo-lean4-tacgen-byt5-small" then let iptGoal ← LeanInfer.ppTacticState [input.goal] let optSuggestions ← LeanInfer.generate iptGoal @@ -19,21 +19,24 @@ def applyNeural (model: String) (md : TransparencyMode) : RuleTac := λ input => match Parser.runParserCategory (← getEnv) `tactic tacticStr (fileName := "") with | .error _ => return none | .ok stx => - initialState.restore - let tac := evalTactic stx - let tstx : TSyntax `tactic := {raw := stx} - let goals ← run input.goal tac |>.run' - let scriptBuilder? := - mkScriptBuilder? generateScript $ - .ofTactic goals.toArray.size do - withAllTransparencySyntax md tstx - let postState ← saveState - let thisApp : RuleApplication := { - postState := postState - goals := goals.toArray - scriptBuilder? := scriptBuilder? - } - return thisApp + try + initialState.restore + let tac := evalTactic stx + -- let tstx : TSyntax `tactic := {raw := stx} + let goals ← run input.goal tac |>.run' + -- let scriptBuilder? := + -- mkScriptBuilder? generateScript $ + -- .ofTactic goals.toArray.size do + -- withAllTransparencySyntax md tstx + let postState ← saveState + let thisApp : RuleApplication := { + postState := postState + goals := goals.toArray + -- scriptBuilder? := scriptBuilder? + scriptBuilder? := none + } + return thisApp + catch _ => pure none restoreState initialState if apps.isEmpty then throwError "failed to apply any tactics generated by {model}" diff --git a/AesopTest/NeuralProver.lean b/AesopTest/NeuralProver.lean index a419e70b..57e04144 100644 --- a/AesopTest/NeuralProver.lean +++ b/AesopTest/NeuralProver.lean @@ -1,6 +1,9 @@ import Aesop -set_option aesop.check.all true +-- set_option aesop.check.all true +-- set_option trace.aesop.tree true +-- set_option trace.aesop true +-- all three flags are for debugging purpose, not necessarily needed. section simpleTest @@ -10,7 +13,24 @@ structure neuralConfig where @[aesop unsafe 50% neural] def conf : neuralConfig := { neuralProver := "onnx-leandojo-lean4-tacgen-byt5-small" } -theorem foo (a: Nat) : a + 1 = Nat.succ a := by +/- [1/2] Simple theorem. + The raw white-box aesop should be able to prove this theorem. + Since we mark the neural prover as `unsafe`, when the `safe` builtin rules of aesop + can already prove the goal, our additional option of `neural` will never be called. + In other words, the theorems that can be proved by the original `aesop` + is a strict subset of that can be proved by our `LLM-aesop`. -/ +theorem foo1 (a: Nat) : a + 1 = Nat.succ a := by + aesop + +/- [2/2] Hard theorem. + The raw white-box `aesop` should not be able to prove this theorem. + After trying all builtin rules, which should all fail on this theorem, + the original `aesop` will fail to close this goal, + while our `LLM-aesop` will try the `unsafe` neural prover, + which can usually prove the goal. + Note that this is not guaranteed for each time you run `LLM-aesop`, + as there is existing uncertainty rooted in any machine learning method. -/ +theorem foo2 (a b c : Nat) : a + b + c = c + b + a := by aesop end simpleTest From abe4b7b79baa4780bbb7e668f616326532e37e04 Mon Sep 17 00:00:00 2001 From: Peiyang-Song Date: Wed, 27 Sep 2023 16:47:15 -0700 Subject: [PATCH 12/31] Rename package --- lakefile.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lakefile.lean b/lakefile.lean index d7a3df8d..c6021824 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -2,7 +2,7 @@ import Lake open Lake DSL -package aesop { +package llmaesop { precompileModules := false -- breaks mathlib cache moreLinkArgs := #["-L./lake-packages/LeanInfer/build/lib", "-lonnxruntime", "-lstdc++"] } From 2e9134f1720b03be66cdab515dba467e04b5a809 Mon Sep 17 00:00:00 2001 From: Peiyang-Song Date: Wed, 27 Sep 2023 18:05:23 -0700 Subject: [PATCH 13/31] Remove or suggested by the model: fake proofs --- Aesop/RuleTac/Neural.lean | 2 ++ 1 file changed, 2 insertions(+) diff --git a/Aesop/RuleTac/Neural.lean b/Aesop/RuleTac/Neural.lean index e695bf25..53c59308 100644 --- a/Aesop/RuleTac/Neural.lean +++ b/Aesop/RuleTac/Neural.lean @@ -16,6 +16,8 @@ def applyNeural (model: String) (md : TransparencyMode) : RuleTac := λ input => let optSuggestions ← LeanInfer.generate iptGoal let suggestions := optSuggestions.map (·.1) let apps ← suggestions.filterMapM λ tacticStr => do + if tacticStr == "sorry" then return none + if tacticStr == "admit" then return none match Parser.runParserCategory (← getEnv) `tactic tacticStr (fileName := "") with | .error _ => return none | .ok stx => From 1ef6a4ae2ccf38ad1c443dd5c91345f5ab6b7741 Mon Sep 17 00:00:00 2001 From: Peiyang-Song Date: Wed, 27 Sep 2023 20:27:10 -0700 Subject: [PATCH 14/31] Detect when part of tactic is sorry or admit --- Aesop/RuleTac/Neural.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Aesop/RuleTac/Neural.lean b/Aesop/RuleTac/Neural.lean index 53c59308..a7f48886 100644 --- a/Aesop/RuleTac/Neural.lean +++ b/Aesop/RuleTac/Neural.lean @@ -16,8 +16,8 @@ def applyNeural (model: String) (md : TransparencyMode) : RuleTac := λ input => let optSuggestions ← LeanInfer.generate iptGoal let suggestions := optSuggestions.map (·.1) let apps ← suggestions.filterMapM λ tacticStr => do - if tacticStr == "sorry" then return none - if tacticStr == "admit" then return none + if tacticStr.containsSubstr "sorry" then return none + if tacticStr.containsSubstr "admit" then return none match Parser.runParserCategory (← getEnv) `tactic tacticStr (fileName := "") with | .error _ => return none | .ok stx => From 100fcd3f829d78ef12fd690d6fcec46ceff4d0c5 Mon Sep 17 00:00:00 2001 From: Peiyang-Song Date: Wed, 27 Sep 2023 21:14:36 -0700 Subject: [PATCH 15/31] Increase number of candidate sequences to 64 --- 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 10ba4aa0..234d5d67 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -4,10 +4,10 @@ [{"git": {"url": "https://github.com/lean-dojo/LeanInfer.git", "subDir?": null, - "rev": "6b4211f30e0bdcd070fd6ca3d0c163693aeca909", + "rev": "ca2b011b6fc564740b6d1170ea1bb5d307eb81d5", "opts": {}, "name": "LeanInfer", - "inputRev?": "v0.0.7", + "inputRev?": "peiyang-dev", "inherited": false}}, {"git": {"url": "https://github.com/leanprover/std4", diff --git a/lakefile.lean b/lakefile.lean index c6021824..2f5aaac0 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -15,4 +15,4 @@ lean_lib AesopTest { } require std from git "https://github.com/leanprover/std4" @ "main" -require LeanInfer from git "https://github.com/lean-dojo/LeanInfer.git" @ "v0.0.7" \ No newline at end of file +require LeanInfer from git "https://github.com/lean-dojo/LeanInfer.git" @ "peiyang-dev" \ No newline at end of file From de4d756fb5f4c0876ebd1fcfd8ffef03316e742f Mon Sep 17 00:00:00 2001 From: Peiyang Song Date: Wed, 27 Sep 2023 21:16:54 -0700 Subject: [PATCH 16/31] Add reminder of LeanInfer cloud build not working --- README.md | 1 + 1 file changed, 1 insertion(+) diff --git a/README.md b/README.md index c4459d4d..294ee13a 100644 --- a/README.md +++ b/README.md @@ -1,3 +1,4 @@ +# [Temporarily disable LeanInfer cloud build] # Aesop-LeanInfer Aesop-LeanInfer is an enhanced version of [Aesop](https://github.com/JLimperg/aesop) (Automated Extensible Search for Obvious Proofs), a proof search tactic for Lean 4 similar to Isabelle's `auto`. In addition to the original Aesop, this version adds a new `RuleBuilder` and its corresponding `RuleTac`, which together enable fast plugin of machine learning models to assist with the proof search process, by seamlessly incorporating [LeanInfer](https://github.com/lean-dojo/LeanInfer)'s tactic suggestion feature into Aesop's workflow. From 002ceca4fde40d513fe76255698dd283454333d8 Mon Sep 17 00:00:00 2001 From: Kaiyu Yang Date: Wed, 27 Sep 2023 21:32:16 -0700 Subject: [PATCH 17/31] detect sorries --- Aesop/RuleTac/Neural.lean | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/Aesop/RuleTac/Neural.lean b/Aesop/RuleTac/Neural.lean index a7f48886..faa7582f 100644 --- a/Aesop/RuleTac/Neural.lean +++ b/Aesop/RuleTac/Neural.lean @@ -26,6 +26,10 @@ def applyNeural (model: String) (md : TransparencyMode) : RuleTac := λ input => let tac := evalTactic stx -- let tstx : TSyntax `tactic := {raw := stx} let goals ← run input.goal tac |>.run' + let some pf ← getExprMVarAssignment? input.goal | unreachable! + let pf ← instantiateMVars pf + if pf.hasSorry then + return none -- let scriptBuilder? := -- mkScriptBuilder? generateScript $ -- .ofTactic goals.toArray.size do From a86552eda099aff5fe895b45b42a411315c41aee Mon Sep 17 00:00:00 2001 From: Kaiyu Yang Date: Wed, 27 Sep 2023 21:45:28 -0700 Subject: [PATCH 18/31] lake update --- Aesop/RuleTac/Neural.lean | 3 +-- lake-manifest.json | 2 +- 2 files changed, 2 insertions(+), 3 deletions(-) diff --git a/Aesop/RuleTac/Neural.lean b/Aesop/RuleTac/Neural.lean index faa7582f..68d1bea6 100644 --- a/Aesop/RuleTac/Neural.lean +++ b/Aesop/RuleTac/Neural.lean @@ -27,8 +27,7 @@ def applyNeural (model: String) (md : TransparencyMode) : RuleTac := λ input => -- let tstx : TSyntax `tactic := {raw := stx} let goals ← run input.goal tac |>.run' let some pf ← getExprMVarAssignment? input.goal | unreachable! - let pf ← instantiateMVars pf - if pf.hasSorry then + if (← instantiateMVars pf) |>.hasSorry then return none -- let scriptBuilder? := -- mkScriptBuilder? generateScript $ diff --git a/lake-manifest.json b/lake-manifest.json index 10ba4aa0..a3565cc3 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -12,7 +12,7 @@ {"git": {"url": "https://github.com/leanprover/std4", "subDir?": null, - "rev": "efcb1a6fe69b57b16d370ffe36551c3d21b5a53e", + "rev": "f2df4ab8c0726fce3bafb73a5727336b0c3120ea", "opts": {}, "name": "std", "inputRev?": "main", From 1abe960dc7c516ae71105bfbf29394307311dd2b Mon Sep 17 00:00:00 2001 From: Kaiyu Yang Date: Wed, 27 Sep 2023 21:50:19 -0700 Subject: [PATCH 19/31] restore states --- Aesop/RuleTac/Neural.lean | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/Aesop/RuleTac/Neural.lean b/Aesop/RuleTac/Neural.lean index 68d1bea6..1d93bbb7 100644 --- a/Aesop/RuleTac/Neural.lean +++ b/Aesop/RuleTac/Neural.lean @@ -23,11 +23,12 @@ def applyNeural (model: String) (md : TransparencyMode) : RuleTac := λ input => | .ok stx => try initialState.restore - let tac := evalTactic stx + let tac := commitIfNoEx $ evalTactic stx -- let tstx : TSyntax `tactic := {raw := stx} let goals ← run input.goal tac |>.run' let some pf ← getExprMVarAssignment? input.goal | unreachable! if (← instantiateMVars pf) |>.hasSorry then + initialState.restore return none -- let scriptBuilder? := -- mkScriptBuilder? generateScript $ From 5ea54ad8da3186d7c003b9804b1c930593cd6e8e Mon Sep 17 00:00:00 2001 From: Kaiyu Yang Date: Wed, 27 Sep 2023 21:57:15 -0700 Subject: [PATCH 20/31] bump to leanprover/lean4:v4.2.0-rc1 --- lean-toolchain | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lean-toolchain b/lean-toolchain index f0a6d660..400394aa 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.0.0 +leanprover/lean4:v4.2.0-rc1 From 5ddb1a3ee768c13901cd325e73b9f9af19bc730d Mon Sep 17 00:00:00 2001 From: Kaiyu Yang Date: Wed, 27 Sep 2023 22:02:20 -0700 Subject: [PATCH 21/31] rollback to v4.0.0 --- lean-toolchain | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lean-toolchain b/lean-toolchain index 400394aa..f0a6d660 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.2.0-rc1 +leanprover/lean4:v4.0.0 From a25763f465f01ae222cb8b28cd3d0667228c8ef7 Mon Sep 17 00:00:00 2001 From: Peiyang-Song Date: Wed, 27 Sep 2023 22:29:49 -0700 Subject: [PATCH 22/31] Disable timeout --- Aesop/RuleTac/Neural.lean | 11 ++++++++++- AesopTest/NeuralProver.lean | 1 + 2 files changed, 11 insertions(+), 1 deletion(-) diff --git a/Aesop/RuleTac/Neural.lean b/Aesop/RuleTac/Neural.lean index a7f48886..37287d1a 100644 --- a/Aesop/RuleTac/Neural.lean +++ b/Aesop/RuleTac/Neural.lean @@ -23,9 +23,14 @@ def applyNeural (model: String) (md : TransparencyMode) : RuleTac := λ input => | .ok stx => try initialState.restore - let tac := evalTactic stx + -- let tac := evalTactic stx + let tac := commitIfNoEx $ evalTactic stx -- let tstx : TSyntax `tactic := {raw := stx} let goals ← run input.goal tac |>.run' + let some pf ← getExprMVarAssignment? input.goal | unreachable! + if (← instantiateMVars pf) |>.hasSorry then + initialState.restore + return none -- let scriptBuilder? := -- mkScriptBuilder? generateScript $ -- .ofTactic goals.toArray.size do @@ -47,3 +52,7 @@ def applyNeural (model: String) (md : TransparencyMode) : RuleTac := λ input => throwError "unknown neural network model: {model}" end RuleTac + + + + \ No newline at end of file diff --git a/AesopTest/NeuralProver.lean b/AesopTest/NeuralProver.lean index 57e04144..33e59002 100644 --- a/AesopTest/NeuralProver.lean +++ b/AesopTest/NeuralProver.lean @@ -4,6 +4,7 @@ import Aesop -- set_option trace.aesop.tree true -- set_option trace.aesop true -- all three flags are for debugging purpose, not necessarily needed. +set_option maxHeartbeats 0 -- disable timeout section simpleTest From 0dc1f4a5d1dc12b5da88d77b3f93942a848c1d3c Mon Sep 17 00:00:00 2001 From: Kaiyu Yang Date: Wed, 27 Sep 2023 22:46:41 -0700 Subject: [PATCH 23/31] minor fix --- Aesop/RuleTac/Neural.lean | 11 +++++------ 1 file changed, 5 insertions(+), 6 deletions(-) diff --git a/Aesop/RuleTac/Neural.lean b/Aesop/RuleTac/Neural.lean index 1d93bbb7..69081aec 100644 --- a/Aesop/RuleTac/Neural.lean +++ b/Aesop/RuleTac/Neural.lean @@ -16,8 +16,6 @@ def applyNeural (model: String) (md : TransparencyMode) : RuleTac := λ input => let optSuggestions ← LeanInfer.generate iptGoal let suggestions := optSuggestions.map (·.1) let apps ← suggestions.filterMapM λ tacticStr => do - if tacticStr.containsSubstr "sorry" then return none - if tacticStr.containsSubstr "admit" then return none match Parser.runParserCategory (← getEnv) `tactic tacticStr (fileName := "") with | .error _ => return none | .ok stx => @@ -26,10 +24,11 @@ def applyNeural (model: String) (md : TransparencyMode) : RuleTac := λ input => let tac := commitIfNoEx $ evalTactic stx -- let tstx : TSyntax `tactic := {raw := stx} let goals ← run input.goal tac |>.run' - let some pf ← getExprMVarAssignment? input.goal | unreachable! - if (← instantiateMVars pf) |>.hasSorry then - initialState.restore - return none + let pf? ← getExprMVarAssignment? input.goal + if pf?.isSome then + if (← instantiateMVars pf?.get!) |>.hasSorry then + initialState.restore + return none -- let scriptBuilder? := -- mkScriptBuilder? generateScript $ -- .ofTactic goals.toArray.size do From 4fb28bcb8c2b6602e976e2da6ba2ba8e76dcad7e Mon Sep 17 00:00:00 2001 From: Peiyang-Song Date: Wed, 27 Sep 2023 22:51:07 -0700 Subject: [PATCH 24/31] Minor fix to get rid of PANIC --- Aesop/RuleTac/Neural.lean | 11 +++++------ 1 file changed, 5 insertions(+), 6 deletions(-) diff --git a/Aesop/RuleTac/Neural.lean b/Aesop/RuleTac/Neural.lean index 1c9debc5..fe451347 100644 --- a/Aesop/RuleTac/Neural.lean +++ b/Aesop/RuleTac/Neural.lean @@ -16,8 +16,6 @@ def applyNeural (model: String) (md : TransparencyMode) : RuleTac := λ input => let optSuggestions ← LeanInfer.generate iptGoal let suggestions := optSuggestions.map (·.1) let apps ← suggestions.filterMapM λ tacticStr => do - if tacticStr.containsSubstr "sorry" then return none - if tacticStr.containsSubstr "admit" then return none match Parser.runParserCategory (← getEnv) `tactic tacticStr (fileName := "") with | .error _ => return none | .ok stx => @@ -26,10 +24,11 @@ def applyNeural (model: String) (md : TransparencyMode) : RuleTac := λ input => let tac := commitIfNoEx $ evalTactic stx -- let tstx : TSyntax `tactic := {raw := stx} let goals ← run input.goal tac |>.run' - let some pf ← getExprMVarAssignment? input.goal | unreachable! - if (← instantiateMVars pf) |>.hasSorry then - initialState.restore - return none + let pf? ← getExprMVarAssignment? input.goal + if pf?.isSome then + if (← instantiateMVars pf?.get!) |>.hasSorry then + initialState.restore + return none -- let scriptBuilder? := -- mkScriptBuilder? generateScript $ -- .ofTactic goals.toArray.size do From ee63cbe2faa927d7c49aa614452f71a14e75e4f5 Mon Sep 17 00:00:00 2001 From: Kaiyu Yang Date: Fri, 6 Oct 2023 18:04:56 -0500 Subject: [PATCH 25/31] simplify --- Aesop/Builder/Neural.lean | 29 +------------- Aesop/Frontend/RuleExpr.lean | 11 ++---- Aesop/RuleTac.lean | 2 +- Aesop/RuleTac/Basic.lean | 2 +- Aesop/RuleTac/Neural.lean | 75 +++++++++++++++++------------------- AesopTest/NeuralProver.lean | 4 -- lake-manifest.json | 4 +- lakefile.lean | 2 +- lean-toolchain | 2 +- 9 files changed, 47 insertions(+), 84 deletions(-) diff --git a/Aesop/Builder/Neural.lean b/Aesop/Builder/Neural.lean index dcf9f488..e434c059 100644 --- a/Aesop/Builder/Neural.lean +++ b/Aesop/Builder/Neural.lean @@ -5,35 +5,10 @@ open Lean.Meta namespace Aesop -structure NeuralBuilderOptions extends RegularBuilderOptions where - /-- The transparency used by the rule tactic. -/ - transparency : TransparencyMode - /-- The transparency used to index the rule. The rule is not indexed unless - this is `.reducible`. -/ - indexTransparency : TransparencyMode - neuralProver : String - numReturnSequences : UInt64 - maxLength : UInt64 - temperature : Float - numBeams : UInt64 - - -instance : Inhabited NeuralBuilderOptions where - default := { - toRegularBuilderOptions := default - transparency := .default - indexTransparency := .reducible - neuralProver := "onnx-leandojo-lean4-tacgen-byt5-small" - numReturnSequences := 64 - maxLength := 256 - temperature := 1.0 - numBeams := 1 - } - -def RuleBuilder.neural (opts : NeuralBuilderOptions) : RuleBuilder := λ input => +def RuleBuilder.neural (opts : RegularBuilderOptions) : RuleBuilder := λ input => match input.kind with | RuleBuilderKind.global _ => do - let tac := .neuralProvers opts.neuralProver opts.transparency + let tac := .neuralProvers RuleBuilderOutput.global <$> mkResult tac | RuleBuilderKind.local _ _ => throwError "neural rule builder does not support local hypotheses" diff --git a/Aesop/Frontend/RuleExpr.lean b/Aesop/Frontend/RuleExpr.lean index aee1f89b..25fa3def 100644 --- a/Aesop/Frontend/RuleExpr.lean +++ b/Aesop/Frontend/RuleExpr.lean @@ -355,17 +355,12 @@ def constructors : BuilderOptions ConstructorsBuilderOptions where some opts | _, _ => none -def neural : BuilderOptions NeuralBuilderOptions where +def neural : BuilderOptions RegularBuilderOptions where builderName := .regular .neural init := default add | opts, .index indexingMode? => some { opts with indexingMode? } - | opts, .transparency transparency alsoForIndex => - let opts := { opts with transparency } - if alsoForIndex then - some { opts with indexTransparency := transparency } - else - some opts + | opts, .transparency _ _ => some opts | _, _ => none end BuilderOptions @@ -388,7 +383,7 @@ inductive Builder | constructors (opts : ConstructorsBuilderOptions) | forward (opts : ForwardBuilderOptions) | cases (opts : CasesBuilderOptions) - | neural (opts: NeuralBuilderOptions) + | neural (opts: RegularBuilderOptions) | «default» deriving Inhabited diff --git a/Aesop/RuleTac.lean b/Aesop/RuleTac.lean index 8d84c7a6..03c8fcff 100644 --- a/Aesop/RuleTac.lean +++ b/Aesop/RuleTac.lean @@ -21,7 +21,7 @@ protected def run : RuleTacDescr → RuleTacInput → MetaM RuleTacOutput | applyConst decl md => RuleTac.applyConst decl md | applyFVar userName md => RuleTac.applyFVar userName md | constructors cs md => RuleTac.applyConsts cs md - | neuralProvers nps md => RuleTac.applyNeural nps md + | neuralProvers => RuleTac.applyNeural | forwardConst decl immediate clear md => RuleTac.forwardConst decl immediate clear md | forwardFVar userName immediate clear md => diff --git a/Aesop/RuleTac/Basic.lean b/Aesop/RuleTac/Basic.lean index 95b56168..5390ad55 100644 --- a/Aesop/RuleTac/Basic.lean +++ b/Aesop/RuleTac/Basic.lean @@ -106,7 +106,7 @@ inductive RuleTacDescr | applyConst (decl : Name) (md : TransparencyMode) | applyFVar (userName : Name) (md : TransparencyMode) | constructors (constructorNames : Array Name) (md : TransparencyMode) - | neuralProvers (neuralProverName : String) (md : TransparencyMode) + | neuralProvers | forwardConst (decl : Name) (immediate : UnorderedArraySet Nat) (clear : Bool) (md : TransparencyMode) | forwardFVar (userName : Name) (immediate : UnorderedArraySet Nat) diff --git a/Aesop/RuleTac/Neural.lean b/Aesop/RuleTac/Neural.lean index fe451347..c6891d98 100644 --- a/Aesop/RuleTac/Neural.lean +++ b/Aesop/RuleTac/Neural.lean @@ -8,46 +8,43 @@ namespace Aesop.RuleTac -- Tries to apply each tactic suggested by a neural network. For each one that -- applies, a rule application is returned. If none applies, the tactic fails. -def applyNeural (model: String) (md : TransparencyMode) : RuleTac := λ input => do +def applyNeural: RuleTac := λ input => do let initialState ← saveState - -- let generateScript := input.options.generateScript - if model == "onnx-leandojo-lean4-tacgen-byt5-small" then - let iptGoal ← LeanInfer.ppTacticState [input.goal] - let optSuggestions ← LeanInfer.generate iptGoal - let suggestions := optSuggestions.map (·.1) - let apps ← suggestions.filterMapM λ tacticStr => do - match Parser.runParserCategory (← getEnv) `tactic tacticStr (fileName := "") with - | .error _ => return none - | .ok stx => - try - initialState.restore - let tac := commitIfNoEx $ evalTactic stx - -- let tstx : TSyntax `tactic := {raw := stx} - let goals ← run input.goal tac |>.run' - let pf? ← getExprMVarAssignment? input.goal - if pf?.isSome then - if (← instantiateMVars pf?.get!) |>.hasSorry then - initialState.restore - return none - -- let scriptBuilder? := - -- mkScriptBuilder? generateScript $ - -- .ofTactic goals.toArray.size do - -- withAllTransparencySyntax md tstx - let postState ← saveState - let thisApp : RuleApplication := { - postState := postState - goals := goals.toArray - -- scriptBuilder? := scriptBuilder? - scriptBuilder? := none - } - return thisApp - catch _ => pure none - restoreState initialState - if apps.isEmpty then throwError - "failed to apply any tactics generated by {model}" - return ⟨apps⟩ - else - throwError "unknown neural network model: {model}" + let iptGoal ← LeanInfer.ppTacticState [input.goal] + let optSuggestions ← LeanInfer.generate iptGoal + let suggestions := optSuggestions.map (·.1) + let apps ← suggestions.filterMapM λ tacticStr => do + match Parser.runParserCategory (← getEnv) `tactic tacticStr (fileName := "") with + | .error _ => return none + | .ok stx => + try + initialState.restore + let tac := commitIfNoEx $ evalTactic stx + -- let tstx : TSyntax `tactic := {raw := stx} + let goals ← run input.goal tac |>.run' + let pf? ← getExprMVarAssignment? input.goal + if pf?.isSome then + if (← instantiateMVars pf?.get!) |>.hasSorry then + initialState.restore + return none + -- let scriptBuilder? := + -- mkScriptBuilder? generateScript $ + -- .ofTactic goals.toArray.size do + -- withAllTransparencySyntax md tstx + let postState ← saveState + let thisApp : RuleApplication := { + postState := postState + goals := goals.toArray + -- scriptBuilder? := scriptBuilder? + scriptBuilder? := none + } + return thisApp + catch _ => pure none + restoreState initialState + if apps.isEmpty then throwError + "failed to apply any tactics generated" + return ⟨apps⟩ + end RuleTac diff --git a/AesopTest/NeuralProver.lean b/AesopTest/NeuralProver.lean index 33e59002..d90a0901 100644 --- a/AesopTest/NeuralProver.lean +++ b/AesopTest/NeuralProver.lean @@ -8,11 +8,7 @@ set_option maxHeartbeats 0 -- disable timeout section simpleTest -structure neuralConfig where - neuralProver : String - @[aesop unsafe 50% neural] -def conf : neuralConfig := { neuralProver := "onnx-leandojo-lean4-tacgen-byt5-small" } /- [1/2] Simple theorem. The raw white-box aesop should be able to prove this theorem. diff --git a/lake-manifest.json b/lake-manifest.json index e55c7214..a3565cc3 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -4,10 +4,10 @@ [{"git": {"url": "https://github.com/lean-dojo/LeanInfer.git", "subDir?": null, - "rev": "ca2b011b6fc564740b6d1170ea1bb5d307eb81d5", + "rev": "6b4211f30e0bdcd070fd6ca3d0c163693aeca909", "opts": {}, "name": "LeanInfer", - "inputRev?": "peiyang-dev", + "inputRev?": "v0.0.7", "inherited": false}}, {"git": {"url": "https://github.com/leanprover/std4", diff --git a/lakefile.lean b/lakefile.lean index 2f5aaac0..c6021824 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -15,4 +15,4 @@ lean_lib AesopTest { } require std from git "https://github.com/leanprover/std4" @ "main" -require LeanInfer from git "https://github.com/lean-dojo/LeanInfer.git" @ "peiyang-dev" \ No newline at end of file +require LeanInfer from git "https://github.com/lean-dojo/LeanInfer.git" @ "v0.0.7" \ No newline at end of file diff --git a/lean-toolchain b/lean-toolchain index 400394aa..f0a6d660 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.2.0-rc1 +leanprover/lean4:v4.0.0 From f1977a49a2be87e83d8b3e0ea62c5b8efd0e3a6b Mon Sep 17 00:00:00 2001 From: Kaiyu Yang Date: Sat, 7 Oct 2023 13:40:44 -0500 Subject: [PATCH 26/31] use LLM-generated scores --- Aesop/BuiltinRules/ApplyHyps.lean | 3 ++- Aesop/BuiltinRules/Assumption.lean | 1 + Aesop/BuiltinRules/DestructProducts.lean | 2 +- Aesop/BuiltinRules/Ext.lean | 4 ++-- Aesop/BuiltinRules/Intros.lean | 2 +- Aesop/BuiltinRules/Split.lean | 4 ++-- Aesop/BuiltinRules/Subst.lean | 2 +- Aesop/RuleTac/Apply.lean | 8 ++++---- Aesop/RuleTac/Basic.lean | 7 ++++--- Aesop/RuleTac/Cases.lean | 6 +++--- Aesop/RuleTac/Forward.lean | 2 +- Aesop/RuleTac/Neural.lean | 7 ++++--- Aesop/RuleTac/Preprocess.lean | 2 +- Aesop/RuleTac/RuleApplicationWithMVarInfo.lean | 1 + Aesop/RuleTac/Tactic.lean | 2 +- Aesop/Search/Expansion.lean | 4 +++- AesopTest/NeuralProver.lean | 2 +- lake-manifest.json | 4 ++-- lakefile.lean | 4 ++-- 19 files changed, 37 insertions(+), 30 deletions(-) diff --git a/Aesop/BuiltinRules/ApplyHyps.lean b/Aesop/BuiltinRules/ApplyHyps.lean index a2cf3f09..b6528a5c 100644 --- a/Aesop/BuiltinRules/ApplyHyps.lean +++ b/Aesop/BuiltinRules/ApplyHyps.lean @@ -19,7 +19,8 @@ def applyHyp (hyp : FVarId) (goal : MVarId) (md : TransparencyMode) let scriptBuilder? := mkScriptBuilder? generateScript $ .ofTactic goals.size $ withTransparencySyntax md $ ← `(tactic| apply $(mkIdent $ ← hyp.getUserName)) - return { postState, goals, scriptBuilder? } + let probabilityModifier := 1.0 + return { postState, goals, probabilityModifier, scriptBuilder? } @[aesop unsafe 75% tactic (rule_sets [builtin])] def applyHyps : RuleTac := λ input => diff --git a/Aesop/BuiltinRules/Assumption.lean b/Aesop/BuiltinRules/Assumption.lean index e6d8ff86..c8f04b95 100644 --- a/Aesop/BuiltinRules/Assumption.lean +++ b/Aesop/BuiltinRules/Assumption.lean @@ -52,6 +52,7 @@ def assumption : RuleTac := λ input => do ← `(tactic| exact $(mkIdent ldecl.userName)) let app := { goals := #[] + probabilityModifier := 1.0 postState, scriptBuilder? } let proofHasMVar := ldecl.type.hasMVar diff --git a/Aesop/BuiltinRules/DestructProducts.lean b/Aesop/BuiltinRules/DestructProducts.lean index 65eb8069..6e9214b0 100644 --- a/Aesop/BuiltinRules/DestructProducts.lean +++ b/Aesop/BuiltinRules/DestructProducts.lean @@ -105,6 +105,6 @@ partial def destructProducts : RuleTac := RuleTac.ofSingleRuleTac λ input => do mkScriptBuilder? input.options.generateScript $ .ofTactic 1 do let tac ← withTransparencySyntax md (← `(tactic| aesop_destruct_products)) `(tactic| unhygienic $tac:tactic) - return (#[goal], scriptBuilder?) + return (#[goal], 1.0, scriptBuilder?) end Aesop.BuiltinRules diff --git a/Aesop/BuiltinRules/Ext.lean b/Aesop/BuiltinRules/Ext.lean index 982e50d1..4b565a53 100644 --- a/Aesop/BuiltinRules/Ext.lean +++ b/Aesop/BuiltinRules/Ext.lean @@ -17,11 +17,11 @@ def unhygienicExt (goal : MVarId) : MetaM (Array MVarId) := return subgoals.map (·.fst) def unhygienicExtWithScript (goal : MVarId) (generateScript : Bool) : - MetaM (Array MVarId × Option RuleTacScriptBuilder) := do + MetaM (Array MVarId × Float × Option RuleTacScriptBuilder) := do let subgoals ← unhygienicExt goal let scriptBuilder? := mkScriptBuilder? generateScript (.unhygienicExt subgoals.size) - return (subgoals, scriptBuilder?) + return (subgoals, 1.0, scriptBuilder?) @[aesop 80% (rule_sets [builtin])] def ext : RuleTac := RuleTac.ofSingleRuleTac λ input => diff --git a/Aesop/BuiltinRules/Intros.lean b/Aesop/BuiltinRules/Intros.lean index 9608690c..58433bce 100644 --- a/Aesop/BuiltinRules/Intros.lean +++ b/Aesop/BuiltinRules/Intros.lean @@ -56,6 +56,6 @@ def intros : RuleTac := RuleTac.ofSingleRuleTac λ input => do else pure none - return (#[goal], scriptBuilder?) + return (#[goal], 1.0, scriptBuilder?) end Aesop.BuiltinRules diff --git a/Aesop/BuiltinRules/Split.lean b/Aesop/BuiltinRules/Split.lean index 19ed4094..d48cd05c 100644 --- a/Aesop/BuiltinRules/Split.lean +++ b/Aesop/BuiltinRules/Split.lean @@ -19,7 +19,7 @@ def splitTarget : RuleTac := RuleTac.ofSingleRuleTac λ input => do let scriptBuilder? := mkScriptBuilder? input.options.generateScript $ .ofTactic goals.size `(tactic| split) - return (goals, scriptBuilder?) + return (goals, 1.0, scriptBuilder?) def splitFirstHypothesis (goal : MVarId) : MetaM (Option (Array MVarId)) := goal.withContext do @@ -44,6 +44,6 @@ def splitHypotheses : RuleTac := RuleTac.ofSingleRuleTac λ input => do let scriptBuilder? := mkScriptBuilder? input.options.generateScript $ .ofTactic goals.size `(tactic| aesop_split_hyps) - return (goals, scriptBuilder?) + return (goals, 1.0, scriptBuilder?) end Aesop.BuiltinRules diff --git a/Aesop/BuiltinRules/Subst.lean b/Aesop/BuiltinRules/Subst.lean index 2bdfc0ba..a255446e 100644 --- a/Aesop/BuiltinRules/Subst.lean +++ b/Aesop/BuiltinRules/Subst.lean @@ -97,6 +97,6 @@ def subst : RuleTac := RuleTac.ofSingleRuleTac λ input => else `(tactic| aesop_subst [ $substitutedUserNames:ident,* ]) .ofTactic 1 tactic - return (#[goal], scriptBuilder?) + return (#[goal], 1.0, scriptBuilder?) end Aesop.BuiltinRules diff --git a/Aesop/RuleTac/Apply.lean b/Aesop/RuleTac/Apply.lean index 2bdf959b..24647aa4 100644 --- a/Aesop/RuleTac/Apply.lean +++ b/Aesop/RuleTac/Apply.lean @@ -13,13 +13,13 @@ namespace Aesop.RuleTac private def applyExpr (goal : MVarId) (e : Expr) (n : Name) (md : TransparencyMode) (generateScript : Bool) : - MetaM (Array MVarId × Option RuleTacScriptBuilder) := do + MetaM (Array MVarId × Float × Option RuleTacScriptBuilder) := do let goals := (← withTransparency md $ goal.apply e).toArray let scriptBuilder? := mkScriptBuilder? generateScript $ .ofTactic goals.size do withAllTransparencySyntax md (← `(tactic| apply $(mkIdent n))) - return (goals, scriptBuilder?) + return (goals, 1.0, scriptBuilder?) def applyConst (decl : Name) (md : TransparencyMode) : RuleTac := RuleTac.ofSingleRuleTac λ input => do @@ -41,10 +41,10 @@ def applyConsts (decls : Array Name) (md : TransparencyMode) : let apps ← decls.filterMapM λ decl => do try let e ← mkConstWithFreshMVarLevels decl - let (goals, scriptBuilder?) ← + let (goals, probabilityModifier, scriptBuilder?) ← applyExpr input.goal e decl md generateScript let postState ← saveState - return some { postState, goals, scriptBuilder? } + return some { postState, goals, probabilityModifier, scriptBuilder? } catch _ => return none finally diff --git a/Aesop/RuleTac/Basic.lean b/Aesop/RuleTac/Basic.lean index 5390ad55..f0d37792 100644 --- a/Aesop/RuleTac/Basic.lean +++ b/Aesop/RuleTac/Basic.lean @@ -48,6 +48,7 @@ goal. Must accurately report the following information: structure RuleApplication where goals : Array MVarId postState : Meta.SavedState + probabilityModifier : Float scriptBuilder? : Option RuleTacScriptBuilder namespace RuleApplication @@ -80,13 +81,13 @@ instance : Inhabited RuleTac := by A `RuleTac` which generates only a single `RuleApplication`. -/ def SingleRuleTac := - RuleTacInput → MetaM (Array MVarId × Option RuleTacScriptBuilder) + RuleTacInput → MetaM (Array MVarId × Float × Option RuleTacScriptBuilder) @[inline] def SingleRuleTac.toRuleTac (t : SingleRuleTac) : RuleTac := λ input => do - let (goals, scriptBuilder?) ← t input + let (goals, probabilityModifier, scriptBuilder?) ← t input let postState ← saveState - return ⟨#[{ postState, goals, scriptBuilder? }]⟩ + return ⟨#[{ postState, goals, probabilityModifier, scriptBuilder? }]⟩ @[inline] def RuleTac.ofSingleRuleTac := SingleRuleTac.toRuleTac diff --git a/Aesop/RuleTac/Cases.lean b/Aesop/RuleTac/Cases.lean index ad0cdfa6..ce839ef5 100644 --- a/Aesop/RuleTac/Cases.lean +++ b/Aesop/RuleTac/Cases.lean @@ -58,7 +58,7 @@ partial def cases (target : CasesTarget) (md : TransparencyMode) (isRecursiveTyp go (newGoals : Array MVarId) (excluded : Array FVarId) (goal : MVarId) (generateScript : Bool) : - MetaM (Option (Array MVarId × Option RuleTacScriptBuilder)) := do + MetaM (Option (Array MVarId × Float × Option RuleTacScriptBuilder)) := do let (some hyp) ← findFirstApplicableHyp excluded goal | return none let (goals, scriptBuilder?) ← @@ -82,7 +82,7 @@ partial def cases (target : CasesTarget) (md : TransparencyMode) (isRecursiveTyp | _ => none excluded ++ fields match ← go newGoals excluded g.mvarId generateScript with - | some (newGoals', newScriptBuilder?) => + | some (newGoals', _, newScriptBuilder?) => newGoals := newGoals' if let some newScriptBuilder := newScriptBuilder? then newScriptBuilders := newScriptBuilders.push newScriptBuilder @@ -90,6 +90,6 @@ partial def cases (target : CasesTarget) (md : TransparencyMode) (isRecursiveTyp newGoals := newGoals.push g.mvarId if generateScript then newScriptBuilders := newScriptBuilders.push .id - return some (newGoals, scriptBuilder?.bind (·.seq newScriptBuilders)) + return some (newGoals, 1.0, scriptBuilder?.bind (·.seq newScriptBuilders)) end Aesop.RuleTac diff --git a/Aesop/RuleTac/Forward.lean b/Aesop/RuleTac/Forward.lean index ad594985..98d3701f 100644 --- a/Aesop/RuleTac/Forward.lean +++ b/Aesop/RuleTac/Forward.lean @@ -147,7 +147,7 @@ def forwardExpr (e : Expr) (immediate : UnorderedArraySet Nat) let (goal, scriptBuilder?) ← applyForwardRule input.goal e immediate (clear := clear) (generateScript := input.options.generateScript) md - return (#[goal], scriptBuilder?) + return (#[goal], 1.0, scriptBuilder?) def forwardConst (decl : Name) (immediate : UnorderedArraySet Nat) (clear : Bool) (md : TransparencyMode) : RuleTac := λ input => do diff --git a/Aesop/RuleTac/Neural.lean b/Aesop/RuleTac/Neural.lean index c6891d98..4c63d408 100644 --- a/Aesop/RuleTac/Neural.lean +++ b/Aesop/RuleTac/Neural.lean @@ -11,9 +11,9 @@ namespace Aesop.RuleTac def applyNeural: RuleTac := λ input => do let initialState ← saveState let iptGoal ← LeanInfer.ppTacticState [input.goal] - let optSuggestions ← LeanInfer.generate iptGoal - let suggestions := optSuggestions.map (·.1) - let apps ← suggestions.filterMapM λ tacticStr => do + let suggestions ← LeanInfer.generate iptGoal + let apps ← suggestions.filterMapM fun (tacticStr, score) => do + assert! 0 ≤ score ∧ score ≤ 1 match Parser.runParserCategory (← getEnv) `tactic tacticStr (fileName := "") with | .error _ => return none | .ok stx => @@ -35,6 +35,7 @@ def applyNeural: RuleTac := λ input => do let thisApp : RuleApplication := { postState := postState goals := goals.toArray + probabilityModifier := score -- scriptBuilder? := scriptBuilder? scriptBuilder? := none } diff --git a/Aesop/RuleTac/Preprocess.lean b/Aesop/RuleTac/Preprocess.lean index b71e8fe2..6b5bba81 100644 --- a/Aesop/RuleTac/Preprocess.lean +++ b/Aesop/RuleTac/Preprocess.lean @@ -17,6 +17,6 @@ tried. def preprocess : RuleTac := RuleTac.ofSingleRuleTac λ input => do let (postMVarId, _, scriptBuilder?) ← renameInaccessibleFVarsWithScript input.goal input.options.generateScript - return (#[postMVarId], scriptBuilder?) + return (#[postMVarId], 1.0, scriptBuilder?) end Aesop.RuleTac diff --git a/Aesop/RuleTac/RuleApplicationWithMVarInfo.lean b/Aesop/RuleTac/RuleApplicationWithMVarInfo.lean index dbb67c5a..3ae21ac5 100644 --- a/Aesop/RuleTac/RuleApplicationWithMVarInfo.lean +++ b/Aesop/RuleTac/RuleApplicationWithMVarInfo.lean @@ -38,6 +38,7 @@ structure RuleApplicationWithMVarInfo where mvars : UnorderedArraySet MVarId introducedMVars : UnorderedArraySet MVarId assignedMVars : UnorderedArraySet MVarId + probabilityModifier : Float scriptBuilder? : Option (ScriptBuilder MetaM) namespace RuleApplicationWithMVarInfo diff --git a/Aesop/RuleTac/Tactic.lean b/Aesop/RuleTac/Tactic.lean index af62089d..011f6bdb 100644 --- a/Aesop/RuleTac/Tactic.lean +++ b/Aesop/RuleTac/Tactic.lean @@ -17,7 +17,7 @@ unsafe def tacticMImpl (decl : Name) : RuleTac := SingleRuleTac.toRuleTac λ input => do let tac ← evalConst (TacticM Unit) decl let goals ← run input.goal tac |>.run' - return (goals.toArray, none) + return (goals.toArray, 1.0, none) -- Precondition: `decl` has type `TacticM Unit`. @[implemented_by tacticMImpl] diff --git a/Aesop/Search/Expansion.lean b/Aesop/Search/Expansion.lean index 79a7df12..38d7819c 100644 --- a/Aesop/Search/Expansion.lean +++ b/Aesop/Search/Expansion.lean @@ -64,12 +64,14 @@ def addRapps (parentRef : GoalRef) (rule : RegularRule) (rapps : Array RuleApplicationWithMVarInfo) : SearchM Q RuleResult := do let parent ← parentRef.get - let successProbability := parent.successProbability * rule.successProbability let mut rrefs := Array.mkEmpty rapps.size let mut subgoals := Array.mkEmpty $ rapps.size * 3 for h : i in [:rapps.size] do let rapp := rapps[i]'(by simp_all [Membership.mem]) + let some probabilityModifier := Percent.ofFloat rapp.probabilityModifier | throwError + "aesop: internal error: rule {rule.name} returned an invalid probability modifier {rapp.probabilityModifier}" + let successProbability := parent.successProbability * rule.successProbability * probabilityModifier let rref ← addRapp { rapp with parent := parentRef diff --git a/AesopTest/NeuralProver.lean b/AesopTest/NeuralProver.lean index d90a0901..7e03b2fa 100644 --- a/AesopTest/NeuralProver.lean +++ b/AesopTest/NeuralProver.lean @@ -8,7 +8,7 @@ set_option maxHeartbeats 0 -- disable timeout section simpleTest -@[aesop unsafe 50% neural] +@[aesop unsafe 80% neural] /- [1/2] Simple theorem. The raw white-box aesop should be able to prove this theorem. diff --git a/lake-manifest.json b/lake-manifest.json index a3565cc3..1832f8a0 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -4,10 +4,10 @@ [{"git": {"url": "https://github.com/lean-dojo/LeanInfer.git", "subDir?": null, - "rev": "6b4211f30e0bdcd070fd6ca3d0c163693aeca909", + "rev": "3bc1b197ac0df2b564ce5041b646a0007151ef18", "opts": {}, "name": "LeanInfer", - "inputRev?": "v0.0.7", + "inputRev?": "dev", "inherited": false}}, {"git": {"url": "https://github.com/leanprover/std4", diff --git a/lakefile.lean b/lakefile.lean index c6021824..47968da6 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -2,7 +2,7 @@ import Lake open Lake DSL -package llmaesop { +package aesop { precompileModules := false -- breaks mathlib cache moreLinkArgs := #["-L./lake-packages/LeanInfer/build/lib", "-lonnxruntime", "-lstdc++"] } @@ -15,4 +15,4 @@ lean_lib AesopTest { } require std from git "https://github.com/leanprover/std4" @ "main" -require LeanInfer from git "https://github.com/lean-dojo/LeanInfer.git" @ "v0.0.7" \ No newline at end of file +require LeanInfer from git "https://github.com/lean-dojo/LeanInfer.git" @ "dev" \ No newline at end of file From 7669ebc5a5591c1d40141226109274ca3378bf3c Mon Sep 17 00:00:00 2001 From: Kaiyu Yang Date: Sat, 7 Oct 2023 15:59:36 -0500 Subject: [PATCH 27/31] use the tactic rule builder --- Aesop/Builder.lean | 1 - Aesop/Builder/Neural.lean | 23 --------------- Aesop/Builder/Tactic.lean | 5 +++- Aesop/Frontend/RuleExpr.lean | 14 ---------- Aesop/Rule/Name.lean | 2 -- Aesop/RuleTac.lean | 3 +- Aesop/RuleTac/Basic.lean | 4 +-- Aesop/RuleTac/Neural.lean | 54 ------------------------------------ Aesop/RuleTac/Tactic.lean | 46 +++++++++++++++++++++++++++++- AesopTest/NeuralCheck.lean | 29 ------------------- AesopTest/NeuralProver.lean | 33 ---------------------- AesopTest/TacGen.lean | 20 +++++++++++++ lakefile.lean | 2 -- 13 files changed, 72 insertions(+), 164 deletions(-) delete mode 100644 Aesop/Builder/Neural.lean delete mode 100644 Aesop/RuleTac/Neural.lean delete mode 100644 AesopTest/NeuralCheck.lean delete mode 100644 AesopTest/NeuralProver.lean create mode 100644 AesopTest/TacGen.lean diff --git a/Aesop/Builder.lean b/Aesop/Builder.lean index bc5a8f8e..69404f69 100644 --- a/Aesop/Builder.lean +++ b/Aesop/Builder.lean @@ -13,4 +13,3 @@ import Aesop.Builder.Forward import Aesop.Builder.NormSimp import Aesop.Builder.Tactic import Aesop.Builder.Unfold -import Aesop.Builder.Neural diff --git a/Aesop/Builder/Neural.lean b/Aesop/Builder/Neural.lean deleted file mode 100644 index e434c059..00000000 --- a/Aesop/Builder/Neural.lean +++ /dev/null @@ -1,23 +0,0 @@ -import Aesop.Builder.Basic - -open Lean -open Lean.Meta - -namespace Aesop - -def RuleBuilder.neural (opts : RegularBuilderOptions) : RuleBuilder := λ input => - match input.kind with - | RuleBuilderKind.global _ => do - let tac := .neuralProvers - RuleBuilderOutput.global <$> mkResult tac - | RuleBuilderKind.local _ _ => - throwError "neural rule builder does not support local hypotheses" - where - mkResult (tac : RuleTacDescr) : MetaM RuleBuilderResult := - return RuleBuilderResult.regular { - builder := BuilderName.neural - tac := tac - indexingMode := ← opts.getIndexingModeM $ pure IndexingMode.unindexed - } - -end Aesop diff --git a/Aesop/Builder/Tactic.lean b/Aesop/Builder/Tactic.lean index a7e8b7a4..87364d04 100644 --- a/Aesop/Builder/Tactic.lean +++ b/Aesop/Builder/Tactic.lean @@ -21,8 +21,11 @@ def RuleBuilder.tactic (opts : RegularBuilderOptions) : RuleBuilder := mkResult $ .singleRuleTac decl else if ← isDefEq (mkConst ``RuleTac) type then mkResult $ .ruleTac decl + else if ← isDefEq (← mkArrow (mkConst ``MVarId) (mkApp (mkConst ``MetaM) (← mkAppM ``Array #[(← mkAppM ``Prod #[(mkConst ``String), (mkConst ``Float)])]))) type then + -- MVarId → MetaM (Array (String × Float)) + mkResult $ .tacGen decl else - throwError "aesop: {decl} was expected to be a tactic, i.e. to have one of these types:\n TacticM Unit\n SimpleRuleTac\n RuleTac\nHowever, it has type{indentExpr type}" + throwError "aesop: {decl} was expected to be a tactic, i.e. to have one of these types:\n TacticM Unit\n SimpleRuleTac\n RuleTac\n MVarId → MetaM (Array (String × Float))\nHowever, it has type{indentExpr type}" where builderName : BuilderName := .tactic diff --git a/Aesop/Frontend/RuleExpr.lean b/Aesop/Frontend/RuleExpr.lean index 25fa3def..b8c98831 100644 --- a/Aesop/Frontend/RuleExpr.lean +++ b/Aesop/Frontend/RuleExpr.lean @@ -103,7 +103,6 @@ syntax "forward" : Aesop.builder_name syntax "destruct" : Aesop.builder_name syntax "cases" : Aesop.builder_name syntax "default" : Aesop.builder_name -syntax "neural" : Aesop.builder_name end Parser @@ -125,7 +124,6 @@ def «elab» (stx : Syntax) : ElabM DBuilderName := | `(builder_name| forward) => return regular .forward | `(builder_name| destruct) => return regular .destruct | `(builder_name| cases) => return regular .cases - | `(builder_name| neural) => return regular .neural | `(builder_name| default) => return «default» | _ => throwUnsupportedSyntax @@ -355,14 +353,6 @@ def constructors : BuilderOptions ConstructorsBuilderOptions where some opts | _, _ => none -def neural : BuilderOptions RegularBuilderOptions where - builderName := .regular .neural - init := default - add - | opts, .index indexingMode? => some { opts with indexingMode? } - | opts, .transparency _ _ => some opts - | _, _ => none - end BuilderOptions @@ -383,7 +373,6 @@ inductive Builder | constructors (opts : ConstructorsBuilderOptions) | forward (opts : ForwardBuilderOptions) | cases (opts : CasesBuilderOptions) - | neural (opts: RegularBuilderOptions) | «default» deriving Inhabited @@ -399,7 +388,6 @@ def elabOptions (b : DBuilderName) (opts : Syntax) : ElabM Builder := do | .regular .forward => forward <$> BuilderOptions.forward.elab opts | .regular .destruct => forward <$> BuilderOptions.destruct.elab opts | .regular .cases => «cases» <$> BuilderOptions.cases.elab opts - | .regular .neural => neural <$> BuilderOptions.neural.elab opts | .default => checkNoOptions; return default where checkNoOptions := BuilderOptions.none b |>.«elab» opts @@ -421,7 +409,6 @@ def toRuleBuilder : Builder → RuleBuilder | constructors opts => RuleBuilder.constructors opts | forward opts => RuleBuilder.forward opts | cases opts => RuleBuilder.cases opts - | neural opts => RuleBuilder.neural opts | «default» => RuleBuilder.default open DBuilderName in @@ -433,7 +420,6 @@ def toDBuilderName : Builder → DBuilderName | constructors .. => regular .constructors | forward .. => regular .forward | cases .. => regular .cases - | neural .. => regular .neural | .«default» => .default end Builder diff --git a/Aesop/Rule/Name.lean b/Aesop/Rule/Name.lean index 6a0b098a..cd79bc73 100644 --- a/Aesop/Rule/Name.lean +++ b/Aesop/Rule/Name.lean @@ -59,7 +59,6 @@ inductive BuilderName | constructors | destruct | forward - | neural | simp | tactic | unfold @@ -79,7 +78,6 @@ instance : ToString BuilderName where | constructors => "constructors" | destruct => "destruct" | forward => "forward" - | neural => "neural" | simp => "simp" | tactic => "tactic" | unfold => "unfold" diff --git a/Aesop/RuleTac.lean b/Aesop/RuleTac.lean index 03c8fcff..90516f86 100644 --- a/Aesop/RuleTac.lean +++ b/Aesop/RuleTac.lean @@ -11,7 +11,6 @@ import Aesop.RuleTac.Forward import Aesop.RuleTac.Preprocess import Aesop.RuleTac.RuleApplicationWithMVarInfo import Aesop.RuleTac.Tactic -import Aesop.RuleTac.Neural open Lean @@ -21,7 +20,6 @@ protected def run : RuleTacDescr → RuleTacInput → MetaM RuleTacOutput | applyConst decl md => RuleTac.applyConst decl md | applyFVar userName md => RuleTac.applyFVar userName md | constructors cs md => RuleTac.applyConsts cs md - | neuralProvers => RuleTac.applyNeural | forwardConst decl immediate clear md => RuleTac.forwardConst decl immediate clear md | forwardFVar userName immediate clear md => @@ -30,6 +28,7 @@ protected def run : RuleTacDescr → RuleTacInput → MetaM RuleTacOutput | tacticM decl => RuleTac.tacticM decl | singleRuleTac decl => RuleTac.singleRuleTac decl | ruleTac decl => RuleTac.ruleTac decl + | tacGen decl => RuleTac.tacGen decl | preprocess => RuleTac.preprocess end RuleTacDescr diff --git a/Aesop/RuleTac/Basic.lean b/Aesop/RuleTac/Basic.lean index f0d37792..355cb61e 100644 --- a/Aesop/RuleTac/Basic.lean +++ b/Aesop/RuleTac/Basic.lean @@ -107,7 +107,6 @@ inductive RuleTacDescr | applyConst (decl : Name) (md : TransparencyMode) | applyFVar (userName : Name) (md : TransparencyMode) | constructors (constructorNames : Array Name) (md : TransparencyMode) - | neuralProvers | forwardConst (decl : Name) (immediate : UnorderedArraySet Nat) (clear : Bool) (md : TransparencyMode) | forwardFVar (userName : Name) (immediate : UnorderedArraySet Nat) @@ -116,6 +115,7 @@ inductive RuleTacDescr (isRecursiveType : Bool) | tacticM (decl : Name) | ruleTac (decl : Name) + | tacGen (decl : Name) | singleRuleTac (decl : Name) | preprocess deriving Inhabited @@ -126,12 +126,12 @@ def isGlobal : RuleTacDescr → Bool | applyConst .. => true | applyFVar .. => false | constructors .. => true - | neuralProvers .. => true | forwardConst .. => true | forwardFVar .. => false | cases .. => true | tacticM .. => true | ruleTac .. => true + | tacGen .. => true | singleRuleTac .. => true | preprocess => true diff --git a/Aesop/RuleTac/Neural.lean b/Aesop/RuleTac/Neural.lean deleted file mode 100644 index 4c63d408..00000000 --- a/Aesop/RuleTac/Neural.lean +++ /dev/null @@ -1,54 +0,0 @@ -import LeanInfer - -import Aesop.RuleTac.Basic - -open Lean Lean.Meta Lean.Elab Lean.Elab.Command Lean.Elab.Tactic - -namespace Aesop.RuleTac - --- Tries to apply each tactic suggested by a neural network. For each one that --- applies, a rule application is returned. If none applies, the tactic fails. -def applyNeural: RuleTac := λ input => do - let initialState ← saveState - let iptGoal ← LeanInfer.ppTacticState [input.goal] - let suggestions ← LeanInfer.generate iptGoal - let apps ← suggestions.filterMapM fun (tacticStr, score) => do - assert! 0 ≤ score ∧ score ≤ 1 - match Parser.runParserCategory (← getEnv) `tactic tacticStr (fileName := "") with - | .error _ => return none - | .ok stx => - try - initialState.restore - let tac := commitIfNoEx $ evalTactic stx - -- let tstx : TSyntax `tactic := {raw := stx} - let goals ← run input.goal tac |>.run' - let pf? ← getExprMVarAssignment? input.goal - if pf?.isSome then - if (← instantiateMVars pf?.get!) |>.hasSorry then - initialState.restore - return none - -- let scriptBuilder? := - -- mkScriptBuilder? generateScript $ - -- .ofTactic goals.toArray.size do - -- withAllTransparencySyntax md tstx - let postState ← saveState - let thisApp : RuleApplication := { - postState := postState - goals := goals.toArray - probabilityModifier := score - -- scriptBuilder? := scriptBuilder? - scriptBuilder? := none - } - return thisApp - catch _ => pure none - restoreState initialState - if apps.isEmpty then throwError - "failed to apply any tactics generated" - return ⟨apps⟩ - - -end RuleTac - - - - \ No newline at end of file diff --git a/Aesop/RuleTac/Tactic.lean b/Aesop/RuleTac/Tactic.lean index 011f6bdb..44a11829 100644 --- a/Aesop/RuleTac/Tactic.lean +++ b/Aesop/RuleTac/Tactic.lean @@ -8,7 +8,8 @@ import Aesop.RuleTac.Basic open Lean open Lean.Meta -open Lean.Elab.Tactic (TacticM run) +open Lean.Elab.Term (TermElabM withSynthesize) +open Lean.Elab.Tactic (TacticM evalTactic run) namespace Aesop.RuleTac @@ -42,4 +43,47 @@ unsafe def singleRuleTacImpl (decl : Name) : RuleTac := @[implemented_by singleRuleTacImpl] opaque singleRuleTac (decl : Name) : RuleTac +-- Precondition: `decl` has type `MVarId → MetaM (Array (String × Float))`. +unsafe def tacGenImpl (decl : Name) : RuleTac := λ input => do + let tac ← evalConst (MVarId → MetaM (Array (String × Float))) decl + let initialState ← saveState + let suggestions ← tac input.goal + let apps ← suggestions.filterMapM fun (tacticStr, score) => do + assert! 0 ≤ score ∧ score ≤ 1 + match Parser.runParserCategory (← getEnv) `tactic tacticStr (fileName := "") with + | .error _ => return none + | .ok stx => + try + initialState.restore + let tac := commitIfNoEx $ evalTactic stx + -- let tstx : TSyntax `tactic := {raw := stx} + let goals ← run input.goal tac |>.run' + let pf? ← getExprMVarAssignment? input.goal + if pf?.isSome then + if (← instantiateMVars pf?.get!) |>.hasSorry then + initialState.restore + return none + -- let scriptBuilder? := + -- mkScriptBuilder? generateScript $ + -- .ofTactic goals.toArray.size do + -- withAllTransparencySyntax md tstx + let postState ← saveState + let thisApp : RuleApplication := { + postState := postState + goals := goals.toArray + probabilityModifier := score + -- scriptBuilder? := scriptBuilder? + scriptBuilder? := none + } + return thisApp + catch _ => pure none + restoreState initialState + if apps.isEmpty then throwError + "failed to apply any tactics generated" + return ⟨apps⟩ + +-- Precondition: `decl` has type `MVarId → MetaM (Array (String × Float))`. +@[implemented_by tacGenImpl] +opaque tacGen (decl : Name) : RuleTac + end Aesop.RuleTac diff --git a/AesopTest/NeuralCheck.lean b/AesopTest/NeuralCheck.lean deleted file mode 100644 index 5f21d056..00000000 --- a/AesopTest/NeuralCheck.lean +++ /dev/null @@ -1,29 +0,0 @@ -import Aesop - -set_option aesop.check.all true - -section buildCheck - -/- [1/2] Check aesop. - Write a simple theorem and try to prove it `by aesop`. - If the goal is closed (i.e., No goals displayed in the InfoView), - aesop is likely to have been properly built. - Additionally, you may try to type `aesop?` to see scripts suggested by aesop. --/ -theorem foo1 (a : Nat) : a + 1 = Nat.succ a := by - aesop - -- aesop? - -/- [2/2] Check LeanInfer. - Write a simple theorem and try to prove it `by LeanInfer`. - If a list of tactics is shown under `Tactic suggestions` in the InfoView - while the goal is not closed, the LeanInfer part is successfully built as well. - For the first time, should it ask you to download the model by running `suggest_tactics!`, - following it will automatically download the model to `~/.cache/lean_infer/` by default, - with the path overridable by setting the `LEAN_INFER_CACHE_DIR` environment variable. --/ -theorem foo2 (a b c : Nat) : a + b + c = a + c + b := by - suggest_tactics - -- suggest_tactics! - -end buildCheck diff --git a/AesopTest/NeuralProver.lean b/AesopTest/NeuralProver.lean deleted file mode 100644 index 7e03b2fa..00000000 --- a/AesopTest/NeuralProver.lean +++ /dev/null @@ -1,33 +0,0 @@ -import Aesop - --- set_option aesop.check.all true --- set_option trace.aesop.tree true --- set_option trace.aesop true --- all three flags are for debugging purpose, not necessarily needed. -set_option maxHeartbeats 0 -- disable timeout - -section simpleTest - -@[aesop unsafe 80% neural] - -/- [1/2] Simple theorem. - The raw white-box aesop should be able to prove this theorem. - Since we mark the neural prover as `unsafe`, when the `safe` builtin rules of aesop - can already prove the goal, our additional option of `neural` will never be called. - In other words, the theorems that can be proved by the original `aesop` - is a strict subset of that can be proved by our `LLM-aesop`. -/ -theorem foo1 (a: Nat) : a + 1 = Nat.succ a := by - aesop - -/- [2/2] Hard theorem. - The raw white-box `aesop` should not be able to prove this theorem. - After trying all builtin rules, which should all fail on this theorem, - the original `aesop` will fail to close this goal, - while our `LLM-aesop` will try the `unsafe` neural prover, - which can usually prove the goal. - Note that this is not guaranteed for each time you run `LLM-aesop`, - as there is existing uncertainty rooted in any machine learning method. -/ -theorem foo2 (a b c : Nat) : a + b + c = c + b + a := by - aesop - -end simpleTest diff --git a/AesopTest/TacGen.lean b/AesopTest/TacGen.lean new file mode 100644 index 00000000..c48b34b0 --- /dev/null +++ b/AesopTest/TacGen.lean @@ -0,0 +1,20 @@ +import Aesop + +open Lean +open Lean.Meta + +theorem foo (a b c : Nat) : a + b + c = c + b + a := by + rw [Nat.add_assoc] + rw [Nat.add_comm] + rw [Nat.add_comm b] + +-- @[aesop unsafe 50% tactic] +-- def x (_ : MVarId) : MetaM (Array (String × Float)) := do +-- return #[("apply foo", 1.0)] + +@[aesop unsafe 80% tactic] +def x : MVarId → MetaM (Array (String × Float)) := fun _ => do + return #[("rw [Nat.add_comm b]", 0.5), ("rw [Nat.add_assoc]", 0.9), ("rw [Nat.add_comm]", 0.8)] + +example (a b c : Nat) : a + b + c = c + b + a := by + aesop \ No newline at end of file diff --git a/lakefile.lean b/lakefile.lean index 47968da6..267a075d 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -4,7 +4,6 @@ open Lake DSL package aesop { precompileModules := false -- breaks mathlib cache - moreLinkArgs := #["-L./lake-packages/LeanInfer/build/lib", "-lonnxruntime", "-lstdc++"] } @[default_target] @@ -15,4 +14,3 @@ lean_lib AesopTest { } require std from git "https://github.com/leanprover/std4" @ "main" -require LeanInfer from git "https://github.com/lean-dojo/LeanInfer.git" @ "dev" \ No newline at end of file From 744bae6ad74401db5b77af78b2530e9550f518ad Mon Sep 17 00:00:00 2001 From: Kaiyu Yang Date: Sat, 7 Oct 2023 16:09:52 -0500 Subject: [PATCH 28/31] further simplify --- Aesop/BuiltinRules/ApplyHyps.lean | 3 +-- Aesop/BuiltinRules/Assumption.lean | 1 - Aesop/BuiltinRules/DestructProducts.lean | 2 +- Aesop/BuiltinRules/Ext.lean | 4 ++-- Aesop/BuiltinRules/Intros.lean | 2 +- Aesop/BuiltinRules/Split.lean | 4 ++-- Aesop/BuiltinRules/Subst.lean | 2 +- Aesop/RuleTac/Apply.lean | 8 ++++---- Aesop/RuleTac/Basic.lean | 8 ++++---- Aesop/RuleTac/Cases.lean | 6 +++--- Aesop/RuleTac/Forward.lean | 2 +- Aesop/RuleTac/Preprocess.lean | 2 +- Aesop/RuleTac/Tactic.lean | 2 +- AesopTest/TacGen.lean | 3 ++- lake-manifest.json | 8 -------- 15 files changed, 24 insertions(+), 33 deletions(-) diff --git a/Aesop/BuiltinRules/ApplyHyps.lean b/Aesop/BuiltinRules/ApplyHyps.lean index b6528a5c..a2cf3f09 100644 --- a/Aesop/BuiltinRules/ApplyHyps.lean +++ b/Aesop/BuiltinRules/ApplyHyps.lean @@ -19,8 +19,7 @@ def applyHyp (hyp : FVarId) (goal : MVarId) (md : TransparencyMode) let scriptBuilder? := mkScriptBuilder? generateScript $ .ofTactic goals.size $ withTransparencySyntax md $ ← `(tactic| apply $(mkIdent $ ← hyp.getUserName)) - let probabilityModifier := 1.0 - return { postState, goals, probabilityModifier, scriptBuilder? } + return { postState, goals, scriptBuilder? } @[aesop unsafe 75% tactic (rule_sets [builtin])] def applyHyps : RuleTac := λ input => diff --git a/Aesop/BuiltinRules/Assumption.lean b/Aesop/BuiltinRules/Assumption.lean index c8f04b95..e6d8ff86 100644 --- a/Aesop/BuiltinRules/Assumption.lean +++ b/Aesop/BuiltinRules/Assumption.lean @@ -52,7 +52,6 @@ def assumption : RuleTac := λ input => do ← `(tactic| exact $(mkIdent ldecl.userName)) let app := { goals := #[] - probabilityModifier := 1.0 postState, scriptBuilder? } let proofHasMVar := ldecl.type.hasMVar diff --git a/Aesop/BuiltinRules/DestructProducts.lean b/Aesop/BuiltinRules/DestructProducts.lean index 6e9214b0..65eb8069 100644 --- a/Aesop/BuiltinRules/DestructProducts.lean +++ b/Aesop/BuiltinRules/DestructProducts.lean @@ -105,6 +105,6 @@ partial def destructProducts : RuleTac := RuleTac.ofSingleRuleTac λ input => do mkScriptBuilder? input.options.generateScript $ .ofTactic 1 do let tac ← withTransparencySyntax md (← `(tactic| aesop_destruct_products)) `(tactic| unhygienic $tac:tactic) - return (#[goal], 1.0, scriptBuilder?) + return (#[goal], scriptBuilder?) end Aesop.BuiltinRules diff --git a/Aesop/BuiltinRules/Ext.lean b/Aesop/BuiltinRules/Ext.lean index 4b565a53..982e50d1 100644 --- a/Aesop/BuiltinRules/Ext.lean +++ b/Aesop/BuiltinRules/Ext.lean @@ -17,11 +17,11 @@ def unhygienicExt (goal : MVarId) : MetaM (Array MVarId) := return subgoals.map (·.fst) def unhygienicExtWithScript (goal : MVarId) (generateScript : Bool) : - MetaM (Array MVarId × Float × Option RuleTacScriptBuilder) := do + MetaM (Array MVarId × Option RuleTacScriptBuilder) := do let subgoals ← unhygienicExt goal let scriptBuilder? := mkScriptBuilder? generateScript (.unhygienicExt subgoals.size) - return (subgoals, 1.0, scriptBuilder?) + return (subgoals, scriptBuilder?) @[aesop 80% (rule_sets [builtin])] def ext : RuleTac := RuleTac.ofSingleRuleTac λ input => diff --git a/Aesop/BuiltinRules/Intros.lean b/Aesop/BuiltinRules/Intros.lean index 58433bce..9608690c 100644 --- a/Aesop/BuiltinRules/Intros.lean +++ b/Aesop/BuiltinRules/Intros.lean @@ -56,6 +56,6 @@ def intros : RuleTac := RuleTac.ofSingleRuleTac λ input => do else pure none - return (#[goal], 1.0, scriptBuilder?) + return (#[goal], scriptBuilder?) end Aesop.BuiltinRules diff --git a/Aesop/BuiltinRules/Split.lean b/Aesop/BuiltinRules/Split.lean index d48cd05c..19ed4094 100644 --- a/Aesop/BuiltinRules/Split.lean +++ b/Aesop/BuiltinRules/Split.lean @@ -19,7 +19,7 @@ def splitTarget : RuleTac := RuleTac.ofSingleRuleTac λ input => do let scriptBuilder? := mkScriptBuilder? input.options.generateScript $ .ofTactic goals.size `(tactic| split) - return (goals, 1.0, scriptBuilder?) + return (goals, scriptBuilder?) def splitFirstHypothesis (goal : MVarId) : MetaM (Option (Array MVarId)) := goal.withContext do @@ -44,6 +44,6 @@ def splitHypotheses : RuleTac := RuleTac.ofSingleRuleTac λ input => do let scriptBuilder? := mkScriptBuilder? input.options.generateScript $ .ofTactic goals.size `(tactic| aesop_split_hyps) - return (goals, 1.0, scriptBuilder?) + return (goals, scriptBuilder?) end Aesop.BuiltinRules diff --git a/Aesop/BuiltinRules/Subst.lean b/Aesop/BuiltinRules/Subst.lean index a255446e..2bdfc0ba 100644 --- a/Aesop/BuiltinRules/Subst.lean +++ b/Aesop/BuiltinRules/Subst.lean @@ -97,6 +97,6 @@ def subst : RuleTac := RuleTac.ofSingleRuleTac λ input => else `(tactic| aesop_subst [ $substitutedUserNames:ident,* ]) .ofTactic 1 tactic - return (#[goal], 1.0, scriptBuilder?) + return (#[goal], scriptBuilder?) end Aesop.BuiltinRules diff --git a/Aesop/RuleTac/Apply.lean b/Aesop/RuleTac/Apply.lean index 24647aa4..2bdf959b 100644 --- a/Aesop/RuleTac/Apply.lean +++ b/Aesop/RuleTac/Apply.lean @@ -13,13 +13,13 @@ namespace Aesop.RuleTac private def applyExpr (goal : MVarId) (e : Expr) (n : Name) (md : TransparencyMode) (generateScript : Bool) : - MetaM (Array MVarId × Float × Option RuleTacScriptBuilder) := do + MetaM (Array MVarId × Option RuleTacScriptBuilder) := do let goals := (← withTransparency md $ goal.apply e).toArray let scriptBuilder? := mkScriptBuilder? generateScript $ .ofTactic goals.size do withAllTransparencySyntax md (← `(tactic| apply $(mkIdent n))) - return (goals, 1.0, scriptBuilder?) + return (goals, scriptBuilder?) def applyConst (decl : Name) (md : TransparencyMode) : RuleTac := RuleTac.ofSingleRuleTac λ input => do @@ -41,10 +41,10 @@ def applyConsts (decls : Array Name) (md : TransparencyMode) : let apps ← decls.filterMapM λ decl => do try let e ← mkConstWithFreshMVarLevels decl - let (goals, probabilityModifier, scriptBuilder?) ← + let (goals, scriptBuilder?) ← applyExpr input.goal e decl md generateScript let postState ← saveState - return some { postState, goals, probabilityModifier, scriptBuilder? } + return some { postState, goals, scriptBuilder? } catch _ => return none finally diff --git a/Aesop/RuleTac/Basic.lean b/Aesop/RuleTac/Basic.lean index 355cb61e..fe1da5bb 100644 --- a/Aesop/RuleTac/Basic.lean +++ b/Aesop/RuleTac/Basic.lean @@ -48,8 +48,8 @@ goal. Must accurately report the following information: structure RuleApplication where goals : Array MVarId postState : Meta.SavedState - probabilityModifier : Float scriptBuilder? : Option RuleTacScriptBuilder + probabilityModifier : Float := 1.0 namespace RuleApplication @@ -81,13 +81,13 @@ instance : Inhabited RuleTac := by A `RuleTac` which generates only a single `RuleApplication`. -/ def SingleRuleTac := - RuleTacInput → MetaM (Array MVarId × Float × Option RuleTacScriptBuilder) + RuleTacInput → MetaM (Array MVarId × Option RuleTacScriptBuilder) @[inline] def SingleRuleTac.toRuleTac (t : SingleRuleTac) : RuleTac := λ input => do - let (goals, probabilityModifier, scriptBuilder?) ← t input + let (goals, scriptBuilder?) ← t input let postState ← saveState - return ⟨#[{ postState, goals, probabilityModifier, scriptBuilder? }]⟩ + return ⟨#[{ postState, goals, scriptBuilder? }]⟩ @[inline] def RuleTac.ofSingleRuleTac := SingleRuleTac.toRuleTac diff --git a/Aesop/RuleTac/Cases.lean b/Aesop/RuleTac/Cases.lean index ce839ef5..ad0cdfa6 100644 --- a/Aesop/RuleTac/Cases.lean +++ b/Aesop/RuleTac/Cases.lean @@ -58,7 +58,7 @@ partial def cases (target : CasesTarget) (md : TransparencyMode) (isRecursiveTyp go (newGoals : Array MVarId) (excluded : Array FVarId) (goal : MVarId) (generateScript : Bool) : - MetaM (Option (Array MVarId × Float × Option RuleTacScriptBuilder)) := do + MetaM (Option (Array MVarId × Option RuleTacScriptBuilder)) := do let (some hyp) ← findFirstApplicableHyp excluded goal | return none let (goals, scriptBuilder?) ← @@ -82,7 +82,7 @@ partial def cases (target : CasesTarget) (md : TransparencyMode) (isRecursiveTyp | _ => none excluded ++ fields match ← go newGoals excluded g.mvarId generateScript with - | some (newGoals', _, newScriptBuilder?) => + | some (newGoals', newScriptBuilder?) => newGoals := newGoals' if let some newScriptBuilder := newScriptBuilder? then newScriptBuilders := newScriptBuilders.push newScriptBuilder @@ -90,6 +90,6 @@ partial def cases (target : CasesTarget) (md : TransparencyMode) (isRecursiveTyp newGoals := newGoals.push g.mvarId if generateScript then newScriptBuilders := newScriptBuilders.push .id - return some (newGoals, 1.0, scriptBuilder?.bind (·.seq newScriptBuilders)) + return some (newGoals, scriptBuilder?.bind (·.seq newScriptBuilders)) end Aesop.RuleTac diff --git a/Aesop/RuleTac/Forward.lean b/Aesop/RuleTac/Forward.lean index 98d3701f..ad594985 100644 --- a/Aesop/RuleTac/Forward.lean +++ b/Aesop/RuleTac/Forward.lean @@ -147,7 +147,7 @@ def forwardExpr (e : Expr) (immediate : UnorderedArraySet Nat) let (goal, scriptBuilder?) ← applyForwardRule input.goal e immediate (clear := clear) (generateScript := input.options.generateScript) md - return (#[goal], 1.0, scriptBuilder?) + return (#[goal], scriptBuilder?) def forwardConst (decl : Name) (immediate : UnorderedArraySet Nat) (clear : Bool) (md : TransparencyMode) : RuleTac := λ input => do diff --git a/Aesop/RuleTac/Preprocess.lean b/Aesop/RuleTac/Preprocess.lean index 6b5bba81..b71e8fe2 100644 --- a/Aesop/RuleTac/Preprocess.lean +++ b/Aesop/RuleTac/Preprocess.lean @@ -17,6 +17,6 @@ tried. def preprocess : RuleTac := RuleTac.ofSingleRuleTac λ input => do let (postMVarId, _, scriptBuilder?) ← renameInaccessibleFVarsWithScript input.goal input.options.generateScript - return (#[postMVarId], 1.0, scriptBuilder?) + return (#[postMVarId], scriptBuilder?) end Aesop.RuleTac diff --git a/Aesop/RuleTac/Tactic.lean b/Aesop/RuleTac/Tactic.lean index 44a11829..91adabfc 100644 --- a/Aesop/RuleTac/Tactic.lean +++ b/Aesop/RuleTac/Tactic.lean @@ -18,7 +18,7 @@ unsafe def tacticMImpl (decl : Name) : RuleTac := SingleRuleTac.toRuleTac λ input => do let tac ← evalConst (TacticM Unit) decl let goals ← run input.goal tac |>.run' - return (goals.toArray, 1.0, none) + return (goals.toArray, none) -- Precondition: `decl` has type `TacticM Unit`. @[implemented_by tacticMImpl] diff --git a/AesopTest/TacGen.lean b/AesopTest/TacGen.lean index c48b34b0..06f560fa 100644 --- a/AesopTest/TacGen.lean +++ b/AesopTest/TacGen.lean @@ -12,9 +12,10 @@ theorem foo (a b c : Nat) : a + b + c = c + b + a := by -- def x (_ : MVarId) : MetaM (Array (String × Float)) := do -- return #[("apply foo", 1.0)] +-- It wouldn't work without this. @[aesop unsafe 80% tactic] def x : MVarId → MetaM (Array (String × Float)) := fun _ => do return #[("rw [Nat.add_comm b]", 0.5), ("rw [Nat.add_assoc]", 0.9), ("rw [Nat.add_comm]", 0.8)] example (a b c : Nat) : a + b + c = c + b + a := by - aesop \ No newline at end of file + aesop diff --git a/lake-manifest.json b/lake-manifest.json index 1832f8a0..bc3d3d63 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -2,14 +2,6 @@ "packagesDir": "lake-packages", "packages": [{"git": - {"url": "https://github.com/lean-dojo/LeanInfer.git", - "subDir?": null, - "rev": "3bc1b197ac0df2b564ce5041b646a0007151ef18", - "opts": {}, - "name": "LeanInfer", - "inputRev?": "dev", - "inherited": false}}, - {"git": {"url": "https://github.com/leanprover/std4", "subDir?": null, "rev": "f2df4ab8c0726fce3bafb73a5727336b0c3120ea", From 76375b4134f21e9e7b426ce696b7f80e5f525ada Mon Sep 17 00:00:00 2001 From: Kaiyu Yang Date: Sat, 7 Oct 2023 16:12:20 -0500 Subject: [PATCH 29/31] clean --- Aesop-README.md | 944 ------------------------------------- Aesop/RuleTac/Tactic.lean | 1 - README.md | 953 +++++++++++++++++++++++++++++++++++++- 3 files changed, 929 insertions(+), 969 deletions(-) delete mode 100644 Aesop-README.md diff --git a/Aesop-README.md b/Aesop-README.md deleted file mode 100644 index 5dcad4d6..00000000 --- a/Aesop-README.md +++ /dev/null @@ -1,944 +0,0 @@ -# Aesop (original) - -Aesop (Automated Extensible Search for Obvious Proofs) is a proof search tactic -for Lean 4. It is broadly similar to Isabelle's `auto`. In essence, Aesop works -like this: - -- As with `simp`, you tag a (large) collection of definitions with the - `@[aesop]` attribute, registering them as Aesop _rules_. Rules can be - arbitrary tactics. We provide convenient ways to create common types of rules, - e.g. rules which apply a lemma. -- Aesop takes these rules and tries to apply each of them to the initial goal. - If a rule succeeds and generates subgoals, Aesop recursively applies the rules - to these subgoals, building a _search tree_. -- The search tree is explored in a _best-first_ manner. You can mark rules as - more or less likely to be useful. Based on this information, Aesop prioritises - the goals in the search tree, visiting more promising goals before less - promising ones. -- Before any rules are applied to a goal, it is _normalised_, using a special - (customisable) set of _normalisation rules_. An important built-in - normalisation rule runs `simp_all`, so your `@[simp]` lemmas are taken into - account by Aesop. -- Rules can be marked as _safe_ to optimise Aesop's performance. A safe rule is - applied eagerly and is never backtracked. For example, Aesop's built-in rules - safely split a goal `P ∧ Q` into goals for `P` and `Q`. After this split, the - original goal `P ∧ Q` is never revisited. -- Aesop provides a set of built-in rules which perform logical operations (e.g. - case-split on hypotheses `P ∨ Q`) and some other straightforward deductions. -- Aesop uses indexing methods similar to those of `simp` and other Lean tactics. - This means it should remain reasonably fast even with a large rule set. -- When called as `aesop?`, Aesop prints a tactic script that proves the goal, - similar to `simp?`. This way you can avoid the performance penalty of running - Aesop all the time. However, the script generation is currently not fully - reliable, so you may have to adjust the generated script. - -Aesop should be suitable for two main use cases: - -- General-purpose automation, where Aesop is used to dispatch 'trivial' goals. - Once mathlib is ported to Lean 4 and we have registered many lemmas as Aesop - rules, Aesop will hopefully serve as a much more powerful `simp`. -- Special-purpose automation, where specific Aesop rule sets are built to - address a certain class of goals. Tactics such as `measurability`, - `continuity` or `tidy`, which perform some sort of recursive search, can - hopefully be replaced by Aesop rule sets. - -I only occasionally update this README, so details may be out of date. If you -have questions, please create an issue or ping me (Jannis Limperg) on the [Lean -Zulip](https://leanprover.zulipchat.com). Pull requests are very welcome! - -There's also [a paper about Aesop](https://zenodo.org/record/7430233) which -covers many of the topics discussed here, sometimes in more detail. - -## Building - -With [elan](https://github.com/leanprover/elan) installed, `lake build` -should suffice. - -## Adding Aesop to Your Project - -To use Aesop in a Lean 4 project, first add this package as a dependency. In -your `lakefile.lean`, add - -```lean -require aesop from git "https://github.com/JLimperg/aesop" -``` - -You also need to make sure that your `lean-toolchain` file contains the same -version of Lean 4 as Aesop's, and that your versions of Aesop's dependencies -(currently only `std4`) match. We unfortunately can't support version ranges at -the moment. - -Now the following test file should compile: - -```lean -import Aesop - -example : α → α := - by aesop -``` - -## Quickstart - -To get you started, I'll explain Aesop's major concepts with a series of -examples. A more thorough, reference-style discussion follows in the next -section. - -We first define our own version of lists (so as not to clash with the standard -library) and an `append` function: - -``` lean -inductive MyList (α : Type _) - | nil - | cons (hd : α) (tl : MyList α) - -namespace MyList - -protected def append : (_ _ : MyList α) → MyList α - | nil, ys => ys - | cons x xs, ys => cons x (MyList.append xs ys) - -instance : Append (MyList α) := - ⟨MyList.append⟩ -``` - -We also tell `simp` to unfold applications of `append`: - -```lean -@[simp] -theorem nil_append : nil ++ xs = xs := rfl - -@[simp] -theorem cons_append : cons x xs ++ ys = cons x (xs ++ ys) := rfl -``` - -When Aesop first encounters a goal, it normalises it by running a customisable -set of normalisation rules. One such normalisation rule effectively runs -`simp_all`, so Aesop automatically takes `simp` lemmas into account. - -Now we define the `NonEmpty` predicate on `MyList`: - -``` lean -@[aesop safe [constructors, cases]] -inductive NonEmpty : MyList α → Prop - | cons : NonEmpty (cons x xs) -``` - -Here we see the first proper Aesop feature: we use the **`@[aesop]`** attribute -to construct two Aesop rules related to the `NonEmpty` type. These rules are -added to a global rule set. When Aesop searches for a proof, it systematically -applies each available rule, then recursively searches for proofs of the -subgoals generated by the rule, and so on, building a search tree. A goal is -proved when Aesop applies a rule that generates no subgoals. - -In general, rules can be arbitrary tactics. But since you probably don't want to -write a tactic for every rule, the `aesop` attribute provides several **rule -builders** which construct common sorts of rules. In our example, we construct: - -- A **`constructors`** rule. This rule tries to apply each constructor of - `NonEmpty` whenever a goal has target `NonEmpty _`. -- A **`cases`** rule. This rule searches for hypotheses `h : NonEmpty _` and - performs case analysis on them (like the `cases` tactic). - -Both rules above are added as **safe** rules. When a safe rule succeeds on a -goal encountered during the proof search, it is applied and the goal is never -visited again. In other words, the search does not backtrack safe rules. We will -later see **unsafe** rules, which can backtrack. - -With these rules, we can prove a theorem about `NonEmpty` and `append`: - -``` lean -@[aesop unsafe 50% apply] -theorem nonEmpty_append₁ {xs : MyList α} ys : - NonEmpty xs → NonEmpty (xs ++ ys) := by - aesop -``` - -Aesop finds this proof in four steps: - -- A built-in rule introduces the hypothesis `h : NonEmpty xs`. By default, - Aesop's rule set contains a number of straightforward rules for handling the - logical connectives `→`, `∧`, `∨` and `¬` as well as the quantifiers `∀` and - `∃` and some other basic types. -- The `cases` rule for `NonEmpty` performs case analysis on `h`. -- The `simp` rule `cons_append`, which we added earlier, unfolds the `++` - operation. -- The `constructor` rule for `NonEmpty` applies `NonEmpty.cons`. - -If you want to see how Aesop proves your goal (or why it doesn't prove your -goal, or why it takes too long to prove your goal), you can enable tracing: - -``` lean -set_option trace.aesop true -``` - -This makes Aesop print out the steps it takes while searching for a proof. You -can also look at the search tree Aesop constructed by enabling the -`trace.aesop.finalTree` option. For more tracing options, type `set_option -trace.aesop` and see what auto-completion suggests. - -If, in the example above, you call `aesop?` instead, then Aesop prints a proof -script. At time of writing, it looks like this: - -``` lean -intro a -unhygienic aesop_cases a -simp_all only [cons_append] -apply MyList.NonEmpty.cons -``` - -With a bit of post-processing, you can use this script instead of the Aesop -call. This way you avoid the performance penalty of making Aesop search for a -proof over and over again. The proof script generation currently has some known -bugs, but it produces usable scripts most of the time. - -The `@[aesop]` attribute on `nonEmpty_append₁` adds this lemma as an **unsafe** -rule to the default rule set. For this rule we use the **`apply`** rule builder, -which generates a rule that tries to apply `nonEmpty_append₁` whenever the -target is of the form `NonEmpty (_ ++ _)`. - -Unsafe rules are rules which can backtrack, so after they have been applied to a -goal, Aesop may still try other rules to solve the same goal. This makes sense -for `nonEmpty_append₁`: if we have a goal `NonEmpty (xs ++ ys)`, we may prove it -either by showing `NonEmpty xs` (i.e., by applying `nonEmpty_append₁`) or by -showing `NonEmpty ys`. If `nonEmpty_append₁` were registered as a safe rule, we -would always choose `NonEmpty xs` and never investigate `NonEmpty ys`. - -Each unsafe rule is annotated with a **success probability**, here 50%. This is -a very rough estimate of how likely it is that the rule will to lead to a -successful proof. It is used to prioritise goals: the initial goal starts with a -priority of 100% and whenever we apply an unsafe rule, the priority of its -subgoals is the priority of its parent goal multiplied with the success -probability of the applied rule. So applying `nonEmpty_append₁` repeatedly would -give us goals with priority 50%, 25%, etc. Aesop always considers the -highest-priority unsolved goal first, so it prefers proof attempts involving few -and high-probability rules. Additionally, when Aesop has a choice between -multiple unsafe rules, it prefers the one with the highest success probability. -(Ties are broken arbitrarily but deterministically.) - -After adding `nonEmpty_append`, Aesop can prove some consequences of this -lemma: - -``` lean -example {α : Type u} {xs : MyList α} ys zs : - NonEmpty xs → NonEmpty (xs ++ ys ++ zs) := by - aesop -``` - -Next, we prove another simple theorem about `NonEmpty`: - -``` lean -theorem nil_not_nonEmpty (xs : MyList α) : xs = nil → ¬ NonEmpty xs := by - aesop (add 10% cases MyList, norm simp Not) -``` - -Here we add two rules in an **`add`** clause. These rules are not part of a -rule set but are added for this Aesop call only. - -The first rule is an unsafe `cases` rule for `MyList`. (As you can see, you can -leave out the `unsafe` keyword and specify only a success probability.) This -rule is dangerous: when we apply it to a hypothesis `xs : MyList α`, we get `x : -α` and `ys : MyList α`, so we can apply the `cases` rule again to `ys`, and so -on. We therefore give this rule a very low success probability, to make sure -that Aesop applies other rules if possible. - -We also add a **norm** or **normalisation** rule. As mentioned above, these -rules are used to normalise the goal before any other rules are applied. As part -of this normalisation process, we run a variant of `simp_all` with the global -`simp` set plus Aesop-specific `simp` lemmas. The **`simp`** builder adds such -an Aesop-specific `simp` lemma which unfolds the `Not` definition. (There is -also a built-in rule which performs the same unfolding, so this rule is -redundant.) - -Here are some other examples where normalisation comes in handy: - -``` lean -@[simp] -theorem append_nil {xs : MyList α} : - xs ++ nil = xs := by - induction xs <;> aesop - -theorem append_assoc {xs ys zs : MyList α} : - (xs ++ ys) ++ zs = xs ++ (ys ++ zs) := by - induction xs <;> aesop -``` - -Since we previously added unfolding lemmas for `append` to the global `simp` -set, Aesop can prove theorems about this function more or less by itself (though -in fact `simp_all` would already suffice.) However, we still need to perform -induction explicitly. This is a deliberate design choice: techniques for -automating induction exist, but they are complex, somewhat slow and not entirely -reliable, so we prefer to do it manually. - -Many more examples can be found in the `tests` folder of this repository. In -particular, the file `tests/run/List.lean` contains an Aesop-ified port of 200 -basic list lemmas from the Lean 3 version of mathlib. The file -`tests/run/SeqCalcProver.lean` shows how Aesop can help with the formalisation -of a simple sequent calculus prover. - -## Reference - -This section contains a systematic and fairly comprehensive account of how Aesop -operates. - -### Rules - -A rule is a tactic plus some associated metadata. Rules come in three flavours: - -- **Normalisation rules** (keyword `norm`) must generate zero or one subgoal. - (Zero means that the rule closed the goal). Each normalisation rule is - associated with an integer **penalty** (default 1). Normalisation rules are - applied in a fixpoint loop in order of penalty, lowest first. For rules with - equal penalties, the order is unspecified. See below for details on - the normalisation algorithm. - - Normalisation rules can also be simp lemmas. These are constructed with the - `simp` builder. They are used by a special `simp` call during - the normalisation process. - -- **Safe rules** (keyword `safe`) are applied after normalisation but before any - unsafe rules. When a safe rule is successfully applied to a goal, the goal - becomes *inactive*, meaning no other rules are considered for it. Like - normalisation rules, safe rules are associated with a penalty (default 1) - which determines the order in which the rules are tried. - - Safe rules should be provability-preserving, meaning that if a goal is - provable and we apply a safe rule to it, the generated subgoals should still - be provable. This is a less precise notion than it may appear since - what is provable depends on the entire Aesop rule set. - -- **Unsafe rules** (keyword `unsafe`) are tried only if all available safe rules - have failed on a goal. When an unsafe rule is applied to a goal, the goal is - not marked as inactive, so other (unsafe) rules may be applied to it. These - rule applications are considered independently until one of them proves the - goal (or until we've exhausted all available rules and determine that the goal - is not provable with the current rule set). - - Each unsafe rule has a **success probability** between 0% and 100%. These - probabilities are used to determine the priority of a goal. The initial goal - has priority 100% and whenever we apply an unsafe rule, the priorities of its - subgoals are the priority of the rule's parent goal times the rule's success - probability. Safe rules are treated as having 100% success probability. - -Rules can also be **multi-rules**. These are rules which add multiple rule -applications to a goal. For example, registering the constructors of the `Or` -type will generate a multi-rule that, given a goal with target `A ∨ B`, -generates one rule application with goal `A` and one with goal `B`. This is -equivalent to registering one rule for each constructor, but multi-rules can be -both slightly more efficient and slightly more natural. - -### Search Tree - -Aesop's central data structure is a search tree. This tree alternates between -two kinds of nodes: - -- **Goal nodes**: these nodes store a goal, plus metadata relevant to the - search. The parent and children of a goal node are rule application nodes. In - particular, each goal node has a **priority** between 0% and 100%. -- **Rule application ('rapp') nodes**: these goals store a rule (plus metadata). - The parent and children of a rapp node are goal nodes. When the search tree - contains a rapp node with rule `r`, parent `p` and children `c₁, ..., cₙ`, - this means that the tactic of rule `r` was applied to the goal of `p`, - generating the subgoals of the `cᵢ`. - -When a goal node has multiple child rapp nodes, we have a choice of how to solve -the goals. This makes the tree an AND-OR tree: to prove a rapp, *all* its child -goals must be proved; to prove a goal, *any* of its child rapps must be proved. - -### Search - -We start with a search tree containing a single goal node. This node's goal is -the goal which Aesop is supposed to solve. Then we perform the following steps -in a loop, stopping if (a) the root goal has been proved; (b) the root goal -becomes unprovable; or (c) one of Aesop's rule limits has been reached. (There -are configurable limits on, e.g., the total number of rules applied or the -search depth.) - -- Pick the highest-priority active goal node `G`. Roughly speaking, a goal node - is active if it is not proved and we haven't yet applied all possible rules to - it. -- If the goal of `G` has not been normalised yet, normalise it. That means we - run the following normalisation loop: - - Run the normalisation rules with negative penalty (lowest penalty first). If - any of these rules is successful, restart the normalisation loop with the - goal produced by the rule. - - Run `simp` on all hypotheses and the target, using the global simp set (i.e. - lemmas tagged `@[simp]`) plus Aesop's `simp` rules. - - Run the normalisation rules with positive penalty (lowest penalty first). - If any of these rules is successful, restart the normalisation loop. - - The loop ends when all normalisation rules fail. It destructively updates - the goal of `G` (and may prove it outright). -- If we haven't tried to apply the safe rules to the goal of `G` yet, try to - apply each safe rule (lowest penalty first). As soon as a rule succeeds, add - the corresponding rapp and child goals to the tree and mark `G` as inactive. - The child goals receive the same priority as `G`. -- Otherwise there is at least one unsafe rule that hasn't been tried on `G` yet - (or else `G` would have been inactive). Try the unsafe rule with the highest - success probability and if it succeeds, add the corresponding rapp and child - goals to the tree. The child goals receive the priority of `G` times the - success probability of the applied rule. - -A goal is **unprovable** if we have applied all possible rules to it and all -resulting child rapps are unprovable. A rapp is unprovable if any of its -subgoals is unprovable. - -During the search, a goal or rapp can also become **irrelevant**. This means -that we don't have to visit it again. Informally, goals and rapps are irrelevant -if they are part of a branch of the search tree which has either successfully -proved its goal already or which can never prove its goal. More formally: - -- A goal is irrelevant if its parent rapp is unprovable. (This means that a - sibling of the goal is already unprovable, in which case we know that the - parent rapp will never be proved.) -- A rapp is irrelevant if its parent goal is proved. (This means that a sibling - of the rapp is already proved, and we only need one proof.) -- A goal or rapp is irrelevant if any of its ancestors is irrelevant. - -### Rule Builders - -A **rule builder** is a metaprogram that turns a declaration or hypothesis into -an Aesop rule. Currently available builders are: - -- **`apply`**: generates a rule which tries to apply the given declaration or - hypothesis `x` to the target. The rule acts like the tactic `apply x`. -- **`forward`**: when applied to a declaration or hypothesis of type `A₁ → ... - Aₙ → B`, generates a rule which looks for hypotheses `h₁ : A₁`, ..., `hₙ : Aₙ` - in the goal and, if they are found, adds a new hypothesis `h : B`. As an - example, consider the lemma `even_or_odd`: - - ```lean - even_or_odd : ∀ (n : Nat), Even n ∨ Odd n - ``` - - Registering this as a forward rule will cause the goal - - ```lean - n : Nat - m : Nat - ⊢ T - ``` - - to be transformed into this: - - ```lean - n : Nat - hn : Even n ∨ Odd n - m : Nat - hm : Even m ∨ Odd m - ⊢ T - ``` - - The forward builder may also be given a list of *immediate names*: - - ``` - (forward (immediate := [n])) even_or_odd - ``` - - The immediate names, here `n`, refer to the arguments of `even_or_odd`. When - Aesop applies a forward rule with explicit immediate names, it only matches - the corresponding arguments to hypotheses. (Here, `even_or_odd` has only one - argument, so there is no difference.) - - When no immediate names are given, Aesop considers every argument immediate, - except for instance arguments and dependent arguments (i.e. those that can be - inferred from the types of later arguments). - - When a forward rule is successful, Aesop remembers the type of the hypothesis - added by the rule, say `T`. If a forward rule (possibly the same one) is - subsequently applied to a subgoal and wants to add another hypothesis of type - `T`, this is forbidden and the rule fails. Without this restriction, forward - rules would in many cases be applied infinitely often. However, note that the - rule is still executed on its own subgoals (and their subgoals, etc.), which - can become a performance issue. You should therefore prefer `destruct` rules - where possible. -- **`destruct`**: works like `forward`, but after the rule has been applied, - hypotheses that were used as immediate arguments are cleared. This is useful - when you want to eliminate a hypothesis. E.g. the rule - ``` - @[aesop norm destruct] - theorem and_elim_right : α ∧ β → α := ... - ``` - will cause the goal - ``` - h₁ : (α ∧ β) ∧ γ - h₂ : δ ∧ ε - ``` - to be transformed into - ``` - h₁ : α - h₂ : δ - ``` - - Unlike with `forward` rules, when an `destruct` rule is successfully applied, - it may be applied again to the resulting subgoals (and their subgoals, etc.). - There is less danger of infinite cycles because the original hypothesis is - cleared. - - However, if the hypothesis or hypotheses to which the `destruct` rule is - applied have dependencies, they are not cleared. In this case, you'll probably - get an infinite cycle. (TODO fix this.) -- **`constructors`**: when applied to an inductive type or structure `T`, - generates a rule which tries to apply each constructor of `T` to the target. - This is a multi-rule, so if multiple constructors apply, they are considered - in parallel. If you use this constructor to build an unsafe rule, each - constructor application receives the same success probability; if this is not - what you want, add separate `apply` rules for the constructors. -- **`cases`**: when applied to an inductive type or structure `T`, generates a - rule that performs case analysis on every hypothesis `h : T` in the context. - The rule recurses into subgoals, so `cases Or` will generate 6 goals when - applied to a goal with hypotheses `h₁ : A ∨ B ∨ C` and `h₂ : D ∨ E`. However, - if `T` is a recursive type (e.g. `List`), we only perform case analysis once - on each hypothesis. Otherwise we would loop infinitely. - - The `patterns` option can be used to apply the rule only on hypotheses of a - certain shape. E.g. the rule `(cases (patterns := [Fin 0])) Fin` will perform - case analysis only on hypotheses of type `Fin 0`. Patterns can contain - underscores, e.g. `0 ≤ _`. Multiple patterns can be given (separated by - commas); the rule is then applied whenever at least one of the patterns - matches a hypothesis. -- **`simp`**: when applied to an equation `eq : A₁ → ... Aₙ → x = y`, registers - `eq` as a simp lemma for the built-in simp pass during normalisation. As such, - this builder can only build normalisation rules. -- **`unfold`**: when applied to a definition or `let` hypothesis `f`, registers - `f` to be unfolded (i.e. replaced with its definition) during normalisation. - As such, this builder can only build normalisation rules. The unfolding - happens in a separate `simp` pass. - - The `simp` builder can also be used to unfold definitions. The difference is - that `simp` rules perform smart unfolding (like the `simp` tactic) and - `unfold` rules perform non-smart unfolding (like the `unfold` tactic). - Non-smart unfolding unfolds functions even when none of their equations - match, so `unfold` rules for recursive functions generally lead to looping. -- **`tactic`**: takes a tactic and directly turns it into a rule. The given - declaration (the builder does not work for hypotheses) must have type `TacticM - Unit`, `Aesop.SimpleRuleTac` or `Aesop.RuleTac`. The latter are Aesop data - types which associate a tactic with additional metadata; using them may allow - the rule to operate somewhat more efficiently. - - The builder may be given an option `uses_branch_state := ` (default - true). This indicates whether the given tactic uses the branch state; see - below. - - Rule tactics should not be 'no-ops': if a rule tactic is not applicable to a - goal, it should fail rather than return the goal unchanged. All no-op rules - waste time and no-op `norm` rules will send normalisation into an infinite - loop. - - Normalisation rules may not assign metavariables (other than the goal - metavariable) or introduce new metavariables (other than the new goal - metavariable). This can be a problem because some Lean tactics, e.g. `cases`, - do so even in cases where you probably would not expect them to. I'm afraid - there is currently no good solution for this. -- **`default`**: The default builder. This is the builder used when you - register a rule without specifying a builder, but you can also use it - explicitly. Depending on the rule's phase, the default builder tries - different builders, using the first one that works. These builders are: - - For `safe` and `unsafe` rules: `constructors`, `tactic`, `apply`. - - For `norm` rules: `constructors`, `tactic`, `simp`, `apply`. - -#### Transparency Options - -The rule builders `apply`, `forward`, `destruct`, `constructors` and `cases` -each have a `transparency` option. This option controls the transparency at -which the rule is executed. For example, registering a rule with the builder -`(apply (transparency := reducible))` makes the rule act like the tactic -`with_reducible apply`. - -However, even if you change the transparency of a rule, it is still indexed at -`reducible` transparency (since the data structure we use for indexing only -supports `reducible` transparency). So suppose you register an `apply` rule with -`default` transparency. Further suppose the rule concludes `A ∧ B` and your -target is `T` with `def T := A ∧ B`. Then the rule could apply to the target -since it can unfold `T` at `default` transparency to discover `A ∧ B`. However, -the rule is never applied because the indexing procedure sees only `T` and does -not consider the rule potentially applicable. - -To override this behaviour, you can write `(apply (transparency! := default))` -(note the bang). This disables indexing, so the rule is tried on every goal. - -### Rule Sets - -Rule sets are declared with the command - -``` lean -declare_aesop_rule_sets [r₁, ..., rₙ] -``` - -where the `rᵢ` are arbitrary names. To avoid clashes, pick names in the -namespace of your package. - -Within a rule set, rules are identified by their name, builder and phase -(safe/unsafe/norm). This means you can add the same declaration as multiple -rules with different builders or in different phases, but not with different -priorities or different builder options (if the rule's builder has any options). - -Rules can appear in multiple rule sets, but in this case you should make sure -that they have the same priority and use the same builder options. Otherwise, -Aesop will consider these rules the same and arbitrarily pick one. - -By default, the `aesop` tactic uses the `builtin` and `default` rule sets. The -`builtin` set contains built-in rules for handling various constructions (see -below). The `default` set contains rules which were added by Aesop users without -specifying a rule set. - -### The `@[aesop]` Attribute - -Declarations can be added to rule sets by annotating them with the `@[aesop]` -attribute. - -#### Single Rule - -In most cases, you'll want to add one rule for the declaration. The syntax for -this is - -``` lean -@[aesop ? ? ? ?] -``` - -where - -- `` is `safe`, `norm` or `unsafe`. Cannot be omitted except under the - conditions in the next bullets. - -- `` is: - - For `simp` rules, a natural number. This is used as the priority of the - `simp` generated `simp` lemmas, so registering a `simp` rule with priority - `n` is roughly equivalent to the attribute `@[simp n]`. If omitted, defaults - to Lean's default `simp` priority. - - For `safe` and `norm` rules (except `simp` rules), an integer penalty. If - omitted, defaults to 1. - - For `unsafe` rules, a percentage between 0% and 100%. Cannot be omitted. - You may omit the `unsafe` phase specification when giving a percentage. - - For `unfold` rules, a penalty can be given, but it is currently ignored. - -- `` is one of the builders given above. If you want to pass options to - a builder, write it like this (with mandatory parentheses): - - ```text - (tactic (uses_branch_state := true)) - ``` - - If no builder is specified, the default builder for the given phase is used. - Since the `simp` builder generates only normalisation rules, the `norm` phase - may be omitted. - -- `` is a clause of the form - - ```text - (rule_sets [r₁, ..., rₙ]) - ``` - - where the `rᵢ` are declared rule sets. (Parentheses are mandatory.) The rule - is added exactly to the specified rule sets. If this clause is omitted, it - defaults to `(rule_sets [default])`. - -#### Multiple Rules - -It is occasionally useful to add multiple rules for a single declaration, e.g. -a `cases` and a `constructors` rule for the same inductive type. In this case, -you can write for example - -``` lean -@[aesop unsafe [constructors 75%, cases 90%]] -inductive T ... - -@[aesop apply [safe (rule_sets [A]), 70% (rule_sets [B])]] -def foo ... - -@[aesop [80% apply, safe 5 (forward (immediate := x))]] -def bar (x : T) ... -``` - -In the first example, two unsafe rules for `T` are registered, one with success -probability 75% and one with 90%. - -In the second example, two rules are registered for `foo`. Both use the `apply` -builder. The first, a `safe` rule with default penalty, is added to rule set -`A`. The second, an `unsafe` rule with 70% success probability, is added to -rule set `B`. - -In the third example, two rules are registered for `bar`: an `unsafe` rule with -80% success probability using the `apply` builder and a `safe` rule with penalty -5 using the `forward` builder. - -In general, the grammar for the `@[aesop]` attribute is - -``` lean -attr ::= @[aesop ] - | @[aesop []] - -rule_expr ::= feature - | feature - | feature [] -``` - -where `feature` is a phase, priority, builder or `rule_sets` clause. This -grammar yields one or more trees of features and each branch of these trees -specifies one rule. (A branch is a list of features.) - -### Adding External Rules - -You can use the `attribute` command to add rules for constants which were -declared previously, either in your own development or in a package you import: - -``` -attribute [aesop norm unfold] List.all -- List.all is from Init -``` - -### Erasing Rules - -There are two ways to erase rules. Usually it suffices to remove the `@[aesop]` -attribute: - -``` lean -attribute [-aesop] foo -``` - -This will remove all rules associated with the declaration `foo` from all rule -sets. However, this erasing is not persistent, so the rule will reappear at the -end of the file. This is a fundamental limitation of Lean's attribute system: -once a declaration is tagged with an attribute, it cannot be permanently -untagged. - -If you want to remove only certain rules, you can use the `erase_aesop_rules` -command: - -``` lean -erase_aesop_rules [safe apply foo, bar (rule_sets [A])] -``` - -This will remove: - -- all safe rules for `foo` with the `apply` builder from all rule sets (but not -other, for example, unsafe rules or `forward` rules); -- all rules for `bar` from rule set `A`. - -In general, the syntax is - -``` lean -erase_aesop_rules [] -``` - -i.e. rules are specified in the same way as for the `@[aesop]` attribute. -However, each rule must also specify the name of the declaration whose rules -should be erased. The `rule_expr` grammar is therefore extended such that a -`feature` can also be the name of a declaration. - -Note that a rule added with one of the default builders (`safe_default`, -`norm_default`, `unsafe_default`) will be registered under the name of the -builder that is ultimately used, e.g. `apply` or `simp`. So if you want to erase -such a rule, you may have to specify that builder instead of the default -builder. - -### The `aesop` Tactic - -In its most basic form, you can call the Aesop tactic just by writing - -``` lean -example : α → α := by - aesop -``` - -This will use the rules in the `default` rule set (i.e. those added via the -attribute with no explicit rule set specified) and the rules in the `builtin` -rule set (i.e. those provided by Aesop itself). - -The tactic's behaviour can also be customised with various options. A more -involved Aesop call might look like this: - -``` text -aesop - (add safe foo, 10% cases Or, safe cases Empty) - (erase A, baz) - (rule_sets [A, B]) - (options := { maxRuleApplicationDepth := 10 }) -``` - -Here we add some rules with an `add` clause, erase other rules with an `erase` -clause, limit the used rule sets and set some options. Each of these clauses -is discussed in more detail below. - -#### Adding Rules to an Aesop Call - -Rules can be added to an Aesop call with an `add` clause. This won't affect any -declared rule sets. The syntax of the `add` clause is - -``` text -(add ) -``` - -i.e. rules can be specified in the same way as for the `@[aesop]` attribute. -As with the `erase_aesop_rules` command, each rule must specify the name of -declaration from which the rule should be built; for example - -``` text -(add safe [foo 1, bar 5]) -``` - -will add the declaration `foo` as a safe rule with penalty 1 and `bar` as a safe -rule with penalty 5. - -The rule names can also refer to hypotheses in the goal context, but not all -builders support this. - -#### Erasing Rules From an Aesop Call - -Rules can be removed from an Aesop call with an `erase` clause. Again, this -affects only the current Aesop call and not the declared rule sets. The syntax -of the `erase` clause is - -``` text -(erase ) -``` - -and it works exactly like the `erase_aesop_rules` command. To erase all rules -associated with `x` and `y`, write - -``` lean -(erase x, y) -``` - -#### Selecting Rule Sets - -By default, Aesop uses the `default` and `builtin` rule sets. A `rule_sets` -clause can be given to include additional rule sets, e.g. - -``` text -(rule_sets [A, B]) -``` - -This will use rule sets `A`, `B`, `default` and `builtin`. Rule sets can also -be disabled with `rule_sets [-default, -builtin]`. - -#### Setting Options - -Various options can be set with an `options` clause, whose syntax is: - -``` text -(options := ) -``` - -The term is an arbitrary Lean expression of type `Aesop.Options`; see there for -details. A notable option is `strategy`, which is one of `.bestFirst`, -`.depthFirst` and `.breadthFirst` and instructs Aesop to use the corresponding -search strategy. Best-first is the default. - -Similarly, options for the built-in norm simp call can be set with - -``` text -(simp_options := ) -``` - -The term has type `Aesop.SimpConfig`; see there for details. The `useHyps` -option may be particularly useful: when `true` (the default), norm simp behaves -like the `simp_all` tactic; when `false`, norm simp behaves like `simp at *`. - -### Built-In Rules - -The set of built-in rules (those in the `builtin` rule set) is currently quite -unstable, so for now I won't document them in detail. See -`Aesop/BuiltinRules.lean` and `Aesop/BuiltinRules/*.lean` - -### Proof Scripts - -By calling `aesop?` instead of `aesop`, you can instruct Aesop to generate a -tactic script which proves the goal (if Aesop succeeds). The script is printed -as a `Try this:` suggestion, similar to `simp?`. - -The scripts generated by Aesop are currently a bit idiosyncratic. For example, -they may contain the `aesop_cases` tactic, which is a slight variation of the -standard `cases`. Additionally, Aesop occasionally generates buggy scripts which -do not solve the goal. We hope to eventually fix these issues; until then, you -may have to lightly adjust the proof scripts by hand. - -### Tracing - -To see how Aesop proves a goal -- or why it doesn't prove a goal, or why it's -slow to prove a goal -- it is useful to see what it's doing. To that end, you -can enable various tracing options. These use the usual syntax, e.g. - -``` lean -set_option trace.aesop true -``` - -The main options are: - -- `trace.aesop`: print a step-by-step log of which goals Aesop tried to - solve, which rules it tried to apply (successfully or unsuccessfully), etc. -- `trace.aesop.ruleSet`: print the rule set used for an Aesop call. -- `trace.aesop.proof`: if Aesop is successful, print the proof that was - generated (as a Lean term). You should be able to copy-and-paste this proof - to replace Aesop. - -### Profiling - -To get an idea of where Aesop spends its time, use - -``` lean -set_option trace.aesop.profile true -``` - -Aesop then prints a summary of how much time its various tasks took. - -To get a more fine-grained picture, enable the `trace.aesop` and `profiler` -options. The trace is then augmented with information about how much time each -step took. Note that only the timing information pertaining to goal expansions -and rule applications is relevant. Other timings, such as those attached to new -rapps and goals, are just artefacts of the Lean tracing API. - -### Checking Internal Invariants - -If you encounter behaviour that looks like an internal error in Aesop, it may -help to set the option `aesop.check.all` (or the more fine-grained -`aesop.check.*` options). This makes Aesop check various invariants while the -tactic is running. These checks are somewhat expensive, so remember to unset the -option after you've reported the bug. - -### Handling Metavariables - -Rules which create metavariables must be handled specially by Aesop. For -example, suppose we register transitivity of `<` as an Aesop rule. Then we may -get a goal state of this form: - -``` lean -n k : Nat -⊢ n < ?m - -n k : Nat -⊢ ?m < k -``` - -We may now solve the first goal by applying different rules. We could, for -example, apply the theorem `∀ n, n < n + 1`. We could also use an assumption `n -< a`. Both proofs close the first goal, but crucially, they modify the second -goal: in the first case, it becomes `n + 1 < k`; in the second case, `a < k`. -And of course one of these could be provable while the other is not. In other -words, the second subgoal now depends on the *proof* of the first subgoal -(whereas usually we don't care *how* a goal was proven, only *that* it was -proven). Aesop could also decide to work on the second subgoal first, in which -case the situation is symmetric. - -Due to this dependency, Aesop in effect treats the instantiations of the second -subgoal as *additional goals*. Thus, when we apply the theorem `∀ n, n < n + 1`, -which closes the first goal, Aesop realises that because this theorem was -applied, we must now prove `n + 1 < k` as well. So it adds this goal as an -additional subgoal of the rule application `∀ n, n < n + 1` (which otherwise -would not have any subgoals). Similarly, when the assumption `n < a` is applied, -its rule application gains an additional subgoal `a < k`. - -This mechanism makes sure that we consider all potential proofs. The downside is -that it's quite explosive: when there are multiple metavariables in multiple -goals, which Aesop may visit in any order, Aesop may spend a lot of time copying -goals with shared metavariables. It may even try to prove the same goal more -than once since different rules may yield the same metavariable instantiations. -For these reasons, rules which create metavariables are best kept out of the -global rule set and added to individual Aesop calls on an ad-hoc basis. - -It is also worth noting that when a safe rule assigns a metavariable, it is -treated as an unsafe rule (with success probability 90%). This is because -assigning metavariables is almost never safe, for the same reason as above: the -usually perfectly safe rule `∀ n, n < n + 1` would, if treated as safe, force us -to commit to one particular instantiation of the metavariable `?m`. - -For more details on the handling of metavariables, see the [Aesop -paper](https://zenodo.org/record/7430233). diff --git a/Aesop/RuleTac/Tactic.lean b/Aesop/RuleTac/Tactic.lean index 91adabfc..5f766cd5 100644 --- a/Aesop/RuleTac/Tactic.lean +++ b/Aesop/RuleTac/Tactic.lean @@ -8,7 +8,6 @@ import Aesop.RuleTac.Basic open Lean open Lean.Meta -open Lean.Elab.Term (TermElabM withSynthesize) open Lean.Elab.Tactic (TacticM evalTactic run) namespace Aesop.RuleTac diff --git a/README.md b/README.md index 294ee13a..cac3f21d 100644 --- a/README.md +++ b/README.md @@ -1,41 +1,946 @@ -# [Temporarily disable LeanInfer cloud build] -# Aesop-LeanInfer +# Aesop -Aesop-LeanInfer is an enhanced version of [Aesop](https://github.com/JLimperg/aesop) (Automated Extensible Search for Obvious Proofs), a proof search tactic for Lean 4 similar to Isabelle's `auto`. In addition to the original Aesop, this version adds a new `RuleBuilder` and its corresponding `RuleTac`, which together enable fast plugin of machine learning models to assist with the proof search process, by seamlessly incorporating [LeanInfer](https://github.com/lean-dojo/LeanInfer)'s tactic suggestion feature into Aesop's workflow. +Aesop (Automated Extensible Search for Obvious Proofs) is a proof search tactic +for Lean 4. It is broadly similar to Isabelle's `auto`. In essence, Aesop works +like this: -This tool is in its alpha stage and we are actively working to further enhance it. It is based on an early version of LeanInfer, which will be enriched in the near future. We aim to always keep this tool updated with the latest LeanInfer and have it support more variations in machine learning models of choice and accompanying features. +- As with `simp`, you tag a (large) collection of definitions with the + `@[aesop]` attribute, registering them as Aesop _rules_. Rules can be + arbitrary tactics. We provide convenient ways to create common types of rules, + e.g. rules which apply a lemma. +- Aesop takes these rules and tries to apply each of them to the initial goal. + If a rule succeeds and generates subgoals, Aesop recursively applies the rules + to these subgoals, building a _search tree_. +- The search tree is explored in a _best-first_ manner. You can mark rules as + more or less likely to be useful. Based on this information, Aesop prioritises + the goals in the search tree, visiting more promising goals before less + promising ones. +- Before any rules are applied to a goal, it is _normalised_, using a special + (customisable) set of _normalisation rules_. An important built-in + normalisation rule runs `simp_all`, so your `@[simp]` lemmas are taken into + account by Aesop. +- Rules can be marked as _safe_ to optimise Aesop's performance. A safe rule is + applied eagerly and is never backtracked. For example, Aesop's built-in rules + safely split a goal `P ∧ Q` into goals for `P` and `Q`. After this split, the + original goal `P ∧ Q` is never revisited. +- Aesop provides a set of built-in rules which perform logical operations (e.g. + case-split on hypotheses `P ∨ Q`) and some other straightforward deductions. +- Aesop uses indexing methods similar to those of `simp` and other Lean tactics. + This means it should remain reasonably fast even with a large rule set. +- When called as `aesop?`, Aesop prints a tactic script that proves the goal, + similar to `simp?`. This way you can avoid the performance penalty of running + Aesop all the time. However, the script generation is currently not fully + reliable, so you may have to adjust the generated script. -## Requirements +Aesop should be suitable for two main use cases: -* Supported platforms: Linux and macOS (:warning: maybe also Windows WSL, but untested) -* [elan](https://github.com/leanprover/elan) -* [Git LFS](https://git-lfs.com/) +- General-purpose automation, where Aesop is used to dispatch 'trivial' goals. + Once mathlib is ported to Lean 4 and we have registered many lemmas as Aesop + rules, Aesop will hopefully serve as a much more powerful `simp`. +- Special-purpose automation, where specific Aesop rule sets are built to + address a certain class of goals. Tactics such as `measurability`, + `continuity` or `tidy`, which perform some sort of recursive search, can + hopefully be replaced by Aesop rule sets. + +I only occasionally update this README, so details may be out of date. If you +have questions, please create an issue or ping me (Jannis Limperg) on the [Lean +Zulip](https://leanprover.zulipchat.com). Pull requests are very welcome! + +There's also [a paper about Aesop](https://zenodo.org/record/7430233) which +covers many of the topics discussed here, sometimes in more detail. ## Building -A direct `lake build` in this directory should suffice. +With [elan](https://github.com/leanprover/elan) installed, `lake build` +should suffice. + +## Adding Aesop to Your Project + +To use Aesop in a Lean 4 project, first add this package as a dependency. In +your `lakefile.lean`, add + +```lean +require aesop from git "https://github.com/JLimperg/aesop" +``` + +You also need to make sure that your `lean-toolchain` file contains the same +version of Lean 4 as Aesop's, and that your versions of Aesop's dependencies +(currently only `std4`) match. We unfortunately can't support version ranges at +the moment. + +Now the following test file should compile: + +```lean +import Aesop + +example : α → α := + by aesop +``` + +## Quickstart + +To get you started, I'll explain Aesop's major concepts with a series of +examples. A more thorough, reference-style discussion follows in the next +section. + +We first define our own version of lists (so as not to clash with the standard +library) and an `append` function: + +``` lean +inductive MyList (α : Type _) + | nil + | cons (hd : α) (tl : MyList α) + +namespace MyList + +protected def append : (_ _ : MyList α) → MyList α + | nil, ys => ys + | cons x xs, ys => cons x (MyList.append xs ys) + +instance : Append (MyList α) := + ⟨MyList.append⟩ +``` + +We also tell `simp` to unfold applications of `append`: + +```lean +@[simp] +theorem nil_append : nil ++ xs = xs := rfl + +@[simp] +theorem cons_append : cons x xs ++ ys = cons x (xs ++ ys) := rfl +``` + +When Aesop first encounters a goal, it normalises it by running a customisable +set of normalisation rules. One such normalisation rule effectively runs +`simp_all`, so Aesop automatically takes `simp` lemmas into account. + +Now we define the `NonEmpty` predicate on `MyList`: + +``` lean +@[aesop safe [constructors, cases]] +inductive NonEmpty : MyList α → Prop + | cons : NonEmpty (cons x xs) +``` + +Here we see the first proper Aesop feature: we use the **`@[aesop]`** attribute +to construct two Aesop rules related to the `NonEmpty` type. These rules are +added to a global rule set. When Aesop searches for a proof, it systematically +applies each available rule, then recursively searches for proofs of the +subgoals generated by the rule, and so on, building a search tree. A goal is +proved when Aesop applies a rule that generates no subgoals. + +In general, rules can be arbitrary tactics. But since you probably don't want to +write a tactic for every rule, the `aesop` attribute provides several **rule +builders** which construct common sorts of rules. In our example, we construct: + +- A **`constructors`** rule. This rule tries to apply each constructor of + `NonEmpty` whenever a goal has target `NonEmpty _`. +- A **`cases`** rule. This rule searches for hypotheses `h : NonEmpty _` and + performs case analysis on them (like the `cases` tactic). + +Both rules above are added as **safe** rules. When a safe rule succeeds on a +goal encountered during the proof search, it is applied and the goal is never +visited again. In other words, the search does not backtrack safe rules. We will +later see **unsafe** rules, which can backtrack. + +With these rules, we can prove a theorem about `NonEmpty` and `append`: + +``` lean +@[aesop unsafe 50% apply] +theorem nonEmpty_append₁ {xs : MyList α} ys : + NonEmpty xs → NonEmpty (xs ++ ys) := by + aesop +``` + +Aesop finds this proof in four steps: + +- A built-in rule introduces the hypothesis `h : NonEmpty xs`. By default, + Aesop's rule set contains a number of straightforward rules for handling the + logical connectives `→`, `∧`, `∨` and `¬` as well as the quantifiers `∀` and + `∃` and some other basic types. +- The `cases` rule for `NonEmpty` performs case analysis on `h`. +- The `simp` rule `cons_append`, which we added earlier, unfolds the `++` + operation. +- The `constructor` rule for `NonEmpty` applies `NonEmpty.cons`. + +If you want to see how Aesop proves your goal (or why it doesn't prove your +goal, or why it takes too long to prove your goal), you can enable tracing: + +``` lean +set_option trace.aesop true +``` + +This makes Aesop print out the steps it takes while searching for a proof. You +can also look at the search tree Aesop constructed by enabling the +`trace.aesop.finalTree` option. For more tracing options, type `set_option +trace.aesop` and see what auto-completion suggests. + +If, in the example above, you call `aesop?` instead, then Aesop prints a proof +script. At time of writing, it looks like this: + +``` lean +intro a +unhygienic aesop_cases a +simp_all only [cons_append] +apply MyList.NonEmpty.cons +``` + +With a bit of post-processing, you can use this script instead of the Aesop +call. This way you avoid the performance penalty of making Aesop search for a +proof over and over again. The proof script generation currently has some known +bugs, but it produces usable scripts most of the time. + +The `@[aesop]` attribute on `nonEmpty_append₁` adds this lemma as an **unsafe** +rule to the default rule set. For this rule we use the **`apply`** rule builder, +which generates a rule that tries to apply `nonEmpty_append₁` whenever the +target is of the form `NonEmpty (_ ++ _)`. + +Unsafe rules are rules which can backtrack, so after they have been applied to a +goal, Aesop may still try other rules to solve the same goal. This makes sense +for `nonEmpty_append₁`: if we have a goal `NonEmpty (xs ++ ys)`, we may prove it +either by showing `NonEmpty xs` (i.e., by applying `nonEmpty_append₁`) or by +showing `NonEmpty ys`. If `nonEmpty_append₁` were registered as a safe rule, we +would always choose `NonEmpty xs` and never investigate `NonEmpty ys`. + +Each unsafe rule is annotated with a **success probability**, here 50%. This is +a very rough estimate of how likely it is that the rule will to lead to a +successful proof. It is used to prioritise goals: the initial goal starts with a +priority of 100% and whenever we apply an unsafe rule, the priority of its +subgoals is the priority of its parent goal multiplied with the success +probability of the applied rule. So applying `nonEmpty_append₁` repeatedly would +give us goals with priority 50%, 25%, etc. Aesop always considers the +highest-priority unsolved goal first, so it prefers proof attempts involving few +and high-probability rules. Additionally, when Aesop has a choice between +multiple unsafe rules, it prefers the one with the highest success probability. +(Ties are broken arbitrarily but deterministically.) + +After adding `nonEmpty_append`, Aesop can prove some consequences of this +lemma: + +``` lean +example {α : Type u} {xs : MyList α} ys zs : + NonEmpty xs → NonEmpty (xs ++ ys ++ zs) := by + aesop +``` + +Next, we prove another simple theorem about `NonEmpty`: + +``` lean +theorem nil_not_nonEmpty (xs : MyList α) : xs = nil → ¬ NonEmpty xs := by + aesop (add 10% cases MyList, norm simp Not) +``` + +Here we add two rules in an **`add`** clause. These rules are not part of a +rule set but are added for this Aesop call only. + +The first rule is an unsafe `cases` rule for `MyList`. (As you can see, you can +leave out the `unsafe` keyword and specify only a success probability.) This +rule is dangerous: when we apply it to a hypothesis `xs : MyList α`, we get `x : +α` and `ys : MyList α`, so we can apply the `cases` rule again to `ys`, and so +on. We therefore give this rule a very low success probability, to make sure +that Aesop applies other rules if possible. + +We also add a **norm** or **normalisation** rule. As mentioned above, these +rules are used to normalise the goal before any other rules are applied. As part +of this normalisation process, we run a variant of `simp_all` with the global +`simp` set plus Aesop-specific `simp` lemmas. The **`simp`** builder adds such +an Aesop-specific `simp` lemma which unfolds the `Not` definition. (There is +also a built-in rule which performs the same unfolding, so this rule is +redundant.) + +Here are some other examples where normalisation comes in handy: + +``` lean +@[simp] +theorem append_nil {xs : MyList α} : + xs ++ nil = xs := by + induction xs <;> aesop + +theorem append_assoc {xs ys zs : MyList α} : + (xs ++ ys) ++ zs = xs ++ (ys ++ zs) := by + induction xs <;> aesop +``` + +Since we previously added unfolding lemmas for `append` to the global `simp` +set, Aesop can prove theorems about this function more or less by itself (though +in fact `simp_all` would already suffice.) However, we still need to perform +induction explicitly. This is a deliberate design choice: techniques for +automating induction exist, but they are complex, somewhat slow and not entirely +reliable, so we prefer to do it manually. + +Many more examples can be found in the `tests` folder of this repository. In +particular, the file `tests/run/List.lean` contains an Aesop-ified port of 200 +basic list lemmas from the Lean 3 version of mathlib. The file +`tests/run/SeqCalcProver.lean` shows how Aesop can help with the formalisation +of a simple sequent calculus prover. + +## Reference + +This section contains a systematic and fairly comprehensive account of how Aesop +operates. + +### Rules + +A rule is a tactic plus some associated metadata. Rules come in three flavours: + +- **Normalisation rules** (keyword `norm`) must generate zero or one subgoal. + (Zero means that the rule closed the goal). Each normalisation rule is + associated with an integer **penalty** (default 1). Normalisation rules are + applied in a fixpoint loop in order of penalty, lowest first. For rules with + equal penalties, the order is unspecified. See below for details on + the normalisation algorithm. + + Normalisation rules can also be simp lemmas. These are constructed with the + `simp` builder. They are used by a special `simp` call during + the normalisation process. + +- **Safe rules** (keyword `safe`) are applied after normalisation but before any + unsafe rules. When a safe rule is successfully applied to a goal, the goal + becomes *inactive*, meaning no other rules are considered for it. Like + normalisation rules, safe rules are associated with a penalty (default 1) + which determines the order in which the rules are tried. + + Safe rules should be provability-preserving, meaning that if a goal is + provable and we apply a safe rule to it, the generated subgoals should still + be provable. This is a less precise notion than it may appear since + what is provable depends on the entire Aesop rule set. + +- **Unsafe rules** (keyword `unsafe`) are tried only if all available safe rules + have failed on a goal. When an unsafe rule is applied to a goal, the goal is + not marked as inactive, so other (unsafe) rules may be applied to it. These + rule applications are considered independently until one of them proves the + goal (or until we've exhausted all available rules and determine that the goal + is not provable with the current rule set). + + Each unsafe rule has a **success probability** between 0% and 100%. These + probabilities are used to determine the priority of a goal. The initial goal + has priority 100% and whenever we apply an unsafe rule, the priorities of its + subgoals are the priority of the rule's parent goal times the rule's success + probability. Safe rules are treated as having 100% success probability. + +Rules can also be **multi-rules**. These are rules which add multiple rule +applications to a goal. For example, registering the constructors of the `Or` +type will generate a multi-rule that, given a goal with target `A ∨ B`, +generates one rule application with goal `A` and one with goal `B`. This is +equivalent to registering one rule for each constructor, but multi-rules can be +both slightly more efficient and slightly more natural. + +### Search Tree + +Aesop's central data structure is a search tree. This tree alternates between +two kinds of nodes: + +- **Goal nodes**: these nodes store a goal, plus metadata relevant to the + search. The parent and children of a goal node are rule application nodes. In + particular, each goal node has a **priority** between 0% and 100%. +- **Rule application ('rapp') nodes**: these goals store a rule (plus metadata). + The parent and children of a rapp node are goal nodes. When the search tree + contains a rapp node with rule `r`, parent `p` and children `c₁, ..., cₙ`, + this means that the tactic of rule `r` was applied to the goal of `p`, + generating the subgoals of the `cᵢ`. + +When a goal node has multiple child rapp nodes, we have a choice of how to solve +the goals. This makes the tree an AND-OR tree: to prove a rapp, *all* its child +goals must be proved; to prove a goal, *any* of its child rapps must be proved. + +### Search + +We start with a search tree containing a single goal node. This node's goal is +the goal which Aesop is supposed to solve. Then we perform the following steps +in a loop, stopping if (a) the root goal has been proved; (b) the root goal +becomes unprovable; or (c) one of Aesop's rule limits has been reached. (There +are configurable limits on, e.g., the total number of rules applied or the +search depth.) + +- Pick the highest-priority active goal node `G`. Roughly speaking, a goal node + is active if it is not proved and we haven't yet applied all possible rules to + it. +- If the goal of `G` has not been normalised yet, normalise it. That means we + run the following normalisation loop: + - Run the normalisation rules with negative penalty (lowest penalty first). If + any of these rules is successful, restart the normalisation loop with the + goal produced by the rule. + - Run `simp` on all hypotheses and the target, using the global simp set (i.e. + lemmas tagged `@[simp]`) plus Aesop's `simp` rules. + - Run the normalisation rules with positive penalty (lowest penalty first). + If any of these rules is successful, restart the normalisation loop. + + The loop ends when all normalisation rules fail. It destructively updates + the goal of `G` (and may prove it outright). +- If we haven't tried to apply the safe rules to the goal of `G` yet, try to + apply each safe rule (lowest penalty first). As soon as a rule succeeds, add + the corresponding rapp and child goals to the tree and mark `G` as inactive. + The child goals receive the same priority as `G`. +- Otherwise there is at least one unsafe rule that hasn't been tried on `G` yet + (or else `G` would have been inactive). Try the unsafe rule with the highest + success probability and if it succeeds, add the corresponding rapp and child + goals to the tree. The child goals receive the priority of `G` times the + success probability of the applied rule. + +A goal is **unprovable** if we have applied all possible rules to it and all +resulting child rapps are unprovable. A rapp is unprovable if any of its +subgoals is unprovable. + +During the search, a goal or rapp can also become **irrelevant**. This means +that we don't have to visit it again. Informally, goals and rapps are irrelevant +if they are part of a branch of the search tree which has either successfully +proved its goal already or which can never prove its goal. More formally: + +- A goal is irrelevant if its parent rapp is unprovable. (This means that a + sibling of the goal is already unprovable, in which case we know that the + parent rapp will never be proved.) +- A rapp is irrelevant if its parent goal is proved. (This means that a sibling + of the rapp is already proved, and we only need one proof.) +- A goal or rapp is irrelevant if any of its ancestors is irrelevant. + +### Rule Builders + +A **rule builder** is a metaprogram that turns a declaration or hypothesis into +an Aesop rule. Currently available builders are: + +- **`apply`**: generates a rule which tries to apply the given declaration or + hypothesis `x` to the target. The rule acts like the tactic `apply x`. +- **`forward`**: when applied to a declaration or hypothesis of type `A₁ → ... + Aₙ → B`, generates a rule which looks for hypotheses `h₁ : A₁`, ..., `hₙ : Aₙ` + in the goal and, if they are found, adds a new hypothesis `h : B`. As an + example, consider the lemma `even_or_odd`: + + ```lean + even_or_odd : ∀ (n : Nat), Even n ∨ Odd n + ``` + + Registering this as a forward rule will cause the goal + + ```lean + n : Nat + m : Nat + ⊢ T + ``` + + to be transformed into this: + + ```lean + n : Nat + hn : Even n ∨ Odd n + m : Nat + hm : Even m ∨ Odd m + ⊢ T + ``` + + The forward builder may also be given a list of *immediate names*: + + ``` + (forward (immediate := [n])) even_or_odd + ``` + + The immediate names, here `n`, refer to the arguments of `even_or_odd`. When + Aesop applies a forward rule with explicit immediate names, it only matches + the corresponding arguments to hypotheses. (Here, `even_or_odd` has only one + argument, so there is no difference.) + + When no immediate names are given, Aesop considers every argument immediate, + except for instance arguments and dependent arguments (i.e. those that can be + inferred from the types of later arguments). + + When a forward rule is successful, Aesop remembers the type of the hypothesis + added by the rule, say `T`. If a forward rule (possibly the same one) is + subsequently applied to a subgoal and wants to add another hypothesis of type + `T`, this is forbidden and the rule fails. Without this restriction, forward + rules would in many cases be applied infinitely often. However, note that the + rule is still executed on its own subgoals (and their subgoals, etc.), which + can become a performance issue. You should therefore prefer `destruct` rules + where possible. +- **`destruct`**: works like `forward`, but after the rule has been applied, + hypotheses that were used as immediate arguments are cleared. This is useful + when you want to eliminate a hypothesis. E.g. the rule + ``` + @[aesop norm destruct] + theorem and_elim_right : α ∧ β → α := ... + ``` + will cause the goal + ``` + h₁ : (α ∧ β) ∧ γ + h₂ : δ ∧ ε + ``` + to be transformed into + ``` + h₁ : α + h₂ : δ + ``` + + Unlike with `forward` rules, when an `destruct` rule is successfully applied, + it may be applied again to the resulting subgoals (and their subgoals, etc.). + There is less danger of infinite cycles because the original hypothesis is + cleared. + + However, if the hypothesis or hypotheses to which the `destruct` rule is + applied have dependencies, they are not cleared. In this case, you'll probably + get an infinite cycle. (TODO fix this.) +- **`constructors`**: when applied to an inductive type or structure `T`, + generates a rule which tries to apply each constructor of `T` to the target. + This is a multi-rule, so if multiple constructors apply, they are considered + in parallel. If you use this constructor to build an unsafe rule, each + constructor application receives the same success probability; if this is not + what you want, add separate `apply` rules for the constructors. +- **`cases`**: when applied to an inductive type or structure `T`, generates a + rule that performs case analysis on every hypothesis `h : T` in the context. + The rule recurses into subgoals, so `cases Or` will generate 6 goals when + applied to a goal with hypotheses `h₁ : A ∨ B ∨ C` and `h₂ : D ∨ E`. However, + if `T` is a recursive type (e.g. `List`), we only perform case analysis once + on each hypothesis. Otherwise we would loop infinitely. + + The `patterns` option can be used to apply the rule only on hypotheses of a + certain shape. E.g. the rule `(cases (patterns := [Fin 0])) Fin` will perform + case analysis only on hypotheses of type `Fin 0`. Patterns can contain + underscores, e.g. `0 ≤ _`. Multiple patterns can be given (separated by + commas); the rule is then applied whenever at least one of the patterns + matches a hypothesis. +- **`simp`**: when applied to an equation `eq : A₁ → ... Aₙ → x = y`, registers + `eq` as a simp lemma for the built-in simp pass during normalisation. As such, + this builder can only build normalisation rules. +- **`unfold`**: when applied to a definition or `let` hypothesis `f`, registers + `f` to be unfolded (i.e. replaced with its definition) during normalisation. + As such, this builder can only build normalisation rules. The unfolding + happens in a separate `simp` pass. + + The `simp` builder can also be used to unfold definitions. The difference is + that `simp` rules perform smart unfolding (like the `simp` tactic) and + `unfold` rules perform non-smart unfolding (like the `unfold` tactic). + Non-smart unfolding unfolds functions even when none of their equations + match, so `unfold` rules for recursive functions generally lead to looping. +- **`tactic`**: takes a tactic and directly turns it into a rule. The given + declaration (the builder does not work for hypotheses) must have type `TacticM + Unit`, `Aesop.SimpleRuleTac` or `Aesop.RuleTac`. The latter are Aesop data + types which associate a tactic with additional metadata; using them may allow + the rule to operate somewhat more efficiently. + + The builder may be given an option `uses_branch_state := ` (default + true). This indicates whether the given tactic uses the branch state; see + below. + + Rule tactics should not be 'no-ops': if a rule tactic is not applicable to a + goal, it should fail rather than return the goal unchanged. All no-op rules + waste time and no-op `norm` rules will send normalisation into an infinite + loop. + + Normalisation rules may not assign metavariables (other than the goal + metavariable) or introduce new metavariables (other than the new goal + metavariable). This can be a problem because some Lean tactics, e.g. `cases`, + do so even in cases where you probably would not expect them to. I'm afraid + there is currently no good solution for this. +- **`default`**: The default builder. This is the builder used when you + register a rule without specifying a builder, but you can also use it + explicitly. Depending on the rule's phase, the default builder tries + different builders, using the first one that works. These builders are: + - For `safe` and `unsafe` rules: `constructors`, `tactic`, `apply`. + - For `norm` rules: `constructors`, `tactic`, `simp`, `apply`. + +#### Transparency Options + +The rule builders `apply`, `forward`, `destruct`, `constructors` and `cases` +each have a `transparency` option. This option controls the transparency at +which the rule is executed. For example, registering a rule with the builder +`(apply (transparency := reducible))` makes the rule act like the tactic +`with_reducible apply`. + +However, even if you change the transparency of a rule, it is still indexed at +`reducible` transparency (since the data structure we use for indexing only +supports `reducible` transparency). So suppose you register an `apply` rule with +`default` transparency. Further suppose the rule concludes `A ∧ B` and your +target is `T` with `def T := A ∧ B`. Then the rule could apply to the target +since it can unfold `T` at `default` transparency to discover `A ∧ B`. However, +the rule is never applied because the indexing procedure sees only `T` and does +not consider the rule potentially applicable. + +To override this behaviour, you can write `(apply (transparency! := default))` +(note the bang). This disables indexing, so the rule is tried on every goal. + +### Rule Sets + +Rule sets are declared with the command + +``` lean +declare_aesop_rule_sets [r₁, ..., rₙ] (default := ) +``` + +where the `rᵢ` are arbitrary names. To avoid clashes, pick names in the +namespace of your package. Setting `default := true` makes the rule set active +by default. The `default` clause can be omitted and defaults to `false`. + +Within a rule set, rules are identified by their name, builder and phase +(safe/unsafe/norm). This means you can add the same declaration as multiple +rules with different builders or in different phases, but not with different +priorities or different builder options (if the rule's builder has any options). + +Rules can appear in multiple rule sets, but in this case you should make sure +that they have the same priority and use the same builder options. Otherwise, +Aesop will consider these rules the same and arbitrarily pick one. + +Out of the box, Aesop uses the default rule sets `builtin`, `default` and +`local`. The `builtin` set contains built-in rules for handling various +constructions (see below). The `default` set contains rules which were added by +Aesop users without specifying a rule set. The `local` set contains rules from +`(add ...)` clauses. + +### The `@[aesop]` Attribute + +Declarations can be added to rule sets by annotating them with the `@[aesop]` +attribute. + +#### Single Rule + +In most cases, you'll want to add one rule for the declaration. The syntax for +this is + +``` lean +@[aesop ? ? ? ?] +``` + +where + +- `` is `safe`, `norm` or `unsafe`. Cannot be omitted except under the + conditions in the next bullets. + +- `` is: + - For `simp` rules, a natural number. This is used as the priority of the + `simp` generated `simp` lemmas, so registering a `simp` rule with priority + `n` is roughly equivalent to the attribute `@[simp n]`. If omitted, defaults + to Lean's default `simp` priority. + - For `safe` and `norm` rules (except `simp` rules), an integer penalty. If + omitted, defaults to 1. + - For `unsafe` rules, a percentage between 0% and 100%. Cannot be omitted. + You may omit the `unsafe` phase specification when giving a percentage. + - For `unfold` rules, a penalty can be given, but it is currently ignored. + +- `` is one of the builders given above. If you want to pass options to + a builder, write it like this (with mandatory parentheses): + + ```text + (tactic (uses_branch_state := true)) + ``` + + If no builder is specified, the default builder for the given phase is used. + Since the `simp` builder generates only normalisation rules, the `norm` phase + may be omitted. + +- `` is a clause of the form + + ```text + (rule_sets [r₁, ..., rₙ]) + ``` + + where the `rᵢ` are declared rule sets. (Parentheses are mandatory.) The rule + is added exactly to the specified rule sets. If this clause is omitted, it + defaults to `(rule_sets [default])`. + +#### Multiple Rules + +It is occasionally useful to add multiple rules for a single declaration, e.g. +a `cases` and a `constructors` rule for the same inductive type. In this case, +you can write for example + +``` lean +@[aesop unsafe [constructors 75%, cases 90%]] +inductive T ... + +@[aesop apply [safe (rule_sets [A]), 70% (rule_sets [B])]] +def foo ... + +@[aesop [80% apply, safe 5 (forward (immediate := x))]] +def bar (x : T) ... +``` + +In the first example, two unsafe rules for `T` are registered, one with success +probability 75% and one with 90%. + +In the second example, two rules are registered for `foo`. Both use the `apply` +builder. The first, a `safe` rule with default penalty, is added to rule set +`A`. The second, an `unsafe` rule with 70% success probability, is added to +rule set `B`. + +In the third example, two rules are registered for `bar`: an `unsafe` rule with +80% success probability using the `apply` builder and a `safe` rule with penalty +5 using the `forward` builder. + +In general, the grammar for the `@[aesop]` attribute is + +``` lean +attr ::= @[aesop ] + | @[aesop []] + +rule_expr ::= feature + | feature + | feature [] +``` + +where `feature` is a phase, priority, builder or `rule_sets` clause. This +grammar yields one or more trees of features and each branch of these trees +specifies one rule. (A branch is a list of features.) + +### Adding External Rules + +You can use the `attribute` command to add rules for constants which were +declared previously, either in your own development or in a package you import: + +``` +attribute [aesop norm unfold] List.all -- List.all is from Init +``` + +### Erasing Rules + +There are two ways to erase rules. Usually it suffices to remove the `@[aesop]` +attribute: + +``` lean +attribute [-aesop] foo +``` + +This will remove all rules associated with the declaration `foo` from all rule +sets. However, this erasing is not persistent, so the rule will reappear at the +end of the file. This is a fundamental limitation of Lean's attribute system: +once a declaration is tagged with an attribute, it cannot be permanently +untagged. + +If you want to remove only certain rules, you can use the `erase_aesop_rules` +command: + +``` lean +erase_aesop_rules [safe apply foo, bar (rule_sets [A])] +``` + +This will remove: + +- all safe rules for `foo` with the `apply` builder from all rule sets (but not +other, for example, unsafe rules or `forward` rules); +- all rules for `bar` from rule set `A`. + +In general, the syntax is + +``` lean +erase_aesop_rules [] +``` + +i.e. rules are specified in the same way as for the `@[aesop]` attribute. +However, each rule must also specify the name of the declaration whose rules +should be erased. The `rule_expr` grammar is therefore extended such that a +`feature` can also be the name of a declaration. + +Note that a rule added with one of the default builders (`safe_default`, +`norm_default`, `unsafe_default`) will be registered under the name of the +builder that is ultimately used, e.g. `apply` or `simp`. So if you want to erase +such a rule, you may have to specify that builder instead of the default +builder. + +### The `aesop` Tactic + +In its most basic form, you can call the Aesop tactic just by writing + +``` lean +example : α → α := by + aesop +``` + +This will use the rules in the `default` rule set (i.e. those added via the +attribute with no explicit rule set specified) and the rules in the `builtin` +rule set (i.e. those provided by Aesop itself). + +The tactic's behaviour can also be customised with various options. A more +involved Aesop call might look like this: + +``` text +aesop + (add safe foo, 10% cases Or, safe cases Empty) + (erase A, baz) + (rule_sets [A, B]) + (options := { maxRuleApplicationDepth := 10 }) +``` + +Here we add some rules with an `add` clause, erase other rules with an `erase` +clause, limit the used rule sets and set some options. Each of these clauses +is discussed in more detail below. + +#### Adding Rules to an Aesop Call + +Rules can be added to an Aesop call with an `add` clause. This won't affect any +declared rule sets. The syntax of the `add` clause is + +``` text +(add ) +``` + +i.e. rules can be specified in the same way as for the `@[aesop]` attribute. +As with the `erase_aesop_rules` command, each rule must specify the name of +declaration from which the rule should be built; for example + +``` text +(add safe [foo 1, bar 5]) +``` + +will add the declaration `foo` as a safe rule with penalty 1 and `bar` as a safe +rule with penalty 5. + +The rule names can also refer to hypotheses in the goal context, but not all +builders support this. + +#### Erasing Rules From an Aesop Call + +Rules can be removed from an Aesop call with an `erase` clause. Again, this +affects only the current Aesop call and not the declared rule sets. The syntax +of the `erase` clause is + +``` text +(erase ) +``` + +and it works exactly like the `erase_aesop_rules` command. To erase all rules +associated with `x` and `y`, write + +``` lean +(erase x, y) +``` + +#### Selecting Rule Sets + +By default, Aesop uses the `default` and `builtin` rule sets. A `rule_sets` +clause can be given to include additional rule sets, e.g. + +``` text +(rule_sets [A, B]) +``` + +This will use rule sets `A`, `B`, `default` and `builtin`. Rule sets can also +be disabled with `rule_sets [-default, -builtin]`. + +#### Setting Options + +Various options can be set with an `options` clause, whose syntax is: + +``` text +(options := ) +``` + +The term is an arbitrary Lean expression of type `Aesop.Options`; see there for +details. A notable option is `strategy`, which is one of `.bestFirst`, +`.depthFirst` and `.breadthFirst` and instructs Aesop to use the corresponding +search strategy. Best-first is the default. + +Similarly, options for the built-in norm simp call can be set with + +``` text +(simp_options := ) +``` + +The term has type `Aesop.SimpConfig`; see there for details. The `useHyps` +option may be particularly useful: when `true` (the default), norm simp behaves +like the `simp_all` tactic; when `false`, norm simp behaves like `simp at *`. + +### Built-In Rules + +The set of built-in rules (those in the `builtin` rule set) is currently quite +unstable, so for now I won't document them in detail. See +`Aesop/BuiltinRules.lean` and `Aesop/BuiltinRules/*.lean` + +### Proof Scripts + +By calling `aesop?` instead of `aesop`, you can instruct Aesop to generate a +tactic script which proves the goal (if Aesop succeeds). The script is printed +as a `Try this:` suggestion, similar to `simp?`. + +The scripts generated by Aesop are currently a bit idiosyncratic. For example, +they may contain the `aesop_cases` tactic, which is a slight variation of the +standard `cases`. Additionally, Aesop occasionally generates buggy scripts which +do not solve the goal. We hope to eventually fix these issues; until then, you +may have to lightly adjust the proof scripts by hand. + +### Tracing + +To see how Aesop proves a goal -- or why it doesn't prove a goal, or why it's +slow to prove a goal -- it is useful to see what it's doing. To that end, you +can enable various tracing options. These use the usual syntax, e.g. + +``` lean +set_option trace.aesop true +``` + +The main options are: + +- `trace.aesop`: print a step-by-step log of which goals Aesop tried to + solve, which rules it tried to apply (successfully or unsuccessfully), etc. +- `trace.aesop.ruleSet`: print the rule set used for an Aesop call. +- `trace.aesop.proof`: if Aesop is successful, print the proof that was + generated (as a Lean term). You should be able to copy-and-paste this proof + to replace Aesop. + +### Profiling + +To get an idea of where Aesop spends its time, use + +``` lean +set_option trace.aesop.profile true +``` + +Aesop then prints a summary of how much time its various tasks took. + +To get a more fine-grained picture, enable the `trace.aesop` and `profiler` +options. The trace is then augmented with information about how much time each +step took. Note that only the timing information pertaining to goal expansions +and rule applications is relevant. Other timings, such as those attached to new +rapps and goals, are just artefacts of the Lean tracing API. + +### Checking Internal Invariants -To quickly test its success, write a simple theorem and try to prove it `by aesop`. If the goal is closed (i.e., `No goals` displayed in the InfoView), `aesop` is likely to have been properly built. Then replace `by aesop` with `by suggest_tactics`. If a list of tactics is shown under `Tactic suggestions` in the InfoView while the goal is not closed, the LeanInfer part is successfully built as well. For the first time, should it ask you to download the model by running `suggest_tactics!`, following it will automatically download the model to `~/.cache/lean_infer/` by default, with the path overridable by setting the `LEAN_INFER_CACHE_DIR` environment variable. A simple guide of this testing process is available [here](./AesopTest/NeuralCheck.lean) as well. +If you encounter behaviour that looks like an internal error in Aesop, it may +help to set the option `aesop.check.all` (or the more fine-grained +`aesop.check.*` options). This makes Aesop check various invariants while the +tactic is running. These checks are somewhat expensive, so remember to unset the +option after you've reported the bug. -## Usage +### Handling Metavariables -Users can opt to add a new rule that calls a pre-trained machine learning model under the hood, by simply defining a structure consisting of a model name and a set of hyperparameters (all optional, if any of them is not specified by the users, built-in default settings automatically apply), and then annotating it with our new rule builder `neural`. See [here](./AesopTest/NeuralProver.lean) for a quick example where the model is specified by the user while hyperparameters are not (thus inheriting the default settings). +Rules which create metavariables must be handled specially by Aesop. For +example, suppose we register transitivity of `<` as an Aesop rule. Then we may +get a goal state of this form: -Note that we always allow the users to choose using the machine learning power or not, as it can be easily turned on/off by adding such a new rule or sticking to the raw Aesop. +``` lean +n k : Nat +⊢ n < ?m -## Questions and Bugs +n k : Nat +⊢ ?m < k +``` -* For general questions and discussions, please use [GitHub Discussions](https://github.com/Peiyang-Song/aesop/discussions). -* To report a potential bug, please open an issue. In the issue, please include your OS information and the exact steps to reproduce the error. The more details you provide, the better we will be able to help you. +We may now solve the first goal by applying different rules. We could, for +example, apply the theorem `∀ n, n < n + 1`. We could also use an assumption `n +< a`. Both proofs close the first goal, but crucially, they modify the second +goal: in the first case, it becomes `n + 1 < k`; in the second case, `a < k`. +And of course one of these could be provable while the other is not. In other +words, the second subgoal now depends on the *proof* of the first subgoal +(whereas usually we don't care *how* a goal was proven, only *that* it was +proven). Aesop could also decide to work on the second subgoal first, in which +case the situation is symmetric. -## Related Links +Due to this dependency, Aesop in effect treats the instantiations of the second +subgoal as *additional goals*. Thus, when we apply the theorem `∀ n, n < n + 1`, +which closes the first goal, Aesop realises that because this theorem was +applied, we must now prove `n + 1 < k` as well. So it adds this goal as an +additional subgoal of the rule application `∀ n, n < n + 1` (which otherwise +would not have any subgoals). Similarly, when the assumption `n < a` is applied, +its rule application gains an additional subgoal `a < k`. -* [LeanDojo Website](https://leandojo.org/) -* [LeanInfer](https://github.com/lean-dojo/LeanInfer) -* [LeanDojo](https://github.com/lean-dojo/LeanDojo) -* [ReProver](https://github.com/lean-dojo/ReProver) -* [Aesop](https://github.com/JLimperg/aesop) +This mechanism makes sure that we consider all potential proofs. The downside is +that it's quite explosive: when there are multiple metavariables in multiple +goals, which Aesop may visit in any order, Aesop may spend a lot of time copying +goals with shared metavariables. It may even try to prove the same goal more +than once since different rules may yield the same metavariable instantiations. +For these reasons, rules which create metavariables are best kept out of the +global rule set and added to individual Aesop calls on an ad-hoc basis. -## Acknowledgements +It is also worth noting that when a safe rule assigns a metavariable, it is +treated as an unsafe rule (with success probability 90%). This is because +assigning metavariables is almost never safe, for the same reason as above: the +usually perfectly safe rule `∀ n, n < n + 1` would, if treated as safe, force us +to commit to one particular instantiation of the metavariable `?m`. -* We thank [Jannis Limperg](https://limperg.de/) for insightful discussions regarding the integration of Aesop and LeanInfer. +For more details on the handling of metavariables, see the [Aesop +paper](https://zenodo.org/record/7430233). \ No newline at end of file From c238fd6e0720d7336e191e68dd32ae17f203ac3e Mon Sep 17 00:00:00 2001 From: Kaiyu Yang Date: Sat, 7 Oct 2023 16:13:23 -0500 Subject: [PATCH 30/31] leanprover/lean4:v4.2.0-rc1 --- lean-toolchain | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lean-toolchain b/lean-toolchain index f0a6d660..03d0a7a7 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.0.0 +leanprover/lean4:v4.2.0-rc1 \ No newline at end of file From 76de8414771ac3905743a4ada8ad6b16a611d9ca Mon Sep 17 00:00:00 2001 From: Kaiyu Yang Date: Sat, 7 Oct 2023 16:14:12 -0500 Subject: [PATCH 31/31] clean --- lean-toolchain | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lean-toolchain b/lean-toolchain index 03d0a7a7..400394aa 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.2.0-rc1 \ No newline at end of file +leanprover/lean4:v4.2.0-rc1