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.

Hypotheses are identified by their FVarId and the RPINF of their type and value (if any). This means that when a hypothesis h : T with FVarId i appears in the old goal and h : T' with FVarId i appears in the new goal, but the RPINF of T is not equal to the RPINF of T', then h is treated as both added (with the new type) and removed (with the old type). This can happen when the type of a hyp changes to another type that is definitionally equal at default, but not at reducible transparency.

The target is identified by RPINF.

• oldGoal : Lean.MVarId

  The old goal.

• newGoal : Lean.MVarId

  The new goal.

• addedFVars : Std.HashSet Lean.FVarId

  FVarIds that appear in the new goal, but not (or with a different type) in the old goal.

• removedFVars : Std.HashSet Lean.FVarId

  FVarIds that appear in the old goal, but not (or with a different type) in the new goal.

• targetChanged : Lean.LBool

  Is the old goal's target RPINF equal to the new goal's target RPINF?

instance Aesop.instInhabitedGoalDiff : Inhabited GoalDiff

Equations

• Aesop.instInhabitedGoalDiff = { default := { oldGoal := default, newGoal := default, addedFVars := default, removedFVars := default, targetChanged := default } }

def Aesop.GoalDiff.empty (oldGoal newGoal : Lean.MVarId) : GoalDiff

Equations

• Aesop.GoalDiff.empty oldGoal newGoal = { oldGoal := oldGoal, newGoal := newGoal, addedFVars := ∅, removedFVars := ∅, targetChanged := Lean.LBool.undef }

def Aesop.isRPINFEqual (goal₁ goal₂ : Lean.MVarId) (e₁ e₂ : Lean.Expr) : BaseM Bool

Equations

• Aesop.isRPINFEqual goal₁ goal₂ e₁ e₂ = do let __do_lift ← goal₁.withContext (Aesop.rpinf e₁) let __do_lift_1 ← goal₂.withContext (Aesop.rpinf e₂) pure (__do_lift == __do_lift_1)

def Aesop.isRPINFEqualLDecl (goal₁ goal₂ : Lean.MVarId) (ldecl₁ ldecl₂ : Lean.LocalDecl) : BaseM Bool

Equations

• One or more equations did not get rendered due to their size.
• Aesop.isRPINFEqualLDecl goal₁ goal₂ x✝¹ x✝ = pure false

def Aesop.getNewFVars (oldGoal newGoal : Lean.MVarId) (oldLCtx newLCtx : Lean.LocalContext) : BaseM (Std.HashSet Lean.FVarId)

Equations

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

def Aesop.diffGoals (old new : Lean.MVarId) : BaseM GoalDiff

Diff two goals.

Equations

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

def Aesop.GoalDiff.targetChanged' (diff : GoalDiff) : BaseM Bool

Equations

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

def Aesop.GoalDiff.comp (diff₁ diff₂ : GoalDiff) : 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₃.

We assume that a hypothesis whose RPINF changed between g₁ and g₂ does not change back, i.e. the hypothesis' RPINF is still different between g₁ and g₃.

Equations

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

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

Equations

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

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

Equations

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