Regressive induction

Stream: Is there code for X?

[Patrick Johnson]

Do we have this induction principle? If no, should I open a PR? I personally find this lemma very useful in many cases.

import data.set

lemma nat.regressive_induction_on {P : ℕ → Prop} (n : ℕ)
  (h₁ : set.infinite P)
  (h₂ : ∀ (k : ℕ), P k.succ → P k) :
  P n :=
begin
  obtain ⟨k, h₃, h₄⟩ : ∃ (k : ℕ), n ≤ k ∧ P k,
  { contrapose! h₁, simp_rw imp_not_comm at h₁, push_neg at h₁,
    rw set.not_infinite, exact (set.finite_lt_nat _).subset h₁ },
  obtain ⟨k, rfl⟩ := le_iff_exists_add.mp h₃, clear h₃,
  induction k with k hk,
  { exact h₄ },
  { exact hk (h₂ _ h₄) },
end

[Kyle Miller]

@Patrick Johnson That seems useful, and I'd PR it. It's very nearly docs#nat.decreasing_induction, and you can connect it up to docs#set.infinite.exists_nat_lt to simplify the proof:

import data.set.finite

lemma nat.decreasing_induction_on_of_infinite {P : ℕ → Prop} (n : ℕ)
  (hinf : set.infinite {n | P n})
  (h : ∀ (n : ℕ), P (n + 1) → P n) :
  P n :=
begin
  obtain ⟨k, hnk, hpk⟩ := set.infinite.exists_nat_lt hinf n,
  exact nat.decreasing_induction h hpk.le hnk,
end

(I changed some variable names here and there to make it look like docs#nat.decreasing_induction)

[Kyle Miller]

API note: docs#set.infinite expects a set, not a predicate. I know that they're definitionally the same, but they're not syntactically the same, and when this is violated, you can run into some annoying expressions when proving things. That's why I changed the hypothesis to set.infinite {n | P n}.

[Patrick Johnson]

A technical question: how to properly import data.set.finite? It seems to mess up the entire data/nat/basic.lean file.

[Yaël Dillies]

Are you trying to import data.set.finite in data.nat.basic?

[Yaël Dillies]

data.nat.basic is too low in the hierarchy for that.

[Patrick Johnson]

Oh, I see. data.set.finite seems to depend on data.nat.basic

[Patrick Johnson]

What is the right way to go then?

[Patrick Johnson]

Move the induction principle to data.set.finite?

[Yaël Dillies]

Put it in data.set.finite

[Reid Barton]

I'm curious, is set.infinite really a convenient hypothesis to check for this form of induction? I mean it will generally be math-obvious but maybe not so easy to prove in Lean

[Yaël Dillies]

The best way to put it would be to use docs#filter.at_top, because that's what you're really using: that in a set of naturals going to infinity any natural is less than some element.

[Reid Barton]

Or just express the unboundedness directly forall n, exists m > n, P m.

[Patrick Johnson]

Or just express the unboundedness directly forall n, exists m > n, P m.

Well, the proof of the induction principle then becomes so trivial, that it probably doesn't deserve a lemma (it's basically just decreasing_induction). The book I am using defines the "regressive induction" as:

Let $P(n)$ be a proposition that depends on natural number $n$. if

• $P(n)$ is true for infinitely many natural numbers and
• for all natural numbers $n$, $P(n+1)\Longrightarrow P(n)$,

then $P(n)$ is true for all $n\in\mathbb N$. Then they used it to prove the inequality of arithmetic and geometric means.

If this induction principle is redundant, or too trivial for mathlib, I am perfectly ok with that.

[Yaël Dillies]

Yeah, it's borderline too trivial.