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?
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 thatP b
. $\endgroup$ind
term should actually be something like(ind : ∀ a : α, f a > 0 → ∃ b : α, f b < f a)
. But I don't apriori know thatP b
. I fixed it in the question. Perhapsind
is not the best name for this term. $\endgroup$P a
out ofP b
whenf b < f a
. $\endgroup$(∀ a : α, f a = 0 + f a > 0)
in your definition offoo
. Then pattern match oncase
. You should provide some term of type∀ n : ℕ, n = 0 + n > 0
. $\endgroup$+
I mean the sum type. I am not sure what symbol Lean uses. $\endgroup$