Rule Tactic Types

structure Aesop.RuleTacInput : Type

Input for a rule tactic. Contains:

• goal: the goal on which the rule is run.
• mvars: the set of mvars which occur in goal.
• 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, if h : max a b = max a c appears in the goal and the rule has pattern max 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 : UnorderedArraySet Lean.MVarId
• indexMatchLocations : Std.HashSet IndexMatchLocation
• patternInstantiations : Std.HashSet RulePatternInstantiation
• options : Options'

instance Aesop.instInhabitedRuleTacInput : Inhabited RuleTacInput

Equations

• Aesop.instInhabitedRuleTacInput = { default := { goal := default, mvars := default, indexMatchLocations := default, patternInstantiations := default, options := default } }

structure Aesop.Subgoal : Type

A subgoal produced by a rule.

• mvarId : Lean.MVarId

  The goal mvar.

• 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 := { mvarId := default, diff := default } }

def Aesop.mvarIdToSubgoal (parentMVarId mvarId : Lean.MVarId) (fvarSubst : FVarIdSubst) : Lean.MetaM Subgoal

Equations

• Aesop.mvarIdToSubgoal parentMVarId mvarId fvarSubst = do let __do_lift ← Aesop.diffGoals parentMVarId mvarId fvarSubst pure { mvarId := mvarId, 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) : Lean.MetaM (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 → Lean.MetaM 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 → Lean.MetaM (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 }

inductive Aesop.RuleTerm : Type

• const (decl : Lean.Name) : RuleTerm
• term (term : Lean.Term) : RuleTerm

inductive Aesop.RuleTacDescr : Type

• apply (term : RuleTerm) (md : Lean.Meta.TransparencyMode) (pat? : Option RulePattern) : RuleTacDescr
• constructors (constructorNames : Array Lean.Name) (md : Lean.Meta.TransparencyMode) : RuleTacDescr
• forward (term : RuleTerm) (pat? : Option RulePattern) (immediate : UnorderedArraySet Nat) (isDestruct : Bool) (md : Lean.Meta.TransparencyMode) : RuleTacDescr
• cases (target : CasesTarget) (md : Lean.Meta.TransparencyMode) (isRecursiveType : Bool) (ctorNames : Array CtorNames) : RuleTacDescr
• tacticM (decl : Lean.Name) : RuleTacDescr
• ruleTac (decl : Lean.Name) : RuleTacDescr
• tacGen (decl : Lean.Name) : RuleTacDescr
• singleRuleTac (decl : Lean.Name) : RuleTacDescr
• tacticStx (stx : Lean.Syntax) : RuleTacDescr
• preprocess : RuleTacDescr

instance Aesop.instInhabitedRuleTacDescr : Inhabited RuleTacDescr

Equations

• Aesop.instInhabitedRuleTacDescr = { default := Aesop.RuleTacDescr.constructors default default }