counterexample(counterexamples/char_p_zero_ne_char_zero.lean): `char_…

…p R 0` and `char_zero R` need not coincide (#13080)

Following the [Zulip discussion](https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F), this counterexample formalizes a `semiring R` for which `char_p R 0` holds, but `char_zero R` does not.

See #13075 for the PR that lead to this example.

counterexamples/char_p_zero_ne_char_zero.lean

@@ -0,0 +1,31 @@
+/-
+Copyright (c) 2022 Damiano Testa. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Damiano Testa, Eric Wieser
+-/
+import algebra.char_p.basic
+
+/-! # `char_p R 0` and `char_zero R` need not coincide for semirings
+
+For rings, the two notions coincide.
+
+In fact, `char_p.of_char_zero` shows that `char_zero R` implies `char_p R 0` for any `char_zero`
+`add_monoid R` with `1`.
+The reverse implication holds for any `add_left_cancel_monoid R` with `1`, by `char_p_to_char_zero`.
+
+This file shows that there are semiring `R` for which `char_p R 0` holds and `char_zero R` does not.
+
+The example is `{0, 1}` with saturating addition.
+--/
+
+local attribute [semireducible] with_zero
+
+@[simp] lemma add_one_eq_one : ∀ (x : with_zero unit), x + 1 = 1
+| 0 := rfl
+| 1 := rfl
+
+lemma with_zero_unit_char_p_zero : char_p (with_zero unit) 0 :=
+⟨λ x, by cases x; simp⟩
+
+lemma with_zero_unit_not_char_zero : ¬ char_zero (with_zero unit) :=
+λ ⟨h⟩, h.ne (by simp : 1 + 1 ≠ 0 + 1) (by simp)

src/algebra/char_p/basic.lean

@@ -26,6 +26,7 @@ variables (R : Type u)
 
 For instance, endowing `{0, 1}` with addition given by `max` (i.e. `1` is absorbing), shows that
 `char_zero {0, 1}` does not hold and yet `char_p {0, 1} 0` does.
+This example is formalized in `counterexamples/char_p_zero_ne_char_zero`.
  -/
 class char_p [add_monoid R] [has_one R] (p : ℕ) : Prop :=
 (cast_eq_zero_iff [] : ∀ x:ℕ, (x:R) = 0 ↔ p ∣ x)

src/algebra/char_zero.lean

@@ -42,6 +42,7 @@ from the natural numbers into it is injective.
 
 For instance, endowing `{0, 1}` with addition given by `max` (i.e. `1` is absorbing), shows that
 `char_zero {0, 1}` does not hold and yet `char_p {0, 1} 0` does.
+This example is formalized in `counterexamples/char_p_zero_ne_char_zero`.
  -/
 class char_zero (R : Type*) [add_monoid R] [has_one R] : Prop :=
 (cast_injective : function.injective (coe : ℕ → R))