feat(data/nat/interval): Cauchy induction (#15880)

This PR shows that if a predicate on the natural numbers is downward closed, i.e. satisfying `∀ n, P (n + 1) → P n`, then in order for it to hold for all natural numbers, it suffices that it holds for a set of natural numbers satisfying the following three equivalent conditions: (1) unbounded (`¬ bdd_above`), (2) `infinite`, and (3) `nonempty` without a maximal element.

The last version (nonempty + no-max) is the essence of Cauchy induction (`cauchy_induction'`): nonemptiness is stated in this PR as a "seed" such that `P seed` holds, and the no-max condition is stated as `∀ x, seed ≤ x → P x → ∃ y, x < y ∧ P y`.

When we have `P x → P (k * x)` for some `k > 1`, we may take `y := k * x`, which satisfies `x < y` when `x > 0`, so we just need to take `seed ≥ 1`; this is the classical, more restricted version of Cauchy induction (`cauchy_induction_mul`).



Co-authored-by: Shimonschlessinger <Shimonschlessinger@users.noreply.github.com>
Co-authored-by: Junyan Xu <junyanxumath@gmail.com>

src/data/nat/interval.lean

@@ -256,3 +256,42 @@ begin
 end
 
 end finset
+
+section induction
+
+variables {P : ℕ → Prop} (h : ∀ n, P (n + 1) → P n)
+
+include h
+
+lemma nat.decreasing_induction_of_not_bdd_above (hP : ¬ bdd_above {x | P x}) (n : ℕ) : P n :=
+let ⟨m, hm, hl⟩ := not_bdd_above_iff.1 hP n in decreasing_induction h hl.le hm
+
+lemma nat.decreasing_induction_of_infinite (hP : {x | P x}.infinite) (n : ℕ) : P n :=
+nat.decreasing_induction_of_not_bdd_above h (mt bdd_above.finite hP) n
+
+lemma nat.cauchy_induction' (seed : ℕ) (hs : P seed)
+  (hi : ∀ x, seed ≤ x → P x → ∃ y, x < y ∧ P y) (n : ℕ) : P n :=
+begin
+  apply nat.decreasing_induction_of_infinite h (λ hf, _),
+  obtain ⟨m, hP, hm⟩ := hf.exists_maximal_wrt id _ ⟨seed, hs⟩,
+  obtain ⟨y, hl, hy⟩ := hi m (le_of_not_lt $ λ hl, hl.ne $ hm seed hs hl.le) hP,
+  exact hl.ne (hm y hy hl.le),
+end
+
+lemma nat.cauchy_induction (seed : ℕ) (hs : P seed) (f : ℕ → ℕ)
+  (hf : ∀ x, seed ≤ x → P x → x < f x ∧ P (f x)) (n : ℕ) : P n :=
+seed.cauchy_induction' h hs (λ x hl hx, ⟨f x, hf x hl hx⟩) n
+
+lemma nat.cauchy_induction_mul (k seed : ℕ) (hk : 1 < k) (hs : P seed.succ)
+  (hm : ∀ x, seed < x → P x → P (k * x)) (n : ℕ) : P n :=
+begin
+  apply nat.cauchy_induction h _ hs ((*) k) (λ x hl hP, ⟨_, hm x hl hP⟩),
+  convert (mul_lt_mul_right $ seed.succ_pos.trans_le hl).2 hk,
+  rw one_mul,
+end
+
+lemma nat.cauchy_induction_two_mul (seed : ℕ) (hs : P seed.succ)
+  (hm : ∀ x, seed < x → P x → P (2 * x)) (n : ℕ) : P n :=
+nat.cauchy_induction_mul h 2 seed one_lt_two hs hm n
+
+end induction

src/data/set/finite.lean

@@ -1121,12 +1121,7 @@ finite.induction_on H
   (by simp only [bUnion_empty, bdd_above_empty, ball_empty_iff])
   (λ a s ha _ hs, by simp only [bUnion_insert, ball_insert_iff, bdd_above_union, hs])
 
-lemma infinite_of_not_bdd_above : ¬ bdd_above s → s.infinite :=
-begin
-  contrapose!,
-  rw not_infinite,
-  apply finite.bdd_above,
-end
+lemma infinite_of_not_bdd_above : ¬ bdd_above s → s.infinite := mt finite.bdd_above
 
 end