Expr helpers

def Lean.Elab.Tactic.BVDecide.Frontend.Normalize.BitVec.mkType (w : Expr) : Expr

Equations

• Lean.Elab.Tactic.BVDecide.Frontend.Normalize.BitVec.mkType w = Lean.mkApp (Lean.Expr.const `BitVec []) w

def Lean.Elab.Tactic.BVDecide.Frontend.Normalize.BitVec.mkInstMul (w : Expr) : Expr

Equations

• Lean.Elab.Tactic.BVDecide.Frontend.Normalize.BitVec.mkInstMul w = Lean.mkApp (Lean.Expr.const `BitVec.instMul []) w

def Lean.Elab.Tactic.BVDecide.Frontend.Normalize.BitVec.mkInstHMul (w : Expr) : Expr

Equations

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

def Lean.Elab.Tactic.BVDecide.Frontend.Normalize.mkBitVecLit (w : Expr) (n : Nat) : Expr

Construct a literal of type BitVec w, with value n.

Equations

• Lean.Elab.Tactic.BVDecide.Frontend.Normalize.mkBitVecLit w n = Lean.mkApp2 (Lean.mkConst `BitVec.ofNat) w (Lean.mkNatLit n)

Types

@[reducible, inline]

abbrev Lean.Elab.Tactic.BVDecide.Frontend.Normalize.VarIndex : Type

Equations

• Lean.Elab.Tactic.BVDecide.Frontend.Normalize.VarIndex = Nat

inductive Lean.Elab.Tactic.BVDecide.Frontend.Normalize.Op : Type

Bitvector operations that we perform AC canonicalization on.

• mul (w : Expr) : Op

instance Lean.Elab.Tactic.BVDecide.Frontend.Normalize.instBEqOp : BEq Op

Equations

• Lean.Elab.Tactic.BVDecide.Frontend.Normalize.instBEqOp = { beq := Lean.Elab.Tactic.BVDecide.Frontend.Normalize.beqOp✝ }

instance Lean.Elab.Tactic.BVDecide.Frontend.Normalize.instReprOp : Repr Op

Equations

• Lean.Elab.Tactic.BVDecide.Frontend.Normalize.instReprOp = { reprPrec := Lean.Elab.Tactic.BVDecide.Frontend.Normalize.reprOp✝ }

def Lean.Elab.Tactic.BVDecide.Frontend.Normalize.Op.ofExpr? (e : Expr) : Option Op

Given an expression of an (unapplied) operation, return the decoded Op. Return none if the expression is not a recognized operation.

Equations

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

def Lean.Elab.Tactic.BVDecide.Frontend.Normalize.Op.ofApp2? : Expr → Option Op

Given an application of a recognized binary operation (to two arguments), return the decoded Op.

Return none if the expression is not an application of a recognized operation.

Equations

• Lean.Elab.Tactic.BVDecide.Frontend.Normalize.Op.ofApp2? ((op.app _x).app _y) = Lean.Elab.Tactic.BVDecide.Frontend.Normalize.Op.ofExpr? op
• Lean.Elab.Tactic.BVDecide.Frontend.Normalize.Op.ofApp2? x✝ = none

def Lean.Elab.Tactic.BVDecide.Frontend.Normalize.Op.toExpr : Op → Expr

Equations

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

def Lean.Elab.Tactic.BVDecide.Frontend.Normalize.Op.neutralElement : Op → Expr

The identity / neutral element of given operation

Equations

• (Lean.Elab.Tactic.BVDecide.Frontend.Normalize.Op.mul a).neutralElement = Lean.Elab.Tactic.BVDecide.Frontend.Normalize.mkBitVecLit a 1

def Lean.Elab.Tactic.BVDecide.Frontend.Normalize.Op.isSameKind (op : Op) (op' : Expr) : Bool

Parse op' using ofExpr? and return true if the resulting operation is of the same kind as op (i.e., both are multiplications). Returns false if op' fails to parse.

Note that the width of the operation is not compared.

Equations

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

instance Lean.Elab.Tactic.BVDecide.Frontend.Normalize.Op.instToMessageData : ToMessageData Op

Equations

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

structure Lean.Elab.Tactic.BVDecide.Frontend.Normalize.VarState : Type

• op : Op

  The associative and commutative operator we are currently canonicalizing with respect to.

• exprToVarIndex : Std.HashMap Expr VarIndex

  Map from atomic expressions to an index.

• varToExpr : Array Expr

  Inverse of exprToVarIndex, which maps a VarIndex to the expression it represents.

We don't verify the state manipulations, but if we would, these are the invariants:

structure LegalVarState extends VarState where
  /-- `varToExpr` and `exprToVarIndex` have the same number of elements. -/
  h_size  : varToExpr.size = exprToVarIndex.size
  /-- `exprToVarIndex` is the inverse of `varToExpr`. -/
  h_elems : ∀ h_lt : i < varToExpr.size, exprToVarIndex[varToExpr[i]]? = some i

@[reducible, inline]

abbrev Lean.Elab.Tactic.BVDecide.Frontend.Normalize.CoefficientsMap : Type

A representation of an expression as a map from variable index to the number of occurrences of the expression represented by that variable.

See CoefficientsMap.toExpr for the explicit conversion.

Equations

• Lean.Elab.Tactic.BVDecide.Frontend.Normalize.CoefficientsMap = Std.HashMap Lean.Elab.Tactic.BVDecide.Frontend.Normalize.VarIndex Nat

VarState monadic boilerplate

@[reducible, inline]

abbrev Lean.Elab.Tactic.BVDecide.Frontend.Normalize.VarStateM (α : Type) : Type

Equations

• Lean.Elab.Tactic.BVDecide.Frontend.Normalize.VarStateM = StateT Lean.Elab.Tactic.BVDecide.Frontend.Normalize.VarState Lean.MetaM

def Lean.Elab.Tactic.BVDecide.Frontend.Normalize.VarStateM.run' {α : Type} (x : VarStateM α) (s : VarState) : MetaM α

Equations

• x.run' s = StateT.run' x s

Implementation

def Lean.Elab.Tactic.BVDecide.Frontend.Normalize.VarStateM.exprToVar (e : Expr) : VarStateM VarIndex

Return the unique variable index for an expression, or none if the expression is a neutral element (see isNeutral).

Modifies the monadic state to add a new mapping, if needed.

Equations

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

def Lean.Elab.Tactic.BVDecide.Frontend.Normalize.VarStateM.varToExpr (idx : VarIndex) : VarStateM Expr

Return the expression that is represented by a specific variable index.

Equations

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

def Lean.Elab.Tactic.BVDecide.Frontend.Normalize.VarStateM.computeCoefficients (op : Op) (e : Expr) : VarStateM CoefficientsMap

Given a binary, associative and commutative operation op, decompose expression e into its variable coefficients.

For example a ⊕ b ⊕ (a ⊕ c) will give the coefficients:

a => 2
b => 1
c => 1

Any compound expression which is not an application of the given op will be abstracted away and treated as a variable (see VarStateM.exprToVar).

Equations

• Lean.Elab.Tactic.BVDecide.Frontend.Normalize.VarStateM.computeCoefficients op e = Lean.Elab.Tactic.BVDecide.Frontend.Normalize.VarStateM.computeCoefficients.go op ∅ e

def Lean.Elab.Tactic.BVDecide.Frontend.Normalize.VarStateM.computeCoefficients.incrVar (coeff : CoefficientsMap) (e : Expr) : VarStateM CoefficientsMap

Equations

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

def Lean.Elab.Tactic.BVDecide.Frontend.Normalize.VarStateM.computeCoefficients.go (op : Op) (coeff : CoefficientsMap) : Expr → VarStateM CoefficientsMap

Equations

• One or more equations did not get rendered due to their size.
• Lean.Elab.Tactic.BVDecide.Frontend.Normalize.VarStateM.computeCoefficients.go op coeff x✝ = Lean.Elab.Tactic.BVDecide.Frontend.Normalize.VarStateM.computeCoefficients.incrVar coeff x✝

structure Lean.Elab.Tactic.BVDecide.Frontend.Normalize.SharedCoefficients : Type

• common : CoefficientsMap
• x : CoefficientsMap
• y : CoefficientsMap

def Lean.Elab.Tactic.BVDecide.Frontend.Normalize.SharedCoefficients.compute (x y : CoefficientsMap) : VarStateM SharedCoefficients

Given two sets of coefficients x and y (computed with the same variable mapping), extract the shared coefficients, such that x (resp. y) is the sum of coefficients in common and x (resp y) of the result.

That is, if { common, x', y' } ← SharedCoeffients.compute x y, then x[idx] = common[idx] + x'[idx] and y[idx] = common[idx] + y'[idx] for all valid variable indices idx.

Equations

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

def Lean.Elab.Tactic.BVDecide.Frontend.Normalize.CoefficientsMap.toExpr (coeff : CoefficientsMap) (op : Op) : VarStateM (Option Expr)

Compute the canonical expression for a given set of coefficients. Returns none if all coefficients are zero.

Equations

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

def Lean.Elab.Tactic.BVDecide.Frontend.Normalize.proveEqualityByAC (x y : Expr) : MetaM Expr

Given two expressions x, y which are equal up to associativity and commutativity, construct and return a proof of x = y.

Uses ac_rfl internally to construct said proof.

Equations

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

def Lean.Elab.Tactic.BVDecide.Frontend.Normalize.canonicalizeWithSharing (P lhs rhs : Expr) : Meta.SimpM Meta.Simp.Step

Given an expression P lhs rhs, where lhs, rhs : ty and P : $ty → $ty → _, canonicalize top-level applications of a recognized associative and commutative operation on both the lhs and the rhs such that the final expression is: P ($common ⊕ $lhs') ($common ⊕ $rhs') That is, in a way that exposes terms that are shared between the lhs and rhs.

For example, x₁ * (y₁ * z) == x₂ * (y₂ * z) is normalized to z * (x₁ * y₁) == z * (x₂ * y₂), pulling the shared variable z to the front on both sides.

See Op.fromExpr? to see which operations are recognized. Other operations are ignored, even if they are associative and commutative.

Equations

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

def Lean.Elab.Tactic.BVDecide.Frontend.Normalize.bvAcNfpost : Meta.Simp.Simproc

Equations

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

Tactic Boilerplate

def Lean.Elab.Tactic.BVDecide.Frontend.Normalize.bvAcNfTarget (mvarId : MVarId) (maxSteps : Nat := Meta.Simp.defaultMaxSteps) : MetaM MVarId

Equations

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

def Lean.Elab.Tactic.BVDecide.Frontend.Normalize.bvAcNfHypMeta (goal : MVarId) (fvarId : FVarId) (maxSteps : Nat := Meta.Simp.defaultMaxSteps) : MetaM (Option MVarId)

Equations

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

def Lean.Elab.Tactic.BVDecide.Frontend.Normalize.bvAcNormalizePass : Pass

Equations

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