inductive Duper.Comparison : Type

• GreaterThan : Comparison
• LessThan : Comparison
• Equal : Comparison
• Incomparable : Comparison

instance Duper.instBEqComparison : BEq Comparison

Equations

• Duper.instBEqComparison = { beq := Duper.beqComparison✝ }

instance Duper.instInhabitedComparison : Inhabited Comparison

Equations

• Duper.instInhabitedComparison = { default := Duper.Comparison.GreaterThan }

inductive Duper.Symbol : Type

• FVarId : Lean.FVarId → Symbol
• Const : Lean.Name → Symbol

instance Duper.instBEqSymbol : BEq Symbol

Equations

• Duper.instBEqSymbol = { beq := Duper.beqSymbol✝ }

instance Duper.instInhabitedSymbol : Inhabited Symbol

Equations

• Duper.instInhabitedSymbol = { default := Duper.Symbol.FVarId default }

instance Duper.instHashableSymbol : Hashable Symbol

Equations

• Duper.instHashableSymbol = { hash := Duper.hashSymbol✝ }

def Duper.Symbol.format : Symbol → Lean.MessageData

Equations

• (Duper.Symbol.FVarId a).format = Lean.toMessageData "FVarId " ++ Lean.toMessageData a.name ++ Lean.toMessageData ""
• (Duper.Symbol.Const a).format = Lean.toMessageData "Const " ++ Lean.toMessageData a ++ Lean.toMessageData ""

def Duper.Symbol.toString : Symbol → String

Equations

• (Duper.Symbol.FVarId a).toString = toString "FVarId " ++ toString a.name ++ toString ""
• (Duper.Symbol.Const a).toString = toString "Const " ++ toString a ++ toString ""

instance Duper.instToMessageDataSymbol : Lean.ToMessageData Symbol

Equations

• Duper.instToMessageDataSymbol = { toMessageData := Duper.Symbol.format }

instance Duper.instToStringSymbol : ToString Symbol

Equations

• Duper.instToStringSymbol = { toString := Duper.Symbol.toString }

@[reducible, inline]

abbrev Duper.SymbolPrecMap : Type

Equations

• Duper.SymbolPrecMap = Std.HashMap Duper.Symbol Nat

def Duper.Comparison.flip : Comparison → Comparison

Equations

• Duper.Comparison.GreaterThan.flip = Duper.Comparison.LessThan
• Duper.Comparison.LessThan.flip = Duper.Comparison.GreaterThan
• Duper.Comparison.Incomparable.flip = Duper.Comparison.Incomparable
• Duper.Comparison.Equal.flip = Duper.Comparison.Equal

instance Duper.Comparison.instToMessageData : Lean.ToMessageData Comparison

Equations

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

def Duper.Order.Weight : Type

Equations

• Duper.Order.Weight = (Int × Int)

instance Duper.Order.instWeightInhabited : Inhabited Weight

Equations

• Duper.Order.instWeightInhabited = instInhabitedProd

instance Duper.Order.instWeightDecidableEq : DecidableEq Weight

Equations

• Duper.Order.instWeightDecidableEq a b = instDecidableEqProd a b

instance Duper.Order.instAddWeight : Add Weight

Equations

• Duper.Order.instAddWeight = { add := fun (x x_1 : Duper.Order.Weight) => match x with | (a₁, b₁) => match x_1 with | (a₂, b₂) => (a₁ + a₂, b₁ + b₂) }

instance Duper.Order.instSubWeight : Sub Weight

Equations

• Duper.Order.instSubWeight = { sub := fun (x x_1 : Duper.Order.Weight) => match x with | (a₁, b₁) => match x_1 with | (a₂, b₂) => (a₁ - a₂, b₁ - b₂) }

instance Duper.Order.instOfNatWeight {n : Nat} : OfNat Weight n

Equations

• Duper.Order.instOfNatWeight = { ofNat := (0, ↑n) }

instance Duper.Order.instLTWeight : LT Weight

Equations

• Duper.Order.instLTWeight = { lt := fun (x x_1 : Duper.Order.Weight) => match x with | (a₁, b₁) => match x_1 with | (a₂, b₂) => a₁ < a₂ ∨ a₁ = a₂ ∧ b₁ < b₂ }

instance Duper.Order.instDecidableLtWeight (v w : Weight) : Decidable (v < w)

Equations

• Duper.Order.instDecidableLtWeight v w = if h : v.fst < w.fst ∨ v.fst = w.fst ∧ v.snd < w.snd then isTrue h else isFalse ⋯

def Duper.Order.absWeight (w : Weight) : Weight

Equations

• Duper.Order.absWeight w = (↑w.fst.natAbs, ↑w.snd.natAbs)

def Duper.Order.VarBalance : Type

Equations

• Duper.Order.VarBalance = Std.HashMap (Lean.Expr × Bool) Duper.Order.Weight

def Duper.Order.VarBalance.addPosVar (vb : VarBalance) (t : Lean.Expr × Bool) : VarBalance

Equations

• vb.addPosVar t = Std.HashMap.insert vb t (Std.HashMap.getD vb t 0 + 1)

def Duper.Order.VarBalance.addNegVar (vb : VarBalance) (t : Lean.Expr × Bool) : VarBalance

Equations

• vb.addNegVar t = Std.HashMap.insert vb t (Std.HashMap.getD vb t 0 - 1)

opaque Duper.Order.LAM : Prop

opaque Duper.Order.FORALL : Prop

opaque Duper.Order.EXISTS : Prop

def Duper.Order.getHead (t : Lean.Expr) : Lean.Expr

Equations

• Duper.Order.getHead (Lean.Expr.lam binderName binderType body binderInfo) = Lean.mkConst `Duper.Order.LAM
• Duper.Order.getHead (Lean.Expr.forallE binderName binderType body binderInfo) = Lean.mkConst `Duper.Order.FORALL
• Duper.Order.getHead (((Lean.Expr.const `Exists us).app arg).app arg_1) = Lean.mkConst `Duper.Order.EXISTS
• Duper.Order.getHead (Lean.Expr.mdata data t_2) = Duper.Order.getHead t_2
• Duper.Order.getHead t = t.getAppFn'

def Duper.Order.getArgs (t : Lean.Expr) : List Lean.Expr

Equations

• Duper.Order.getArgs (Lean.Expr.lam binderName binderType body binderInfo) = [binderType, body]
• Duper.Order.getArgs (Lean.Expr.forallE binderName binderType body binderInfo) = [binderType, body]
• Duper.Order.getArgs (((Lean.Expr.const `Exists us).app arg).app (Lean.Expr.lam binderName binderType b_1 binderInfo)) = [arg, b_1]
• Duper.Order.getArgs (((Lean.Expr.const `Exists us).app arg).app arg_1) = [arg, (arg_1.liftLooseBVars 0 1).app (Lean.Expr.bvar 0)]
• Duper.Order.getArgs (Lean.Expr.mdata data t_2) = Duper.Order.getArgs t_2
• Duper.Order.getArgs t = t.getAppArgs.toList

def Duper.Order.headWeight (f : Lean.Expr) (symbolPrecMap : SymbolPrecMap) (highesetPrecSymbolHasArityZero belowLam : Bool) : Weight

Computes headWeight according to firstmaximal0 weight generation scheme. The head is given weight 1 unless if the head is the unique symbol with the highest precedence in symbolPrecMap, in which case, it is given weight 0.

Note: In order to make the firstmaximal0 weight generation scheme compliant with KBO, if the highest precedence symbol has arity 0 (i.e. is a first-order 'constant'), then I cannot assign the highest precedence symbol weight 0 (because this would violate KBO's constraint that all first-order 'constants' share some positive weight μ). In this case, I simply assign the highest precedence symbol weight 1, as with everything else.

Equations

• One or more equations did not get rendered due to their size.
• Duper.Order.headWeight (Lean.Expr.mvar mvarId) symbolPrecMap highesetPrecSymbolHasArityZero belowLam = 1
• Duper.Order.headWeight (Lean.Expr.bvar deBruijnIndex) symbolPrecMap highesetPrecSymbolHasArityZero belowLam = 1
• Duper.Order.headWeight (Lean.Expr.sort u) symbolPrecMap highesetPrecSymbolHasArityZero belowLam = 1
• Duper.Order.headWeight (Lean.Expr.lit a) symbolPrecMap highesetPrecSymbolHasArityZero belowLam = 1
• Duper.Order.headWeight (Lean.Expr.proj typeName idx struct) symbolPrecMap highesetPrecSymbolHasArityZero belowLam = 1

def Duper.Order.weightVarHeaded : Weight

Equations

• Duper.Order.weightVarHeaded = 1

def Duper.Order.VarBalance.noNegatives (vb : VarBalance) : Bool

Equations

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

def Duper.Order.VarBalance.noPositives (vb : VarBalance) : Bool

Equations

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

def Duper.Order.nameCompare (n1 n2 : Lean.Name) : Comparison

A last resort comparison function to use if symbolPrecCompare needs to compare two symbols, neither of which appeared in symbolPrecMap. We use the convention: Anonymous < Num < Str

Equations

• One or more equations did not get rendered due to their size.
• Duper.Order.nameCompare Lean.Name.anonymous Lean.Name.anonymous = Duper.Comparison.Equal
• Duper.Order.nameCompare (pre1.str s1) (pre2.str s2) = if s1 < s2 then Duper.Comparison.LessThan else if s1 > s2 then Duper.Comparison.GreaterThan else Duper.Order.nameCompare pre1 pre2
• Duper.Order.nameCompare Lean.Name.anonymous (pre.num i) = Duper.Comparison.LessThan
• Duper.Order.nameCompare Lean.Name.anonymous (pre.str str) = Duper.Comparison.LessThan
• Duper.Order.nameCompare (pre.num i) Lean.Name.anonymous = Duper.Comparison.GreaterThan
• Duper.Order.nameCompare (pre.num i) (pre_1.str str) = Duper.Comparison.LessThan
• Duper.Order.nameCompare (pre.str str) Lean.Name.anonymous = Duper.Comparison.GreaterThan
• Duper.Order.nameCompare (pre.str str) (pre_1.num i) = Duper.Comparison.GreaterThan

def Duper.Order.symbolPrecCompare (e1 e2 : Lean.Expr) (s1 s2 : Symbol) (symbolPrecMap : SymbolPrecMap) : Lean.MetaM Comparison

A comparison function for comparing fvars and consts based on precomputed precedences. Note that lower numbers in symbolPrecMap correspond to higher precedences. e1 is the expression that produces symbol s1 and e2 is the expression that produces symbol s2 (e1 and e2 need to be included in addition to s1 and s2 in case if we need to determine the arity of e1 or e2)

Equations

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

def Duper.Order.precCompare (f g : Lean.Expr) (symbolPrecMap : SymbolPrecMap) : Lean.MetaM Comparison

def Duper.Order.isFluid (t : Lean.Expr) : Bool

Overapproximation of being fluid

Equations

• Duper.Order.isFluid t = (t.consumeMData.isApp && t.consumeMData.getAppFn'.isMVar' || t.consumeMData.isLambda && t.consumeMData.hasMVar)

def Duper.Order.kbo (t1 t2 : Lean.Expr) (alreadyReduced : Bool) (symbolPrecMap : SymbolPrecMap) (highesetPrecSymbolHasArityZero : Bool) : Lean.MetaM Comparison

Higher-Order KBO, inspired by https://github.com/sneeuwballen/zipperposition/blob/master/src/core/Ordering.ml.

Follows Section 3.9 of https://matryoshka-project.github.io/pubs/hosup_article.pdf and the article "Things to Know when Implementing KBO" by Bernd Löchner.

Equations

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

partial def Duper.Order.balance_weight (wb : Weight) (vb : VarBalance) (t : Lean.Expr) (s : Option Lean.Expr) (pos belowLam : Bool) (symbolPrecMap : SymbolPrecMap) (highesetPrecSymbolHasArityZero : Bool) : Lean.MetaM (Weight × VarBalance × Bool)

Update variable balance, weight balance, and check whether the term contains the fluid term s. The argument pos determines whether weights and variables will be counted positively or negatively, i.e., whether t is the left term in the comparison. Returns the weight balance and whether s was found.

def Duper.Order.balance_weight_var (wb : Weight) (vb : VarBalance) (t : Lean.Expr) (s : Option Lean.Expr) (pos belowLam : Bool) (symbolPrecMap : SymbolPrecMap) (highesetPrecSymbolHasArityZero : Bool) : Lean.MetaM (Weight × VarBalance × Bool)

balance_weight for the case where t is an applied variable

Equations

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

partial def Duper.Order.balance_weight_rec (wb : Weight) (vb : VarBalance) (terms : List Lean.Expr) (s : Option Lean.Expr) (pos belowLam res : Bool) (symbolPrecMap : SymbolPrecMap) (highesetPrecSymbolHasArityZero : Bool) : Lean.MetaM (Weight × VarBalance × Bool)

list version of the previous one, threaded with the check result

partial def Duper.Order.tckbolex (wb : Weight) (vb : VarBalance) (terms1 terms2 : List Lean.Expr) (belowLam : Bool) (symbolPrecMap : SymbolPrecMap) (highesetPrecSymbolHasArityZero : Bool) : Lean.MetaM (Weight × VarBalance × Comparison)

lexicographic comparison

partial def Duper.Order.tckbolenlex (wb : Weight) (vb : VarBalance) (terms1 terms2 : List Lean.Expr) (belowLam : Bool) (symbolPrecMap : SymbolPrecMap) (highesetPrecSymbolHasArityZero : Bool) : Lean.MetaM (Weight × VarBalance × Comparison)

length-lexicographic comparison

partial def Duper.Order.tckbo (wb : Weight) (vb : VarBalance) (t1 t2 : Lean.Expr) (belowLam : Bool) (symbolPrecMap : SymbolPrecMap) (highesetPrecSymbolHasArityZero : Bool) : Lean.MetaM (Weight × VarBalance × Comparison)

tupled version of kbo (kbo_5 of the paper)

partial def Duper.Order.tckbo_composite (wb : Weight) (vb : VarBalance) (f g : Lean.Expr) (ss ts : List Lean.Expr) (belowLam : Bool) (symbolPrecMap : SymbolPrecMap) (highesetPrecSymbolHasArityZero : Bool) : Lean.MetaM (Weight × VarBalance × Comparison)

tckbo, for non-variable-headed terms).

partial def Duper.Order.tckbo_rec (wb : Weight) (vb : VarBalance) (f g : Lean.Expr) (ss ts : List Lean.Expr) (belowLam : Bool) (symbolPrecMap : SymbolPrecMap) (highesetPrecSymbolHasArityZero : Bool) : Lean.MetaM (Weight × VarBalance × Comparison)

recursive comparison

def Duper.Order.getNetWeight (t1 t2 : Lean.Expr) (alreadyReduced : Bool) (symbolPrecMap : SymbolPrecMap) (highesetPrecSymbolHasArityZero : Bool) : Lean.MetaM Weight

getLitNetWeight takes two expressions t1 and t2 and calculates weight(t1) - weight(t2), returning the difference of the two expressions' weights.

Equations

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