Rule Tactic Types

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.

instance Aesop.instInhabitedRuleTacInput : Inhabited RuleTacInput

Equations

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

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.

instance Aesop.instInhabitedSubgoal : Inhabited Subgoal

Equations

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

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

Equations

• g.mvarId = g.diff.newGoal

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 }

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

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.

structure Aesop.RuleTacOutput : Type

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

• applications : Array RuleApplication

instance Aesop.instInhabitedRuleTacOutput : Inhabited RuleTacOutput

Equations

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

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)

instance Aesop.instInhabitedRuleTac : Inhabited RuleTac

Equations

• Aesop.instInhabitedRuleTac = id inferInstance

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))

@[inline]

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

Equations

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

@[inline]

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

Equations

• Aesop.RuleTac.ofSingleRuleTac = Aesop.SingleRuleTac.toRuleTac

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.

@[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

• Aesop.TacGen = (Lean.MVarId → Lean.MetaM (Array (String × Float)))

Rule Tactic Descriptions

def Aesop.CasesPattern : Type

Equations

• Aesop.CasesPattern = Lean.Meta.AbstractMVarsResult

instance Aesop.instCasesPatternInhabited : Inhabited CasesPattern

Equations

• Aesop.instCasesPatternInhabited = Lean.Meta.instInhabitedAbstractMVarsResult

inductive Aesop.CasesTarget : Type

• decl (decl : Lean.Name) : CasesTarget
• patterns (patterns : Array CasesPattern) : CasesTarget

instance Aesop.instInhabitedCasesTarget : Inhabited CasesTarget

Equations

• Aesop.instInhabitedCasesTarget = { default := Aesop.CasesTarget.decl default }