Lean.Elab.Tactic.BVDecide.Frontend.Normalize.AC

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

Instances For

source

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

ToMessageData Op

Equations

source

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.

Instances For

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

source

@[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

Instances For

VarState monadic boilerplate #

source

@[reducible, inline]

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

Type

Equations

Instances For

source

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

MetaM α

Equations

Instances For

Implementation #

source

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

Instances For

source

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

Instances For

source

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

Instances For

source

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

VarStateM CoefficientsMap

Equations

Instances For

source

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

Expr → VarStateM CoefficientsMap

Equations

Instances For

source

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

Type

Instances For

source

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

Instances For

source

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

Instances For

source

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

Instances For

source

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

Instances For

source

def Lean.Elab.Tactic.BVDecide.Frontend.Normalize.bvAcNfpost :

Meta.Simp.Simproc

Equations

Instances For