Strong induction on ℕ with function α → ℕ

Question

I have the following problem. I have a type $\alpha$, function $f : \alpha \to \mathbb{N}$ and predicate $P : \alpha \to \mathrm{Prop}$ and I want to prove that for all $a : \alpha, P a$.

How could prove this with induction on the value $f a$, i.e. cases where $f a = 0$ and $f a > 0$?

My current trial in Lean looks like this:

lemma foo (α : Type) (f : α → ℕ) (P : α → Prop)
  (base : ∀ a : α, f a = 0 → P a)
  (ind : ∀ a : α, f a > 0 → ∃ b : α, f b < f a) :
  ∀ a : α, P a

In the inductive case, I want to get the hypothesis P b. I tried to use nat.strong_induction_on, but I can't figure out what to apply it on.

Am I doing something wrong?

Answer 1

theorem foo (α : Type) (f : α → ℕ) (P : α → Prop)
  (base : ∀ a, f a = 0 → P a)
  (ind : ∀ a, (∀ b, f b < f a → P b) → P a) :
  ∀ a, P a
:=
begin
  intro a,
  let Q := λ n, ∀ a, f a = n → P a,
  have Qstep : ∀ (n : ℕ), (∀ (m : ℕ), m < n → Q m) → Q n,
  { intros n h a ξ,
    apply (ind a),
    intros b fb_lt_fa,
    rewrite ξ at fb_lt_fa,
    apply (h (f b)) fb_lt_fa, refl 
  },
  exact @well_founded.fix _ Q nat.lt nat.lt_wf Qstep (f a) a rfl,
end

Answer 2

Here's how to prove Andrej Bauer's corrected statement using the induction tactic:

theorem foo (α : Type) (f : α → ℕ) (P : α → Prop)
  (ind : ∀ a, (∀ b, f b < f a → P b) → P a) :
  ∀ a, P a :=
begin
  intro a,
  induction hn : f a using nat.strong_induction_on with n ih generalizing a,
  apply ind,
  intros b fb_lt_fa,
  rw hn at fb_lt_fa,
  exact ih _ fb_lt_fa _ rfl,
end

We're using lots of its optional features at once here:

• hn : _ lets us remember that the variable we're inducting on is equal to f a
• using nat.strong_induction_on tells it to use a non-default recursion scheme
• generalizing a ensure that a is in a binder in our inductive hypothesis ih

Note that we don't need base.