8
$\begingroup$

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?

$\endgroup$
8
  • $\begingroup$ 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. $\endgroup$ Mar 14, 2022 at 16:30
  • $\begingroup$ 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. $\endgroup$
    – burek
    Mar 14, 2022 at 16:39
  • $\begingroup$ 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. $\endgroup$ Mar 14, 2022 at 17:00
  • $\begingroup$ 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. $\endgroup$ Mar 14, 2022 at 17:44
  • $\begingroup$ P.S. By + I mean the sum type. I am not sure what symbol Lean uses. $\endgroup$ Mar 14, 2022 at 17:46

2 Answers 2

9
$\begingroup$
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
$\endgroup$
3
  • $\begingroup$ Excellent, exactly what I needed, thank you. $\endgroup$
    – burek
    Mar 15, 2022 at 10:35
  • 1
    $\begingroup$ You don't need the @ on that last line, exact nat.lt_wf.fix Qstep (f a) a rfl works too. $\endgroup$
    – Eric
    Mar 17, 2022 at 12:02
  • $\begingroup$ Thanks for the tip! $\endgroup$ Mar 17, 2022 at 12:39
10
$\begingroup$

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.

$\endgroup$
3
  • $\begingroup$ 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) $\endgroup$ Mar 27, 2022 at 22:19
  • $\begingroup$ Indeed; though I was trying to be less cryptic than Andrej's answer, not more! $\endgroup$
    – Eric
    Mar 27, 2022 at 22:48
  • $\begingroup$ I do wonder if induction h : _ should handle the subst and rfl automatically, but haven't thought about it very hard. $\endgroup$
    – Eric
    Mar 27, 2022 at 22:49

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.