Node IDs

structure Aesop.GoalId : Type

• toNat : Nat

@[implicit_reducible]

instance Aesop.instInhabitedGoalId : Inhabited GoalId

Equations

• Aesop.instInhabitedGoalId = { default := Aesop.instInhabitedGoalId.default }

def Aesop.instInhabitedGoalId.default : GoalId

Equations

• Aesop.instInhabitedGoalId.default = { toNat := default }

@[implicit_reducible]

instance Aesop.instDecidableEqGoalId : DecidableEq GoalId

Equations

• Aesop.instDecidableEqGoalId = Aesop.instDecidableEqGoalId.decEq

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

Equations

• Aesop.instDecidableEqGoalId.decEq { toNat := a } { toNat := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

def Aesop.GoalId.zero : GoalId

Equations

• Aesop.GoalId.zero = { toNat := 0 }

def Aesop.GoalId.one : GoalId

Equations

• Aesop.GoalId.one = { toNat := 1 }

def Aesop.GoalId.succ : GoalId → GoalId

Equations

• { toNat := n }.succ = { toNat := n + 1 }

def Aesop.GoalId.dummy : GoalId

Equations

• Aesop.GoalId.dummy = { toNat := 1000000000000000 }

@[implicit_reducible]

instance Aesop.GoalId.instLT : LT GoalId

Equations

• Aesop.GoalId.instLT = { lt := fun (n m : Aesop.GoalId) => n.toNat < m.toNat }

@[implicit_reducible]

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

Equations

• n.instDecidableRelLt m = inferInstanceAs (Decidable (n.toNat < m.toNat))

@[implicit_reducible]

instance Aesop.GoalId.instToString : ToString GoalId

Equations

• Aesop.GoalId.instToString = { toString := fun (n : Aesop.GoalId) => toString n.toNat }

@[implicit_reducible]

instance Aesop.GoalId.instHashable : Hashable GoalId

Equations

• Aesop.GoalId.instHashable = { hash := fun (n : Aesop.GoalId) => hash n.toNat }

Rule Application IDs

structure Aesop.RappId : Type

• toNat : Nat

@[implicit_reducible]

instance Aesop.instInhabitedRappId : Inhabited RappId

Equations

• Aesop.instInhabitedRappId = { default := Aesop.instInhabitedRappId.default }

def Aesop.instInhabitedRappId.default : RappId

Equations

• Aesop.instInhabitedRappId.default = { toNat := default }

@[implicit_reducible]

instance Aesop.instDecidableEqRappId : DecidableEq RappId

Equations

• Aesop.instDecidableEqRappId = Aesop.instDecidableEqRappId.decEq

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

Equations

• Aesop.instDecidableEqRappId.decEq { toNat := a } { toNat := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

def Aesop.RappId.zero : RappId

Equations

• Aesop.RappId.zero = { toNat := 0 }

def Aesop.RappId.succ : RappId → RappId

Equations

• { toNat := n }.succ = { toNat := n + 1 }

def Aesop.RappId.one : RappId

Equations

• Aesop.RappId.one = { toNat := 1 }

def Aesop.RappId.dummy : RappId

Equations

• Aesop.RappId.dummy = { toNat := 1000000000000000 }

@[implicit_reducible]

instance Aesop.RappId.instLT : LT RappId

Equations

• Aesop.RappId.instLT = { lt := fun (n m : Aesop.RappId) => n.toNat < m.toNat }

@[implicit_reducible]

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

Equations

• n.instDecidableRelLt m = inferInstanceAs (Decidable (n.toNat < m.toNat))

@[implicit_reducible]

instance Aesop.RappId.instToString : ToString RappId

Equations

• Aesop.RappId.instToString = { toString := fun (n : Aesop.RappId) => toString n.toNat }

@[implicit_reducible]

instance Aesop.RappId.instHashable : Hashable RappId

Equations

• Aesop.RappId.instHashable = { hash := fun (n : Aesop.RappId) => hash n.toNat }

Iterations

def Aesop.Iteration : Type

Equations

• Aesop.Iteration = Nat

@[implicit_reducible]

instance Aesop.instInhabitedIteration : Inhabited Iteration

Equations

• Aesop.instInhabitedIteration = instInhabitedNat

@[inline]

def Aesop.Iteration.one : Iteration

Equations

• Aesop.Iteration.one = Aesop.Iteration.ofNat✝ 1

@[inline]

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

Equations

• i.succ = Aesop.Iteration.ofNat✝ (Aesop.Iteration.toNat✝ i + 1)

def Aesop.Iteration.none : Iteration

Equations

• Aesop.Iteration.none = Aesop.Iteration.ofNat✝ 0

@[implicit_reducible]

instance Aesop.Iteration.instDecidableEq : DecidableEq Iteration

Equations

• Aesop.Iteration.instDecidableEq = inferInstanceAs (DecidableEq Nat)

@[implicit_reducible]

instance Aesop.Iteration.instToString : ToString Iteration

Equations

• Aesop.Iteration.instToString = inferInstanceAs (ToString Nat)

@[implicit_reducible]

instance Aesop.Iteration.instLT : LT Iteration

Equations

• Aesop.Iteration.instLT = inferInstanceAs (LT Nat)

@[implicit_reducible]

instance Aesop.Iteration.instLE : LE Iteration

Equations

• Aesop.Iteration.instLE = inferInstanceAs (LE Nat)

@[implicit_reducible]

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

Equations

• Aesop.Iteration.instDecidableRelLt = inferInstanceAs (DecidableRel fun (x1 x2 : Nat) => x1 < x2)

@[implicit_reducible]

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

Equations

• Aesop.Iteration.instDecidableRelLe = inferInstanceAs (DecidableRel fun (x1 x2 : Nat) => 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

Equations

• Aesop.instInhabitedNodeState.default = Aesop.NodeState.unknown

@[implicit_reducible]

instance Aesop.instInhabitedNodeState : Inhabited NodeState

Equations

• Aesop.instInhabitedNodeState = { default := Aesop.instInhabitedNodeState.default }

@[implicit_reducible]

instance Aesop.instBEqNodeState : BEq NodeState

Equations

• Aesop.instBEqNodeState = { beq := Aesop.instBEqNodeState.beq }

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

Equations

• Aesop.instBEqNodeState.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

@[implicit_reducible]

instance Aesop.NodeState.instToString : ToString NodeState

Equations

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

def Aesop.NodeState.isUnknown : NodeState → Bool

Equations

• Aesop.NodeState.unknown.isUnknown = true
• x✝.isUnknown = false

def Aesop.NodeState.isProven : NodeState → Bool

Equations

• Aesop.NodeState.proven.isProven = true
• x✝.isProven = false

def Aesop.NodeState.isUnprovable : NodeState → Bool

Equations

• Aesop.NodeState.unprovable.isUnprovable = true
• x✝.isUnprovable = false

def Aesop.NodeState.isIrrelevant : NodeState → Bool

Equations

• Aesop.NodeState.proven.isIrrelevant = true
• Aesop.NodeState.unprovable.isIrrelevant = true
• Aesop.NodeState.unknown.isIrrelevant = false

def Aesop.NodeState.toEmoji : NodeState → String

Equations

• Aesop.NodeState.proven.toEmoji = Aesop.nodeProvedEmoji
• Aesop.NodeState.unprovable.toEmoji = Aesop.nodeUnprovableEmoji
• Aesop.NodeState.unknown.toEmoji = Aesop.nodeUnknownEmoji

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

Equations

• Aesop.instInhabitedGoalState.default = Aesop.GoalState.unknown

@[implicit_reducible]

instance Aesop.instInhabitedGoalState : Inhabited GoalState

Equations

• Aesop.instInhabitedGoalState = { default := Aesop.instInhabitedGoalState.default }

@[implicit_reducible]

instance Aesop.instBEqGoalState : BEq GoalState

Equations

• Aesop.instBEqGoalState = { beq := Aesop.instBEqGoalState.beq }

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

Equations

• Aesop.instBEqGoalState.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

@[implicit_reducible]

instance Aesop.GoalState.instToString : ToString GoalState

Equations

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

def Aesop.GoalState.isProvenByRuleApplication : GoalState → Bool

Equations

• Aesop.GoalState.provenByRuleApplication.isProvenByRuleApplication = true
• x✝.isProvenByRuleApplication = false

def Aesop.GoalState.isProvenByNormalization : GoalState → Bool

Equations

• Aesop.GoalState.provenByNormalization.isProvenByNormalization = true
• x✝.isProvenByNormalization = false

def Aesop.GoalState.isProven : GoalState → Bool

Equations

• Aesop.GoalState.provenByRuleApplication.isProven = true
• Aesop.GoalState.provenByNormalization.isProven = true
• x✝.isProven = false

def Aesop.GoalState.isUnprovable : GoalState → Bool

Equations

• Aesop.GoalState.unprovable.isUnprovable = true
• x✝.isUnprovable = false

def Aesop.GoalState.isUnknown : GoalState → Bool

Equations

• Aesop.GoalState.unknown.isUnknown = true
• x✝.isUnknown = false

def Aesop.GoalState.toNodeState : GoalState → NodeState

Equations

• Aesop.GoalState.unknown.toNodeState = Aesop.NodeState.unknown
• Aesop.GoalState.provenByRuleApplication.toNodeState = Aesop.NodeState.proven
• Aesop.GoalState.provenByNormalization.toNodeState = Aesop.NodeState.proven
• Aesop.GoalState.unprovable.toNodeState = Aesop.NodeState.unprovable

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

Equations

• s.isIrrelevant = s.toNodeState.isIrrelevant

def Aesop.GoalState.toEmoji : GoalState → String

Equations

• Aesop.GoalState.unknown.toEmoji = Aesop.nodeUnknownEmoji
• Aesop.GoalState.provenByRuleApplication.toEmoji = Aesop.nodeProvedEmoji
• Aesop.GoalState.provenByNormalization.toEmoji = Aesop.nodeProvedEmoji
• Aesop.GoalState.unprovable.toEmoji = Aesop.nodeUnprovableEmoji

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

Equations

• Aesop.instInhabitedNormalizationState = { default := Aesop.instInhabitedNormalizationState.default }

def Aesop.instInhabitedNormalizationState.default : NormalizationState

Equations

• Aesop.instInhabitedNormalizationState.default = Aesop.NormalizationState.notNormal

def Aesop.NormalizationState.isNormal : NormalizationState → Bool

Equations

• Aesop.NormalizationState.notNormal.isNormal = false
• (Aesop.NormalizationState.normal postGoal postState script).isNormal = true
• (Aesop.NormalizationState.provenByNormalization postState script).isNormal = true

def Aesop.NormalizationState.isProvenByNormalization : NormalizationState → Bool

Equations

• Aesop.NormalizationState.notNormal.isProvenByNormalization = false
• (Aesop.NormalizationState.normal postGoal postState script).isProvenByNormalization = false
• (Aesop.NormalizationState.provenByNormalization postState script).isProvenByNormalization = true

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

Equations

• Aesop.NormalizationState.notNormal.normalizedGoal? = none
• (Aesop.NormalizationState.provenByNormalization postState script).normalizedGoal? = none
• (Aesop.NormalizationState.normal g postState script).normalizedGoal? = some g

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

Equations

• Aesop.instInhabitedGoalOrigin.default = Aesop.GoalOrigin.subgoal

@[implicit_reducible]

instance Aesop.instInhabitedGoalOrigin : Inhabited GoalOrigin

Equations

• Aesop.instInhabitedGoalOrigin = { default := Aesop.instInhabitedGoalOrigin.default }

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

Equations

• (Aesop.GoalOrigin.copied «from» rep).originalGoalId? = some rep
• x✝.originalGoalId? = none

def Aesop.GoalOrigin.toString : GoalOrigin → String

Equations

• Aesop.GoalOrigin.subgoal.toString = "subgoal"
• (Aesop.GoalOrigin.copied «from» rep).toString = toString "copy of " ++ toString «from» ++ toString ", originally " ++ toString rep
• Aesop.GoalOrigin.droppedMVar.toString = "dropped mvar"

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✝¹

Equations

• Aesop.instInhabitedMVarClusterData.default = { parent? := default, goals := default, isIrrelevant := default, state := default }

@[implicit_reducible]

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

Equations

• Aesop.instInhabitedMVarClusterData = { default := Aesop.instInhabitedMVarClusterData.default }

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

Equations

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

@[implemented_by Aesop.treeImpl]

opaque Aesop.tree : TreeSpec

def Aesop.Goal : Type

Equations

• Aesop.Goal = Aesop.tree.Goal

def Aesop.Rapp : Type

Equations

• Aesop.Rapp = Aesop.tree.Rapp

def Aesop.MVarCluster : Type

Equations

• Aesop.MVarCluster = Aesop.tree.MVarCluster

@[reducible, inline]

abbrev Aesop.GoalRef : Type

Equations

• Aesop.GoalRef = IO.Ref Aesop.Goal

@[reducible, inline]

abbrev Aesop.RappRef : Type

Equations

• Aesop.RappRef = IO.Ref Aesop.Rapp

@[reducible, inline]

abbrev Aesop.MVarClusterRef : Type

Equations

• Aesop.MVarClusterRef = IO.Ref Aesop.MVarCluster

@[inline]

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

Equations

• Aesop.MVarCluster.mk = Aesop.tree.introMVarCluster

instance Aesop.MVarCluster.instNonempty : Nonempty MVarCluster

@[inline]

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

Equations

• Aesop.MVarCluster.elim = Aesop.tree.elimMVarCluster

@[inline]

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

Equations

• Aesop.MVarCluster.modify f c = Aesop.MVarCluster.mk (f c.elim)

@[inline]

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

Equations

• c.parent? = c.elim.parent?

@[inline]

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

Equations

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

@[inline]

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

Equations

• c.goals = c.elim.goals

@[inline]

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

Equations

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

@[inline]

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

Equations

• c.isIrrelevant = c.elim.isIrrelevant

@[inline]

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

Equations

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

@[inline]

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

Equations

• c.state = c.elim.state

@[inline]

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

Equations

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

@[inline]

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

Equations

• Aesop.Goal.mk = Aesop.tree.introGoal

@[inline]

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

Equations

• Aesop.Goal.elim = Aesop.tree.elimGoal

@[inline]

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

Equations

• Aesop.Goal.modify f g = Aesop.Goal.mk (f g.elim)

@[inline]

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

Equations

• g.id = g.elim.id

@[inline]

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

Equations

• g.parent = g.elim.parent

@[inline]

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

Equations

• g.children = g.elim.children

@[inline]

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

Equations

• g.origin = g.elim.origin

@[inline]

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

Equations

• g.depth = g.elim.depth

@[inline]

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

Equations

• g.state = g.elim.state

@[inline]

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

Equations

• g.isIrrelevant = g.elim.isIrrelevant

@[inline]

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

Equations

• g.isForcedUnprovable = g.elim.isForcedUnprovable

@[inline]

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

Equations

• g.preNormGoal = g.elim.preNormGoal

@[inline]

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

Equations

• g.normalizationState = g.elim.normalizationState

@[inline]

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

Equations

• g.mvars = g.elim.mvars

@[inline]

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

Equations

• g.forwardState = g.elim.forwardState

@[inline]

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

Equations

• g.forwardRuleMatches = g.elim.forwardRuleMatches

@[inline]

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

Equations

• g.successProbability = g.elim.successProbability

@[inline]

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

Equations

• g.addedInIteration = g.elim.addedInIteration

@[inline]

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

Equations

• g.lastExpandedInIteration = g.elim.lastExpandedInIteration

@[inline]

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

Equations

• g.failedRapps = g.elim.failedRapps

@[inline]

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

Equations

• g.unsafeRulesSelected = g.elim.unsafeRulesSelected

@[inline]

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

Equations

• g.unsafeQueue = g.elim.unsafeQueue

@[inline]

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

Equations

• g.unsafeQueue? = if g.unsafeRulesSelected = true then some g.unsafeQueue else none

@[inline]

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

Equations

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

@[inline]

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

Equations

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

@[inline]

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

Equations

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

@[inline]

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

Equations

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

@[inline]

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

Equations

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

@[inline]

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

Equations

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

@[inline]

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

Equations

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

@[inline]

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

Equations

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

@[inline]

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

Equations

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

@[inline]

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

Equations

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

@[inline]

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

Equations

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

@[inline]

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

Equations

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

@[inline]

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

Equations

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

@[inline]

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

Equations

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

@[inline]

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

Equations

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

@[inline]

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

Equations

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

@[inline]

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

Equations

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

@[inline]

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

Equations

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

@[inline]

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

Equations

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

instance Aesop.Goal.instNonempty : Nonempty Goal

@[implicit_reducible]

instance Aesop.Goal.instBEq : BEq Goal

Equations

• Aesop.Goal.instBEq = { beq := fun (g₁ g₂ : Aesop.Goal) => g₁.id == g₂.id }

@[implicit_reducible]

instance Aesop.Goal.instHashable : Hashable Goal

Equations

• Aesop.Goal.instHashable = { hash := fun (g : Aesop.Goal) => hash g.id }

@[inline]

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

Equations

• Aesop.Rapp.mk = Aesop.tree.introRapp

@[inline]

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

Equations

• Aesop.Rapp.elim = Aesop.tree.elimRapp

@[inline]

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

Equations

• Aesop.Rapp.modify f r = Aesop.Rapp.mk (f r.elim)

@[inline]

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

Equations

• r.id = r.elim.id

@[inline]

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

Equations

• r.parent = r.elim.parent

@[inline]

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

Equations

• r.children = r.elim.children

@[inline]

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

Equations

• r.state = r.elim.state

@[inline]

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

Equations

• r.isIrrelevant = r.elim.isIrrelevant

@[inline]

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

Equations

• r.appliedRule = r.elim.appliedRule

@[inline]

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

Equations

• r.scriptSteps? = r.elim.scriptSteps?

@[inline]

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

Equations

• r.originalSubgoals = r.elim.originalSubgoals

@[inline]

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

Equations

• r.successProbability = r.elim.successProbability

@[inline]

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

Equations

• r.metaState = r.elim.metaState

@[inline]

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

Equations

• r.introducedMVars = r.elim.introducedMVars

@[inline]

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

Equations

• r.assignedMVars = r.elim.assignedMVars

@[inline]

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

Equations

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

@[inline]

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

Equations

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

@[inline]

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

Equations

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

@[inline]

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

Equations

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

@[inline]

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

Equations

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

@[inline]

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

Equations

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

@[inline]

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

Equations

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

@[inline]

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

Equations

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

@[inline]

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

Equations

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

@[inline]

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

Equations

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

@[inline]

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

Equations

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

@[inline]

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

Equations

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

instance Aesop.Rapp.instNonempty : Nonempty Rapp

@[implicit_reducible]

instance Aesop.Rapp.instBEq : BEq Rapp

Equations

• Aesop.Rapp.instBEq = { beq := fun (r₁ r₂ : Aesop.Rapp) => r₁.id == r₂.id }

@[implicit_reducible]

instance Aesop.Rapp.instHashable : Hashable Rapp

Equations

• Aesop.Rapp.instHashable = { hash := fun (r : Aesop.Rapp) => hash r.id }

Miscellaneous Queries

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

Equations

• r.isSafe = (r.appliedRule.isSafe && r.assignedMVars.isEmpty)

@[inline]

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

Equations

• g.postNormGoalAndMetaState? = match g.normalizationState with | Aesop.NormalizationState.normal postGoal postState script => some (postGoal, postState) | x => none

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

Equations

• g.postNormGoal? = Option.map (fun (x : Lean.MVarId × Lean.Meta.SavedState) => x.fst) g.postNormGoalAndMetaState?

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

Equations

• g.currentGoal = g.postNormGoal?.getD g.preNormGoal

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

Equations

• g.parentRapp? = do let __do_lift ← ST.Ref.get g.parent pure __do_lift.parent?

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

Equations

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

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

Equations

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

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

Equations

• g.safeRapps = Array.filterM (fun (rref : Aesop.RappRef) => do let __do_lift ← ST.Ref.get rref pure __do_lift.isSafe) g.children

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

Equations

• g.hasSafeRapp = Array.anyM (fun (rref : Aesop.RappRef) => do let __do_lift ← ST.Ref.get rref pure __do_lift.isSafe) g.children

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

Equations

• g.isUnsafeExhausted = (g.unsafeRulesSelected && Subarray.isEmpty g.unsafeQueue)

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

Equations

• g.isExhausted = (pure g.isUnsafeExhausted <||> g.hasSafeRapp)

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

Equations

• g.isActive = do let __do_lift ← pure g.isIrrelevant <||> g.isExhausted pure !__do_lift

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

Equations

• g.hasProvableRapp = Array.anyM (fun (r : Aesop.RappRef) => do let __do_lift ← ST.Ref.get r pure !__do_lift.state.isUnprovable) g.children

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

Equations

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

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

Equations

• g.hasMVar = !g.mvars.isEmpty

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

Equations

• g.priority = g.successProbability * Aesop.unificationGoalPenalty ^ g.mvars.size

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

Equations

• g.isNormal = g.normalizationState.isNormal

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

Equations

• g.originalGoalId = g.origin.originalGoalId?.getD g.id

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

Equations

• g.isRoot = do let __do_lift ← g.parentRapp? pure __do_lift.isNone

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

Equations

• r.introducesMVar = !r.introducedMVars.isEmpty

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

Equations

• r.parentPostNormMetaState rootMetaState = do let __do_lift ← ST.Ref.get r.parent __do_lift.parentMetaState rootMetaState

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

Equations

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

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

Equations

• Aesop.Rapp.forSubgoalsM f r = Array.forM (fun (cref : Aesop.MVarClusterRef) => do let __do_lift ← ST.Ref.get cref Array.forM f __do_lift.goals) r.children

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

Equations

• r.subgoals = Aesop.Rapp.foldSubgoalsM #[] (fun (subgoals : Array Aesop.GoalRef) (gref : Aesop.GoalRef) => pure (subgoals.push gref)) r

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

Equations

• r.depth = do let __do_lift ← ST.Ref.get r.parent pure __do_lift.depth

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

Equations

• c.provenGoal? = Array.findM? (fun (gref : Aesop.GoalRef) => do let __do_lift ← ST.Ref.get gref pure __do_lift.state.isProven) c.goals

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.

Equations

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