nat.le_cases

Stream: general

[Johan Commelin]

Is the following snippet useful enough to PR to mathlib?

import data.nat.basic
import tactic

def nat.le_cases.aux (k : ℕ) : ℕ → Prop
| 0     := k = 0
| (n+1) := nat.le_cases.aux n ∨ k = (n+1)

lemma nat.le_cases {k n : ℕ} (h : k ≤ n) :
  nat.le_cases.aux k n :=
begin
  induction n with n ih,
  { exact nat.eq_zero_of_le_zero h },
  { rw nat.le_add_one_iff at h,
    exact h.imp ih id }
end

example (k : ℕ) (h : k ≤ 2) : (k:ℤ)^3 - 3*k^2 + 2*k = 0 :=
begin
  -- ring,     -- does nothing useful
  -- norm_num, -- does nothing useful
  replace h := nat.le_cases h,
  repeat { rcases h with h|rfl },
  -- all_goals { ring },     -- works
  all_goals { norm_num }, -- works
end

I think @Scott Morrison had some tactic in the making that would do such case-bashing. Maybe we want something more general, that also handles k ∈ finset.Ico 3 7, etc...

[Rob Lewis]

That was Scott's plan, but I don't think it's materialized yet. He did do fin_cases which you can force to work here. Not the most elegant way.

import tactic.fin_cases tactic.linarith

example (k : ℕ) (h : k ≤ 2) : (k:ℤ)^3 - 3*k^2 + 2*k = 0 :=
begin
  let k' : fin 3 := ⟨k, by linarith⟩,
  change k with k'.val,
  fin_cases k'; rw [h_1]; dsimp; norm_num
end

[Johan Commelin]

Aha, that already a useful start. I guess that is already good enough to not PR nat.le_cases to mathlib.

[Scott Morrison]

I think there's still an branch nat_cases that contains most of the tactic you're looking for.

[Scott Morrison]

It would be good to finish that off!

[Scott Morrison]

Similarly our hom tactic, @Johan Commelin!

[Johan Commelin]

@Scott Morrison Yeah, you are right... with the move to bundled homs the hom tactic is getting less urgent every day, but still...