Normalisation Rules

structure Aesop.NormRuleInfo : Type

• penalty : Int

@[implicit_reducible]

instance Aesop.instInhabitedNormRuleInfo : Inhabited NormRuleInfo

Equations

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

def Aesop.instInhabitedNormRuleInfo.default : NormRuleInfo

Equations

• Aesop.instInhabitedNormRuleInfo.default = { penalty := default }

@[implicit_reducible]

instance Aesop.instOrdNormRuleInfo : Ord NormRuleInfo

Equations

• Aesop.instOrdNormRuleInfo = { compare := fun (i j : Aesop.NormRuleInfo) => compare i.penalty j.penalty }

@[implicit_reducible]

instance Aesop.instLTNormRuleInfo : LT NormRuleInfo

Equations

• Aesop.instLTNormRuleInfo = ltOfOrd

@[implicit_reducible]

instance Aesop.instLENormRuleInfo : LE NormRuleInfo

Equations

• Aesop.instLENormRuleInfo = leOfOrd

@[reducible, inline]

abbrev Aesop.NormRule : Type

Equations

• Aesop.NormRule = Aesop.Rule Aesop.NormRuleInfo

@[implicit_reducible]

instance Aesop.instToStringNormRule : ToString NormRule

Equations

• Aesop.instToStringNormRule = { toString := fun (r : Aesop.NormRule) => toString "[" ++ toString r.extra.penalty ++ toString "] " ++ toString r.name }

def Aesop.defaultNormPenalty : Int

Equations

• Aesop.defaultNormPenalty = 1

def Aesop.defaultSimpRulePriority : Int

Equations

• Aesop.defaultSimpRulePriority = 1000

Safe and Almost Safe Rules

inductive Aesop.Safety : Type

• safe : Safety
• almostSafe : Safety

@[implicit_reducible]

instance Aesop.instInhabitedSafety : Inhabited Safety

Equations

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

def Aesop.instInhabitedSafety.default : Safety

Equations

• Aesop.instInhabitedSafety.default = Aesop.Safety.safe

@[implicit_reducible]

instance Aesop.Safety.instToString : ToString Safety

Equations

• Aesop.Safety.instToString = { toString := fun (x : Aesop.Safety) => match x with | Aesop.Safety.safe => "safe" | Aesop.Safety.almostSafe => "almostSafe" }

structure Aesop.SafeRuleInfo : Type

• penalty : Int
• safety : Safety

def Aesop.instInhabitedSafeRuleInfo.default : SafeRuleInfo

Equations

• Aesop.instInhabitedSafeRuleInfo.default = { penalty := default, safety := default }

@[implicit_reducible]

instance Aesop.instInhabitedSafeRuleInfo : Inhabited SafeRuleInfo

Equations

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

@[implicit_reducible]

instance Aesop.instOrdSafeRuleInfo : Ord SafeRuleInfo

Equations

• Aesop.instOrdSafeRuleInfo = { compare := fun (i j : Aesop.SafeRuleInfo) => compare i.penalty j.penalty }

@[implicit_reducible]

instance Aesop.instLTSafeRuleInfo : LT SafeRuleInfo

Equations

• Aesop.instLTSafeRuleInfo = ltOfOrd

@[implicit_reducible]

instance Aesop.instLESafeRuleInfo : LE SafeRuleInfo

Equations

• Aesop.instLESafeRuleInfo = leOfOrd

@[reducible, inline]

abbrev Aesop.SafeRule : Type

Equations

• Aesop.SafeRule = Aesop.Rule Aesop.SafeRuleInfo

@[implicit_reducible]

instance Aesop.instToStringSafeRule : ToString SafeRule

Equations

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

def Aesop.defaultSafePenalty : Int

Equations

• Aesop.defaultSafePenalty = 1

Unsafe Rules

structure Aesop.UnsafeRuleInfo : Type

• successProbability : Percent

@[implicit_reducible]

instance Aesop.instInhabitedUnsafeRuleInfo : Inhabited UnsafeRuleInfo

Equations

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

def Aesop.instInhabitedUnsafeRuleInfo.default : UnsafeRuleInfo

Equations

• Aesop.instInhabitedUnsafeRuleInfo.default = { successProbability := default }

@[implicit_reducible]

instance Aesop.instOrdUnsafeRuleInfo : Ord UnsafeRuleInfo

Equations

• Aesop.instOrdUnsafeRuleInfo = { compare := fun (i j : Aesop.UnsafeRuleInfo) => compare j.successProbability i.successProbability }

@[implicit_reducible]

instance Aesop.instLTUnsafeRuleInfo : LT UnsafeRuleInfo

Equations

• Aesop.instLTUnsafeRuleInfo = ltOfOrd

@[implicit_reducible]

instance Aesop.instLEUnsafeRuleInfo : LE UnsafeRuleInfo

Equations

• Aesop.instLEUnsafeRuleInfo = leOfOrd

@[reducible, inline]

abbrev Aesop.UnsafeRule : Type

Equations

• Aesop.UnsafeRule = Aesop.Rule Aesop.UnsafeRuleInfo

@[implicit_reducible]

instance Aesop.instToStringUnsafeRule : ToString UnsafeRule

Equations

• Aesop.instToStringUnsafeRule = { toString := fun (r : Aesop.UnsafeRule) => toString "[" ++ toString r.extra.successProbability.toHumanString ++ toString "] " ++ toString r.name }

def Aesop.defaultSuccessProbability : Percent

Equations

• Aesop.defaultSuccessProbability = Aesop.Percent.fifty

Regular Rules

inductive Aesop.RegularRule : Type

• safe (r : SafeRule) : RegularRule
• unsafe (r : UnsafeRule) : RegularRule

def Aesop.instInhabitedRegularRule.default : RegularRule

Equations

• Aesop.instInhabitedRegularRule.default = Aesop.RegularRule.safe default

@[implicit_reducible]

instance Aesop.instInhabitedRegularRule : Inhabited RegularRule

Equations

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

def Aesop.instBEqRegularRule.beq : RegularRule → RegularRule → Bool

Equations

• Aesop.instBEqRegularRule.beq (Aesop.RegularRule.safe a) (Aesop.RegularRule.safe b) = (a == b)
• Aesop.instBEqRegularRule.beq (Aesop.RegularRule.unsafe a) (Aesop.RegularRule.unsafe b) = (a == b)
• Aesop.instBEqRegularRule.beq x✝¹ x✝ = false

@[implicit_reducible]

instance Aesop.instBEqRegularRule : BEq RegularRule

Equations

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

@[implicit_reducible]

instance Aesop.RegularRule.instToFormat : Std.ToFormat RegularRule

Equations

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

def Aesop.RegularRule.successProbability : RegularRule → Percent

Equations

• (Aesop.RegularRule.safe r).successProbability = Aesop.Percent.hundred
• (Aesop.RegularRule.unsafe r).successProbability = r.extra.successProbability

def Aesop.RegularRule.isSafe : RegularRule → Bool

Equations

• (Aesop.RegularRule.safe r).isSafe = true
• (Aesop.RegularRule.unsafe r).isSafe = false

def Aesop.RegularRule.isUnsafe : RegularRule → Bool

Equations

• (Aesop.RegularRule.safe r).isUnsafe = false
• (Aesop.RegularRule.unsafe r).isUnsafe = true

@[inline]

def Aesop.RegularRule.withRule {β : Sort u_1} (f : {α : Type} → Rule α → β) : RegularRule → β

Equations

• Aesop.RegularRule.withRule f (Aesop.RegularRule.safe r) = f r
• Aesop.RegularRule.withRule f (Aesop.RegularRule.unsafe r) = f r

def Aesop.RegularRule.name (r : RegularRule) : RuleName

Equations

• r.name = Aesop.RegularRule.withRule (fun {α : Type} (x : Aesop.Rule α) => x.name) r

def Aesop.RegularRule.indexingMode (r : RegularRule) : IndexingMode

Equations

• r.indexingMode = Aesop.RegularRule.withRule (fun {α : Type} (x : Aesop.Rule α) => x.indexingMode) r

def Aesop.RegularRule.tac (r : RegularRule) : RuleTacDescr

Equations

• r.tac = Aesop.RegularRule.withRule (fun {α : Type} (x : Aesop.Rule α) => x.tac) r

Normalisation Simp Rules

structure Aesop.NormSimpRule : Type

A global rule for the norm simplifier. Each SimpEntry represents a member of the simp set, e.g. a declaration whose type is an equality or a smart unfolding theorem for a declaration.

• name : RuleName
• entries : Array Lean.Meta.SimpEntry

@[implicit_reducible]

instance Aesop.instInhabitedNormSimpRule : Inhabited NormSimpRule

Equations

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

def Aesop.instInhabitedNormSimpRule.default : NormSimpRule

Equations

• Aesop.instInhabitedNormSimpRule.default = { name := default, entries := default }

@[implicit_reducible]

instance Aesop.NormSimpRule.instBEq : BEq NormSimpRule

Equations

• Aesop.NormSimpRule.instBEq = { beq := fun (r s : Aesop.NormSimpRule) => r.name == s.name }

@[implicit_reducible]

instance Aesop.NormSimpRule.instHashable : Hashable NormSimpRule

Equations

• Aesop.NormSimpRule.instHashable = { hash := fun (r : Aesop.NormSimpRule) => hash r.name }

structure Aesop.LocalNormSimpRule : Type

A local rule for the norm simplifier.

• id : Lean.Name
• simpTheorem : Lean.Term

@[implicit_reducible]

instance Aesop.instInhabitedLocalNormSimpRule : Inhabited LocalNormSimpRule

Equations

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

def Aesop.instInhabitedLocalNormSimpRule.default : LocalNormSimpRule

Equations

• Aesop.instInhabitedLocalNormSimpRule.default = { id := default, simpTheorem := default }

@[implicit_reducible]

instance Aesop.LocalNormSimpRule.instBEq : BEq LocalNormSimpRule

Equations

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

@[implicit_reducible]

instance Aesop.LocalNormSimpRule.instHashable : Hashable LocalNormSimpRule

Equations

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

def Aesop.LocalNormSimpRule.name (r : LocalNormSimpRule) : RuleName

Equations

• r.name = { name := r.id, builder := Aesop.BuilderName.simp, phase := Aesop.PhaseName.norm, scope := Aesop.ScopeName.local }

structure Aesop.UnfoldRule : Type

• decl : Lean.Name
• unfoldThm? : Option Lean.Name

@[implicit_reducible]

instance Aesop.instInhabitedUnfoldRule : Inhabited UnfoldRule

Equations

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

def Aesop.instInhabitedUnfoldRule.default : UnfoldRule

Equations

• Aesop.instInhabitedUnfoldRule.default = { decl := default, unfoldThm? := default }

@[implicit_reducible]

instance Aesop.UnfoldRule.instBEq : BEq UnfoldRule

Equations

• Aesop.UnfoldRule.instBEq = { beq := fun (r s : Aesop.UnfoldRule) => r.decl == s.decl }

@[implicit_reducible]

instance Aesop.UnfoldRule.instHashable : Hashable UnfoldRule

Equations

• Aesop.UnfoldRule.instHashable = { hash := fun (r : Aesop.UnfoldRule) => hash r.decl }

def Aesop.UnfoldRule.name (r : UnfoldRule) : RuleName

Equations

• r.name = { name := r.decl, builder := Aesop.BuilderName.unfold, phase := Aesop.PhaseName.norm, scope := Aesop.ScopeName.global }