Node IDs

structure Aesop.GoalId : Type

• toNat : Nat

instance Aesop.instInhabitedGoalId : Inhabited Aesop.GoalId

Equations

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

instance Aesop.instDecidableEqGoalId : DecidableEq Aesop.GoalId

Equations

• Aesop.instDecidableEqGoalId = Aesop.decEqGoalId✝

def Aesop.GoalId.zero : Aesop.GoalId

Equations

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

def Aesop.GoalId.one : Aesop.GoalId

Equations

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

def Aesop.GoalId.succ : Aesop.GoalId → Aesop.GoalId

Equations

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

def Aesop.GoalId.dummy : Aesop.GoalId

Equations

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

instance Aesop.GoalId.instLT : LT Aesop.GoalId

Equations

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

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

Equations

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

instance Aesop.GoalId.instToString : ToString Aesop.GoalId

Equations

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

instance Aesop.GoalId.instHashable : Hashable Aesop.GoalId

Equations

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

Rule Application IDs

structure Aesop.RappId : Type

• toNat : Nat

instance Aesop.instInhabitedRappId : Inhabited Aesop.RappId

Equations

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

instance Aesop.instDecidableEqRappId : DecidableEq Aesop.RappId

Equations

• Aesop.instDecidableEqRappId = Aesop.decEqRappId✝

def Aesop.RappId.zero : Aesop.RappId

Equations

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

def Aesop.RappId.succ : Aesop.RappId → Aesop.RappId

Equations

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

def Aesop.RappId.one : Aesop.RappId

Equations

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

def Aesop.RappId.dummy : Aesop.RappId

Equations

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

instance Aesop.RappId.instLT : LT Aesop.RappId

Equations

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

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

Equations

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

instance Aesop.RappId.instToString : ToString Aesop.RappId

Equations

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

instance Aesop.RappId.instHashable : Hashable Aesop.RappId

Equations

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

Iterations

def Aesop.Iteration : Type

Equations

• Aesop.Iteration = Nat

instance Aesop.instIterationInhabited : Inhabited Aesop.Iteration

Equations

• Aesop.instIterationInhabited = instInhabitedNat

@[inline]

def Aesop.Iteration.one : Aesop.Iteration

Equations

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

@[inline]

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

Equations

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

def Aesop.Iteration.none : Aesop.Iteration

Equations

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

instance Aesop.Iteration.instDecidableEq : DecidableEq Aesop.Iteration

Equations

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

instance Aesop.Iteration.instToString : ToString Aesop.Iteration

Equations

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

instance Aesop.Iteration.instLT : LT Aesop.Iteration

Equations

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

instance Aesop.Iteration.instLE : LE Aesop.Iteration

Equations

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

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

Equations

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

instance Aesop.Iteration.instDecidableRelLe : DecidableRel fun (x1 x2 : Aesop.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: Aesop.NodeState
• proven: Aesop.NodeState
• unprovable: Aesop.NodeState

instance Aesop.instInhabitedNodeState : Inhabited Aesop.NodeState

Equations

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

instance Aesop.instBEqNodeState : BEq Aesop.NodeState

Equations

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

instance Aesop.NodeState.instToString : ToString Aesop.NodeState

Equations

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

def Aesop.NodeState.isUnknown : Aesop.NodeState → Bool

Equations

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

def Aesop.NodeState.isProven : Aesop.NodeState → Bool

Equations

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

def Aesop.NodeState.isUnprovable : Aesop.NodeState → Bool

Equations

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

def Aesop.NodeState.isIrrelevant : Aesop.NodeState → Bool

Equations

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

def Aesop.NodeState.toEmoji : Aesop.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: Aesop.GoalState
• provenByRuleApplication: Aesop.GoalState
• provenByNormalization: Aesop.GoalState
• unprovable: Aesop.GoalState

instance Aesop.instInhabitedGoalState : Inhabited Aesop.GoalState

Equations

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

instance Aesop.instBEqGoalState : BEq Aesop.GoalState

Equations

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

instance Aesop.GoalState.instToString : ToString Aesop.GoalState

Equations

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

def Aesop.GoalState.isProvenByRuleApplication : Aesop.GoalState → Bool

Equations

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

def Aesop.GoalState.isProvenByNormalization : Aesop.GoalState → Bool

Equations

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

def Aesop.GoalState.isProven : Aesop.GoalState → Bool

Equations

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

def Aesop.GoalState.isUnprovable : Aesop.GoalState → Bool

Equations

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

def Aesop.GoalState.isUnknown : Aesop.GoalState → Bool

Equations

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

def Aesop.GoalState.toNodeState : Aesop.GoalState → Aesop.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 : Aesop.GoalState) : Bool

Equations

• s.isIrrelevant = s.toNodeState.isIrrelevant

def Aesop.GoalState.toEmoji : Aesop.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: Aesop.NormalizationState
• normal: Lean.MVarId → Lean.Meta.SavedState → Array (Aesop.DisplayRuleName × Option (Array Aesop.Script.LazyStep)) → Aesop.NormalizationState
• provenByNormalization: Lean.Meta.SavedState → Array (Aesop.DisplayRuleName × Option (Array Aesop.Script.LazyStep)) → Aesop.NormalizationState

instance Aesop.instInhabitedNormalizationState : Inhabited Aesop.NormalizationState

Equations

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

def Aesop.NormalizationState.isNormal : Aesop.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 : Aesop.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? : Aesop.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: Aesop.GoalOrigin
• copied: Aesop.GoalId → Aesop.GoalId → Aesop.GoalOrigin
• droppedMVar: Aesop.GoalOrigin

instance Aesop.instInhabitedGoalOrigin : Inhabited Aesop.GoalOrigin

Equations

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

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

Equations

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

def Aesop.GoalOrigin.toString : Aesop.GoalOrigin → String

Equations

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

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

• id : Aesop.GoalId
• parent : IO.Ref MVarCluster
• children : Array (IO.Ref Rapp)
• origin : Aesop.GoalOrigin
• depth : Nat
• state : Aesop.GoalState
• isIrrelevant : Bool
• isForcedUnprovable : Bool
• preNormGoal : Lean.MVarId
• normalizationState : Aesop.NormalizationState
• mvars : Aesop.UnorderedArraySet Lean.MVarId
• successProbability : Aesop.Percent
• addedInIteration : Aesop.Iteration
• lastExpandedInIteration : Aesop.Iteration
• unsafeRulesSelected : Bool
• unsafeQueue : Aesop.UnsafeQueue
• failedRapps : Array Aesop.RegularRule

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

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

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

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

Equations

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

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

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

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

unsafe inductive Aesop.GoalUnsafe : Type

• mk: Aesop.GoalData Aesop.RappUnsafe Aesop.MVarClusterUnsafe → Aesop.GoalUnsafe

unsafe inductive Aesop.MVarClusterUnsafe : Type

• mk: Aesop.MVarClusterData Aesop.GoalUnsafe Aesop.RappUnsafe → Aesop.MVarClusterUnsafe

unsafe inductive Aesop.RappUnsafe : Type

• mk: Aesop.RappData Aesop.GoalUnsafe Aesop.MVarClusterUnsafe → Aesop.RappUnsafe

structure Aesop.TreeSpec : Type 1

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

theorem Aesop.instNonemptyTreeSpec : Nonempty Aesop.TreeSpec

unsafe def Aesop.treeImpl : Aesop.TreeSpec

@[implemented_by Aesop.treeImpl]

opaque Aesop.tree : Aesop.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 : Aesop.MVarClusterData Aesop.Goal Aesop.Rapp → Aesop.MVarCluster

Equations

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

theorem Aesop.MVarCluster.instNonempty : Nonempty Aesop.MVarCluster

@[inline]

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

Equations

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

@[inline]

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

Equations

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

@[inline]

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

Equations

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

@[inline]

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

Equations

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

@[inline]

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

Equations

• c.goals = c.elim.goals

@[inline]

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

Equations

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

@[inline]

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

Equations

• c.isIrrelevant = c.elim.isIrrelevant

@[inline]

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

Equations

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

@[inline]

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

Equations

• c.state = c.elim.state

@[inline]

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

Equations

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

@[inline]

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

Equations

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

@[inline]

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

Equations

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

@[inline]

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

Equations

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

@[inline]

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

Equations

• g.id = g.elim.id

@[inline]

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

Equations

• g.parent = g.elim.parent

@[inline]

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

Equations

• g.children = g.elim.children

@[inline]

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

Equations

• g.origin = g.elim.origin

@[inline]

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

Equations

• g.depth = g.elim.depth

@[inline]

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

Equations

• g.state = g.elim.state

@[inline]

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

Equations

• g.isIrrelevant = g.elim.isIrrelevant

@[inline]

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

Equations

• g.isForcedUnprovable = g.elim.isForcedUnprovable

@[inline]

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

Equations

• g.preNormGoal = g.elim.preNormGoal

@[inline]

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

Equations

• g.normalizationState = g.elim.normalizationState

@[inline]

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

Equations

• g.mvars = g.elim.mvars

@[inline]

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

Equations

• g.successProbability = g.elim.successProbability

@[inline]

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

Equations

• g.addedInIteration = g.elim.addedInIteration

@[inline]

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

Equations

• g.lastExpandedInIteration = g.elim.lastExpandedInIteration

@[inline]

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

Equations

• g.failedRapps = g.elim.failedRapps

@[inline]

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

Equations

• g.unsafeRulesSelected = g.elim.unsafeRulesSelected

@[inline]

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

Equations

• g.unsafeQueue = g.elim.unsafeQueue

@[inline]

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

Equations

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

@[inline]

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

Equations

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

@[inline]

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

Equations

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

@[inline]

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

Equations

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

@[inline]

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

Equations

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

@[inline]

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

Equations

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

@[inline]

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

Equations

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

@[inline]

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

Equations

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

@[inline]

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

Equations

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

@[inline]

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

Equations

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

@[inline]

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

Equations

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

@[inline]

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

Equations

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

@[inline]

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

Equations

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

@[inline]

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

Equations

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

@[inline]

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

Equations

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

@[inline]

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

Equations

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

@[inline]

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

Equations

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

@[inline]

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

Equations

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

theorem Aesop.Goal.instNonempty : Nonempty Aesop.Goal

instance Aesop.Goal.instBEq : BEq Aesop.Goal

Equations

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

instance Aesop.Goal.instHashable : Hashable Aesop.Goal

Equations

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

@[inline]

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

Equations

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

@[inline]

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

Equations

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

@[inline]

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

Equations

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

@[inline]

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

Equations

• r.id = r.elim.id

@[inline]

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

Equations

• r.parent = r.elim.parent

@[inline]

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

Equations

• r.children = r.elim.children

@[inline]

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

Equations

• r.state = r.elim.state

@[inline]

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

Equations

• r.isIrrelevant = r.elim.isIrrelevant

@[inline]

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

Equations

• r.appliedRule = r.elim.appliedRule

@[inline]

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

Equations

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

@[inline]

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

Equations

• r.originalSubgoals = r.elim.originalSubgoals

@[inline]

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

Equations

• r.successProbability = r.elim.successProbability

@[inline]

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

Equations

• r.metaState = r.elim.metaState

@[inline]

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

Equations

• r.introducedMVars = r.elim.introducedMVars

@[inline]

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

Equations

• r.assignedMVars = r.elim.assignedMVars

@[inline]

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

Equations

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

@[inline]

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

Equations

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

@[inline]

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

Equations

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

@[inline]

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

Equations

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

@[inline]

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

Equations

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

@[inline]

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

Equations

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

@[inline]

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

Equations

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

@[inline]

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

Equations

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

@[inline]

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

Equations

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

@[inline]

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

Equations

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

@[inline]

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

Equations

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

@[inline]

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

Equations

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

theorem Aesop.Rapp.instNonempty : Nonempty Aesop.Rapp

instance Aesop.Rapp.instBEq : BEq Aesop.Rapp

Equations

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

instance Aesop.Rapp.instHashable : Hashable Aesop.Rapp

Equations

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

Miscellaneous Queries

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

Equations

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

@[inline]

def Aesop.Goal.postNormGoalAndMetaState? (g : Aesop.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 : Aesop.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 : Aesop.Goal) : Lean.MVarId

Equations

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

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

Equations

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

def Aesop.Goal.parentMetaState (g : Aesop.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 : Aesop.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 : Aesop.Goal) : BaseIO (Array Aesop.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 : Aesop.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 : Aesop.Goal) : Bool

Equations

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

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

Equations

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

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

Equations

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

def Aesop.Goal.hasProvableRapp (g : Aesop.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 : Aesop.Goal) : BaseIO (Option Aesop.RappRef)

Equations

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

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

Equations

• g.hasMVar = !g.mvars.isEmpty

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

Equations

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

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

Equations

• g.isNormal = g.normalizationState.isNormal

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

Equations

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

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

Equations

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

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

Equations

• r.introducesMVar = !r.introducedMVars.isEmpty

def Aesop.Rapp.parentPostNormMetaState (r : Aesop.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 : σ → Aesop.GoalRef → m σ) (r : Aesop.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 : Aesop.GoalRef → m Unit) (r : Aesop.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 : Aesop.Rapp) : m (Array Aesop.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 : Aesop.Rapp) : BaseIO Nat

Equations

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

def Aesop.MVarCluster.provenGoal? (c : Aesop.MVarCluster) : BaseIO (Option Aesop.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