Rule Tactic Types #
Input for a rule tactic. Contains:
goal
: the goal on which the rule is run.mvars
: the set of mvars which occur ingoal
.indexMatchLocations
: if the rule is indexed, the locations (e.g. hyps or the target) matched by the rule's index entries. Otherwise an empty set.patternInstantiations
: if the rule has a pattern, the pattern instantiations that were found in the goal. Each instantiation is a list of expressions which were found by matching the pattern against expressions in the goal. For example, ifh : max a b = max a c
appears in the goal and the rule has patternmax x y
, there will be two pattern instantiations[a, b]
(representing the substitution{x ↦ a, y ↦ b}
) and[a, c]
. If the rule does not have a pattern,patternInstantiations
is empty; otherwise it's guaranteed to be non-empty.options
: the options given to Aesop.
- goal : Lean.MVarId
- mvars : Aesop.UnorderedArraySet Lean.MVarId
- indexMatchLocations : Std.HashSet Aesop.IndexMatchLocation
- patternInstantiations : Std.HashSet Aesop.RulePatternInstantiation
- options : Aesop.Options'
Instances For
A subgoal produced by a rule.
- mvarId : Lean.MVarId
The goal mvar.
- diff : Aesop.GoalDiff
A diff between the goal the rule was run on and this goal. Many
MetaM
tactics report information that allows you to easily construct aGoalDiff
. If you don't have access to such information, usediffGoals
, but note that it may not give optimal results.
Instances For
Equations
- Aesop.instInhabitedSubgoal = { default := { mvarId := default, diff := default } }
Equations
- Aesop.mvarIdToSubgoal parentMVarId mvarId fvarSubst = do let __do_lift ← Aesop.diffGoals parentMVarId mvarId fvarSubst pure { mvarId := mvarId, diff := __do_lift }
Instances For
A single rule application, representing the application of a tactic to the input goal. Must accurately report the following information:
goals
: the goals generated by the tactic.postState
: theMetaM
state after the tactic was run.scriptSteps?
: script steps which produce the same effect as the rule tactic. Ifinput.options.generateScript = false
(whereinput
is theRuleTacInput
), this field is ignored. If the tactic does not support script generation, usenone
.successProbability
: The success probability of this rule application. Ifnone
, we use the success probability of the applied rule.
- goals : Array Aesop.Subgoal
- postState : Lean.Meta.SavedState
- scriptSteps? : Option (Array Aesop.Script.LazyStep)
- successProbability? : Option Aesop.Percent
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
The result of a rule tactic is a list of rule applications.
- applications : Array Aesop.RuleApplication
Instances For
Equations
- Aesop.instInhabitedRuleTacOutput = { default := { applications := default } }
Equations
Equations
- One or more equations did not get rendered due to their size.
Instances For
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
A tactic generator is a special sort of rule tactic, intended for use with
generative machine learning methods. It generates zero or more tactics
(represented as strings) that could be applied to the goal, plus a success
probability for each tactic. When Aesop executes a tactic generator, it executes
each of the tactics and, if the tactic succeeds, adds a rule application for it.
The tactic's success probability (which must be between 0 and 1, inclusive)
becomes the success probability of the rule application. A TacGen
rule
succeeds if at least one of its suggested tactics succeeds.
Equations
- Aesop.TacGen = (Lean.MVarId → Lean.MetaM (Array (String × Float)))
Instances For
Rule Tactic Descriptions #
Instances For
- decl (decl : Lean.Name) : Aesop.CasesTarget
- patterns (patterns : Array Aesop.CasesPattern) : Aesop.CasesTarget
Instances For
Equations
- Aesop.instInhabitedCasesTarget = { default := Aesop.CasesTarget.decl default }
- const (decl : Lean.Name) : Aesop.RuleTerm
- term (term : Lean.Term) : Aesop.RuleTerm
Instances For
- apply (term : Aesop.RuleTerm) (md : Lean.Meta.TransparencyMode) (pat? : Option Aesop.RulePattern) : Aesop.RuleTacDescr
- constructors (constructorNames : Array Lean.Name) (md : Lean.Meta.TransparencyMode) : Aesop.RuleTacDescr
- forward (term : Aesop.RuleTerm) (pat? : Option Aesop.RulePattern) (immediate : Aesop.UnorderedArraySet Nat) (isDestruct : Bool) (md : Lean.Meta.TransparencyMode) : Aesop.RuleTacDescr
- cases (target : Aesop.CasesTarget) (md : Lean.Meta.TransparencyMode) (isRecursiveType : Bool) (ctorNames : Array Aesop.CtorNames) : Aesop.RuleTacDescr
- tacticM (decl : Lean.Name) : Aesop.RuleTacDescr
- ruleTac (decl : Lean.Name) : Aesop.RuleTacDescr
- tacGen (decl : Lean.Name) : Aesop.RuleTacDescr
- singleRuleTac (decl : Lean.Name) : Aesop.RuleTacDescr
- tacticStx (stx : Lean.Syntax) : Aesop.RuleTacDescr
- preprocess : Aesop.RuleTacDescr