# Zulip Chat Archive

## 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 }, { 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 (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