trichotomy of naturals

Stream: new members

[Bhavik Mehta]

I have the hypothesis ¬a = 2, where a : ℕ, and I'd like to reduce this to a <= 1 and a >= 3, is there something in the standard libs to help me?

[Mario Carneiro]

example {n : ℕ} (h : n ≠ 2) : n ≤ 1 ∨ 3 ≤ n :=
begin
  cases ne_iff_lt_or_gt.1 h with h' h',
  exact or.inl (nat.le_of_lt_succ h'),
  exact or.inr (nat.succ_le_of_lt h'),
end

[Kenny Lau]

import tactic.omega

example {n : ℕ} (h : n ≠ 2) : n ≤ 1 ∨ 3 ≤ n :=
by rw ne_iff_lt_or_gt at h; omega

[Bhavik Mehta]

Thanks both! Is there somewhere I can search for things like this?

[Bryan Gin-ge Chen]

This doc on naming conventions may be helpful, since it will help with using autocomplete in VS Code (or emacs?) to get a list of relevant suggestions.

There's also #find:

import tactic.find

-- need to have some declaration before #find starts to work
example : true := trivial

#find _ ≠ _ → _ ≤ _ ∨ _ ≥ _
-- returns nothing, probably because using < and > would be better
#find _ ≠ _ → _ < _ ∨ _ > _
-- lt_or_gt_of_ne: ∀ {α : Type u} [_inst_1 : linear_order α] {a b : α}, a ≠ b → a < b ∨ a > b

[Kevin Buzzard]

To give an example of autocomplete here -- for a general totally ordered thing (e.g. the reals) the theorem is going to be a != x iff a < x or a > x, so I write

import tactic.linarith -- mega import to make sure I get lots of mathlib in

example (a : ℕ) : a ≠ 2 ↔ a < 2 ∨ a > 2 :=
begin
  exact ne_iff
end

(because I know ne_iff... is what this thing will be called, by the naming conventions) and then I move to just after the last f of iff and (in VS Code) hit esc, ctrl-space, and then if I don't get enough stuff I hit esc, ctrl-space again (I don't know why I have to do it twice sometimes). I can now see a big list of lots of theorems which have ne_iff in, and then I can use the arrow keys to scroll around and find the one I want.