## Node IDs #

## Equations

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

## Equations

- Aesop.GoalId.succ x = match x with | { toNat := n } => { toNat := n + 1 }

## Instances For

## Equations

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

## Instances For

## Equations

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

instance
Aesop.GoalId.instDecidableRelGoalIdLtInstLTGoalId :

DecidableRel fun (x x_1 : Aesop.GoalId) => x < x_1

## Equations

- Aesop.GoalId.instDecidableRelGoalIdLtInstLTGoalId n m = inferInstanceAs (Decidable (n.toNat < m.toNat))

## Equations

- Aesop.GoalId.instToStringGoalId = { toString := fun (n : Aesop.GoalId) => toString n.toNat }

## Equations

- Aesop.GoalId.instHashableGoalId = { hash := fun (n : Aesop.GoalId) => hash n.toNat }

## Rule Application IDs #

## Equations

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

## Equations

- Aesop.RappId.succ x = match x with | { toNat := n } => { toNat := n + 1 }

## Instances For

## Equations

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

## Instances For

## Equations

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

instance
Aesop.RappId.instDecidableRelRappIdLtInstLTRappId :

DecidableRel fun (x x_1 : Aesop.RappId) => x < x_1

## Equations

- Aesop.RappId.instDecidableRelRappIdLtInstLTRappId n m = inferInstanceAs (Decidable (n.toNat < m.toNat))

## Equations

- Aesop.RappId.instToStringRappId = { toString := fun (n : Aesop.RappId) => toString n.toNat }

## Equations

- Aesop.RappId.instHashableRappId = { hash := fun (n : Aesop.RappId) => hash n.toNat }

## Iterations #

@[inline]

## Equations

## Instances For

@[inline]

## Equations

## Instances For

## Equations

## Instances For

## Equations

## Equations

instance
Aesop.Iteration.instDecidableRelIterationLtInstLTIteration :

DecidableRel fun (x x_1 : Aesop.Iteration) => x < x_1

## Equations

- Aesop.Iteration.instDecidableRelIterationLtInstLTIteration = inferInstanceAs (DecidableRel fun (x x_1 : Nat) => x < x_1)

instance
Aesop.Iteration.instDecidableRelIterationLeInstLEIteration :

DecidableRel fun (x x_1 : Aesop.Iteration) => x ≤ x_1

## Equations

- Aesop.Iteration.instDecidableRelIterationLeInstLEIteration = inferInstanceAs (DecidableRel fun (x x_1 : Nat) => x ≤ x_1)

## The Tree #

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

## Instances For

## Equations

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

## Equations

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

## Equations

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

## Equations

- Aesop.NodeState.isUnknown x = match x with | Aesop.NodeState.unknown => true | x => false

## Instances For

## Equations

- Aesop.NodeState.isProven x = match x with | Aesop.NodeState.proven => true | x => false

## Instances For

## Equations

- Aesop.NodeState.isUnprovable x = match x with | Aesop.NodeState.unprovable => true | x => false

## Instances For

## Equations

- Aesop.NodeState.isIrrelevant x = match x with | Aesop.NodeState.proven => true | Aesop.NodeState.unprovable => true | Aesop.NodeState.unknown => false

## Instances For

## Equations

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

## Instances For

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

## Instances For

## Equations

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

## Equations

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

## Equations

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

## Equations

- Aesop.GoalState.isProvenByRuleApplication x = match x with | Aesop.GoalState.provenByRuleApplication => true | x => false

## Instances For

## Equations

- Aesop.GoalState.isProvenByNormalization x = match x with | Aesop.GoalState.provenByNormalization => true | x => false

## Instances For

## Equations

- Aesop.GoalState.isProven x = match x with | Aesop.GoalState.provenByRuleApplication => true | Aesop.GoalState.provenByNormalization => true | x => false

## Instances For

## Equations

- Aesop.GoalState.isUnprovable x = match x with | Aesop.GoalState.unprovable => true | x => false

## Instances For

## Equations

- Aesop.GoalState.isUnknown x = match x with | Aesop.GoalState.unknown => true | x => false

## Instances For

## Equations

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

## Instances For

## Equations

## Instances For

## Equations

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

## Instances For

- notNormal: Aesop.NormalizationState
- normal: Lean.MVarId → Lean.Meta.SavedState → Except Aesop.DisplayRuleName Aesop.UnstructuredScript → Aesop.NormalizationState
- provenByNormalization: Lean.Meta.SavedState → Except Aesop.DisplayRuleName Aesop.UnstructuredScript → Aesop.NormalizationState

## Instances For

## Equations

## Equations

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

## Instances For

## Equations

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

## Instances For

## Equations

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

## Instances For

A goal `G`

can be added to the tree for three reasons:

`G`

was produced by its parent rule as a subgoal. This is the most common reason.`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

## Instances For

## Equations

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

## Equations

- Aesop.GoalOrigin.originalGoalId? x = match x with | Aesop.GoalOrigin.copied from rep => some rep | x => none

## Instances For

## Equations

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

## Instances For

- id : Aesop.GoalId
- parent : IO.Ref MVarCluster
- 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

## Instances For

instance
Aesop.instNonemptyGoalData :

∀ {Rapp MVarCluster : Type} [inst : Nonempty MVarCluster], Nonempty (Aesop.GoalData Rapp MVarCluster)

## Equations

- (_ : Nonempty (Aesop.GoalData Rapp MVarCluster)) = (_ : Nonempty (Aesop.GoalData Rapp MVarCluster))

instance
Aesop.instInhabitedMVarClusterData :

{a a_1 : Type} → Inhabited (Aesop.MVarClusterData a a_1)

## Equations

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

- id : Aesop.RappId
- parent : IO.Ref Goal
- state : Aesop.NodeState
- isIrrelevant : Bool
- appliedRule : Aesop.RegularRule
- scriptBuilder? : Option Aesop.RuleTacScriptBuilder
- originalSubgoals : Array Lean.MVarId
- successProbability : Aesop.Percent
- metaState : Lean.Meta.SavedState
- introducedMVars : Aesop.UnorderedArraySet Lean.MVarId
- assignedMVars : Aesop.UnorderedArraySet Lean.MVarId

## Instances For

instance
Aesop.instNonemptyRappData :

∀ {Goal : Type} [inst : Nonempty Goal] {MVarCluster : Type}, Nonempty (Aesop.RappData Goal MVarCluster)

## Equations

- (_ : Nonempty (Aesop.RappData Goal MVarCluster)) = (_ : Nonempty (Aesop.RappData Goal MVarCluster))

## Instances For

## Instances For

## Instances For

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

## Instances For

## Equations

## Equations

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

## Instances For

@[inline, reducible]

## Equations

## Instances For

@[inline, reducible]

## Equations

## Instances For

@[inline, reducible]

## Equations

## Instances For

@[inline]

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

## Equations

## Instances For

@[inline]

## Equations

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

## Instances For

@[inline]

## Equations

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

## Instances For

@[inline]

## Equations

- Aesop.MVarCluster.isIrrelevant c = (Aesop.MVarCluster.elim c).isIrrelevant

## Instances For

@[inline]

## Equations

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

## Instances For

@[inline]

## Equations

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

## Instances For

@[inline]

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

## Equations

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

## Instances For

@[inline]

## Equations

- Aesop.Goal.isForcedUnprovable g = (Aesop.Goal.elim g).isForcedUnprovable

## Instances For

@[inline]

## Equations

- Aesop.Goal.normalizationState g = (Aesop.Goal.elim g).normalizationState

## Instances For

@[inline]

## Equations

- Aesop.Goal.successProbability g = (Aesop.Goal.elim g).successProbability

## Instances For

@[inline]

## Equations

- Aesop.Goal.addedInIteration g = (Aesop.Goal.elim g).addedInIteration

## Instances For

@[inline]

## Equations

- Aesop.Goal.lastExpandedInIteration g = (Aesop.Goal.elim g).lastExpandedInIteration

## Instances For

@[inline]

## Equations

- Aesop.Goal.unsafeRulesSelected g = (Aesop.Goal.elim g).unsafeRulesSelected

## Instances For

@[inline]

## Equations

- Aesop.Goal.unsafeQueue? g = if Aesop.Goal.unsafeRulesSelected g = true then some (Aesop.Goal.unsafeQueue g) else none

## Instances For

@[inline]

## Equations

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

## Instances For

@[inline]

## Equations

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

## Instances For

@[inline]

## Equations

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

## Instances For

@[inline]

## Equations

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

## Instances For

@[inline]

## Equations

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

## Instances For

@[inline]

## Equations

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

## Instances For

@[inline]

## Equations

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

## Instances For

@[inline]

## Equations

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

## Instances For

@[inline]

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

## Equations

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

## Instances For

@[inline]

## Equations

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

## Instances For

@[inline]

## Equations

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

## Instances For

@[inline]

## Equations

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

## Instances For

@[inline]

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

## Equations

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

## Instances For

@[inline]

## Equations

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

## Instances For

@[inline]

## Equations

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

## Instances For

@[inline]

## Equations

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

## Instances For

@[inline]

## Equations

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

## Instances For

## Equations

## Equations

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

## Equations

- Aesop.Goal.instHashableGoal = { hash := fun (g : Aesop.Goal) => hash (Aesop.Goal.id g) }

@[inline]

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

## Equations

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

## Instances For

@[inline]

## Equations

- Aesop.Rapp.originalSubgoals r = (Aesop.Rapp.elim r).originalSubgoals

## Instances For

@[inline]

## Equations

- Aesop.Rapp.successProbability r = (Aesop.Rapp.elim r).successProbability

## Instances For

@[inline]

## Equations

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

## Instances For

@[inline]

## Equations

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

## Instances For

@[inline]

## Equations

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

## Instances For

@[inline]

## Equations

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

## Instances For

@[inline]

## Equations

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

## Instances For

@[inline]

## Equations

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

## Instances For

@[inline]

def
Aesop.Rapp.setScriptBuilder?
(scriptBuilder? : Option Aesop.RuleTacScriptBuilder)
(r : Aesop.Rapp)
:

## Equations

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

## Instances For

@[inline]

## Equations

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

## Instances For

@[inline]

## Equations

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

## Instances For

@[inline]

## Equations

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

## Instances For

@[inline]

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

## Equations

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

## Instances For

@[inline]

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

## Equations

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

## Instances For

## Equations

## Equations

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

## Equations

- Aesop.Rapp.instHashableRapp = { hash := fun (r : Aesop.Rapp) => hash (Aesop.Rapp.id r) }

## Miscellaneous Queries #

@[inline]

## Equations

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

## Instances For

## Equations

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

## Instances For

## Equations

## Instances For

## Equations

- Aesop.Goal.parentRapp? g = do let __do_lift ← ST.Ref.get (Aesop.Goal.parent g) pure (Aesop.MVarCluster.parent? __do_lift)

## Instances For

## Equations

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

## Instances For

## Equations

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

## Instances For

## Equations

## Instances For

## Equations

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

## Instances For

## Equations

- Aesop.Goal.isActive g = do let __do_lift ← pure (Aesop.Goal.isIrrelevant g) <||> Aesop.Goal.isExhausted g pure !__do_lift

## Instances For

## Equations

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

## Instances For

## Equations

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

## Instances For

## Equations

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

## Instances For

## Equations

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

## Instances For

## Equations

## Instances For

## Equations

## Instances For

## Equations

## Instances For

## Equations

## Instances For

## Equations

- Aesop.Goal.isRoot g = do let __do_lift ← Aesop.Goal.parentRapp? g pure (Option.isNone __do_lift)

## Instances For

## Equations

## Instances For

## Equations

- Aesop.Rapp.parentPostNormMetaState r rootMetaState = do let __do_lift ← ST.Ref.get (Aesop.Rapp.parent r) Aesop.Goal.parentMetaState __do_lift rootMetaState

## Instances For

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.

## Instances For

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

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

## Instances For

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

m (Array Aesop.GoalRef)

## Equations

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

## Instances For

## Equations

- Aesop.Rapp.depth r = do let __do_lift ← ST.Ref.get (Aesop.Rapp.parent r) pure (Aesop.Goal.depth __do_lift)

## Instances For

## Equations

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