Documentation

Aesop.RuleTac.Basic

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 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.
Instances For
Equations
structure Aesop.Subgoal :

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.

Instances For
Equations
def Aesop.mvarIdToSubgoal (parentMVarId mvarId : Lean.MVarId) (fvarSubst : FVarIdSubst) :
Equations

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.
Equations
  • One or more equations did not get rendered due to their size.

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

Instances For

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

Equations
Instances For
@[inline]
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.
@[reducible, inline]

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

Rule Tactic Descriptions #

inductive Aesop.RuleTerm :
Instances For