## Stream: general

### Topic: nat.le_cases

#### Johan Commelin (Sep 16 2019 at 08:04):

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 },
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 (Sep 16 2019 at 08:31):

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 (Sep 16 2019 at 08:42):

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

#### Scott Morrison (Sep 16 2019 at 08:51):

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

#### Scott Morrison (Sep 16 2019 at 08:51):

It would be good to finish that off!

#### Scott Morrison (Sep 16 2019 at 08:51):

Similarly our hom tactic, @Johan Commelin!

#### Johan Commelin (Sep 16 2019 at 09:05):

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

Last updated: May 08 2021 at 19:11 UTC