# Strong induction on ℕ with function α → ℕ

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?

• Your ind term looks a bit odd to me. I would have expected the "exists" term to be something like (∀ b, f b < f a -> P b). Your term says that there exists some b such that P b. Commented Mar 14, 2022 at 16:30
• Aha sorry, I actually wrote it incorrectly, the ind term should actually be something like (ind : ∀ a : α, f a > 0 → ∃ b : α, f b < f a). But I don't apriori know that P b. I fixed it in the question. Perhaps ind is not the best name for this term. Commented Mar 14, 2022 at 16:39
• Well, that hypothesis doesn't give you an inductive step: you still need something that says how to get P a out of P b when f b < f a. Commented Mar 14, 2022 at 17:00
• Add (∀ a : α, f a = 0 + f a > 0) in your definition of foo. Then pattern match on case. You should provide some term of type ∀ n : ℕ, n = 0 + n > 0. Commented Mar 14, 2022 at 17:44
• P.S. By + I mean the sum type. I am not sure what symbol Lean uses. Commented Mar 14, 2022 at 17:46

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

• Excellent, exactly what I needed, thank you. Commented Mar 15, 2022 at 10:35
• You don't need the @ on that last line, exact nat.lt_wf.fix Qstep (f a) a rfl works too.
– Eric
Commented Mar 17, 2022 at 12:02
• Thanks for the tip! Commented Mar 17, 2022 at 12:39

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.

• If terseness is wanted, everything after the induction line can be replaced by subst hn, exact ind _ (λ b fb_lt_fa, ih _ fb_lt_fa _ rfl) Commented Mar 27, 2022 at 22:19
• Indeed; though I was trying to be less cryptic than Andrej's answer, not more!
– Eric
Commented Mar 27, 2022 at 22:48
• I do wonder if induction h : _ should handle the subst and rfl automatically, but haven't thought about it very hard.
– Eric
Commented Mar 27, 2022 at 22:49