Documentation

Aesop.RuleTac.GoalDiff

structure Aesop.GoalDiff :

A representation of the differences between two goals. Each Aesop rule produces a GoalDiff between the goal on which the rule was run (the 'old goal') and each of the subgoals produced by the rule (the 'new goals').

We use the produced GoalDiffs to update stateful data structures which cache information about Aesop goals and for which it is more efficient to update the cached information than to recompute it for each goal.

For a goal diff between an old goal with local context Γ and a new goal with local context Δ, we expect that

Δ = (Γ \ removedFVars) ∪ addedFVars

when the local contexts are viewed as sets of FVarIds (excluding implementation detail hypotheses).

As an optimisation, the goal diff additionally contains an fvarSubst : FVarIdSubst which tracks renamings of hypotheses. When the substitution contains a mapping h ↦ h', this means that h was renamed to h'. Note that we do not guarantee that for all such mappings, h actually appears in the old goal and h' in the new goal. But if they do, fvarSubst(T) and T' must be defeq in the context of the new goal, where h : T, h' : T' and fvarSubst(T) is the application of the substitution to T. If h and h' are let decls with values v and v', fvarSubst(v) must additionally be defeq to v'.

The fvarSubst is semantically irrelevant: it does not influence the sets of added and removed hypotheses. However, it is an important performance optimisation, so rules should strive to generate accurate substitutions whenever possible.

  • FVarIds that appear in the new goal, but not in the old goal.

  • removedFVars : Lean.HashSet Lean.FVarId

    FVarIds that appear in the old goal, but not in the new goal.

  • fvarSubst : Aesop.FVarIdSubst

    An FVarId substitution that tracks hypotheses which have been renamed (but have not otherwise been modified).

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

        Diff two goals.

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

          If diff₁ is the difference between goals g₁ and g₂ and diff₂ is the difference between g₂ and g₃, then diff₁.comp diff₂ is the difference between g₁ and g₃.

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