function-specific induction rules

Stream: general

[Jakub Kądziołka]

I have defined a function as follows:

def as_fib_sum_aux : ℕ → ℕ → finset ℕ
| n 0 := ∅
| n 1 := ∅
| n (i + 2) := if fib (i + 2) ≤ n then
    insert (i + 2) (as_fib_sum_aux (n - fib (i + 2)) i)
  else
    as_fib_sum_aux n (i + 1)

I clumsily proved the following theorem:

lemma as_fib_sum_aux.bounded : ∀ n i, ∀ x ∈ as_fib_sum_aux n i, x ≤ i
| n 0 := by clear as_fib_sum_aux.bounded; tauto
| n 1 := by clear as_fib_sum_aux.bounded; tauto
| n (i + 2) := begin
  by_cases h : fib (i + 2) ≤ n,
  { unfold as_fib_sum_aux,
    rw [if_pos h],
    assume (x : ℕ) (Hx : x ∈ insert (i + 2) (as_fib_sum_aux _ i)),
    rw finset.mem_insert at Hx, cases Hx,
    { rw Hx },
    { calc x ≤ i     : as_fib_sum_aux.bounded (n - fib (i + 2)) i x Hx
      ...    ≤ i + 2 : by norm_num } },
  { unfold as_fib_sum_aux,
    rw [if_neg h],
    assume (x : ℕ) (Hx : x ∈ as_fib_sum_aux n i.succ),
    calc x ≤ i + 1 : as_fib_sum_aux.bounded n (i + 1) x Hx
    ...    ≤ i + 2 : by norm_num }
end

As you can see, the proof structure closely mirrors the recursive structure of the definition. In other theorem provers, there is a feature that generates induction principles for each recursive function, to help with this kind of proof. However, I couldn't find the corresponding Lean syntax in the docs...

(fwiw, the structure of the if is also mirrored and requires more manual finagling than I would like, but I'm not sure the induction principle would take care of that. golfs appreciated ;)

[Adam Topaz]

What do you mean by "generate an induction principle for a recursive function"? Lean does generate an induction principle for any inductive type (like nat in this case). You can use the induction tactic (or (r)cases, depending on what you want to do)

[Jakub Kądziołka]

In this case I would like

P 0 -> P 1 -> (\all n i, P (n - fib (i + 2)) i -> P n (i + 1) -> P n (i + 2)) -> \all n, P n

[Jakub Kądziołka]

in Isabelle I'd say apply (induction rule: as_fib_sum_aux.induct) IIRC

[Kevin Buzzard]

Is it as_fib_sum_aux.rec or one of the other variants you can see with #print prefix as_fib_sum_aux?

[Jakub Kądziołka]

#check as_fib_sum_aux.rec gives invalid field notation, type is not of the form (C ...) where C is a constant. #print prefix as_fib_sum_aux gives no declaration starting with prefix 'as_fib_sum_aux'

[Jakub Kądziołka]

Ah, looks like that's because I'm in a namespace

[Jakub Kądziołka]

rec still doesn't work though

[Kevin Buzzard]

Oh of course, sorry, I'm talking nonsense. You are making a plain definition, not an inductive one.

[Jannis Limperg]

Lean currently doesn't have a mechanism to derive induction principles for functions. (Coq does, so there's nothing stopping us in principle, but nobody has invested the time yet.) So you either have to prove the induction principle yourself or use the same match structure in your proof.