feat(data/int/basic): lemmas about int and int.to_nat (#6253)

Golfing welcome.

This adds a `@[simp]` lemma `int.add_minus_one : i + -1 = i - 1`, which I think is mostly helpful, but needs to be turned off in `data/num/lemmas.lean`, which is perhaps an argument against it.

I've also added a lemma
```
@[simp] lemma lt_self_iff_false [preorder α] (a : α) : a < a ↔ false :=
```
(not just for `int`), which I've often found useful (e.g. `simpa` works well when it can reduce a hypothesis to `false`). This lemma seems harmless, but I'm happy to hear objections if it is too general.

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Co-authored-by: Johan Commelin <johan@commelin.net>

Author: kim-em

src/algebra/group_power/lemmas.lean

@@ -717,7 +717,7 @@ by induction b; simp [*, mul_add, pow_succ, add_comm]
 @[simp] lemma int.to_add_gpow (a : multiplicative ℤ) (b : ℤ) : to_add (a ^ b) = to_add a * b :=
 int.induction_on b (by simp)
   (by simp [gpow_add, mul_add] {contextual := tt})
-  (by simp [gpow_add, mul_add, sub_eq_add_neg] {contextual := tt})
+  (by simp [gpow_add, mul_add, sub_eq_add_neg, -int.add_minus_one] {contextual := tt})
 
 @[simp] lemma int.of_add_mul (a b : ℤ) : of_add (a * b) = of_add a ^ b :=
 (int.to_add_gpow _ _).symm

src/data/int/basic.lean

@@ -60,6 +60,8 @@ instance : linear_ordered_comm_ring int :=
 instance : linear_ordered_add_comm_group int :=
 by apply_instance
 
+@[simp] lemma add_minus_one (i : ℤ) : i + -1 = i - 1 := rfl
+
 theorem abs_eq_nat_abs : ∀ a : ℤ, abs a = nat_abs a
 | (n : ℕ) := abs_of_nonneg $ coe_zero_le _
 | -[1+ n] := abs_of_nonpos $ le_of_lt $ neg_succ_lt_zero _
@@ -81,6 +83,13 @@ attribute [simp] int.of_nat_eq_coe int.bodd
 @[simp] theorem add_def {a b : ℤ} : int.add a b = a + b := rfl
 @[simp] theorem mul_def {a b : ℤ} : int.mul a b = a * b := rfl
 
+@[simp] lemma neg_succ_not_nonneg (n : ℕ) : 0 ≤ -[1+ n] ↔ false :=
+by { simp only [not_le, iff_false], exact int.neg_succ_lt_zero n, }
+
+@[simp] lemma neg_succ_not_pos (n : ℕ) : 0 < -[1+ n] ↔ false :=
+by simp only [not_lt, iff_false]
+
+@[simp] lemma neg_succ_sub_one (n : ℕ) : -[1+ n] - 1 = -[1+ (n+1)] := rfl
 @[simp] theorem coe_nat_mul_neg_succ (m n : ℕ) : (m : ℤ) * -[1+ n] = -(m * succ n) := rfl
 @[simp] theorem neg_succ_mul_coe_nat (m n : ℕ) : -[1+ m] * n = -(succ m * n) := rfl
 @[simp] theorem neg_succ_mul_neg_succ (m n : ℕ) : -[1+ m] * -[1+ n] = succ m * succ n := rfl
@@ -154,6 +163,12 @@ theorem add_one_le_iff {a b : ℤ} : a + 1 ≤ b ↔ a < b := iff.rfl
 theorem lt_add_one_iff {a b : ℤ} : a < b + 1 ↔ a ≤ b :=
 @add_le_add_iff_right _ _ a b 1
 
+@[simp] lemma succ_coe_nat_pos (n : ℕ) : 0 < (n : ℤ) + 1 :=
+lt_add_one_iff.mpr (by simp)
+
+@[norm_cast] lemma coe_pred_of_pos (n : ℕ) (h : 0 < n) : ((n - 1 : ℕ) : ℤ) = (n : ℤ) - 1 :=
+by { cases n, cases h, simp, }
+
 lemma le_add_one {a b : ℤ} (h : a ≤ b) : a ≤ b + 1 :=
 le_of_lt (int.lt_add_one_iff.mpr h)
 
@@ -1012,6 +1027,16 @@ end
 lemma to_nat_add_one {a : ℤ} (h : 0 ≤ a) : (a + 1).to_nat = a.to_nat + 1 :=
 to_nat_add h (zero_le_one)
 
+@[simp]
+lemma pred_to_nat : ∀ (i : ℤ), (i - 1).to_nat = i.to_nat - 1
+| (0:ℕ)   := rfl
+| (n+1:ℕ) := by simp
+| -[1+ n] := rfl
+
+@[simp]
+lemma to_nat_pred_coe_of_pos {i : ℤ} (h : 0 < i) : ((i.to_nat - 1 : ℕ) : ℤ) = i - 1 :=
+by simp [h, le_of_lt h] with push_cast
+
 /-- If `n : ℕ`, then `int.to_nat' n = some n`, if `n : ℤ` is negative, then `int.to_nat' n = none`.
 -/
 def to_nat' : ℤ → option ℕ

src/data/num/lemmas.lean

@@ -822,7 +822,7 @@ begin
   conv { to_lhs, rw ← zneg_zneg n },
   rw [← zneg_bit1, cast_zneg, cast_bit1],
   have : ((-1 + n + n : ℤ) : α) = (n + n + -1 : ℤ), {simp [add_comm, add_left_comm]},
-  simpa [_root_.bit1, _root_.bit0, sub_eq_add_neg]
+  simpa [_root_.bit1, _root_.bit0, sub_eq_add_neg, -int.add_minus_one]
 end
 
 theorem add_zero (n : znum) : n + 0 = n := by cases n; refl
@@ -843,6 +843,8 @@ theorem cast_to_znum : ∀ n : pos_num, (n : znum) = znum.pos n
 | (bit0 p) := (znum.bit0_of_bit0 p).trans $ congr_arg _ (cast_to_znum p)
 | (bit1 p) := (znum.bit1_of_bit1 p).trans $ congr_arg _ (cast_to_znum p)
 
+local attribute [-simp] int.add_minus_one
+
 theorem cast_sub' [add_group α] [has_one α] : ∀ m n : pos_num, (sub' m n : α) = m - n
 | a        1        := by rw [sub'_one, num.cast_to_znum,
                               ← num.cast_to_nat, pred'_to_nat, ← nat.sub_one];

src/data/rat/basic.lean

@@ -577,7 +577,7 @@ theorem coe_int_eq_mk : ∀ (z : ℤ), ↑z = z /. 1
   induction n with n IH, {refl},
   show -(n + 1 + 1 : ℚ) = -[1+ n.succ] /. 1,
   rw [neg_add, IH],
-  simpa [show -1 = (-1) /. 1, from rfl]
+  simp [show -1 = (-1) /. 1, from rfl],
 end
 
 theorem mk_eq_div (n d : ℤ) : n /. d = ((n : ℚ) / d) :=

src/data/string/basic.lean

@@ -36,7 +36,7 @@ instance decidable_lt : @decidable_rel string (<) := by apply_instance -- short-
     intros,
     induction s₁ with a s₁ IH generalizing p₁ p₂ s₂;
       cases s₂ with b s₂; rw ltb; simp [iterator.has_next],
-    { exact iff_of_false bool.ff_ne_tt (lt_irrefl _) },
+    { refl, },
     { exact iff_of_true rfl list.lex.nil },
     { exact iff_of_false bool.ff_ne_tt (not_lt_of_lt list.lex.nil) },
     { dsimp [iterator.has_next,

src/group_theory/free_group.lean

@@ -648,7 +648,7 @@ def free_group_unit_equiv_int : free_group unit ≃ ℤ :=
   right_inv :=
     λ x, int.induction_on x (by simp)
     (λ i ih, by simp at ih; simp [gpow_add, ih])
-    (λ i ih, by simp at ih; simp [gpow_add, ih, sub_eq_add_neg])
+    (λ i ih, by simp at ih; simp [gpow_add, ih, sub_eq_add_neg, -int.add_minus_one])
 }
 
 section category

src/order/basic.lean

@@ -56,6 +56,9 @@ preorder, order, partial order, linear order, monotone, strictly monotone
 universes u v w
 variables {α : Type u} {β : Type v} {γ : Type w} {r : α → α → Prop}
 
+@[simp] lemma lt_self_iff_false [preorder α] (a : α) : a < a ↔ false :=
+by simp [lt_irrefl a]
+
 theorem preorder.ext {α} {A B : preorder α}
   (H : ∀ x y : α, (by haveI := A; exact x ≤ y) ↔ x ≤ y) : A = B :=
 begin