Documentation

Aesop.RuleTac.Basic

Rule Tactic Types #

Input for a rule tactic.

  • The goal on which the rule is run.

  • 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.

Instances For
    structure Aesop.Subgoal :

    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.

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

              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.
              Instances For

                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

                      A RuleTac which generates only a single RuleApplication.

                      Equations
                        Instances For
                          @[inline]
                          Equations
                            Instances For
                              @[inline]
                              Equations
                                Instances For
                                  @[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
                                    Instances For

                                      Rule Tactic Descriptions #

                                      Equations
                                        Instances For
                                          Instances For