ring tactics for characteristic p?

Stream: Is there code for X?

[Jz Pan]

Is ring tactics make use of the fact that the ring has characteristic p?

[Mario Carneiro]

no

[Jz Pan]

For example if given the fact that a ring has characteristic p, then the tactic will rewrite all "-" to "+" and rewrite the integer appeared in the expression to [0,p-1]

[Mario Carneiro]

I don't even know if we have any examples of characteristic p fields in mathlib where p is not a variable

[Jz Pan]

Oh ok. How can I implement such tactics? Any suggestions?

[Mario Carneiro]

If p is a variable then that will do more harm than good

[Jz Pan]

Ok I mean p is a constant, not a variable

[Mario Carneiro]

right. who does that?

[Mario Carneiro]

plus the typeclass problem could be tricky - it has to discover this char p fact somehow

[Jz Pan]

Ask the user to provide that information explicitly

[Mario Carneiro]

Do you have an example?

[Jz Pan]

That is used a lot, for example, some basic properties of Weierstrass equations in char 2 or 3 case

[Mario Carneiro]

What I would suggest is something similar to our faux-grobner basis proof method: use ring to prove that your polynomial is equal to a multiple of 2 or 3, then rewrite with 2 = 0

[Mario Carneiro]

In fact this might even just be a special case of grobner basis

[Jz Pan]

Currently I just use ring tactics and manually identify which integers I need to rewrite to make both sides equal, then I write a simple lemma to produce such identities

[Mario Carneiro]

Do you have an example?

[Jz Pan]

Please wait a moment; let me extract a piece of code

[Mario Carneiro]

It should be possible to do this in ~2 lines without a lemma

[Jz Pan]

import algebra.field
import algebra.char_zero
import algebra.char_p
import tactic

noncomputable theory

@[ext]
structure weierstrass_equation (K : Type*) [field K] :=
mk :: (a1 a2 a3 a4 a6 : K)

def weierstrass_equation.b2 {K : Type*} [field K] (E : weierstrass_equation K) : K :=
E.a1^2 + 4*E.a2

def weierstrass_equation.b4 {K : Type*} [field K] (E : weierstrass_equation K) : K :=
2*E.a4 + E.a1*E.a3

def weierstrass_equation.b6 {K : Type*} [field K] (E : weierstrass_equation K) : K :=
E.a3^2 + 4*E.a6

def weierstrass_equation.b8 {K : Type*} [field K] (E : weierstrass_equation K) : K :=
E.a1^2*E.a6 + 4*E.a2*E.a6 - E.a1*E.a3*E.a4 + E.a2*E.a3^2 - E.a4^2

def weierstrass_equation.disc {K : Type*} [field K] (E : weierstrass_equation K) : K :=
-E.b2^2*E.b8 - 8*E.b4^3 - 27*E.b6^2 + 9*E.b2*E.b4*E.b6

def weierstrass_equation.is_model_of_char_2_j_non_zero {K : Type*} [field K]
(E : weierstrass_equation K) :=
E.a1 = 1 ∧ E.a3 = 0 ∧ E.a4 = 0

lemma dvd_char_is_zero
{K : Type*} [field K] {p : ℕ} (hp : ring_char K = p) (n : ℤ) (hdvd : (p : ℤ) ∣ n) : (n : K) = 0 :=
begin
  rw ring_char.eq_iff at hp,
  rw @char_p.int_cast_eq_zero_iff K _ p hp n,
  exact hdvd,
end

-- unused in this example but you got the point
lemma cong_char_is_eq
{K : Type*} [field K] {p : ℕ} (hp : ring_char K = p) (a b : ℤ) (hdvd : (p : ℤ) ∣ (b - a)) : (a : K) = (b : K) :=
begin
  rw ring_char.eq_iff at hp,
  rw @char_p.int_coe_eq_int_coe_iff K _ p hp a b,
  rw int.modeq.modeq_iff_dvd,
  exact hdvd,
end

lemma weierstrass_equation.disc_of_model_of_char_2_j_non_zero {K : Type*} [field K]
(E : weierstrass_equation K) (h : E.is_model_of_char_2_j_non_zero) (hchar2 : ring_char K = 2) :
E.disc = E.a6 :=
begin
  unfold weierstrass_equation.disc
  weierstrass_equation.b2
  weierstrass_equation.b4
  weierstrass_equation.b6
  weierstrass_equation.b8,
  rw [h.1, h.2.1, h.2.2],
  -- here I imagine a tactic 'ring_char_p hchar2' should do all the tricks
  simp [zero_pow], ring,
  have h := dvd_char_is_zero hchar2 432 (by norm_num), norm_cast at h, rw h, clear h,
  have h := dvd_char_is_zero hchar2 64 (by norm_num), norm_cast at h, rw h, clear h,
  have h := dvd_char_is_zero hchar2 48 (by norm_num), norm_cast at h, rw h, clear h,
  have h := dvd_char_is_zero hchar2 12 (by norm_num), norm_cast at h, rw h, clear h,
  ring,
  calc -E.a6 = E.a6 - 2*E.a6 : by ring
  ... = E.a6 : by {
    have h := dvd_char_is_zero hchar2 2 (by norm_num), norm_cast at h, rw h, clear h,
    ring,
  },
end

[Jz Pan]

In this example I need to manually find out all integer constants 432,64,48,12 and rewrites all of them to zero. I imagine there could be an automatic way to do this.

[Mario Carneiro]

lemma weierstrass_equation.disc_of_model_of_char_2_j_non_zero {K : Type*} [field K]
(E : weierstrass_equation K) (h : E.is_model_of_char_2_j_non_zero) (hchar2 : ring_char K = 2) :
E.disc = E.a6 :=
sub_eq_zero.1 begin
  have := (ring_char.spec K 2).2 (by rwa hchar2), norm_cast at this,
  transitivity 2 * -(E.a6 * (1 + 6 * E.a2 + 24 * E.a2^2 + 32 * E.a2^3 + 216 * E.a6)),
  { simp [weierstrass_equation.disc, weierstrass_equation.b2, weierstrass_equation.b4,
      weierstrass_equation.b6, weierstrass_equation.b8, h.1, h.2.1, h.2.2], ring },
  rw [this, zero_mul]
end

[Mario Carneiro]

I didn't prove 2=0 but I'm sure you have theorems for that

[Eric Wieser]

Do we have a typeclass for ring_char K = 2? If so, could we add a special case for that that says bit0 x = 0 and bit1 x = 1?

[Eric Wieser]

Which would knock out all the integer literals very quickly

[Mario Carneiro]

yeah it's char_p K 2

[Mario Carneiro]

This wouldn't work for 3 though

[Eric Wieser]

Do you think those lemmas would be a bad idea then?

[Mario Carneiro]

Because of the trick I just showed above, I don't find the need for a new decision procedure particularly pressing. norm_fin does a lot of similar reasoning but that's on fin n, not a ring of finite characteristic

[Mario Carneiro]

Reducing the constants is only one possible thing you can do here, and it's not particularly helpful to solving the goal

[Mario Carneiro]

what you actually want is to factor the polynomial into sums of multiples of things that you know are zero, which is what a grobner basis tactic would do

[Mario Carneiro]

See https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/groebner.20basis.20algorithm

[Mario Carneiro]

Eric Wieser said:

Do you think those lemmas would be a bad idea then?

It would fire on every subterm of every numeral, triggering a typeclass search that almost always fails. Sounds like a bad idea

[Mario Carneiro]

maybe as an opt in simp lemma

[Johan Commelin]

I think they are great lemmas, but they shouldn't be in the default simp-set.

[Johan Commelin]

Special case calculations for p = 2 show up often enough that I think a bit of extra support for them doesn't hurt.

[Damiano Testa]

For the ring_char K = 3, could you use bit0 x = - x and bit1 x = 1 - x?

Or would the bit1 lemma be undoing the good that bit1 does?

[Johan Commelin]

Hah, I guess that would help! Together with neg_neg which will cancel all the negations.

[Damiano Testa]

Ok, I just got myself confused with signs and bit1: is what I wrote correct for bit1? [bit1 x = 1 - x]

[Damiano Testa]

This is like "divisibility by 11" in decimals: the alternating sign of the digits-mod-two is the remainder of division by 3.

[Johan Commelin]

bit1 x = 2x + 1 = -x + 1

[Damiano Testa]

Ok, so I did get it right! Thanks, Johan!

[Damiano Testa]

I would say that, by far, the most computations modulo a specific prime happen mod 2 or mod 3. Other primes are very often just "generic".

[Jz Pan]

Sorry, but I think I don't quite understand your discussions. (Why are they only applicable for char 2 or 3 case? And why are there bit0, bit1, etc. Why do you need a Grobener basis algorithm?)

What tactics I think, in its basic form, only reduces all integer literals appears in the expression. I assume it's easy to implement? Just traverse the whole expression, find all integer literals m, check that if it's in a ring whose characteristic is also an integer literal n, then replace m by m%n. Also it replaces all A - m * B by A + ((-m)%n) * B.

Example: if R is a ring, say of characteristic 10 (characteristic of a ring is not necessarily a prime number), x is a variable in R. Then after providing all necessary information to the tactics, it should transform 34 * x^2 - 193 * x + 1720 into 4 * x^2 + 7 * x.

[Jz Pan]

A more advanced implementation also checks whether an integer literal m is a zero divisor, or is invertible, in a ring R whose characteristic is an integer literal n. Example: if R is a ring of characteristic 10, then it should transform 7*x=0 into x=0 since 7 is invertible in R, transform 7*x\neq 0 into x\neq 0, etc.

[Johan Commelin]

@Jz Pan If you have the number 5 in Lean, how does Lean handle it? the way it works is that there is a binary system under the hood.
So 5 = 2 * (2 * 1) + 1. Now bit0 x = x + x and bit1 x = x + x + 1. So 5 = bit1 (bit0 1).

[Johan Commelin]

In a specific characteristics, like 2 or 3, we can have special simplification rules, that will turn bit0 x into 0 (when p = 2), etc...

[Eric Wieser]

Namely, these rules:

import algebra.char_p.basic

variables {R : Type*}

section char_two
variables [semiring R] [char_p R 2]

@[simp]
lemma char_two_bit0 (x : R) : bit0 x = 0 := begin
  unfold bit0,
  rw [←two_smul ℕ x, nsmul_eq_mul, char_p.cast_eq_zero, zero_mul],
end

@[simp]
lemma char_two_bit1 (x : R) : bit1 x = 1 := begin
  unfold bit1,
  rw [char_two_bit0, zero_add],
end

example : (35 : R) = 37 := by simp

end char_two

[Johan Commelin]

Right, and Damiano gave the rules for p = 3.

[Johan Commelin]

But I agree with Mario that these lemmas should probably not be @[simp] globally.

[Johan Commelin]

We can probably enable them with open_locale char2

[Eric Wieser]

The rules for p = 3 aren't enough:

section char_three

variables [ring R] [char_p R 3]

@[simp]
lemma char_three_bit0 (x : R) : bit0 x = -x := begin
  unfold bit0,
  rw [←two_smul ℕ x, eq_neg_iff_add_eq_zero,
    add_comm, ←succ_nsmul, nsmul_eq_mul, char_p.cast_eq_zero, zero_mul],
end

@[simp]
lemma char_three_bit1 (x : R) : bit1 x = 1 - x := begin
  unfold bit1,
  rw [char_three_bit0, add_comm, sub_eq_add_neg],
end

example : (34 : R) = 37 := by simp  -- fails

end char_three

[Yakov Pechersky]

Seems like a job for a norm_num plugin

[Yakov Pechersky]

A la norm_fin

[Gabriel Ebner]

For p=3 you just need more lemmas:

@[simp] lemma char_three_bit1_zero : bit1 (0 : R) = 1 := by simp [bit1]
@[simp] lemma char_three_bit1_one : bit1 (1 : R) = 0 := by simp [bit1]
@[simp] lemma char_three_bit1_two : bit1 (-1 : R) = (-1) := by simp [bit0, bit1]

[Damiano Testa]

Just a funny remark.

If you add Gabriel's lemmas after Eric's char_three_bit1, they close the example.
If you add Gabriel's lemmas just before Eric's char_three_bit1, they do not close the example.

[Jz Pan]

Thank you for your replies. I'll try these suggestions.

Seems like a job for a norm_num plugin

I think this describes my idea best.

[Mario Carneiro]

My point is that reducing the numerals in a polynomial is not a particularly useful thing to do, unless you combine it with other things. In fact, factoring a polynomial sometimes requires writing the coefficients in an unnormalized way

[Mario Carneiro]

If you just want the polynomial to look good in the tactic state, then okay, but if you actually want to close the goal (which is what ring is trying to do) then you need to do more

[Johan Commelin]

But if you are multiplying by 42 in a char 2 ring, then there are plenty situations where it helps if there is a cheap tactic that just cancels that term.

[Mario Carneiro]

maybe, but it still sounds strictly less powerful than this grobner basis approach

[Mario Carneiro]

which we currently have semi-automatic support for

[Mario Carneiro]

In particular, I want to point out that in Jz Pan 's first version they had to use this number cancelling tactic several times and still had to do some funky algebra afterward, while the factoring approach only requires one application: supply the magical witness coefficient -(E.a6 * (1 + 6 * E.a2 + 24 * E.a2^2 + 32 * E.a2^3 + 216 * E.a6)) and then the problem is solved

[Mario Carneiro]

(By the way, I found that coefficient by asking mathematica)

[Johan Commelin]

[Where is my emoji for cheating :stuck_out_tongue_wink: ] /s

[Mario Carneiro]

The role of a true grobner tactic in lean would be to determine that coefficient and then replace itself with ring_rw using the coefficient

[Mario Carneiro]

(ring_rw doesn't exist yet either)

[Jz Pan]

OK I have the first working example of char 2 tactics, adapting the codes by @Eric Wieser .

variables {R : Type*} [semiring R]

lemma char_two_bit0 (hchar : ring_char R = 2) (x : R) : bit0 x = 0 := begin
  unfold bit0,
  transitivity (2:R) * x,
  { rw [bit0, add_mul, one_mul], },
  rw ring_char.eq_iff at hchar,
  have := @char_p.cast_eq_zero R _ 2 hchar,
  norm_cast at this,
  rw [this, zero_mul],
end

lemma char_two_bit1 (hchar : ring_char R = 2) (x : R) : bit1 x = 1 := begin
  unfold bit1,
  rw [char_two_bit0 hchar, zero_add],
end

example (hchar : ring_char R = 2) : (35 : R) = 37 := begin
  simp [char_two_bit0 hchar, char_two_bit1 hchar],
end

open tactic (get_local infer_type)
open interactive (parse)
open lean.parser (ident)
open interactive (loc.ns)
open interactive.types (texpr location)

meta def tactic.interactive.simp_char2 (hchar_ : parse texpr) : tactic unit :=
do
  hchar ← tactic.i_to_expr hchar_,
  `(ring_char _ = 2) ← infer_type hchar,
  `[ repeat { simp [char_two_bit0 hchar, char_two_bit1 hchar, pow_zero, pow_one, zero_mul, mul_zero] <|> ring_nf } ]

example (hchar : ring_char R = 2) : (35 : R) = 37 := begin
  simp_char2 hchar,
end

[Eric Rodriguez]

may be good to make a simp-set for this! cf here

[Jz Pan]

But there are some problems need to be fixed:

1. the char assumption in the tactics is hard-coded as hchar. I tried char_two_bit0 %%hchar, char_two_bit1 %%hchar according to this tutorial, but Lean refused to accept my code, complains "kernel failed to type check declaration 'tactic.interactive.simp_char2' this is usually due to a buggy tactic or a bug in the builtin elaborator".
2. I want it shows a proper error message when (ring_char _ = 2) ← infer_type hchar fails.

How to fix them?

[Scott Morrison]

Unfortunately you can't use antiquotations inside `[...]. You'll need to build the simp set by hand. There are many examples; the last time I did this was tactic#elementwise, so if it was me I'd start reconstructing how to do it from there. :-)

[Scott Morrison]

For 2. just put | fail ":-(" at the end of the line (before the comma)

[Scott Morrison]

(or maybe failed? I can never remember which one is which)

[Mario Carneiro]

Don't forget failure

[Jz Pan]

Scott Morrison said:

Unfortunately you can't use antiquotations inside `[...]. You'll need to build the simp set by hand. There are many examples; the last time I did this was tactic#elementwise, so if it was me I'd start reconstructing how to do it from there. :-)

Thanks for your comments. Now I try to build simp set manually, but I have a new problem:

import algebra.field
import algebra.char_zero
import algebra.char_p
import tactic

  variables {R : Type*} [semiring R]

  lemma char_two_bit0 (hchar : ring_char R = 2) (x : R) : bit0 x = 0 := begin
    unfold bit0,
    transitivity (2:R) * x,
    { rw [bit0, add_mul, one_mul], },
    rw ring_char.eq_iff at hchar,
    have := @char_p.cast_eq_zero R _ 2 hchar,
    norm_cast at this,
    rw [this, zero_mul],
  end

  lemma char_two_bit1 (hchar : ring_char R = 2) (x : R) : bit1 x = 1 := begin
    unfold bit1,
    rw [char_two_bit0 hchar, zero_add],
  end

  example (hchar : ring_char R = 2) : (35 : R) = 37 := begin
    simp [char_two_bit0 hchar, char_two_bit1 hchar],
  end

  open tactic (get_local infer_type)
  open interactive (parse)
  open lean.parser (ident)
  open interactive (loc.ns)
  open interactive.types (texpr location)

  /--
  Experimental ring tactic for characteristic 2.
  FIXME: You must provide a `hchar2 : ring_char R = 2` hypothesis.
  -/
  meta def tactic.interactive.ring_char2 (loc : parse location) : tactic unit :=
  do
    hchar ← get_local `hchar2,
    `(ring_char _ = 2) ← infer_type hchar | tactic.fail "hchar2 : ring_char R = 2 is expected",
    let s := simp_lemmas.mk,
    s ← s.add hchar,
    s ← s.add_simp ``char_two_bit0,
    s ← s.add_simp ``char_two_bit1,
    s ← s.add_simp ``pow_zero,
    s ← s.add_simp ``pow_one,
    s ← s.add_simp ``zero_mul,
    s ← s.add_simp ``mul_zero,
    ns ← loc.get_locals,
    tactic.simp_target s,
    tactic.skip
    /-
    -- tactic.repeat (do
      ret1 ← tactic.replace_at (
        λ e, do (a1, a2, a3) ← tactic.simplify s [] e, return (a1, a2)
      ) ns loc.include_goal,
      ret2 ← tactic.replace_at (
        tactic.ring.normalize tactic.transparency.reducible
      ) ns loc.include_goal,
      tactic.skip
    --  if ret1 || ret2 then tactic.skip else tactic.failed
    -- )
    -/

  example (hchar2 : ring_char R = 2) : (35 : R) = 37 := begin
    ring_char2,
    -- error here
  end

It doesn't work and complains that "deep recursion was detected at 'level constraints' (potential solution: increase stack space in your system)". What's the problem?

[Scott Morrison]

#mwe?

[Jz Pan]

Sorry, I have added all necessary codes now.

[Jz Pan]

I think I have found the problem, but note sure how to fix it: in fact if I replace the first example by simp [hchar, char_two_bit0, char_two_bit1] it will also fall into a deadloop.

[Jz Pan]

OK I fixed it by myself; replace these 3 lines

    s ← s.add hchar,
    s ← s.add_simp ``char_two_bit0,
    s ← s.add_simp ``char_two_bit1,

by

    char_two_bit0 ← tactic.to_expr ``(char_two_bit0 %%hchar),
    s ← s.add char_two_bit0,
    char_two_bit1 ← tactic.to_expr ``(char_two_bit1 %%hchar),
    s ← s.add char_two_bit1,

then it works.

[Jz Pan]

OK, now I'd like to share the ring_charp tactics I write:

import data.nat.basic
import algebra.char_zero
import algebra.char_p
import tactic

lemma dvd_char_is_zero_N
{R : Type*} [semiring R] {p : ℕ} (hp : ring_char R = p) (n : ℕ) (hdvd : p ∣ n) : (n : R) = 0 :=
begin
  rw ring_char.eq_iff at hp,
  rw @char_p.cast_eq_zero_iff R _ p hp n,
  exact hdvd,
end

lemma cong_char_is_eq_N'
{R : Type*} [semiring R] {p : ℕ} (hp : ring_char R = p) (a b : ℕ) (hleq : a ≤ b) (hdvd : (p : ℤ) ∣ (b - a)) : (a : R) = (b : R) :=
begin
  by_cases hpzero : p = 0, {
    rw hpzero at hdvd,
    simp [sub_eq_zero] at hdvd,
    rw hdvd,
  },
  replace hpzero := pos_iff_ne_zero.mpr hpzero,
  zify at hpzero,
  cases hdvd with c hdvd,
  rw ring_char.eq_iff at hp,
  zify at hleq,
  replace hleq : ((b:ℤ) - a) ≥ 0 := by linarith,
  rw hdvd at hleq,
  simp [hpzero] at hleq,
  lift c to ℕ using hleq,
  replace hdvd : (b:ℤ) = a + p * c := by { rw ← hdvd, ring, },
  norm_cast at hdvd,
  rw hdvd,
  push_cast,
  simp [(@char_p.cast_eq_zero_iff R _ p hp p).2 (dvd_refl p)],
end

lemma cong_char_is_eq_N
{R : Type*} [semiring R] {p : ℕ} (hp : ring_char R = p) (a b : ℕ) (hdvd : (p : ℤ) ∣ (b - a)) : (a : R) = (b : R) :=
begin
  by_cases h : b ≥ a, {
    exact cong_char_is_eq_N' hp a b h hdvd,
  },
  replace h : a ≥ b := by linarith,
  replace hdvd : (p : ℤ) ∣ (a - b) := by {
    cases hdvd with c hdvd,
    use -c,
    replace hdvd : (b:ℤ) = a + p * c := by { rw ← hdvd, ring, },
    rw hdvd,
    ring,
  },
  exact (cong_char_is_eq_N' hp b a h hdvd).symm,
end

section char_specific

  lemma char_two_bit0 {R : Type*} [semiring R] (hchar : ring_char R = 2) (x : R) : bit0 x = 0 := begin
    unfold bit0,
    transitivity (2:R) * x,
    { rw [bit0, add_mul, one_mul], },
    rw ring_char.eq_iff at hchar,
    have := @char_p.cast_eq_zero R _ 2 hchar,
    norm_cast at this,
    rw [this, zero_mul],
  end

  lemma char_two_bit1 {R : Type*} [semiring R] (hchar : ring_char R = 2) (x : R) : bit1 x = 1 := begin
    unfold bit1,
    rw [char_two_bit0 hchar, zero_add],
  end

  example {R : Type*} [semiring R] (hchar : ring_char R = 2) : (35 : R) = 37 := begin
    simp [char_two_bit0 hchar, char_two_bit1 hchar],
  end

  open tactic (get_local infer_type)
  open interactive (parse)
  open lean.parser (ident)
  open interactive (loc.ns)
  open interactive.types (texpr location)

  meta def repeat_at_most : ℕ → tactic unit → tactic unit
  | 0 t := tactic.skip
  | (n+1) t := (do t, repeat_at_most n t) <|> tactic.skip

  meta def ring_char_tactic_internal (s : simp_lemmas) (u : list name) (loc : parse location) : tactic unit :=
  do
    s ← s.add_simp ``pow_zero,
    s ← s.add_simp ``pow_one,
    s ← s.add_simp ``zero_mul,
    s ← s.add_simp ``mul_zero,
    ns ← loc.get_locals,
    -- FIXME: add a maximal repeat time since sometimes simp will change the goal randomly
    repeat_at_most 4 (do
      ret1 ← tactic.replace_at (
        λ e, do (a1, a2, _) ← tactic.simplify s u e, return (a1, a2)
      ) ns loc.include_goal,
      ret2 ← tactic.replace_at (
        tactic.ring.normalize tactic.transparency.reducible
      ) ns loc.include_goal,
      if ret1 || ret2 then tactic.skip else tactic.failed
    ),
    when loc.include_goal $ tactic.try (tactic.triv <|> tactic.reflexivity <|> tactic.contradiction)

  /--
  Experimental ring tactic for characteristic 2.
  FIXME: You must provide a `hchar2 : ring_char R = 2` hypothesis.
  -/
  meta def tactic.interactive.ring_char2 (loc : parse location) : tactic unit :=
  do
    hchar ← get_local `hchar2,
    `(ring_char _ = 2) ← infer_type hchar | tactic.fail "hchar2 : ring_char R = 2 is expected",
    (s, u) ← tactic.mk_simp_set ff [] [], -- FIXME: this includes all default simp lemmas into it
    s ← tactic.to_expr ``(char_two_bit0 %%hchar) >>= s.add,
    s ← tactic.to_expr ``(char_two_bit1 %%hchar) >>= s.add,
    ring_char_tactic_internal s u loc

  example {R : Type*} [semiring R] (hchar2 : ring_char R = 2) : (35 : R) = 37 := begin
    ring_char2,
  end

  example {R : Type*} [semiring R] (hchar2 : ring_char R = 2) (x : R) (h : (35 : R) * x = 37) : x = 39 := begin
    ring_char2 at h ⊢,
    exact h,
  end

  lemma char_three_3_eq_0 {R : Type*} [semiring R] (hchar : ring_char R = 3) : (3:R) = 0 := begin
    exact_mod_cast dvd_char_is_zero_N hchar 3 (by norm_num),
  end

  lemma char_three_4_eq_1 {R : Type*} [semiring R] (hchar : ring_char R = 3) : (4:R) = 1 := begin
    exact_mod_cast cong_char_is_eq_N hchar 4 1 (by norm_num),
  end

  lemma char_three_5_eq_2 {R : Type*} [semiring R] (hchar : ring_char R = 3) : (5:R) = 2 := begin
    exact_mod_cast cong_char_is_eq_N hchar 5 2 (by norm_num),
  end

  example {R : Type*} [semiring R] (hchar : ring_char R = 3) : (34 : R) = 37 := begin
    simp [char_three_3_eq_0 hchar, char_three_4_eq_1 hchar, char_three_5_eq_2 hchar],
  end

  /--
  Experimental ring tactic for characteristic 3.
  FIXME: You must provide a `hchar3 : ring_char R = 3` hypothesis.
  -/
  meta def tactic.interactive.ring_char3 (loc : parse location) : tactic unit :=
  do
    hchar ← get_local `hchar3,
    `(ring_char _ = 3) ← infer_type hchar | tactic.fail "hchar3 : ring_char R = 3 is expected",
    (s, u) ← tactic.mk_simp_set ff [] [], -- FIXME: this includes all default simp lemmas into it
    s ← tactic.to_expr ``(char_three_3_eq_0 %%hchar) >>= s.add,
    s ← tactic.to_expr ``(char_three_4_eq_1 %%hchar) >>= s.add,
    s ← tactic.to_expr ``(char_three_5_eq_2 %%hchar) >>= s.add,
    ring_char_tactic_internal s u loc

  example {R : Type*} [semiring R] (hchar3 : ring_char R = 3) : (34 : R) = 37 := begin
    ring_char3,
  end

  lemma char_p_a_plus_p_eq_a {R : Type*} [semiring R] {p : ℕ} (hchar : ring_char R = p)
  (a : ℕ) : ((a+p) : R) = a :=
  begin
    exact_mod_cast (cong_char_is_eq_N hchar a (a+p) (by simp)).symm,
  end

  meta def repeat_n_times {T : Type*} : ℕ → (ℕ → T → tactic T) → T → tactic T
  | 0 func t := (do return t)
  | (n+1) func t := (do func n t >>= repeat_n_times n func)

  /--
  Experimental ring tactic for characteristic p for p an integer literal.
  FIXME: You must provide a `hchar : ring_char R = p` hypothesis.
  -/
  meta def tactic.interactive.ring_charp (loc : parse location) : tactic unit :=
  do
    hchar ← get_local `hchar,
    `(ring_char _ = %%pp) ← infer_type hchar | tactic.fail "hchar : ring_char R = p is expected",
    p ← pp.to_nat <|> tactic.fail "p must be an integer literal",
    step ← norm_num.get_step,
    (s, u) ← tactic.mk_simp_set ff [] [], -- FIXME: this includes all default simp lemmas into it
    s ← repeat_n_times p (λ n (ss : simp_lemmas), do
      char_p_a_plus_p_eq_a ← tactic.to_expr ``(char_p_a_plus_p_eq_a %%hchar %%n),
      (_, a2) ← infer_type char_p_a_plus_p_eq_a >>= norm_num.derive' step,
      ss ← tactic.mk_eq_mp a2 char_p_a_plus_p_eq_a >>= ss.add,
      return ss
    ) s,
    ring_char_tactic_internal s u loc

  example {R : Type*} [semiring R] (hchar : ring_char R = 5) : (123567 : R) = 51832 := begin
    ring_charp,
  end

end char_specific

and they magically works, for example, here
An obvious problem is that ring_charp runs slow if the characteristic is large lol