This module contains the implementation of the pre processing pass for handling enum inductive types.

The implementation:

1. generates mappings from enum inductives occurring in the goal to sufficiently large BitVec and replaces equality on the enum inductives with equality on these mapping functions.
2. Constant folds these mappings if appropriate.
3. Adds bounds on the values returned by the mappings if the size of the enum inductive does not fit into a power of two.
4. Handles applications of these mappings to ite, cond and basic match statements.

def Lean.Elab.Tactic.BVDecide.Frontend.Normalize.enumToBitVecSuffix : String

Equations

• Lean.Elab.Tactic.BVDecide.Frontend.Normalize.enumToBitVecSuffix = "enumToBitVec"

def Lean.Elab.Tactic.BVDecide.Frontend.Normalize.eqIffEnumToBitVecEqSuffix : String

Equations

• Lean.Elab.Tactic.BVDecide.Frontend.Normalize.eqIffEnumToBitVecEqSuffix = "eq_iff_enumToBitVec_eq"

def Lean.Elab.Tactic.BVDecide.Frontend.Normalize.enumToBitVecLeSuffix : String

Equations

• Lean.Elab.Tactic.BVDecide.Frontend.Normalize.enumToBitVecLeSuffix = "enumToBitVec_le"

def Lean.Elab.Tactic.BVDecide.Frontend.Normalize.matchEqCondSuffix : String

Equations

• Lean.Elab.Tactic.BVDecide.Frontend.Normalize.matchEqCondSuffix = "eq_cond_enumToBitVec"

def Lean.Elab.Tactic.BVDecide.Frontend.Normalize.getEnumToBitVecFor (declName : Name) : MetaM Name

Assuming that declName is an enum inductive construct a function of type declName → BitVec w that maps declName constructors to their numeric indices as BitVec.

Equations

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

def Lean.Elab.Tactic.BVDecide.Frontend.Normalize.getEqIffEnumToBitVecEqFor (declName : Name) : MetaM Name

Assuming that declName is an enum inductive, construct a proof of ∀ (x y : declName) : x = y ↔ x.enumToBitVec = y.enumToBitVec.

Equations

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

def Lean.Elab.Tactic.BVDecide.Frontend.Normalize.getEnumToBitVecLeFor (declName : Name) : MetaM Name

Assuming that declName is an enum inductive, construct a proof of ∀ (x : declName) : x.enumToBitVec ≤ domainSize - 1 where domainSize is the amount of constructors of declName.

Equations

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

def Lean.Elab.Tactic.BVDecide.Frontend.Normalize.getMatchEqCondFor (declName : Name) : MetaM Name

Obtain a theorem that translates .match_x applications on enum inductives to chains of cond applications. If the specific .match_x that this is being called on is unsupported throw an error.

Equations

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

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

This simproc should be set up to trigger on expressions of the form EnumInductive.enumToBitVec x. It will check if x is a constructor and if that is the case constant fold it to the corresponding BitVec value.

Equations

• One or more equations did not get rendered due to their size.
• Lean.Elab.Tactic.BVDecide.Frontend.Normalize.enumToBitVecCtor ((Lean.Expr.const fn us).app (Lean.Expr.const arg us_1)) = pure Lean.Meta.Simp.Step.continue
• Lean.Elab.Tactic.BVDecide.Frontend.Normalize.enumToBitVecCtor e = pure Lean.Meta.Simp.Step.continue

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

Equations

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