feat(data/nat/cast,...): add char_zero typeclass for cast_inj

As pointed out by @kbuzzard, the complex numbers are an important example of an unordered characteristic zero field for which we will want cast_inj to be available.

Author: digama0

data/int/basic.lean

@@ -862,6 +862,19 @@ end
 theorem cast_sub [add_group α] [has_one α] (m n) : ((m - n : ℤ) : α) = m - n :=
 by simp
 
+@[simp] theorem cast_eq_zero [add_group α] [has_one α] [char_zero α] {n : ℤ} : (n : α) = 0 ↔ n = 0 :=
+⟨λ h, begin cases n,
+  { exact congr_arg coe (nat.cast_eq_zero.1 h) },
+  { rw [cast_neg_succ_of_nat, neg_eq_zero, ← cast_succ, nat.cast_eq_zero] at h,
+    contradiction }
+end, λ h, by rw [h, cast_zero]⟩
+
+@[simp] theorem cast_inj [add_group α] [has_one α] [char_zero α] {m n : ℤ} : (m : α) = n ↔ m = n :=
+by rw [← sub_eq_zero, ← cast_sub, cast_eq_zero, sub_eq_zero]
+
+@[simp] theorem cast_ne_zero [add_group α] [has_one α] [char_zero α] {n : ℤ} : (n : α) ≠ 0 ↔ n ≠ 0 :=
+not_congr cast_eq_zero
+
 @[simp] theorem cast_mul [ring α] : ∀ m n, ((m * n : ℤ) : α) = m * n
 | (m : ℕ) (n : ℕ) := nat.cast_mul _ _
 | (m : ℕ) -[1+ n] := (cast_neg_of_nat _).trans $
@@ -901,15 +914,6 @@ by rw [← cast_zero, cast_lt]
 @[simp] theorem cast_lt_zero [linear_ordered_ring α] {n : ℤ} : (n : α) < 0 ↔ n < 0 :=
 by rw [← cast_zero, cast_lt]
 
-@[simp] theorem cast_inj [linear_ordered_ring α] {m n : ℤ} : (m : α) = n ↔ m = n :=
-by simp [le_antisymm_iff]
-
-@[simp] theorem cast_eq_zero [linear_ordered_ring α] {n : ℤ} : (n : α) = 0 ↔ n = 0 :=
-by rw [← cast_zero, cast_inj]
-
-@[simp] theorem cast_ne_zero [linear_ordered_ring α] {n : ℤ} : (n : α) ≠ 0 ↔ n ≠ 0 :=
-not_congr cast_eq_zero
-
 @[simp] theorem cast_id : ∀ n : ℤ, ↑n = n
 | (n : ℕ) := (cast_coe_nat n).trans (nat_cast_eq_coe_nat n)
 | -[1+ n] := eq.trans (by rw ← nat_cast_eq_coe_nat; refl) (neg_succ_of_nat_eq _).symm

data/nat/cast.lean

@@ -67,15 +67,6 @@ by simpa [-cast_le] using not_congr (@cast_le α _ n m)
 @[simp] theorem cast_pos [linear_ordered_ring α] {n : ℕ} : (0 : α) < n ↔ 0 < n :=
 by rw [← cast_zero, cast_lt]
 
-@[simp] theorem cast_inj [linear_ordered_semiring α] {m n : ℕ} : (m : α) = n ↔ m = n :=
-by simp [le_antisymm_iff]
-
-@[simp] theorem cast_eq_zero [linear_ordered_semiring α] {n : ℕ} : (n : α) = 0 ↔ n = 0 :=
-by rw [← cast_zero, cast_inj]
-
-@[simp] theorem cast_ne_zero [linear_ordered_semiring α] {n : ℕ} : (n : α) ≠ 0 ↔ n ≠ 0 :=
-not_congr cast_eq_zero
-
 @[simp] theorem cast_id : ∀ n : ℕ, ↑n = n
 | 0     := rfl
 | (n+1) := congr_arg (+1) (cast_id n)
@@ -87,3 +78,48 @@ by by_cases a ≤ b; simp [h, min]
 by by_cases a ≤ b; simp [h, max]
 
 end nat
+
+class char_zero (α : Type*) [add_monoid α] [has_one α] : Prop :=
+(cast_inj : ∀ {m n : ℕ}, (m : α) = n ↔ m = n)
+
+theorem char_zero_of_inj_zero {α : Type*} [add_monoid α] [has_one α]
+  (add_left_cancel : ∀ a b c : α, a + b = a + c → b = c)
+  (H : ∀ n:ℕ, (n:α) = 0 → n = 0) : char_zero α :=
+⟨λ m n, ⟨suffices ∀ {m n : ℕ}, (m:α) = n → m ≤ n,
+  from λ h, le_antisymm (this h) (this h.symm),
+  λ m n h, (le_total m n).elim id $ λ h2, le_of_eq $ begin
+    cases nat.le.dest h2 with k e,
+    suffices : k = 0, {simp [this] at e, rw e},
+    apply H, apply add_left_cancel n,
+    rw [← nat.cast_add, e, add_zero, h]
+  end,
+congr_arg _⟩⟩
+
+theorem add_group.char_zero_of_inj_zero {α : Type*} [add_group α] [has_one α]
+  (H : ∀ n:ℕ, (n:α) = 0 → n = 0) : char_zero α :=
+char_zero_of_inj_zero (@add_left_cancel _ _) H
+
+theorem ordered_cancel_comm_monoid.char_zero_of_inj_zero {α : Type*}
+  [ordered_cancel_comm_monoid α] [has_one α]
+  (H : ∀ n:ℕ, (n:α) = 0 → n = 0) : char_zero α :=
+char_zero_of_inj_zero (@add_left_cancel _ _) H
+
+instance linear_ordered_semiring.to_char_zero {α : Type*}
+  [linear_ordered_semiring α] : char_zero α :=
+ordered_cancel_comm_monoid.char_zero_of_inj_zero $
+λ n h, nat.eq_zero_of_le_zero $
+  (@nat.cast_le α _ _ _).1 (by simp [h])
+
+namespace nat
+variables {α : Type*} [add_monoid α] [has_one α] [char_zero α]
+
+@[simp] theorem cast_inj {m n : ℕ} : (m : α) = n ↔ m = n :=
+char_zero.cast_inj _
+
+@[simp] theorem cast_eq_zero {n : ℕ} : (n : α) = 0 ↔ n = 0 :=
+by rw [← cast_zero, cast_inj]
+
+@[simp] theorem cast_ne_zero {n : ℕ} : (n : α) ≠ 0 ↔ n ≠ 0 :=
+not_congr cast_eq_zero
+
+end nat

data/rat.lean

@@ -723,32 +723,54 @@ have (n⁻¹.denom : α) = 0 → (n.num : α) = 0, from
      rwa [int.cast_mul, int.cast_coe_nat, h, zero_mul] at this,
 by rw [division_def, cast_mul_of_ne_zero md (mt this nn), cast_inv_of_ne_zero nn nd, division_def]
 
+@[simp] theorem cast_inj [char_zero α] : ∀ {m n : ℚ}, (m : α) = n ↔ m = n
+| ⟨n₁, d₁, h₁, c₁⟩ ⟨n₂, d₂, h₂, c₂⟩ := begin
+  refine ⟨λ h, _, congr_arg _⟩,
+  have d₁0 : d₁ ≠ 0 := ne_of_gt h₁,
+  have d₂0 : d₂ ≠ 0 := ne_of_gt h₂,
+  have d₁a : (d₁:α) ≠ 0 := nat.cast_ne_zero.2 d₁0,
+  have d₂a : (d₂:α) ≠ 0 := nat.cast_ne_zero.2 d₂0,
+  rw [num_denom', num_denom'] at h ⊢,
+  rw [cast_mk_of_ne_zero, cast_mk_of_ne_zero] at h; simp [d₁0, d₂0] at h ⊢,
+  rwa [eq_div_iff_mul_eq _ _ d₂a, division_def, mul_assoc,
+    inv_comm_of_comm d₁a (nat.mul_cast_comm _ _),
+    ← mul_assoc, ← division_def, eq_comm, eq_div_iff_mul_eq _ _ d₁a, eq_comm,
+    ← int.cast_coe_nat, ← int.cast_mul, ← int.cast_coe_nat, ← int.cast_mul,
+    int.cast_inj, ← mk_eq (int.coe_nat_ne_zero.2 d₁0) (int.coe_nat_ne_zero.2 d₂0)] at h
 end
 
-theorem cast_mk [discrete_linear_ordered_field α] (a b : ℤ) : ((a /. b) : α) = a / b :=
+@[simp] theorem cast_eq_zero [char_zero α] {n : ℚ} : (n : α) = 0 ↔ n = 0 :=
+by rw [← cast_zero, cast_inj]
+
+@[simp] theorem cast_ne_zero [char_zero α] {n : ℚ} : (n : α) ≠ 0 ↔ n ≠ 0 :=
+not_congr cast_eq_zero
+
+end
+
+theorem cast_mk [discrete_field α] [char_zero α] (a b : ℤ) : ((a /. b) : α) = a / b :=
 if b0 : b = 0 then by simp [b0, div_zero]
 else cast_mk_of_ne_zero a b (int.cast_ne_zero.2 b0)
 
-@[simp] theorem cast_add [linear_ordered_field α] (m n) : ((m + n : ℚ) : α) = m + n :=
+@[simp] theorem cast_add [division_ring α] [char_zero α] (m n) : ((m + n : ℚ) : α) = m + n :=
 cast_add_of_ne_zero (nat.cast_ne_zero.2 $ ne_of_gt m.pos) (nat.cast_ne_zero.2 $ ne_of_gt n.pos)
 
-@[simp] theorem cast_sub [linear_ordered_field α] (m n) : ((m - n : ℚ) : α) = m - n :=
+@[simp] theorem cast_sub [division_ring α] [char_zero α] (m n) : ((m - n : ℚ) : α) = m - n :=
 cast_sub_of_ne_zero (nat.cast_ne_zero.2 $ ne_of_gt m.pos) (nat.cast_ne_zero.2 $ ne_of_gt n.pos)
 
-@[simp] theorem cast_mul [linear_ordered_field α] (m n) : ((m * n : ℚ) : α) = m * n :=
+@[simp] theorem cast_mul [division_ring α] [char_zero α] (m n) : ((m * n : ℚ) : α) = m * n :=
 cast_mul_of_ne_zero (nat.cast_ne_zero.2 $ ne_of_gt m.pos) (nat.cast_ne_zero.2 $ ne_of_gt n.pos)
 
-@[simp] theorem cast_inv [discrete_linear_ordered_field α] (n) : ((n⁻¹ : ℚ) : α) = n⁻¹ :=
+@[simp] theorem cast_inv [discrete_field α] [char_zero α] (n) : ((n⁻¹ : ℚ) : α) = n⁻¹ :=
 if n0 : n.num = 0 then
   by simp [show n = 0, by rw [num_denom n, n0]; simp, inv_zero] else
 cast_inv_of_ne_zero (int.cast_ne_zero.2 n0) (nat.cast_ne_zero.2 $ ne_of_gt n.pos)
 
-@[simp] theorem cast_div [discrete_linear_ordered_field α] (m n) : ((m / n : ℚ) : α) = m / n :=
+@[simp] theorem cast_div [discrete_field α] [char_zero α] (m n) : ((m / n : ℚ) : α) = m / n :=
 by rw [division_def, cast_mul, cast_inv, division_def]
 
-@[simp] theorem cast_bit0 [linear_ordered_field α] (n : ℚ) : ((bit0 n : ℚ) : α) = bit0 n := cast_add _ _
+@[simp] theorem cast_bit0 [division_ring α] [char_zero α] (n : ℚ) : ((bit0 n : ℚ) : α) = bit0 n := cast_add _ _
 
-@[simp] theorem cast_bit1 [linear_ordered_field α] (n : ℚ) : ((bit1 n : ℚ) : α) = bit1 n :=
+@[simp] theorem cast_bit1 [division_ring α] [char_zero α] (n : ℚ) : ((bit1 n : ℚ) : α) = bit1 n :=
 by rw [bit1, cast_add, cast_one, cast_bit0]; refl
 
 @[simp] theorem cast_nonneg [linear_ordered_field α] : ∀ {n : ℚ}, 0 ≤ (n : α) ↔ 0 ≤ n
@@ -763,9 +785,6 @@ by rw [← sub_nonneg, ← cast_sub, cast_nonneg, sub_nonneg]
 @[simp] theorem cast_lt [linear_ordered_field α] {m n : ℚ} : (m : α) < n ↔ m < n :=
 by simpa [-cast_le] using not_congr (@cast_le α _ n m)
 
-@[simp] theorem cast_inj [linear_ordered_field α] {m n : ℚ} : (m : α) = n ↔ m = n :=
-by simp [le_antisymm_iff]
-
 @[simp] theorem cast_nonpos [linear_ordered_field α] {n : ℚ} : (n : α) ≤ 0 ↔ n ≤ 0 :=
 by rw [← cast_zero, cast_le]
 
@@ -775,12 +794,6 @@ by rw [← cast_zero, cast_lt]
 @[simp] theorem cast_lt_zero [linear_ordered_field α] {n : ℚ} : (n : α) < 0 ↔ n < 0 :=
 by rw [← cast_zero, cast_lt]
 
-@[simp] theorem cast_eq_zero [linear_ordered_field α] {n : ℚ} : (n : α) = 0 ↔ n = 0 :=
-by rw [← cast_zero, cast_inj]
-
-@[simp] theorem cast_ne_zero [linear_ordered_field α] {n : ℚ} : (n : α) ≠ 0 ↔ n ≠ 0 :=
-not_congr cast_eq_zero
-
 @[simp] theorem cast_id : ∀ n : ℚ, ↑n = n
 | ⟨n, d, h, c⟩ := show (n / (d : ℤ) : ℚ) = _, by rw [num_denom', mk_eq_div]