Zulip Chat Archive

Stream: new members

Topic: trichotomy of naturals


view this post on Zulip Bhavik Mehta (Oct 27 2019 at 02:50):

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?

view this post on Zulip Mario Carneiro (Oct 27 2019 at 03:11):

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

view this post on Zulip Kenny Lau (Oct 27 2019 at 03:14):

import tactic.omega

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

view this post on Zulip Bhavik Mehta (Oct 27 2019 at 14:17):

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

view this post on Zulip Bryan Gin-ge Chen (Oct 27 2019 at 14:33):

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

view this post on Zulip Kevin Buzzard (Oct 27 2019 at 14:50):

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.


Last updated: May 13 2021 at 05:21 UTC