Documentation

Mathlib.Tactic.ReduceModChar

reduce_mod_char tactic #

Define the reduce_mod_char tactic, which traverses expressions looking for numerals n, such that the type of n is a ring of (positive) characteristic p, and reduces these numerals modulo p, to lie between 0 and p.

Implementation #

The main entry point is ReduceModChar.derive, which uses simp to traverse expressions and calls matchAndNorm on each subexpression. The type of each subexpression is matched syntactically to determine if it is a ring with positive characteristic in typeToCharP. Using syntactic matching should be faster than trying to infer a CharP instance on each subexpression. The actual reduction happens in normIntNumeral. This is written to be compatible with norm_num so it can serve as a drop-in replacement for some norm_num-based routines (specifically, the intended use is as an option for the ring tactic).

In addition to the main functionality, we call normNeg and normNegCoeffMul to replace negation with multiplication by p - 1, and simp lemmas tagged @[reduce_mod_char] to clean up the resulting expression: e.g. 1 * X + 0 becomes X.

theorem Tactic.ReduceModChar.CharP.intCast_eq_mod (R : Type u_1) [Ring R] (p : ) [CharP R p] (k : ) :
k = (k % p)
theorem Tactic.ReduceModChar.CharP.isInt_of_mod {e' : } {r : } {α : Type u_1} [Ring α] {n : } {n' : } (inst : CharP α n) {e : α} (he : Mathlib.Meta.NormNum.IsInt e e') (hn : Mathlib.Meta.NormNum.IsNat n n') (h₂ : Mathlib.Meta.NormNum.IsInt (e' % n') r) :
def Tactic.ReduceModChar.normIntNumeral {u : Lean.Level} {α : Q(Type u)} (n : Q()) (e : Q(«$α»)) (instRing : Q(Ring «$α»)) (instCharP : Q(CharP «$α» «$n»)) :

Given an integral expression e : t such that t is a ring of characteristic n, reduce e modulo n.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    theorem Tactic.ReduceModChar.CharP.neg_eq_sub_one_mul {α : Type u_1} [Ring α] (n : ) (inst : CharP α n) (b : α) (a : ) (a' : α) (p : Mathlib.Meta.NormNum.IsNat (n - 1) a) (pa : a = a') :
    -b = a' * b
    def Tactic.ReduceModChar.normNeg {u : Lean.Level} {α : Q(Type u)} (n : Q()) (e : Q(«$α»)) (_instRing : Q(Ring «$α»)) (instCharP : Q(CharP «$α» «$n»)) :

    Given an expression (-e) : t such that t is a ring of characteristic n, simplify this to (n - 1) * e.

    This should be called only when normIntNumeral fails, because normIntNumeral would otherwise be more useful by evaluating -e mod n to an actual numeral.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      theorem Tactic.ReduceModChar.CharP.neg_mul_eq_sub_one_mul {α : Type u_1} [Ring α] (n : ) (inst : CharP α n) (a : α) (b : α) (na : ) (na' : α) (p : Mathlib.Meta.NormNum.IsNat ((n - 1) * a) na) (pa : na = na') :
      -(a * b) = na' * b
      def Tactic.ReduceModChar.normNegCoeffMul {u : Lean.Level} {α : Q(Type u)} (n : Q()) (e : Q(«$α»)) (_instRing : Q(Ring «$α»)) (instCharP : Q(CharP «$α» «$n»)) :

      Given an expression -(a * b) : t such that t is a ring of characteristic n, and a is a numeral, simplify this to ((n - 1) * a) * b.

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

        A TypeToCharPResult α indicates if α can be determined to be a ring of characteristic p.

        Instances For
          Equations
          • Tactic.ReduceModChar.instInhabitedTypeToCharPResult = { default := Tactic.ReduceModChar.TypeToCharPResult.failure }

          Determine the characteristic of a ring from the type. This should be fast, so this pattern-matches on the type, rather than searching for a CharP instance. Use typeToCharP (expensive := true) to do more work in finding the characteristic, in particular it will search for a CharP instance in the context.

          Given an expression e, determine whether it is a numeric expression in characteristic n, and if so, reduce e modulo n.

          This is not a norm_num plugin because it does not match on the syntax of e, rather it matches on the type of e.

          Use matchAndNorm (expensive := true) to do more work in finding the characteristic of the type of e.

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

            Reduce all numeric subexpressions of e modulo their characteristic.

            Use derive (expensive := true) to do more work in finding the characteristic of the type of e.

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

              Reduce all numeric subexpressions of the goal modulo their characteristic.

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

                Reduce all numeric subexpressions of the given hypothesis modulo their characteristic.

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

                  The tactic reduce_mod_char looks for numeric expressions in characteristic p and reduces these to lie between 0 and p.

                  For example:

                  example : (5 : ZMod 4) = 1 := by reduce_mod_char
                  example : (X ^ 2 - 3 * X + 4 : (ZMod 4)[X]) = X ^ 2 + X := by reduce_mod_char
                  

                  It also handles negation, turning it into multiplication by p - 1, and similarly subtraction.

                  This tactic uses the type of the subexpression to figure out if it is indeed of positive characteristic, for improved performance compared to trying to synthesise a CharP instance. The variant reduce_mod_char! also tries to use CharP R n hypotheses in the context. (Limitations of the typeclass system mean the tactic can't search for a CharP R n instance if n is not yet known; use have : CharP R n := inferInstance; reduce_mod_char! as a workaround.)

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

                    The tactic reduce_mod_char looks for numeric expressions in characteristic p and reduces these to lie between 0 and p.

                    For example:

                    example : (5 : ZMod 4) = 1 := by reduce_mod_char
                    example : (X ^ 2 - 3 * X + 4 : (ZMod 4)[X]) = X ^ 2 + X := by reduce_mod_char
                    

                    It also handles negation, turning it into multiplication by p - 1, and similarly subtraction.

                    This tactic uses the type of the subexpression to figure out if it is indeed of positive characteristic, for improved performance compared to trying to synthesise a CharP instance. The variant reduce_mod_char! also tries to use CharP R n hypotheses in the context. (Limitations of the typeclass system mean the tactic can't search for a CharP R n instance if n is not yet known; use have : CharP R n := inferInstance; reduce_mod_char! as a workaround.)

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