Inducting directly on recursive calls

Stream: new members

[Ryan Greenblatt]

I'd like to be able to induct directly on the recursion of a function instead of on the inputs to that function.
I want to prove a property of a function and have the inductive hypothesis that all of the recursive calls satisfy the property for their inputs.

Something like this silly example (which can obviously be done in another way):

def fib : ℕ → ℕ
| 0 := 0
| 1 := 1
| 2 := 1
| (nat.succ (nat.succ n)) := fib n.succ + fib n

lemma property_of_function (k : ℕ) : fib k > 0 ↔ k > 0 :=
begin
  -- base cases etc...

  -- I want to be able to get this inductive hypothesis in the case where k > 2 and we recur
  have ih : fib k.pred > 0 ↔ k.pred > 0 ∧ fib k.pred.pred > 0 ↔ k.pred.pred > 0 := sorry,
end

[Kyle Miller]

Are you asking about how to do strong induction?

induction k using nat.strong_induction_on with k ih

This gives you the hypotheses ∀ (m : ℕ), m < k → (fib m > 0 ↔ m > 0)

[Kyle Miller]

(I guess it's just an example, but if you simplify the definition of fib to not include the the 2 case, then you'll have fewer things to prove in the induction.)

[Ryan Greenblatt]

Strong induction should work in the case I have in mind, but it would be nice if you could just induct on recursion itself.
This would make things easier when the well_foundedness measure is a pain to work with I think.
Fair enough if this isn't possible in general.

[Ryan Greenblatt]

I've been using mathlib's induction' which generalizes everything by default.
Do you know the syntax for generalizing a given variable with the standard induction or how to do strong induction with mathlib (google/docs don't seem to very helpful here...)

[Ryan Greenblatt]

Ah, looks like mathlib induction' doesn't support using

[Kyle Miller]

@Ryan Greenblatt One way to induct on the recursion itself is to have an inductive type that implements the function. I'm not sure how to really set this up properly, but here's an attempt:

import tactic

def fib : ℕ → ℕ
| 0 := 0
| 1 := 1
| (nat.succ (nat.succ n)) := fib n.succ + fib n

inductive fib_fun : ℕ → ℕ → Prop
| case0 : fib_fun 0 0
| case1 : fib_fun 1 1
| recur (n a b : ℕ) (fsn : fib_fun n.succ a) (fn : fib_fun n b) : fib_fun n.succ.succ (a + b)

/-- not used here -/
lemma fib_fun_is_fib (n m : ℕ) (f : fib_fun n m) : fib n = m :=
begin
  induction f,
  refl,
  refl,
  simp [fib, *],
end

lemma fib_is_fib_fun (n : ℕ) : fib_fun n (fib n) :=
begin
  induction n using nat.strong_induction_on with n ih,
  cases n,
  apply fib_fun.case0,
  cases n,
  apply fib_fun.case1,
  apply fib_fun.recur,
  apply ih, apply nat.less_than_or_equal.refl,
  apply ih, apply nat.less_than_or_equal.step, apply nat.less_than_or_equal.refl,
end

lemma property_of_function (k : ℕ) : fib k > 0 ↔ k > 0 :=
begin
  have h := fib_is_fib_fun k,
  induction h, -- induct on the recursion
  simp,
  simp,
  simp [nat.succ_eq_add_one] at *,
  omega,
end

[Kyle Miller]

Ryan Greenblatt said:

I've been using mathlib's induction' which generalizes everything by default.
Do you know the syntax for generalizing a given variable with the standard induction or how to do strong induction with mathlib (google/docs don't seem to very helpful here...)

Does induction ... generalizing ... do what you want? tactic#induction

[Ryan Greenblatt]

Huh, cool. Thanks for all the help!

[Ryan Greenblatt]

Will probably just use strong induction.