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
    • Aesop.instInhabitedRuleTacInput = { default := { goal := default, mvars := default, indexMatchLocations := default, patternInstantiations := default, options := default } }

    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.
    Instances For
      Equations
      • One or more equations did not get rendered due to their size.
      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
            @[inline]
            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              @[inline, reducible]

              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 #