Expr helpers

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

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

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

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

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

Types

@[reducible, inline]

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

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

Bitvector operations that we perform AC canonicalization on.

• mul (w : Expr) : Op

@[implicit_reducible]

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

def Lean.Elab.Tactic.BVDecide.Frontend.Normalize.instBEqOp.beq : Op → Op → Bool

@[implicit_reducible]

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

def Lean.Elab.Tactic.BVDecide.Frontend.Normalize.instReprOp.repr : Op → Nat → Format

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.

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.

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

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

The identity / neutral element of given operation

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.

@[implicit_reducible]

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

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.

VarState monadic boilerplate

@[reducible, inline]

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

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

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.

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

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

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).

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' } ← SharedCoefficients.compute x y, then x[idx] = common[idx] + x'[idx] and y[idx] = common[idx] + y'[idx] for all valid variable indices idx.

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.

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.

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.

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

Tactic Boilerplate

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

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

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