structure Aesop.GoalDiff : Type

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.

• addedFVars : Std.HashSet Lean.FVarId

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

• removedFVars : Std.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).

instance Aesop.instInhabitedGoalDiff : Inhabited Aesop.GoalDiff

Equations

• Aesop.instInhabitedGoalDiff = { default := { addedFVars := default, removedFVars := default, fvarSubst := default } }

def Aesop.GoalDiff.empty : Aesop.GoalDiff

Equations

• Aesop.GoalDiff.empty = { addedFVars := ∅, removedFVars := ∅, fvarSubst := ∅ }

instance Aesop.instEmptyCollectionGoalDiff : EmptyCollection Aesop.GoalDiff

Equations

• Aesop.instEmptyCollectionGoalDiff = { emptyCollection := Aesop.GoalDiff.empty }

def Aesop.getNewFVars (oldLCtx newLCtx : Lean.LocalContext) : Std.HashSet Lean.FVarId

Equations

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

def Aesop.diffGoals (old new : Lean.MVarId) (fvarSubst : Aesop.FVarIdSubst) : Lean.MetaM Aesop.GoalDiff

Diff two goals.

Equations

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

def Aesop.GoalDiff.comp (diff₁ diff₂ : Aesop.GoalDiff) : Aesop.GoalDiff

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.

def Aesop.GoalDiff.checkCore (diff : Aesop.GoalDiff) (old new : Lean.MVarId) : Lean.MetaM (Option Lean.MessageData)

Equations

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

def Aesop.GoalDiff.checkCore.isDefeqLocalDecl : Lean.LocalDecl → Lean.LocalDecl → Lean.MetaM Bool

Equations

• One or more equations did not get rendered due to their size.
• Aesop.GoalDiff.checkCore.isDefeqLocalDecl x✝ x = pure false

def Aesop.GoalDiff.check (diff : Aesop.GoalDiff) (old new : Lean.MVarId) : Lean.MetaM (Option Lean.MessageData)

Equations

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