Documentation

Lean.Elab.Tactic.BVDecide.Frontend.Normalize.Enums

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.

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
    Instances For

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

      Equations
        Instances For

          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
            Instances For

              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
                Instances For

                  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
                    Instances For