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

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

source

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

ToMessageData Op

Equations

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

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.

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 occurences 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 #

source

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

source

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

MetaM α

Equations

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

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

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

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

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

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

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

source

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.

source

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✝

source

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

Type

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

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

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

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

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 contruct said proof.

Equations

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

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