Rule Tactic Types #

source

structure Aesop.RuleTacInput :

Type

Input for a rule tactic.

goal : Lean.MVarId
The goal on which the rule is run.
mvars : UnorderedArraySet Lean.MVarId
The set of mvars that goal depends on.
indexMatchLocations : Std.HashSet IndexMatchLocation
If the rule is indexed, the locations (i.e. hyps or the target) matched by the rule's index entries. Otherwise an empty set.
patternSubsts? : Option (Std.HashSet Substitution)
If the rule has a pattern, the pattern substitutions that were found in the goal. Each substitution is a list of expressions which were found by matching the pattern against expressions in the goal. For example, if h : max a b = max a c appears in the goal and the rule has pattern max x y, there will be two substitutions {x ↦ a, y ↦ b}) and {x ↦ a, y ↦ c}.
If the rule does not have a pattern, this is none. Otherwise it is guaranteed to be some xs with xs non-empty.
options : Options'
The options given to Aesop.
hypTypes : Lean.PHashSet RPINF
Normalised types of all non-implementation detail hypotheses in the local context of goal.

source

instance Aesop.instInhabitedRuleTacInput :

Inhabited RuleTacInput

Equations

One or more equations did not get rendered due to their size.

source

structure Aesop.Subgoal :

Type

A subgoal produced by a rule.

diff : 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 a GoalDiff. If you don't have access to such information, use diffGoals, but note that it may not give optimal results.

source

instance Aesop.instInhabitedSubgoal :

Inhabited Subgoal

Equations

Aesop.instInhabitedSubgoal = { default := { diff := default } }

source

def Aesop.Subgoal.mvarId (g : Subgoal) :

Lean.MVarId

Equations

g.mvarId = g.diff.newGoal

source

def Aesop.mvarIdToSubgoal (parentMVarId mvarId : Lean.MVarId) :

BaseM Subgoal

Equations

Aesop.mvarIdToSubgoal parentMVarId mvarId = do let __do_lift ← Aesop.diffGoals parentMVarId mvarId pure { diff := __do_lift }

source

structure Aesop.RuleApplication :

Type

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: the MetaM state after the tactic was run.
scriptSteps?: script steps which produce the same effect as the rule tactic. If input.options.generateScript = false (where input is the RuleTacInput), this field is ignored. If the tactic does not support script generation, use none.
successProbability: The success probability of this rule application. If none, we use the success probability of the applied rule.

goals : Array Subgoal
postState : Lean.Meta.SavedState
scriptSteps? : Option (Array Script.LazyStep)
successProbability? : Option Percent

source

def Aesop.RuleApplication.check (r : RuleApplication) (input : RuleTacInput) :

BaseM (Option Lean.MessageData)

Equations

One or more equations did not get rendered due to their size.

source

structure Aesop.RuleTacOutput :

Type

The result of a rule tactic is a list of rule applications.

applications : Array RuleApplication

source

instance Aesop.instInhabitedRuleTacOutput :

Inhabited RuleTacOutput

Equations

Aesop.instInhabitedRuleTacOutput = { default := { applications := default } }

source

def Aesop.RuleTac :

Type

A RuleTac is the tactic that is run when a rule is applied to a goal.

Equations

Aesop.RuleTac = (Aesop.RuleTacInput → Aesop.BaseM Aesop.RuleTacOutput)

source

instance Aesop.instInhabitedRuleTac :

Inhabited RuleTac

Equations

Aesop.instInhabitedRuleTac = id inferInstance

source

def Aesop.SingleRuleTac :

Type

A RuleTac which generates only a single RuleApplication.

Equations

Aesop.SingleRuleTac = (Aesop.RuleTacInput → Aesop.BaseM (Array Aesop.Subgoal × Option (Array Aesop.Script.LazyStep) × Option Aesop.Percent))

source

@[inline]

def Aesop.SingleRuleTac.toRuleTac (t : SingleRuleTac) :

RuleTac

Equations

One or more equations did not get rendered due to their size.

source

@[inline]

def Aesop.RuleTac.ofSingleRuleTac (t : SingleRuleTac) :

RuleTac

Equations

Aesop.RuleTac.ofSingleRuleTac = Aesop.SingleRuleTac.toRuleTac

source

def Aesop.RuleTac.ofTacticSyntax (t : RuleTacInput → Lean.MetaM Lean.Syntax.Tactic) :

RuleTac

Equations

One or more equations did not get rendered due to their size.

source

@[reducible, inline]

abbrev Aesop.TacGen :

Type

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