feat(order/monotone): add monotone_int_of_le_succ etc (#10895)

Also use new lemmas to golf `zpow_strict_mono` and prove `zpow_strict_anti`.

src/algebra/field_power.lean

@@ -195,15 +195,16 @@ ne_of_gt (nat.zpow_pos_of_pos h n)
 
 lemma zpow_strict_mono {x : K} (hx : 1 < x) :
   strict_mono (λ n:ℤ, x ^ n) :=
-λ m n h, show x ^ m < x ^ n,
-begin
-  have xpos : 0 < x := zero_lt_one.trans hx,
-  have h₀ : x ≠ 0 := xpos.ne',
-  have hxm : 0 < x^m := zpow_pos_of_pos xpos m,
-  have h : 1 < x ^ (n - m) := one_lt_zpow hx _ (sub_pos_of_lt h),
-  replace h := mul_lt_mul_of_pos_right h hxm,
-  rwa [sub_eq_add_neg, zpow_add₀ h₀, mul_assoc, zpow_neg_mul_zpow_self _ h₀, one_mul, mul_one] at h,
-end
+strict_mono_int_of_lt_succ $ λ n,
+have xpos : 0 < x, from zero_lt_one.trans hx,
+calc x ^ n < x ^ n * x : lt_mul_of_one_lt_right (zpow_pos_of_pos xpos _) hx
+... = x ^ (n + 1) : (zpow_add_one₀ xpos.ne' _).symm
+
+lemma zpow_strict_anti {x : K} (h₀ : 0 < x) (h₁ : x < 1) : strict_anti (λ n : ℤ, x ^ n) :=
+strict_anti_int_of_succ_lt $ λ n,
+calc x ^ (n + 1) = x ^ n * x : zpow_add_one₀ h₀.ne' _
+... < x ^ n * 1 : (mul_lt_mul_left $ zpow_pos_of_pos h₀ _).2 h₁
+... = x ^ n : mul_one _
 
 @[simp] lemma zpow_lt_iff_lt {x : K} (hx : 1 < x) {m n : ℤ} :
   x ^ m < x ^ n ↔ m < n :=

src/data/complex/exponential.lean

@@ -49,7 +49,7 @@ begin
   rw [not_imp, not_lt] at hi,
   existsi i,
   assume j hj,
-  have hfij : f j ≤ f i := forall_ge_le_of_forall_le_succ f hnm hi.1 hj,
+  have hfij : f j ≤ f i := (nat.rel_of_forall_rel_succ_of_le_of_le (≥) hnm hi.1 hj).le,
   rw [abs_of_nonpos (sub_nonpos.2 hfij), neg_sub, sub_lt_iff_lt_add'],
   calc f i ≤ a - (nat.pred l) • ε : hi.2
     ... = a - l • ε + ε :

src/order/monotone.lean

@@ -5,6 +5,7 @@ Authors: Jeremy Avigad, Mario Carneiro, Yaël Dillies
 -/
 import order.compare
 import order.order_dual
+import order.rel_classes
 
 /-!
 # Monotonicity
@@ -28,14 +29,14 @@ to mean "decreasing".
 
 ## Main theorems
 
-* `monotone_nat_of_le_succ`: If `f : ℕ → α` and `f n ≤ f (n + 1)` for all `n`, then `f` is
-  monotone.
-* `antitone_nat_of_succ_le`: If `f : ℕ → α` and `f (n + 1) ≤ f n` for all `n`, then `f` is
-  antitone.
-* `strict_mono_nat_of_lt_succ`: If `f : ℕ → α` and `f n < f (n + 1)` for all `n`, then `f` is
-  strictly monotone.
-* `strict_anti_nat_of_succ_lt`: If `f : ℕ → α` and `f (n + 1) < f n` for all `n`, then `f` is
-  strictly antitone.
+* `monotone_nat_of_le_succ`, `monotone_int_of_le_succ`: If `f : ℕ → α` or `f : ℤ → α` and
+  `f n ≤ f (n + 1)` for all `n`, then `f` is monotone.
+* `antitone_nat_of_succ_le`, `antitone_int_of_succ_le`: If `f : ℕ → α` or `f : ℤ → α` and
+  `f (n + 1) ≤ f n` for all `n`, then `f` is antitone.
+* `strict_mono_nat_of_lt_succ`, `strict_mono_int_of_lt_succ`: If `f : ℕ → α` or `f : ℤ → α` and
+  `f n < f (n + 1)` for all `n`, then `f` is strictly monotone.
+* `strict_anti_nat_of_succ_lt`, `strict_anti_int_of_succ_lt`: If `f : ℕ → α` or `f : ℤ → α` and
+  `f (n + 1) < f n` for all `n`, then `f` is strictly antitone.
 
 ## Implementation notes
 
@@ -46,9 +47,8 @@ https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Order.20dia
 
 ## TODO
 
-The above theorems are also true in `ℤ`, `ℕ+`, `fin n`... To make that work, we need `succ_order α`
-along with another typeclass we don't yet have roughly stating "everything is reachable using
-finitely many `succ`".
+The above theorems are also true in `ℕ+`, `fin n`... To make that work, we need `succ_order α`
+and `succ_archimedean α`.
 
 ## Tags
 
@@ -539,39 +539,71 @@ end linear_order
 section preorder
 variables [preorder α]
 
-lemma monotone_nat_of_le_succ {f : ℕ → α} (hf : ∀ n, f n ≤ f (n + 1)) :
-  monotone f | n m h :=
+lemma nat.rel_of_forall_rel_succ_of_le_of_lt (r : β → β → Prop) [is_trans β r]
+  {f : ℕ → β} {a : ℕ} (h : ∀ n, a ≤ n → r (f n) (f (n + 1))) ⦃b c : ℕ⦄
+  (hab : a ≤ b) (hbc : b < c) :
+  r (f b) (f c) :=
 begin
-  induction h,
-  { refl },
-  { transitivity, assumption, exact hf _ }
+  induction hbc with k b_lt_k r_b_k,
+  exacts [h _ hab, trans r_b_k (h _ (hab.trans_lt b_lt_k).le)]
 end
 
+lemma nat.rel_of_forall_rel_succ_of_le_of_le (r : β → β → Prop) [is_refl β r] [is_trans β r]
+  {f : ℕ → β} {a : ℕ} (h : ∀ n, a ≤ n → r (f n) (f (n + 1))) ⦃b c : ℕ⦄
+  (hab : a ≤ b) (hbc : b ≤ c) :
+  r (f b) (f c) :=
+hbc.eq_or_lt.elim (λ h, h ▸ refl _) (nat.rel_of_forall_rel_succ_of_le_of_lt r h hab)
+
+lemma nat.rel_of_forall_rel_succ_of_lt (r : β → β → Prop) [is_trans β r]
+  {f : ℕ → β} (h : ∀ n, r (f n) (f (n + 1))) ⦃a b : ℕ⦄ (hab : a < b) : r (f a) (f b) :=
+nat.rel_of_forall_rel_succ_of_le_of_lt r (λ n _, h n) le_rfl hab
+
+lemma nat.rel_of_forall_rel_succ_of_le (r : β → β → Prop) [is_refl β r] [is_trans β r]
+  {f : ℕ → β} (h : ∀ n, r (f n) (f (n + 1))) ⦃a b : ℕ⦄ (hab : a ≤ b) : r (f a) (f b) :=
+nat.rel_of_forall_rel_succ_of_le_of_le r (λ n _, h n) le_rfl hab
+
+lemma monotone_nat_of_le_succ {f : ℕ → α} (hf : ∀ n, f n ≤ f (n + 1)) :
+  monotone f :=
+nat.rel_of_forall_rel_succ_of_le (≤) hf
+
 lemma antitone_nat_of_succ_le {f : ℕ → α} (hf : ∀ n, f (n + 1) ≤ f n) :
-  antitone f | n m h :=
-begin
-  induction h,
-  { refl },
-  { transitivity, exact hf _, assumption }
-end
+  antitone f :=
+@monotone_nat_of_le_succ (order_dual α) _ _ hf
 
-lemma strict_mono_nat_of_lt_succ [preorder β] {f : ℕ → β} (hf : ∀ n, f n < f (n + 1)) :
+lemma strict_mono_nat_of_lt_succ {f : ℕ → α} (hf : ∀ n, f n < f (n + 1)) :
   strict_mono f :=
-by { intros n m hnm, induction hnm with m' hnm' ih, apply hf, exact ih.trans (hf _) }
+nat.rel_of_forall_rel_succ_of_lt (<) hf
 
-lemma strict_anti_nat_of_succ_lt [preorder β] {f : ℕ → β} (hf : ∀ n, f (n + 1) < f n) :
+lemma strict_anti_nat_of_succ_lt {f : ℕ → α} (hf : ∀ n, f (n + 1) < f n) :
   strict_anti f :=
-by { intros n m hnm, induction hnm with m' hnm' ih, apply hf, exact (hf _).trans ih }
+@strict_mono_nat_of_lt_succ (order_dual α) _ f hf
 
-lemma forall_ge_le_of_forall_le_succ (f : ℕ → α) {a : ℕ} (h : ∀ n, a ≤ n → f n.succ ≤ f n) {b c : ℕ}
-  (hab : a ≤ b) (hbc : b ≤ c) :
-  f c ≤ f b :=
+lemma int.rel_of_forall_rel_succ_of_lt (r : β → β → Prop) [is_trans β r]
+  {f : ℤ → β} (h : ∀ n, r (f n) (f (n + 1))) ⦃a b : ℤ⦄ (hab : a < b) : r (f a) (f b) :=
 begin
-  induction hbc with k hbk hkb,
-  { exact le_rfl },
-  { exact (h _ $ hab.trans hbk).trans hkb }
+  rcases hab.dest with ⟨n, rfl⟩, clear hab,
+  induction n with n ihn,
+  { rw int.coe_nat_one, apply h },
+  { rw [int.coe_nat_succ, ← int.add_assoc],
+    exact trans ihn (h _) }
 end
 
+lemma int.rel_of_forall_rel_succ_of_le (r : β → β → Prop) [is_refl β r] [is_trans β r]
+  {f : ℤ → β} (h : ∀ n, r (f n) (f (n + 1))) ⦃a b : ℤ⦄ (hab : a ≤ b) : r (f a) (f b) :=
+hab.eq_or_lt.elim (λ h, h ▸ refl _) (λ h', int.rel_of_forall_rel_succ_of_lt r h h')
+
+lemma monotone_int_of_le_succ {f : ℤ → α} (hf : ∀ n, f n ≤ f (n + 1)) : monotone f :=
+int.rel_of_forall_rel_succ_of_le (≤) hf
+
+lemma antitone_int_of_succ_le {f : ℤ → α} (hf : ∀ n, f (n + 1) ≤ f n) : antitone f :=
+int.rel_of_forall_rel_succ_of_le (≥) hf
+
+lemma strict_mono_int_of_lt_succ {f : ℤ → α} (hf : ∀ n, f n < f (n + 1)) : strict_mono f :=
+int.rel_of_forall_rel_succ_of_lt (<) hf
+
+lemma strict_anti_int_of_succ_lt {f : ℤ → α} (hf : ∀ n, f (n + 1) < f n) : strict_anti f :=
+int.rel_of_forall_rel_succ_of_lt (>) hf
+
 -- TODO@Yael: Generalize the following four to succ orders
 /-- If `f` is a monotone function from `ℕ` to a preorder such that `x` lies between `f n` and
   `f (n + 1)`, then `x` doesn't lie in the range of `f`. -/

src/order/order_iso_nat.lean

@@ -28,12 +28,7 @@ variables {α : Type*} {r : α → α → Prop} [is_strict_order α r]
 /-- If `f` is a strictly `r`-increasing sequence, then this returns `f` as an order embedding. -/
 def nat_lt (f : ℕ → α) (H : ∀ n : ℕ, r (f n) (f (n + 1))) :
   ((<) : ℕ → ℕ → Prop) ↪r r :=
-of_monotone f $ λ a b h, begin
-  induction b with b IH, {exact (nat.not_lt_zero _ h).elim},
-  cases nat.lt_succ_iff_lt_or_eq.1 h with h e,
-  { exact trans (IH h) (H _) },
-  { subst b, apply H }
-end
+of_monotone f $ nat.rel_of_forall_rel_succ_of_lt r H
 
 @[simp]
 lemma nat_lt_apply {f : ℕ → α} {H : ∀ n : ℕ, r (f n) (f (n + 1))} {n : ℕ} :