proof about recursive function

Stream: new members

[Somo S.]

Hi, I am having some trouble reasoning about a recursive function I wrote. I am realizing that maybe my understanding about recursive function proofs is lacking in general. So I have put together a little example adapted from FPIL, with the hope that someone can show me how one goes about this kind of thing:

namespace mydiv

def div (n k : Nat) (ok : k > 0) : Nat :=
  if h : n < k then
    0
  else
    1 + div (n - k) k ok
decreasing_by sorry -- skip: already proved

theorem foo (n k : Nat) (ok : k > 0) : div n k ok ≤ n := sorry -- NEED HELP
end mydiv

[Somo S.]

I do see that Nat.div_le_self is a similar theorem that's already proved but I dont understand it. Dont understand using Nat.strongInductionOn, the ind n ih or the cases (inferInstance : Decidable (0 < k ∧ k ≤ n)) terms

[Somo S.]

so I'd rather focus on elementary technique for solving the above example (from scratch or "as scratch as is reasonable").. with the hope that I can generalize this to what I'm actually working on

[Ruben Van de Velde]

I came up with

theorem foo (n k : Nat) (ok : k > 0) : div n k ok ≤ n := by
  unfold div
  split_ifs with h
  · apply Nat.zero_le
  · simp at h
    have := foo (n - k) k ok
    rw [Nat.le_sub_iff_add_le h] at this
    apply le_trans ?_ this
    rw [add_comm]
    gcongr
    rwa [Nat.succ_le]

but it doesn't pass termination checking

[Somo S.]

Somo S. said:

so I'd rather focus on elementary technique for solving the above example (from scratch or "as scratch as is reasonable").. with the hope that I can generalize this to what I'm actually working on

thanks @Ruben Van de Velde .. actually, I'd like to avoid mathlib tactics. I dont want to depend on mathlib in my actual project if i can help it

[Ruben Van de Velde]

If you mean gcongr, I replaced that by show_term gcongr which tells me Try this: refine add_le_add_left ?bc (div (n - k) k ok)

[Ruben Van de Velde]

I suppose there are ways to avoid split_ifs as well

[Somo S.]

yes and split_ifs, rwa

[Somo S.]

okay I will try the strategy of using show_term to get equivalents..

[Ruben Van de Velde]

rwa is from Std

[Somo S.]

also can you explain what ?_ does.. I am familiar with _ but not ?_

[Ruben Van de Velde]

But this is closer to mathlib-free:

theorem foo (n k : Nat) (ok : k > 0) : div n k ok ≤ n := by
  unfold div
  split_ifs with h
  · apply Nat.zero_le
  · simp only [Nat.not_lt] at h
    have := foo (n - k) k ok
    rw [Nat.le_sub_iff_add_le h] at this
    apply Nat.le_trans ?_ this
    rw [Nat.add_comm]
    refine Nat.add_le_add_left ?bc (div (n - k) k ok)
    rw [Nat.succ_le]
    assumption
decreasing_by sorry -- skip: already proved

(mostly using nat-specific lemmas rather than their generalizations)

[Ruben Van de Velde]

?_ means "create a new goal to fill this hole"

[Somo S.]

is split_ifs similar to by_cases ?

[Ruben Van de Velde]

split_ifs looks at the if expressions in the goal (in this case) and creates new goals for the positive and negative cases and replaces the if term by the relevant case

[Somo S.]

ok thanks. I will try to adapt this. Already useful to know I should have started by unfolding