Proof by infinite descent

Stream: new members

[Stuart Presnell]

Do we already have this (or a suitable generalisation of it) somewhere? I can't find it under the name "infinite descent" anywhere, but maybe it's called something else?

example {S : set ℕ} {P : ℕ → Prop} (h : ∀ x ∈ S, (¬ P x → ∃ y ∈ S, y < x ∧ ¬ P y)) : ∀ x ∈ S, P x

[Patrick Johnson]

I don't think there is such theorem. But the proof is pretty straightforward:

example
  {S : set ℕ}
  {P : ℕ → Prop}
  (h : ∀ x ∈ S, (¬ P x → ∃ y ∈ S, y < x ∧ ¬ P y)) :
  ∀ x ∈ S, P x :=
begin
  intro x,
  induction x using nat.strong_induction_on with x h₁,
  intro h₂, by_contra h₃,
  obtain ⟨y, ⟨h₄, ⟨h₅, h₆⟩⟩⟩ := h _ h₂ h₃,
  exact h₆ (h₁ _ h₅ h₄),
end

[Stuart Presnell]

It seems like this would be a useful lemma to have since this proof method comes up fairly often in informal mathematics. Is it worth PRing it?

[Eric Wieser]

An even shorter proof:

import tactic
example
  {S : set ℕ}
  {P : ℕ → Prop}
  (h : ∀ x ∈ S, (¬ P x → ∃ y ∈ S, y < x ∧ ¬ P y)) :
  ∀ x ∈ S, P x :=
begin
  simp_rw [@not_imp_comm (P _), not_exists, not_and_not_right, @imp.swap (_ ∈ S)] at h,
  exact λ x, nat.strong_induction_on x h,
end

[Eric Wieser]

Which demonstrates that there are many equivalent ways that you could have stated h there (try putting the cursor before each comma in simp_rw):

• ∀ x ∈ S, (¬ P x → ∃ y ∈ S, y < x ∧ ¬ P y) (yours)
• ∀ x ∈ S, (∀ y ∈ S, y < x → P y) → P x (a variant with no ¬s)
• ∀ x, (∀ y, y < x → y ∈ S → P y) → x ∈ S → P x (the version with the ∈ S moved to the end, which makes the statement just strong induction with p x = (x ∈ S → P x))

[Eric Wieser]

So unless there's anything particularly special about the way you have it stated, I doubt it's worth giving that version a name