Zulip Chat Archive

Stream: lean4

Topic: Working with inequalities


Omnikar (Oct 13 2022 at 02:53):

How do I, for example, construct a proof that a / 2 > 4 given that a > 8?

example (a : Nat) (h : a > 8) : a / 2 > 4 := sorry

Mario Carneiro (Oct 13 2022 at 03:16):

It's false...

Mario Carneiro (Oct 13 2022 at 03:18):

example : ¬∀ (a : Nat) (h : a > 8), a / 2 > 4 :=
  mt (· 9) (by decide)

(pointlessly golfed)

Omnikar (Oct 14 2022 at 09:24):

Oh I forgot about that. In that case, what if you change the 8 to say 10? Then a/2 should be greater than 4.

Mario Carneiro (Oct 14 2022 at 09:32):

import Std.Data.Nat.Lemmas

example (a : Nat) (h : a > 9) : a / 2 > 4 :=
  (Nat.le_div_iff_mul_le (by decide)).2 h

Omnikar (Oct 14 2022 at 23:57):

Other question: I've found that you can prove n < 2 given n < 1 like this, but is there a shorter way to express this?

example (n : Nat) (h : n < 1) : n < 2 := Trans.trans h (show 1 < 2 by simp)

Mario Carneiro (Oct 15 2022 at 03:26):

that last line is (by decide) as well

Omnikar (Oct 15 2022 at 16:49):

How do I show False given n : Nat and h : n < 0?

Henrik Böving (Oct 15 2022 at 16:52):

I would

example {n : Nat} (h : n < 0) : False := by
  cases n <;> cases h

Omnikar (Oct 15 2022 at 17:11):

Thanks

Omnikar (Oct 15 2022 at 21:19):

Oh, I just found out about Nat.not_lt_zero which I think is a way more readable way to do it.


Last updated: Dec 20 2023 at 11:08 UTC