Documentation

Lean.Meta.Tactic.Grind.NormSymProcs

Sym.simp simprocs of the grind normalizer #

Ports of the Meta.simp simprocs in SimpUtil.lean and ForallProp.lean whose rewrite rules are not first-order (they bind variables or dispatch on the shape of the term). Results are built with the maximal-sharing builders (mkAppS, ...); proofs are built without inferType. The definitional reductions (beta, zeta, projections, matchers) are the shared ones in Lean.Meta.Sym.Simp.Reduce.

source
def Lean.Meta.Grind.NormSym.eraseMData :
Sym.Simp.Simproc

Erases metadata. grind never internalizes Expr.mdata.

Instances For
    source
    def Lean.Meta.Grind.NormSym.preMatchCond :
    Sym.Simp.Simproc

    Grind.PreMatchCond p is left as is: p is a condition of a match equation and must keep the shape produced by annotateMatchEqnType; replacePreMatchCond turns it into Grind.MatchCond after normalization.

    Instances For
      source
      def Lean.Meta.Grind.NormSym.simpMatchDiscrsOnly :
      Sym.Simp.Simproc

      Grind.simpMatchDiscrsOnly m, where m is a match application: only the discriminants of m are simplified, the alternatives are not visited. The annotation stays and is erased by eraseSimpMatchDiscrsOnly after normalization.

      Instances For
        source
        def Lean.Meta.Grind.NormSym.simpEq :
        Sym.Simp.Simproc

        Normalizes equalities:

        • Bool: true = b becomes b = true; (a && b) = c becomes ((a && b) = true) = (c = true).
        • a = a becomes True, p = True becomes p, p = False becomes ¬p.
        Instances For
          source
          def Lean.Meta.Grind.NormSym.simpDIte :
          Sym.Simp.Simproc

          Converts dite with non-dependent branches into ite.

          Instances For
            source
            def Lean.Meta.Grind.NormSym.pushNot :
            Sym.Simp.Simproc

            Pushes negations inwards through the propositional connectives, ite, and the quantifiers. Negated arithmetic comparisons are handled by the rewrite rules Nat.not_le_eq and Int.not_le_eq.

            Instances For
              source
              def Lean.Meta.Grind.NormSym.simpOr :
              Sym.Simp.Simproc

              Normalizes disjunctions: units, right-associativity, and universally quantified disjuncts moved to the front.

              Instances For
                source
                def Lean.Meta.Grind.NormSym.reduceCtorEq :
                Sym.Simp.Simproc

                Reduces c₁ ... = c₂ ... to False for distinct constructors c₁ and c₂.

                Instances For
                  source
                  def Lean.Meta.Grind.NormSym.simpForall :
                  Sym.Simp.Simproc

                  Normalizes universally quantified propositions and implications: Grind.imp_true_eq, Grind.imp_false_eq, Grind.true_imp_eq, Grind.false_imp_eq, Grind.imp_self_eq, Grind.forall_true, forall_false, Grind.forall_or_forall, Grind.forall_forall_or, Grind.forall_and (see forallImpAnd?).

                  Instances For
                    source
                    def Lean.Meta.Grind.NormSym.simpExists :
                    Sym.Simp.Simproc

                    Normalizes existentially quantified propositions: Grind.exists_or, Grind.exists_and_left, Grind.exists_and_right, Grind.exists_prop, Grind.exists_const.

                    Instances For