decreasing induction

Stream: maths

[Sebastien Gouezel]

I can not find the fact that, if a property P n holds and if P (i+1) implies P i for all i, then P m holds whenever m <= n. Is this already in mathlib?

[Sebastien Gouezel]

We have currently a decreasing induction principle on nat, in the form

def decreasing_induction {P : ℕ → Sort*} (h : ∀k, P (k+1) → P k) {m n : ℕ} (mn : m ≤ n)
  (hP : P n) : P m :=
le_rec_on mn (λ k ih hsk, ih $ h k hsk) (λ h, h) hP

(notice the completely unreadable proof :-). This is even able to construct data, as testified by the fact that P takes values in Sort*. Unfortunately, the assumption is too strong: one should only need h for k < n, not for all k. It is easy to prove it with this weaker assumption (just write m = n - i and do a usual induction on i), but it is not obvious to me if this kind of proof is able to construct data. So, I came up with the following proof, which avoids subtraction and is based on the above decreasing_induction, but my proof takes 30 lines instead of 1, so it is obviously wrong. Here it is:

import data.nat.basic

open nat

@[elab_as_eliminator]
def decreasing_induction' {P : ℕ → Sort*} {m n : ℕ} (h : ∀ k < n, P (k+1) → P k) (mn : m ≤ n)
  (hP : P n) : P m :=
begin
  let Q := λ k, if k ≤ n then P k else P n,
  let H : ∀ k, Q (k+1) → Q k := λ k a, if hk : k < n then
  begin
    have Qk' : Q (k+1) = P (k+1),
    { simp only [not_le, ite_eq_left_iff],
      assume hk',
      exact (lt_irrefl _ ((succ_le_iff.2 hk).trans_lt hk')).elim },
    have Qk : Q k = P k,
    { simp only [not_le, ite_eq_left_iff],
      assume hk',
      exact (lt_irrefl _ (hk.trans hk')).elim },
    exact cast Qk.symm (h k hk (cast Qk' a))
  end else begin
    simp only [not_lt] at hk,
    have Qk' : Q (k+1) = P n,
    { simp only [ite_eq_right_iff],
      assume hk',
      exact (lt_irrefl _ ((succ_le_iff.1 hk').trans_le hk)).elim },
    have Qk : Q k = P n,
    { simp only [ite_eq_right_iff],
      assume hk',
      rw le_antisymm hk hk' },
    exact cast Qk.symm ((cast Qk' a))
  end,
  have Qn : Q n = P n, by simp [Q],
  have Qm : Q m = P m,
  { simp only [not_le, ite_eq_left_iff],
    assume hmn,
    exact (lt_irrefl _ (hmn.trans_le mn)).elim },
  exact cast Qm (decreasing_induction H mn (cast Qn.symm hP)),
end

How would a more proper proof look like?

[Floris van Doorn]

Here is the proof in the unreadable style:

import data.nat.basic

open nat

@[elab_as_eliminator]
def decreasing_induction' {P : ℕ → Sort*} {m n : ℕ} (h : ∀ k < n, P (k+1) → P k)
  (mn : m ≤ n) (hP : P n) : P m :=
le_rec_on mn (λ n ih h hn, ih (λ k hk, h k hk.step) (h n (lt_succ_self n) hn)) (λ _, id) h hP

[Floris van Doorn]

or, the same but more readable:

@[elab_as_eliminator]
def decreasing_induction' {P : ℕ → Sort*} {m n : ℕ} (h : ∀ k < n, P (k+1) → P k)
  (mn : m ≤ n) (hP : P n) : P m :=
begin
  -- induction mn using nat.le_rec_on generalizing h hP -- this doesn't work unfortunately
  refine le_rec_on mn _ _ h hP; clear h hP mn n,
  { intros n ih h hP,
    apply ih,
    { exact λ k hk, h k hk.step },
    { exact h n (lt_succ_self n) hP } },
  { intros h hP, exact hP }
end

[Floris van Doorn]

You could even weaken the assumption more:

/-- Recursion starting at a non-zero number: given a map `C k → C (k+1)` for each `k ≥ n`,
there is a map from `C n` to each `C m`, `n ≤ m`. -/
@[elab_as_eliminator]
def le_rec_on' {C : ℕ → Sort*} {n : ℕ} :
  Π {m : ℕ}, n ≤ m → (Π ⦃k⦄, n ≤ k → C k → C (k+1)) → C n → C m
| 0     H next x := eq.rec_on (nat.eq_zero_of_le_zero H) x
| (m+1) H next x := or.by_cases (of_le_succ H) (λ h : n ≤ m, next h $ le_rec_on' h next x)
  (λ h : n = m + 1, eq.rec_on h x)

@[elab_as_eliminator]
def decreasing_induction' {P : ℕ → Sort*} {m n : ℕ} (h : ∀ k < n, m ≤ k → P (k+1) → P k)
  (mn : m ≤ n) (hP : P n) : P m :=
begin
  -- induction mn using nat.le_rec_on' generalizing h hP -- this doesn't work unfortunately
  refine le_rec_on' mn _ _ h hP; clear h hP mn n,
  { intros n mn ih h hP,
    apply ih,
    { exact λ k hk, h k hk.step },
    { exact h n (lt_succ_self n) mn hP } },
  { intros h hP, exact hP }
end

[Scott Morrison]

Thanks for doing this, @Sebastien Gouezel and @Floris van Doorn: I'd just been sad yesterday that this was missing.