Node IDs

structure Aesop.GoalId : Type

• toNat : Nat

@[implicit_reducible]

instance Aesop.instInhabitedGoalId : Inhabited GoalId

def Aesop.instInhabitedGoalId.default : GoalId

@[implicit_reducible]

instance Aesop.instDecidableEqGoalId : DecidableEq GoalId

def Aesop.instDecidableEqGoalId.decEq (x✝ x✝¹ : GoalId) : Decidable (x✝ = x✝¹)

def Aesop.GoalId.zero : GoalId

def Aesop.GoalId.one : GoalId

def Aesop.GoalId.succ : GoalId → GoalId

def Aesop.GoalId.dummy : GoalId

@[implicit_reducible]

instance Aesop.GoalId.instLT : LT GoalId

@[implicit_reducible]

instance Aesop.GoalId.instDecidableRelLt : DecidableRel fun (x1 x2 : GoalId) => x1 < x2

@[implicit_reducible]

instance Aesop.GoalId.instToString : ToString GoalId

@[implicit_reducible]

instance Aesop.GoalId.instHashable : Hashable GoalId

Rule Application IDs

structure Aesop.RappId : Type

• toNat : Nat

@[implicit_reducible]

instance Aesop.instInhabitedRappId : Inhabited RappId

def Aesop.instInhabitedRappId.default : RappId

@[implicit_reducible]

instance Aesop.instDecidableEqRappId : DecidableEq RappId

def Aesop.instDecidableEqRappId.decEq (x✝ x✝¹ : RappId) : Decidable (x✝ = x✝¹)

def Aesop.RappId.zero : RappId

def Aesop.RappId.succ : RappId → RappId

def Aesop.RappId.one : RappId

def Aesop.RappId.dummy : RappId

@[implicit_reducible]

instance Aesop.RappId.instLT : LT RappId

@[implicit_reducible]

instance Aesop.RappId.instDecidableRelLt : DecidableRel fun (x1 x2 : RappId) => x1 < x2

@[implicit_reducible]

instance Aesop.RappId.instToString : ToString RappId

@[implicit_reducible]

instance Aesop.RappId.instHashable : Hashable RappId

Iterations

def Aesop.Iteration : Type

@[implicit_reducible]

instance Aesop.instInhabitedIteration : Inhabited Iteration

@[inline]

def Aesop.Iteration.one : Iteration

@[inline]

def Aesop.Iteration.succ (i : Iteration) : Iteration

def Aesop.Iteration.none : Iteration

@[implicit_reducible]

instance Aesop.Iteration.instDecidableEq : DecidableEq Iteration

@[implicit_reducible]

instance Aesop.Iteration.instToString : ToString Iteration

@[implicit_reducible]

instance Aesop.Iteration.instLT : LT Iteration

@[implicit_reducible]

instance Aesop.Iteration.instLE : LE Iteration

@[implicit_reducible]

instance Aesop.Iteration.instDecidableRelLt : DecidableRel fun (x1 x2 : Iteration) => x1 < x2

@[implicit_reducible]

instance Aesop.Iteration.instDecidableRelLe : DecidableRel fun (x1 x2 : Iteration) => x1 ≤ x2

The Tree

inductive Aesop.NodeState : Type

At each point during the search, every node of the tree (goal, rapp or mvar cluster) is in one of these states:

• proven: the node is proven.
• unprovable: the node is unprovable, i.e. it will never be proven regardless of any future expansions that might be performed.
• unknown: neither of the above.

Every node starts in the unknown state and may later become either proven or unprovable. After this, the state does not change any more.

• unknown : NodeState
• proven : NodeState
• unprovable : NodeState

def Aesop.instInhabitedNodeState.default : NodeState

@[implicit_reducible]

instance Aesop.instInhabitedNodeState : Inhabited NodeState

@[implicit_reducible]

instance Aesop.instBEqNodeState : BEq NodeState

def Aesop.instBEqNodeState.beq : NodeState → NodeState → Bool

@[implicit_reducible]

instance Aesop.NodeState.instToString : ToString NodeState

def Aesop.NodeState.isUnknown : NodeState → Bool

def Aesop.NodeState.isProven : NodeState → Bool

def Aesop.NodeState.isUnprovable : NodeState → Bool

def Aesop.NodeState.isIrrelevant : NodeState → Bool

def Aesop.NodeState.toEmoji : NodeState → String

inductive Aesop.GoalState : Type

A refinement of the NodeState, distinguishing between goals proven during normalisation and goals proven by a child rule application.

• unknown : GoalState
• provenByRuleApplication : GoalState
• provenByNormalization : GoalState
• unprovable : GoalState

def Aesop.instInhabitedGoalState.default : GoalState

@[implicit_reducible]

instance Aesop.instInhabitedGoalState : Inhabited GoalState

@[implicit_reducible]

instance Aesop.instBEqGoalState : BEq GoalState

def Aesop.instBEqGoalState.beq : GoalState → GoalState → Bool

@[implicit_reducible]

instance Aesop.GoalState.instToString : ToString GoalState

def Aesop.GoalState.isProvenByRuleApplication : GoalState → Bool

def Aesop.GoalState.isProvenByNormalization : GoalState → Bool

def Aesop.GoalState.isProven : GoalState → Bool

def Aesop.GoalState.isUnprovable : GoalState → Bool

def Aesop.GoalState.isUnknown : GoalState → Bool

def Aesop.GoalState.toNodeState : GoalState → NodeState

def Aesop.GoalState.isIrrelevant (s : GoalState) : Bool

def Aesop.GoalState.toEmoji : GoalState → String

inductive Aesop.NormalizationState : Type

• notNormal : NormalizationState
• normal (postGoal : Lean.MVarId) (postState : Lean.Meta.SavedState) (script : Array (DisplayRuleName × Option (Array Script.LazyStep))) : NormalizationState
• provenByNormalization (postState : Lean.Meta.SavedState) (script : Array (DisplayRuleName × Option (Array Script.LazyStep))) : NormalizationState

@[implicit_reducible]

instance Aesop.instInhabitedNormalizationState : Inhabited NormalizationState

def Aesop.instInhabitedNormalizationState.default : NormalizationState

def Aesop.NormalizationState.isNormal : NormalizationState → Bool

def Aesop.NormalizationState.isProvenByNormalization : NormalizationState → Bool

def Aesop.NormalizationState.normalizedGoal? : NormalizationState → Option Lean.MVarId

inductive Aesop.GoalOrigin : Type

A goal G can be added to the tree for three reasons:

1. G was produced by its parent rule as a subgoal. This is the most common reason.
2. G was copied because it contains some metavariables which were assigned by its parent rule. In this case, we record goal of which G is a copy. We also record the representative of the equivalence class of goals which are copies of each other. E.g. if goal 1 is copied to goal 2 and goal 2 is copied to goal 3, they are all part of the equivalence class with representative 1.

• subgoal : GoalOrigin
• copied («from» rep : GoalId) : GoalOrigin
• droppedMVar : GoalOrigin

def Aesop.instInhabitedGoalOrigin.default : GoalOrigin

@[implicit_reducible]

instance Aesop.instInhabitedGoalOrigin : Inhabited GoalOrigin

def Aesop.GoalOrigin.originalGoalId? : GoalOrigin → Option GoalId

def Aesop.GoalOrigin.toString : GoalOrigin → String

structure Aesop.GoalData (Rapp MVarCluster : Type) : Type

• id : GoalId
• parent : IO.Ref MVarCluster
• children : Array (IO.Ref Rapp)
• origin : GoalOrigin
• depth : Nat
• state : GoalState
• isIrrelevant : Bool
• isForcedUnprovable : Bool
• preNormGoal : Lean.MVarId
• normalizationState : NormalizationState
• mvars : UnorderedArraySet Lean.MVarId
• forwardState : ForwardState

  The forward state reflects the local context of the current goal. Before normalisation, this is the local context of preNormGoal; after normalisation, it is the local context of the post-normalisation goal (unless normalisation solved the goal, in which case the forward state is undetermined).

• forwardRuleMatches : ForwardRuleMatches

  Complete matches of forward rules for the current goal (in the same sense as above).

• successProbability : Percent
• addedInIteration : Iteration
• lastExpandedInIteration : Iteration
• unsafeRulesSelected : Bool
• unsafeQueue : UnsafeQueue
• failedRapps : Array RegularRule

instance Aesop.instNonemptyGoalData {Rapp✝ MVarCluster✝ : Type} [Nonempty MVarCluster✝] : Nonempty (GoalData Rapp✝ MVarCluster✝)

structure Aesop.MVarClusterData (Goal Rapp : Type) : Type

• parent? : Option (IO.Ref Rapp)
• goals : Array (IO.Ref Goal)
• isIrrelevant : Bool
• state : NodeState

def Aesop.instInhabitedMVarClusterData.default {a✝ a✝¹ : Type} : MVarClusterData a✝ a✝¹

@[implicit_reducible]

instance Aesop.instInhabitedMVarClusterData {a✝ a✝¹ : Type} : Inhabited (MVarClusterData a✝ a✝¹)

structure Aesop.RappData (Goal MVarCluster : Type) : Type

• id : RappId
• parent : IO.Ref Goal
• children : Array (IO.Ref MVarCluster)
• state : NodeState
• isIrrelevant : Bool
• appliedRule : RegularRule
• scriptSteps? : Option (Array Script.LazyStep)
• originalSubgoals : Array Lean.MVarId
• successProbability : Percent
• metaState : Lean.Meta.SavedState
• introducedMVars : UnorderedArraySet Lean.MVarId
• assignedMVars : UnorderedArraySet Lean.MVarId

instance Aesop.instNonemptyRappData {Goal✝ : Type} [Nonempty Goal✝] {MVarCluster✝ : Type} : Nonempty (RappData Goal✝ MVarCluster✝)

unsafe inductive Aesop.GoalUnsafe : Type

• mk (d : GoalData RappUnsafe MVarClusterUnsafe) : GoalUnsafe

unsafe inductive Aesop.MVarClusterUnsafe : Type

• mk (d : MVarClusterData GoalUnsafe RappUnsafe) : MVarClusterUnsafe

unsafe inductive Aesop.RappUnsafe : Type

• mk (d : RappData GoalUnsafe MVarClusterUnsafe) : RappUnsafe

structure Aesop.TreeSpec : Type 1

• Goal : Type
• Rapp : Type
• MVarCluster : Type
• introGoal : GoalData self.Rapp self.MVarCluster → self.Goal
• elimGoal : self.Goal → GoalData self.Rapp self.MVarCluster
• introRapp : RappData self.Goal self.MVarCluster → self.Rapp
• elimRapp : self.Rapp → RappData self.Goal self.MVarCluster
• introMVarCluster : MVarClusterData self.Goal self.Rapp → self.MVarCluster
• elimMVarCluster : self.MVarCluster → MVarClusterData self.Goal self.Rapp

instance Aesop.instNonemptyTreeSpec : Nonempty TreeSpec

unsafe def Aesop.treeImpl : TreeSpec

@[implemented_by Aesop.treeImpl]

opaque Aesop.tree : TreeSpec

def Aesop.Goal : Type

def Aesop.Rapp : Type

def Aesop.MVarCluster : Type

@[reducible, inline]

abbrev Aesop.GoalRef : Type

@[reducible, inline]

abbrev Aesop.RappRef : Type

@[reducible, inline]

abbrev Aesop.MVarClusterRef : Type

@[inline]

def Aesop.MVarCluster.mk : MVarClusterData Goal Rapp → MVarCluster

instance Aesop.MVarCluster.instNonempty : Nonempty MVarCluster

@[inline]

def Aesop.MVarCluster.elim : MVarCluster → MVarClusterData Goal Rapp

@[inline]

def Aesop.MVarCluster.modify (f : MVarClusterData Goal Rapp → MVarClusterData Goal Rapp) (c : MVarCluster) : MVarCluster

@[inline]

def Aesop.MVarCluster.parent? (c : MVarCluster) : Option RappRef

@[inline]

def Aesop.MVarCluster.setParent (parent? : Option RappRef) (c : MVarCluster) : MVarCluster

@[inline]

def Aesop.MVarCluster.goals (c : MVarCluster) : Array GoalRef

@[inline]

def Aesop.MVarCluster.setGoals (goals : Array GoalRef) (c : MVarCluster) : MVarCluster

@[inline]

def Aesop.MVarCluster.isIrrelevant (c : MVarCluster) : Bool

@[inline]

def Aesop.MVarCluster.setIsIrrelevant (isIrrelevant : Bool) (c : MVarCluster) : MVarCluster

@[inline]

def Aesop.MVarCluster.state (c : MVarCluster) : NodeState

@[inline]

def Aesop.MVarCluster.setState (state : NodeState) (c : MVarCluster) : MVarCluster

@[inline]

def Aesop.Goal.mk : GoalData Rapp MVarCluster → Goal

@[inline]

def Aesop.Goal.elim : Goal → GoalData Rapp MVarCluster

@[inline]

def Aesop.Goal.modify (f : GoalData Rapp MVarCluster → GoalData Rapp MVarCluster) (g : Goal) : Goal

@[inline]

def Aesop.Goal.id (g : Goal) : GoalId

@[inline]

def Aesop.Goal.parent (g : Goal) : MVarClusterRef

@[inline]

def Aesop.Goal.children (g : Goal) : Array RappRef

@[inline]

def Aesop.Goal.origin (g : Goal) : GoalOrigin

@[inline]

def Aesop.Goal.depth (g : Goal) : Nat

@[inline]

def Aesop.Goal.state (g : Goal) : GoalState

@[inline]

def Aesop.Goal.isIrrelevant (g : Goal) : Bool

@[inline]

def Aesop.Goal.isForcedUnprovable (g : Goal) : Bool

@[inline]

def Aesop.Goal.preNormGoal (g : Goal) : Lean.MVarId

@[inline]

def Aesop.Goal.normalizationState (g : Goal) : NormalizationState

@[inline]

def Aesop.Goal.mvars (g : Goal) : UnorderedArraySet Lean.MVarId

@[inline]

def Aesop.Goal.forwardState (g : Goal) : ForwardState

@[inline]

def Aesop.Goal.forwardRuleMatches (g : Goal) : ForwardRuleMatches

@[inline]

def Aesop.Goal.successProbability (g : Goal) : Percent

@[inline]

def Aesop.Goal.addedInIteration (g : Goal) : Iteration

@[inline]

def Aesop.Goal.lastExpandedInIteration (g : Goal) : Iteration

@[inline]

def Aesop.Goal.failedRapps (g : Goal) : Array RegularRule

@[inline]

def Aesop.Goal.unsafeRulesSelected (g : Goal) : Bool

@[inline]

def Aesop.Goal.unsafeQueue (g : Goal) : UnsafeQueue

@[inline]

def Aesop.Goal.unsafeQueue? (g : Goal) : Option UnsafeQueue

@[inline]

def Aesop.Goal.setId (id : GoalId) (g : Goal) : Goal

@[inline]

def Aesop.Goal.setParent (parent : MVarClusterRef) (g : Goal) : Goal

@[inline]

def Aesop.Goal.setChildren (children : Array RappRef) (g : Goal) : Goal

@[inline]

def Aesop.Goal.setOrigin (origin : GoalOrigin) (g : Goal) : Goal

@[inline]

def Aesop.Goal.setDepth (depth : Nat) (g : Goal) : Goal

@[inline]

def Aesop.Goal.setIsIrrelevant (isIrrelevant : Bool) (g : Goal) : Goal

@[inline]

def Aesop.Goal.setIsForcedUnprovable (isForcedUnprovable : Bool) (g : Goal) : Goal

@[inline]

def Aesop.Goal.setPreNormGoal (preNormGoal : Lean.MVarId) (g : Goal) : Goal

@[inline]

def Aesop.Goal.setNormalizationState (normalizationState : NormalizationState) (g : Goal) : Goal

@[inline]

def Aesop.Goal.setMVars (mvars : UnorderedArraySet Lean.MVarId) (g : Goal) : Goal

@[inline]

def Aesop.Goal.setForwardState (forwardState : ForwardState) (g : Goal) : Goal

@[inline]

def Aesop.Goal.setForwardRuleMatches (forwardRuleMatches : ForwardRuleMatches) (g : Goal) : Goal

@[inline]

def Aesop.Goal.setSuccessProbability (successProbability : Percent) (g : Goal) : Goal

@[inline]

def Aesop.Goal.setAddedInIteration (addedInIteration : Iteration) (g : Goal) : Goal

@[inline]

def Aesop.Goal.setLastExpandedInIteration (lastExpandedInIteration : Iteration) (g : Goal) : Goal

@[inline]

def Aesop.Goal.setUnsafeRulesSelected (unsafeRulesSelected : Bool) (g : Goal) : Goal

@[inline]

def Aesop.Goal.setUnsafeQueue (unsafeQueue : UnsafeQueue) (g : Goal) : Goal

@[inline]

def Aesop.Goal.setState (state : GoalState) (g : Goal) : Goal

@[inline]

def Aesop.Goal.setFailedRapps (failedRapps : Array RegularRule) (g : Goal) : Goal

instance Aesop.Goal.instNonempty : Nonempty Goal

@[implicit_reducible]

instance Aesop.Goal.instBEq : BEq Goal

@[implicit_reducible]

instance Aesop.Goal.instHashable : Hashable Goal

@[inline]

def Aesop.Rapp.mk : RappData Goal MVarCluster → Rapp

@[inline]

def Aesop.Rapp.elim : Rapp → RappData Goal MVarCluster

@[inline]

def Aesop.Rapp.modify (f : RappData Goal MVarCluster → RappData Goal MVarCluster) (r : Rapp) : Rapp

@[inline]

def Aesop.Rapp.id (r : Rapp) : RappId

@[inline]

def Aesop.Rapp.parent (r : Rapp) : GoalRef

@[inline]

def Aesop.Rapp.children (r : Rapp) : Array MVarClusterRef

@[inline]

def Aesop.Rapp.state (r : Rapp) : NodeState

@[inline]

def Aesop.Rapp.isIrrelevant (r : Rapp) : Bool

@[inline]

def Aesop.Rapp.appliedRule (r : Rapp) : RegularRule

@[inline]

def Aesop.Rapp.scriptSteps? (r : Rapp) : Option (Array Script.LazyStep)

@[inline]

def Aesop.Rapp.originalSubgoals (r : Rapp) : Array Lean.MVarId

@[inline]

def Aesop.Rapp.successProbability (r : Rapp) : Percent

@[inline]

def Aesop.Rapp.metaState (r : Rapp) : Lean.Meta.SavedState

@[inline]

def Aesop.Rapp.introducedMVars (r : Rapp) : UnorderedArraySet Lean.MVarId

@[inline]

def Aesop.Rapp.assignedMVars (r : Rapp) : UnorderedArraySet Lean.MVarId

@[inline]

def Aesop.Rapp.setId (id : RappId) (r : Rapp) : Rapp

@[inline]

def Aesop.Rapp.setParent (parent : GoalRef) (r : Rapp) : Rapp

@[inline]

def Aesop.Rapp.setChildren (children : Array MVarClusterRef) (r : Rapp) : Rapp

@[inline]

def Aesop.Rapp.setState (state : NodeState) (r : Rapp) : Rapp

@[inline]

def Aesop.Rapp.setIsIrrelevant (isIrrelevant : Bool) (r : Rapp) : Rapp

@[inline]

def Aesop.Rapp.setAppliedRule (appliedRule : RegularRule) (r : Rapp) : Rapp

@[inline]

def Aesop.Rapp.setScriptSteps? (scriptSteps? : Option (Array Script.LazyStep)) (r : Rapp) : Rapp

@[inline]

def Aesop.Rapp.setOriginalSubgoals (originalSubgoals : Array Lean.MVarId) (r : Rapp) : Rapp

@[inline]

def Aesop.Rapp.setSuccessProbability (successProbability : Percent) (r : Rapp) : Rapp

@[inline]

def Aesop.Rapp.setMetaState (metaState : Lean.Meta.SavedState) (r : Rapp) : Rapp

@[inline]

def Aesop.Rapp.setIntroducedMVars (introducedMVars : UnorderedArraySet Lean.MVarId) (r : Rapp) : Rapp

@[inline]

def Aesop.Rapp.setAssignedMVars (assignedMVars : UnorderedArraySet Lean.MVarId) (r : Rapp) : Rapp

instance Aesop.Rapp.instNonempty : Nonempty Rapp

@[implicit_reducible]

instance Aesop.Rapp.instBEq : BEq Rapp

@[implicit_reducible]

instance Aesop.Rapp.instHashable : Hashable Rapp

Miscellaneous Queries

def Aesop.Rapp.isSafe (r : Rapp) : Bool

@[inline]

def Aesop.Goal.postNormGoalAndMetaState? (g : Goal) : Option (Lean.MVarId × Lean.Meta.SavedState)

def Aesop.Goal.postNormGoal? (g : Goal) : Option Lean.MVarId

def Aesop.Goal.currentGoal (g : Goal) : Lean.MVarId

def Aesop.Goal.parentRapp? (g : Goal) : BaseIO (Option RappRef)

def Aesop.Goal.parentMetaState (g : Goal) (rootMetaState : Lean.Meta.SavedState) : BaseIO Lean.Meta.SavedState

def Aesop.Goal.currentGoalAndMetaState (g : Goal) (rootMetaState : Lean.Meta.SavedState) : Lean.MetaM (Lean.MVarId × Lean.Meta.SavedState)

def Aesop.Goal.safeRapps (g : Goal) : BaseIO (Array RappRef)

def Aesop.Goal.hasSafeRapp (g : Goal) : BaseIO Bool

def Aesop.Goal.isUnsafeExhausted (g : Goal) : Bool

def Aesop.Goal.isExhausted (g : Goal) : BaseIO Bool

def Aesop.Goal.isActive (g : Goal) : BaseIO Bool

def Aesop.Goal.hasProvableRapp (g : Goal) : BaseIO Bool

def Aesop.Goal.firstProvenRapp? (g : Goal) : BaseIO (Option RappRef)

def Aesop.Goal.hasMVar (g : Goal) : Bool

def Aesop.Goal.priority (g : Goal) : Percent

def Aesop.Goal.isNormal (g : Goal) : Bool

def Aesop.Goal.originalGoalId (g : Goal) : GoalId

def Aesop.Goal.isRoot (g : Goal) : BaseIO Bool

def Aesop.Rapp.introducesMVar (r : Rapp) : Bool

def Aesop.Rapp.parentPostNormMetaState (r : Rapp) (rootMetaState : Lean.Meta.SavedState) : BaseIO Lean.Meta.SavedState

def Aesop.Rapp.foldSubgoalsM {m : Type → Type} {σ : Type} [Monad m] [MonadLiftT (ST IO.RealWorld) m] (init : σ) (f : σ → GoalRef → m σ) (r : Rapp) : m σ

def Aesop.Rapp.forSubgoalsM {m : Type → Type} [Monad m] [MonadLiftT (ST IO.RealWorld) m] (f : GoalRef → m Unit) (r : Rapp) : m Unit

def Aesop.Rapp.subgoals {m : Type → Type} [Monad m] [MonadLiftT (ST IO.RealWorld) m] (r : Rapp) : m (Array GoalRef)

def Aesop.Rapp.depth (r : Rapp) : BaseIO Nat

def Aesop.MVarCluster.provenGoal? (c : MVarCluster) : BaseIO (Option GoalRef)

def Aesop.RappRef.getChildAuxDeclNameGenerator (r : RappRef) : BaseIO Lean.DeclNameGenerator

Get a DeclNameGenerator for auxiliary declarations that can be used by children of this rapp. Successive calls to this function return DeclNameGenerators that are guaranteed to generate distinct names.