Zulip Chat Archive

Stream: new members

Topic: From n<=1, get n=0 or n=1


view this post on Zulip Patrick Stevens (May 11 2020 at 17:34):

I'm sure I've seen before that there's a tactic to turn a hypothesis n <= 1 into n = 1 \/ n = 0, but I can't find it :( I could prove it by induction, but I think I remember someone mentioning a more general tactic that splits inequalities into individual cases. Can anyone remember what that was?

view this post on Zulip Jeremy Avigad (May 11 2020 at 17:36):

https://leanprover-community.github.io/mathlib_docs/tactics.html#interval_cases

view this post on Zulip Jeremy Avigad (May 11 2020 at 17:44):

For small examples like this, cases is also sometimes useful:

example (n : ) (h : n  1) : n = 0  n =1 :=
begin
  cases h with h h,
  { right, refl },
  cases h with h h,
  { left, refl }
end

It's also mentioned and used briefly in the last example here, https://avigad.github.io/mathematics_in_lean/the_natural_numbers.html. Some of the tricks in Section 3.2 may also be helpful.

import data.nat.basic

example :  n, n  1  n = 0  n = 1 :=
dec_trivial

view this post on Zulip Kevin Buzzard (May 11 2020 at 17:44):

Back in the old days, before that tactic, I would just do cases on n and then cases on everything that showed up until I was down to the two cases. For n<=1 this would work fine but for any larger ranges the tactic is definitely the way to proceed. Actually I bet this can be done with rcases in some cool way.

view this post on Zulip Kevin Buzzard (May 11 2020 at 17:44):

Hah Jeremy beat me to it :-)

view this post on Zulip Jeremy Avigad (May 11 2020 at 17:45):

The new tutorial doesn't yet mention the interval_cases tactic, but I'll add that.

view this post on Zulip Chris Hughes (May 11 2020 at 18:02):

You could use omega as well.


Last updated: May 12 2021 at 04:19 UTC