The llarith tactic

llarith proves lattice-linear identities and non-strict inequalities in vector lattices by reducing them to the corresponding statement over ℝ. It quotes the goal as an LLexpr, proves the real identity by expanding lattice operations to max and min and splitting cases, and transfers the result back with LLexpr.vanishes_of_vanishes_real.

The supported expression language consists of vector-valued atoms, 0, addition, subtraction, negation, real scalar multiplication, ⊔, ⊓, positive parts, negative parts, and absolute values. A goal a ≤ b is handled as the equivalent lattice-linear identity a ⊔ b = b. Local hypotheses of the form 0 ≤ x, x ≤ 0, 0 < x, and x < 0 are used when x is one of the quoted atoms.

inductive LLexpr.Tactic.Quoted : Type

A quoted lattice-linear expression whose coefficients are elaborated Lean expressions.

Unsupported vector-valued subterms are represented by var; they are treated as atomic variables in the real identity check.

• zero : Quoted

  The constant zero expression.

• var (idx : ℕ) : Quoted

  A vector-valued atom, represented by its index in the collected atom list.

• add (lhs rhs : Quoted) : Quoted

  Addition of quoted expressions.

• smul (coeff : Lean.Expr) (arg : Quoted) : Quoted

  Real scalar multiplication of a quoted expression.

• sup (lhs rhs : Quoted) : Quoted

  Supremum of quoted expressions.

• inf (lhs rhs : Quoted) : Quoted

  Infimum of quoted expressions.

def LLexpr.Tactic.instBEqQuoted.beq : Quoted → Quoted → Bool

Equations

• LLexpr.Tactic.instBEqQuoted.beq LLexpr.Tactic.Quoted.zero LLexpr.Tactic.Quoted.zero = true
• LLexpr.Tactic.instBEqQuoted.beq (LLexpr.Tactic.Quoted.var a) (LLexpr.Tactic.Quoted.var b) = (a == b)
• LLexpr.Tactic.instBEqQuoted.beq (a.add a_1) (b.add b_1) = (LLexpr.Tactic.instBEqQuoted.beq a b && LLexpr.Tactic.instBEqQuoted.beq a_1 b_1)
• LLexpr.Tactic.instBEqQuoted.beq (LLexpr.Tactic.Quoted.smul a a_1) (LLexpr.Tactic.Quoted.smul b b_1) = (a == b && LLexpr.Tactic.instBEqQuoted.beq a_1 b_1)
• LLexpr.Tactic.instBEqQuoted.beq (a.sup a_1) (b.sup b_1) = (LLexpr.Tactic.instBEqQuoted.beq a b && LLexpr.Tactic.instBEqQuoted.beq a_1 b_1)
• LLexpr.Tactic.instBEqQuoted.beq (a.inf a_1) (b.inf b_1) = (LLexpr.Tactic.instBEqQuoted.beq a b && LLexpr.Tactic.instBEqQuoted.beq a_1 b_1)
• LLexpr.Tactic.instBEqQuoted.beq x✝¹ x✝ = false

@[instance_reducible]

instance LLexpr.Tactic.instBEqQuoted : BEq Quoted

Equations

• LLexpr.Tactic.instBEqQuoted = { beq := LLexpr.Tactic.instBEqQuoted.beq }

inductive LLexpr.Tactic.AtomSign : Type

The sign information about a quoted atom that llarith can use.

• unknown : AtomSign

  No usable sign information was found.

• nonneg : AtomSign

  The atom is known to be non-negative.

• nonpos : AtomSign

  The atom is known to be non-positive.

@[instance_reducible]

instance LLexpr.Tactic.instBEqAtomSign : BEq AtomSign

Equations

• LLexpr.Tactic.instBEqAtomSign = { beq := LLexpr.Tactic.instBEqAtomSign.beq }

def LLexpr.Tactic.instBEqAtomSign.beq : AtomSign → AtomSign → Bool

Equations

• LLexpr.Tactic.instBEqAtomSign.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

@[instance_reducible]

instance LLexpr.Tactic.instInhabitedAtomSign : Inhabited AtomSign

Equations

• LLexpr.Tactic.instInhabitedAtomSign = { default := LLexpr.Tactic.instInhabitedAtomSign.default }

structure LLexpr.Tactic.AtomSignInfo : Type

Sign information for an atom, together with a proof of the corresponding weak inequality.

• sign : AtomSign

  Whether the atom is known to be non-negative or non-positive.

• proof : Lean.Expr

  A proof of 0 ≤ x in the non-negative case, or x ≤ 0 in the non-positive case.

structure LLexpr.Tactic.QuoteState : Type

State threaded through quotation: the distinct vector-valued atoms already found.

• atoms : Array Lean.Expr

  The vector-valued atoms, in the order used for the generated Fin n → X tuple.

@[reducible, inline]

abbrev LLexpr.Tactic.QuoteM (α : Type) : Type

The monad used while quoting a goal into an LLexpr.

Equations

• LLexpr.Tactic.QuoteM = StateT LLexpr.Tactic.QuoteState Lean.Elab.Tactic.TacticM

def LLexpr.Tactic.throwUnsupportedTarget {α : Type} : Lean.Elab.Tactic.TacticM α

Report that the current target is outside the goal shapes supported by llarith.

Equations

• LLexpr.Tactic.throwUnsupportedTarget = Lean.throwError (Lean.toMessageData "llarith only supports equality and non-strict inequality goals")

def LLexpr.Tactic.sameAtom (x y : Lean.Expr) : Bool

Syntactic comparison of vector-valued atoms, ignoring metadata.

Equations

• LLexpr.Tactic.sameAtom x y = (x.consumeMData == y.consumeMData)

def LLexpr.Tactic.registerAtom (e : Lean.Expr) : QuoteM ℕ

Return the index of an atom, adding it to the quotation state if it is new.

Equations

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

def LLexpr.Tactic.findAtom (atoms : Array Lean.Expr) (e : Lean.Expr) : Option ℕ

Return the index of an already collected atom, if any.

Equations

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

def LLexpr.Tactic.isZeroOfType (type e : Lean.Expr) : Lean.Elab.Tactic.TacticM Bool

Test whether an expression is definitionally the zero element of the given type.

Equations

• LLexpr.Tactic.isZeroOfType type e = do let z ← liftM (Lean.Meta.mkAppOptM `OfNat.ofNat #[some type, some (Lean.mkNatLit 0), none]) Lean.Meta.withReducible (liftM (Lean.Meta.isDefEq e z))

def LLexpr.Tactic.isRealType (type : Lean.Expr) : Lean.Elab.Tactic.TacticM Bool

Test whether an elaborated type expression is definitionally ℝ.

Equations

• LLexpr.Tactic.isRealType type = Lean.Meta.withReducible (liftM (Lean.Meta.isDefEq type q(ℝ)))

def LLexpr.Tactic.quoteExprWithFuel : ℕ → (type e : Lean.Expr) → QuoteM Quoted

Quote a vector-valued expression as a lattice-linear expression.

Recognized syntax is translated to the corresponding Quoted constructor. Any other vector-valued subterm is registered as an atomic variable.

Equations

• One or more equations did not get rendered due to their size.
• LLexpr.Tactic.quoteExprWithFuel 0 x✝¹ x✝ = Lean.throwError (Lean.toMessageData "llarith expression traversal exhausted its structural bound")

def LLexpr.Tactic.quoteExpr (type e : Lean.Expr) : QuoteM Quoted

The expression size bounds the number of recursive quotation steps along any branch.

Equations

• LLexpr.Tactic.quoteExpr type e = LLexpr.Tactic.quoteExprWithFuel (e.sizeWithoutSharing + 1) type e

def LLexpr.Tactic.Quoted.applySigns (signs : Array AtomSign) : Quoted → Quoted

Replace atoms with sign-parametrized expressions when a sign hypothesis is available.

For a non-negative atom x, the real side uses x⁺; for a non-positive atom, it uses -(-x)⁺. After transfer, the original sign hypothesis rewrites these expressions back to x.

Equations

• One or more equations did not get rendered due to their size.
• LLexpr.Tactic.Quoted.applySigns signs LLexpr.Tactic.Quoted.zero = LLexpr.Tactic.Quoted.zero
• LLexpr.Tactic.Quoted.applySigns signs (lhs.add rhs) = (LLexpr.Tactic.Quoted.applySigns signs lhs).add (LLexpr.Tactic.Quoted.applySigns signs rhs)
• LLexpr.Tactic.Quoted.applySigns signs (LLexpr.Tactic.Quoted.smul coeff arg) = LLexpr.Tactic.Quoted.smul coeff (LLexpr.Tactic.Quoted.applySigns signs arg)
• LLexpr.Tactic.Quoted.applySigns signs (lhs.sup rhs) = (LLexpr.Tactic.Quoted.applySigns signs lhs).sup (LLexpr.Tactic.Quoted.applySigns signs rhs)
• LLexpr.Tactic.Quoted.applySigns signs (lhs.inf rhs) = (LLexpr.Tactic.Quoted.applySigns signs lhs).inf (LLexpr.Tactic.Quoted.applySigns signs rhs)

def LLexpr.Tactic.isNegOneCoeff (coeff : Lean.Expr) : Lean.Elab.Tactic.TacticM Bool

Test whether an elaborated scalar coefficient is definitionally -1.

Equations

• LLexpr.Tactic.isNegOneCoeff coeff = Lean.Meta.withReducible (liftM (Lean.Meta.isDefEq coeff q(-1)))

def LLexpr.Tactic.Quoted.simplify : Quoted → Lean.Elab.Tactic.TacticM Quoted

Remove simple redundancies introduced while quoting and applying signs.

Equations

• One or more equations did not get rendered due to their size.
• LLexpr.Tactic.Quoted.zero.simplify = pure LLexpr.Tactic.Quoted.zero
• (LLexpr.Tactic.Quoted.var idx).simplify = pure (LLexpr.Tactic.Quoted.var idx)

def LLexpr.Tactic.AtomSignInfo.toSigns (infos : Array (Option AtomSignInfo)) : Array AtomSign

Convert an array of optional sign information to the sign array used by quotation.

Equations

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

def LLexpr.Tactic.signFromHyp (type : Lean.Expr) (atoms : Array Lean.Expr) (proof prop : Lean.Expr) : Lean.Elab.Tactic.TacticM (Option (ℕ × AtomSignInfo))

If a proposition gives sign information about a collected atom, return that information.

Equations

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

def LLexpr.Tactic.collectAtomSigns (type : Lean.Expr) (atoms : Array Lean.Expr) : Lean.Elab.Tactic.TacticM (Array (Option AtomSignInfo))

Collect atom-level sign information from the local context.

Equations

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

def LLexpr.Tactic.assertAtomSignFacts (infos : Array (Option AtomSignInfo)) : Lean.Elab.Tactic.TacticM Unit

Add the weak inequalities extracted from sign hypotheses to the local context.

Equations

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

def LLexpr.Tactic.mkFinExpr (idx arity : ℕ) : Lean.Expr

Build a closed expression for the idxth element of Fin arity.

def LLexpr.Tactic.Quoted.toLLexpr (arity : ℕ) : Quoted → Lean.Elab.Tactic.TacticM Lean.Expr

Convert quoted syntax into the corresponding formal LLexpr.

Equations

• One or more equations did not get rendered due to their size.
• LLexpr.Tactic.Quoted.toLLexpr arity LLexpr.Tactic.Quoted.zero = liftM (Lean.Meta.mkAppOptM `LLexpr.zero #[some (Lean.mkNatLit arity)])
• LLexpr.Tactic.Quoted.toLLexpr arity (LLexpr.Tactic.Quoted.smul coeff arg) = do let __do_lift ← LLexpr.Tactic.Quoted.toLLexpr arity arg liftM (Lean.Meta.mkAppM `LLexpr.smul #[coeff, __do_lift])

def LLexpr.Tactic.mkFinFun (type : Lean.Expr) (atoms : Array Lean.Expr) : Lean.MetaM Lean.Expr

Build the finite tuple of vector-valued atoms used to evaluate the quoted LLexprs.

The tuple is emitted as a PiFin literal so that the final simplification step can unfold each variable lookup.

Equations

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

def LLexpr.Tactic.proveRealVanishes (hreal : Lean.MVarId) : Lean.Elab.Tactic.TacticM Unit

Prove the generated real vanishing statement.

After introducing the real variables, this unfolds LLexpr.eval and first tries grind on the real lattice expression. If that does not close the goal, it falls back to expanding max and min, splitting cases, and closing the resulting arithmetic goals with linarith or nlinarith.

Equations

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

def LLexpr.Tactic.closeByTransfer (type : Lean.Expr) (lhsQ rhsQ : Quoted) (atoms : Array Lean.Expr) (asLe hasSigns : Bool) : Lean.Elab.Tactic.TacticM Unit

Transfer a quoted real identity back to the original vector-lattice goal.

If asLe is true, the quoted equality has the form lhs ⊔ rhs = rhs and is post-processed as a proof of lhs ≤ rhs.

Equations

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

def LLexpr.Tactic.evalLlarith : Lean.Elab.Tactic.TacticM Unit

Implementation of the user-facing llarith tactic.

Equations

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

def LLexpr.Tactic.tacticLlarith : Lean.ParserDescr

Prove lattice-linear identities by checking the corresponding identity over ℝ.

The tactic supports equality and non-strict inequality goals built from vector-valued atoms, 0, +, -, unary negation, real scalar multiplication, ⊔, ⊓, positive and negative parts, and absolute values. It also uses atom-level sign hypotheses of the form 0 ≤ x, x ≤ 0, 0 < x, or x < 0.

Equations

• LLexpr.Tactic.tacticLlarith = Lean.ParserDescr.node `LLexpr.Tactic.tacticLlarith 1024 (Lean.ParserDescr.nonReservedSymbol "llarith" false)