Golfing strong induction on sum

Stream: general

[Peter Nelson]

What is the most idiomatic way to do something like this?

import tactic

lemma foo (P : ℕ → ℕ → Prop) (IH : ∀ x y, (∀ a b, a + b < x + y → P a b) → P x y) :
∀ x y, P x y := sorry

[Mario Carneiro]

using_well_founded can do it

[Mario Carneiro]

lemma foo (P : ℕ → ℕ → Prop) (IH : ∀ x y, (∀ a b, a + b < x + y → P a b) → P x y) :
  ∀ x y, P x y
  | x y := IH x y (λ a b h, foo a b)
using_well_founded { rel_tac := λ _ _, `[exact ⟨_, measure_wf (λ a : Σ'_,_, a.1 + a.2)⟩] }

[Mario Carneiro]

(the syntax for doing this is significantly better in lean 4)

[Peter Nelson]

Thanks! I did bring this about myself with ‘golfing’, but is there a solution that might be easier for a beginner to digest? I’m working with one at the moment.

[Mario Carneiro]

lemma foo (P : ℕ → ℕ → Prop) (IH : ∀ x y, (∀ a b, a + b < x + y → P a b) → P x y)
  (x y) : P x y :=
begin
  refine @nat.strong_induction_on (λ n, ∀ x y, x + y = n → P x y) (x + y) _ x y rfl,
  rintro n H x y rfl,
  exact IH _ _ (λ a b h, H _ h _ _ rfl)
end

[Kevin Buzzard]

import tactic

lemma foo (P : ℕ → ℕ → Prop) (IH : ∀ x y, (∀ a b, a + b < x + y → P a b) → P x y) :
∀ x y, P x y :=
begin
  -- want to do induction on x + y, so let n be x + y
  suffices : ∀ (n : ℕ), ∀ x y, x + y = n → P x y,
  { -- obviously the same as the goal; let n be x + y
    intros x y, apply this (x + y), refl },
  -- let n be arbitrary
  intro n,
  -- use strong induction on n
  apply nat.strong_induction_on n, clear n,
  -- now assume we have n and x and y with x + y = n, and assume we
  -- know the result for all m < n
  rintros n hn x y rfl,
  -- apply given hypothesis
  apply IH,
  -- now say a + b < x + y
  intros a b hab,
  -- use the strong inductive hypothesis
  apply hn (a + b) hab,
  -- and now it's easy
  refl,
end

[Eric Wieser]

Or with the induction tactic:

lemma foo (P : ℕ → ℕ → Prop) (IH : ∀ x y, (∀ a b, a + b < x + y → P a b) → P x y)
  (x y) : P x y :=
begin
  induction h : x + y using nat.strong_induction_on with n hn generalizing x y,
  subst h,
  apply IH,
  intros a b hab,
  apply hn _ hab _ _ rfl,
end