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 : Aesop.UnorderedArraySet Lean.MVarId
• indexMatchLocations : Lean.HashSet Aesop.IndexMatchLocation
• patternInstantiations : Lean.HashSet Aesop.RulePatternInstantiation
• options : Aesop.Options'

instance Aesop.instInhabitedRuleTacInput : Inhabited Aesop.RuleTacInput

Equations

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

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.
• scriptBuilder?: script builder for the tactic. If input.options.generateScript = false (where input is the RuleTacInput), this field is ignored, so you can use none. If the tactic does not support script generation, also use none.
• successProbability: The success probability of this rule application. If none, we use the success probability of the applied rule.

• goals : Array Lean.MVarId
• postState : Lean.Meta.SavedState
• scriptBuilder? : Option Aesop.RuleTacScriptBuilder
• successProbability? : Option Aesop.Percent

def Aesop.RuleApplication.check (r : Aesop.RuleApplication) : 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 Aesop.RuleApplication

instance Aesop.instInhabitedRuleTacOutput : Inhabited Aesop.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 Aesop.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 Lean.MVarId × Option Aesop.RuleTacScriptBuilder × Option Aesop.Percent))

@[inline]

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

Equations

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

@[inline]

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

Equations

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

@[inline, reducible]

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

inductive Aesop.CasesTarget : Type

• decl: Lean.Name → Aesop.CasesTarget
• patterns: Array Aesop.CasesPattern → Aesop.CasesTarget

instance Aesop.instInhabitedCasesTarget : Inhabited Aesop.CasesTarget

Equations

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

inductive Aesop.RuleTacDescr : Type

• applyConst: Lean.Name → Lean.Meta.TransparencyMode → Option Aesop.RulePattern → Aesop.RuleTacDescr
• applyTerm: Lean.Term → Lean.Meta.TransparencyMode → Option Aesop.RulePattern → Aesop.RuleTacDescr
• constructors: Array Lean.Name → Lean.Meta.TransparencyMode → Aesop.RuleTacDescr
• forwardConst: Lean.Name → Option Aesop.RulePattern → Aesop.UnorderedArraySet Nat → Bool → Lean.Meta.TransparencyMode → Aesop.RuleTacDescr
• forwardTerm: Lean.Term → Option Aesop.RulePattern → Aesop.UnorderedArraySet Nat → Bool → Lean.Meta.TransparencyMode → Aesop.RuleTacDescr
• cases: Aesop.CasesTarget → Lean.Meta.TransparencyMode → Bool → Aesop.RuleTacDescr
• tacticM: Lean.Name → Aesop.RuleTacDescr
• ruleTac: Lean.Name → Aesop.RuleTacDescr
• tacGen: Lean.Name → Aesop.RuleTacDescr
• singleRuleTac: Lean.Name → Aesop.RuleTacDescr
• tacticStx: Lean.Syntax → Aesop.RuleTacDescr
• preprocess: Aesop.RuleTacDescr

instance Aesop.instInhabitedRuleTacDescr : Inhabited Aesop.RuleTacDescr

Equations

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