Zulip Chat Archive

Stream: general

Topic: nat.le_cases


view this post on Zulip 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...

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Scott Morrison (Sep 16 2019 at 08:51):

It would be good to finish that off!

view this post on Zulip Scott Morrison (Sep 16 2019 at 08:51):

Similarly our hom tactic, @Johan Commelin!

view this post on Zulip 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