Documentation

Lean.Meta.Tactic.Grind.NormSym

Sym.simp-based grind normalizer #

The grind normalizer runs on Meta.simp (see simpCore). This module is the Sym.simp replacement, developed side by side with the legacy one: normLegacy and normSym apply the respective simplification step to a term, and the grind_norm tactic exposes both so that discrepancies can be collected as tests and fixed one by one.

grind_norm and the normLegacy/normSym pair are debugging aids for this migration only. They will be deleted once grind runs on Sym.simp.

The Sym.simp theorem set is derived from the legacy normExt set on demand, so both normalizers always see the same [grind norm] and [grind unfold] declarations.

source
structure Lean.Meta.Grind.NormSymTheorems :
Type

The grind normalization theorems as Sym.simp theorem sets.

  • pre : Sym.Simp.Theorems

    Theorems applied before visiting subterms ([grind norm ↓]).

  • post : Sym.Simp.Theorems

    Theorems applied after visiting subterms ([grind norm]), and the equational theorems of the declarations to unfold ([grind unfold]).

  • dsimp : Sym.DSimp.Decls

    The rfl-theorems of post and the declarations to unfold, for Sym.dsimp. grind needs dsimp in one place: the right-hand side of a generalized pattern (mkGeneralizedPatternEqProof) must stay definitionally equal to the term it replaces, e.g. Nat.succ x becomes x + 1.

Instances For
    source
    def Lean.Meta.Grind.mkNormSymTheorems :
    MetaM NormSymTheorems

    Builds the Sym.simp theorem sets from the legacy grind normalization theorem set.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def Lean.Meta.Grind.mkNormSymMethods (config : Grind.Config) (thms : NormSymTheorems) :
      Sym.Simp.Methods

      Sym.simp methods approximating the legacy grind normalizer.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        def Lean.Meta.Grind.mkNormSymDSimpMethods (config : Grind.Config) (thms : NormSymTheorems) :
        Sym.DSimp.Methods

        Sym.dsimp methods approximating the legacy grind dsimp step (dsimpCore).

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          def Lean.Meta.Grind.normLegacy (e : Expr) :
          GrindM Simp.Result

          Applies the legacy simp-based normalization step to e, and the metadata erasure that preprocess performs after it. The Sym.simp chain erases metadata as part of the step.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            def Lean.Meta.Grind.normSym (e : Expr) :
            GrindM Simp.Result

            Applies the Sym.simp-based normalization step (symNorm) to e.

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