Simpler proof of injectivity {0,1,-1} --> R?

Stream: Is there code for X?

[Michael Stoll]

I need the fact that when a b : ℤ are both in {0, 1, -1} and (a : R) = (b : R) in a nontrivial ring R of characteristic ≠ 2, then a = b. I'm wondering if the following proof can be simplified.

import tactic.basic
import algebra.char_p.basic

/-- We have `2 ≠ 0` in a nontrivial ring whose characteristic is not `2`. -/
lemma ring.two_ne_zero {R : Type*} [non_assoc_ring R] [nontrivial R] (hR : ring_char R ≠ 2) :
  (2 : R) ≠ 0 :=
begin
  change ¬ (2 : R) = 0,
  rw [(by norm_cast : (2 : R) = (2 : ℤ)), char_p.int_cast_eq_zero_iff R (ring_char R) 2,
      (by norm_cast : (2 : ℤ) = (2 : ℕ)), int.coe_nat_dvd, nat.dvd_prime nat.prime_two],
  exact mt (or_iff_left hR).mp char_p.ring_char_ne_one,
end

/-- If two integers from `{0, 1, -1}` result in equal elements in a ring `R`
that is nontrivial and of characteristic not `2`, then they are equal. -/
lemma ring.int_sign_eq_of_coe_eq
 {R : Type*} [non_assoc_ring R] [nontrivial R] (hR : ring_char R ≠ 2)
 {a b : ℤ} (ha : a = 0 ∨ a = 1 ∨ a = -1) (hb : b = 0 ∨ b = 1 ∨ b = -1) (h : (a : R) = b) :
  a = b :=
begin
  apply eq_of_sub_eq_zero,
  by_contra hf,
  have hh : a - b = 1 ∨ b - a = 1 ∨ a - b = 2 ∨ b - a = 2 := by
  { rcases ha with ha | ha | ha; rcases hb with hb | hb | hb,
    swap 5, swap 9, -- move goals with `a = b` to the front
    iterate 3 { rw [ha, hb, sub_self] at hf, tauto, }, -- 6 goals remain
    all_goals { rw [ha, hb], norm_num, }, },
  have h' : ((a - b : ℤ) : R) = 0 := by exact_mod_cast sub_eq_zero_of_eq h,
  have h'' : ((b - a : ℤ) : R) = 0 := by exact_mod_cast sub_eq_zero_of_eq h.symm,
  rcases hh with hh | hh | hh | hh,
  { rw [hh, (by norm_cast : ((1 : ℤ) : R) = 1)] at h', exact one_ne_zero h', },
  { rw [hh, (by norm_cast : ((1 : ℤ) : R) = 1)] at h'', exact one_ne_zero h'', },
  { rw [hh, (by norm_cast : ((2 : ℤ) : R) = 2)] at h', exact ring.two_ne_zero hR h', },
  { rw [hh, (by norm_cast : ((2 : ℤ) : R) = 2)] at h'', exact ring.two_ne_zero hR h'', },
end

(Fiddling with casts of numerals is especially annoying...)

[Michael Stoll]

Somehow I had the feeling that the proof of hh in the above should just be dec_trivial, but that does not seem to work.

[Kevin Buzzard]

Here's a minor golf for two_ne_zero, plus two more lemmas which I thought would be useful but turned out not to be because you can go straight from R to nat. I don't really see any way of dealing with all 9 cases in the big theorem; I mean, that's how we'd do it in our heads, right? I guess a more general approach would be to have a and b in set.Icc (-N) N and the assumption that the characteristic is 0 or bigger than 2N; that would force you to "do it properly" as it were.

lemma coe_eq_zero_iff_nat_abs (R : Type*) [non_assoc_ring R] (x : ℤ) :
  (x : R) = 0 ↔ (x.nat_abs : R) = 0 :=
begin
  cases int.nat_abs_eq x with hx hx;
  { conv_lhs {rw [hx] }, simp },
end

lemma ring_char.zspec (R : Type*) [non_assoc_ring R] (x : ℤ) :
  (x : R) = 0 ↔ (ring_char R : ℤ) ∣ x :=
by rw [coe_eq_zero_iff_nat_abs, int.coe_nat_dvd_left, ring_char.spec]

/-- We have `2 ≠ 0` in a nontrivial ring whose characteristic is not `2`. -/
lemma ring.two_ne_zero {R : Type*} [non_assoc_ring R] [nontrivial R] (hR : ring_char R ≠ 2) :
  (2 : R) ≠ 0 :=
begin
  change ¬ (2 : R) = 0,
  rw [(by norm_cast : (2 : R) = (2 : ℕ)), ring_char.spec, nat.dvd_prime nat.prime_two],
  exact mt (or_iff_left hR).mp char_p.ring_char_ne_one,
end

[Michael Stoll]

Thanks!

Kevin Buzzard said:

I don't really see any way of dealing with all 9 cases in the big theorem; I mean, that's how we'd do it in our heads, right? I guess a more general approach would be to have a and b in set.Icc (-N) N and the assumption that the characteristic is 0 or bigger than 2N; that would force you to "do it properly" as it were.

Well, but that would make the handling of the assumption on the characteristic much more unpleasant in my use case...

[Kevin Buzzard]

Here's a slightly shorter proof using the rintro rfl trick many times:

lemma ring.int_sign_eq_of_coe_eq
 {R : Type*} [non_assoc_ring R] [nontrivial R] (hR : ring_char R ≠ 2)
 {a b : ℤ} (ha : a = 0 ∨ a = 1 ∨ a = -1) (hb : b = 0 ∨ b = 1 ∨ b = -1) (h : (a : R) = b) :
  a = b :=
begin
  apply eq_of_sub_eq_zero,
  by_contra hf,
  have hh : a = 1 + b ∨ b = 1 + a ∨ a = 2 + b ∨ b = 2 + a := by
  { rcases ha with rfl | rfl | rfl;
    rcases hb with rfl | rfl | rfl;
    norm_num; apply hf; norm_num, },
  rcases hh with rfl | rfl | rfl | rfl,
  { simpa using h },
  { simpa using h },
  { apply ring.two_ne_zero hR, simp at h, exact_mod_cast h, },
  { apply ring.two_ne_zero hR, simp at h, exact_mod_cast h, },
end

[Yaël Dillies]

Any reason you're not using docs#sign_type?

[Yaël Dillies]

This translates into "The canonical map from sign_type is injective"

[Michael Stoll]

Yaël Dillies said:

Any reason you're not using docs#sign_type?

Yes: I want to add values.
How much simpler would the proof be when a b : sign_type? You still have nine cases to deal with...

[Michael Stoll]

Kevin Buzzard said:

Here's a slightly shorter proof using the rintro rfl trick many times: (...)

It is shorter, but a bit less efficient (although not by much).

[Eric Rodriguez]

The point of sign_type is basically to be coerced into the correct structure

[Damiano Testa]

The proof of ring.two_ne_zero can also be golfed to

lemma ring.two_ne_zero {R : Type*} [non_assoc_ring R] [nontrivial R] (hR : ring_char R ≠ 2) :
  (2 : R) ≠ 0 :=
λ h, hR $ char_p.ring_char_of_prime_eq_zero nat.prime_two (by simpa using h)

if you really want to obscure it.

[Damiano Testa]

Also, in the spirit of ring.int_sign_eq_of_coe_eq, this lemma seems potentially useful:

lemma window {R : Type*} [add_group R] [has_one R] {d e : ℕ}
  (de : d ≤ e) (x : ℤ) (hR : char_p R e) :
  set.inj_on (coe : ℤ → R) (set.Ico x (x + d)) :=
begin
  rintros a ⟨a0, ad⟩ b ⟨b0, bd⟩ ab,
  rw [char_p.int_coe_eq_int_coe_iff R e, int.modeq_iff_dvd] at ab,
  rcases ab with ⟨c, hc⟩,
  have c0 : c = 0,
  { refine le_antisymm (int.lt_add_one_iff.mp _) (neg_nonpos.mp (int.lt_add_one_iff.mp _));
    simp only [zero_add, ← mul_lt_iff_lt_one_right (by linarith : (0 : ℤ) < e), ← hc];
    linarith },
  rwa [c0, mul_zero, sub_eq_zero, eq_comm] at hc,
end

[Damiano Testa]

In fact, using window, you can prove

lemma ring.int_sign_eq_of_coe_eq_Ico
 {R : Type*} [non_assoc_ring R] [nontrivial R] (hR0 : ring_char R ≠ 0) (hR : ring_char R ≠ 2)
 {a b : ℤ} (ha : a ∈ set.Ico (-1 : ℤ) 2) (hb : b ∈ set.Ico (-1 : ℤ) 2) (h : (a : R) = b) :
  a = b :=
begin
  refine window (_ : 3 ≤ ring_char R) (-1) (ring_char.of_eq rfl) ha hb h,
  repeat { refine nat.succ_le_iff.mpr (lt_of_le_of_ne _ (ne.symm _)) },
  exacts [nat.zero_le _, hR0, char_p.ring_char_ne_one, hR],
end

[Damiano Testa]

Note that, besides replacing the explicit equalities of a, b I am using intervals. Still, the main reason this feels simpler is the extra assumption ring_char R ≠ 0. There was a discussion recently about the fact that char_p R 0 is not an equivalent of char_zero.

To me, your example seems to be further indication that ring_char R = 0 should be mean char_zero R and not char_p R 0.

[Damiano Testa]

This is a proof that in your case, the ring_char assumption also implies char_zero R:

lemma ch0 {R : Type*} [non_assoc_ring R] (hR0 : ring_char R = 0) :
  char_zero R :=
@char_p.char_p_to_char_zero _ _ _ (ring_char.of_eq hR0)