Zulip Chat Archive

Stream: new members

Topic: inequality


view this post on Zulip Alexandre Rademaker (May 30 2020 at 22:03):

I was expecting to learn how to prove example {x y : ℕ} {h : x + 1 = y + 2} : x > y := sorry from NNG but it looks like NNG defines > differently from the Lean 3 standard library. Any idea?

view this post on Zulip Chris Hughes (May 30 2020 at 22:24):

by omega or by linarith should work.

view this post on Zulip Alexandre Rademaker (May 30 2020 at 22:28):

hum, not directly, and both are in mathlib, right?

view this post on Zulip Jalex Stark (May 30 2020 at 22:42):

why are you asking about mathlib? did you try one of those proofs and it told you it couldn't find the name?

view this post on Zulip Alexandre Rademaker (May 30 2020 at 22:43):

yes. Lean 3.

view this post on Zulip Jalex Stark (May 30 2020 at 22:44):

are you able to import anything from mathlib?

view this post on Zulip Jalex Stark (May 30 2020 at 22:44):

are you in a project where you installed mathlib using leanproject?

view this post on Zulip Alexandre Rademaker (May 30 2020 at 22:45):

no, I am trying to prove without mathlib, only using Lean 3 standard definitions.

view this post on Zulip Jalex Stark (May 30 2020 at 22:46):

oh, okay, I think that was not clear

view this post on Zulip Jalex Stark (May 30 2020 at 22:46):

well you could start by unfolding the definition of <

view this post on Zulip Jalex Stark (May 30 2020 at 22:46):

the NNG-style proof would probably be an induction

view this post on Zulip Jalex Stark (May 30 2020 at 22:47):

(I don't know why anyone would want to do math in lean without mathlib; if you give more context maybe we can be more helpful)

view this post on Zulip Kevin Buzzard (May 30 2020 at 22:51):

I probably don't use > at all in NNG -- all the lemmas are for < and <=. I can believe I defined it differently -- I played around with several definitions and tested them on undergraduates before deciding which one to go with. You can just switch notation off and unfold if you want to see the definition you're playing with.

view this post on Zulip Kevin Buzzard (May 30 2020 at 22:52):

But there will probably be a lemma of the form y < x iff y+1 le x and then another one saying you can cancel +1 in an inequality. These both sound like natural lemmas so they'll be in...oh, they might be in mathlib. I have no idea what's in core lean. Core lean wasn't designed for this kind of question

view this post on Zulip Jalex Stark (May 30 2020 at 22:53):

in fact we're doing our best to take math out of core lean

view this post on Zulip Alexandre Rademaker (May 30 2020 at 22:54):

@Jalex Stark The example looks very simple and my goal is to understand the details. surely mathlb provides tactics like omega and linarith but I want to explore the basics here. Actually, the example came from a very simple exercise that I am trying to show how to formalize in Lean. See the balances in https://www.youtube.com/watch?v=4JpFWfkAtHY&t=2088s (video in Portuguese).

view this post on Zulip Jalex Stark (May 30 2020 at 22:55):

sure, I think it's fine to not want to use a high-powered tactic for this

view this post on Zulip Jalex Stark (May 30 2020 at 22:55):

but not using mathlib is silly

view this post on Zulip Kevin Buzzard (May 30 2020 at 22:55):

If you don't import data.nat.basic from mathlib then you will probably be missing a bunch of random lemmas though

view this post on Zulip Kevin Buzzard (May 30 2020 at 22:55):

So you might end up having to reprove them all by induction

view this post on Zulip Kevin Buzzard (May 30 2020 at 22:58):

Files like data.nat.basic used to be in core lean before they dumped the maths out into mathlib

view this post on Zulip Kevin Buzzard (May 30 2020 at 23:03):

open nat

example {x y : } {h : x + 1 = y + 2} : x > y :=
begin
  apply nat.lt_of_succ_le,
  rw succ_eq_add_one,
  rw nat.add_le_add_iff_le_right 1,
  rw h,
end

view this post on Zulip Kevin Buzzard (May 30 2020 at 23:03):

Enough of what I wanted was in core

view this post on Zulip Kevin Buzzard (May 30 2020 at 23:06):

I use the fact that y>x is definitionally x<y

view this post on Zulip Alexandre Rademaker (May 30 2020 at 23:15):

Jalex Stark said:

but not using mathlib is silly

sure, if my goal was something more complex and I had some inequalities on my way.. I can understand the value of mathlib. But that is not the case, it is much more basic stuff that I want to explore.

view this post on Zulip Jalex Stark (May 30 2020 at 23:23):

i still don't really understand your goals. what if core lean literally didn't have a definition of the natural numbers? would you still want to avoid mathlib?

view this post on Zulip Alexandre Rademaker (May 31 2020 at 00:07):

thank you @Kevin Buzzard, clear and direct solution as always! ;-)

view this post on Zulip Alexandre Rademaker (May 31 2020 at 00:15):

No @Jalex Stark, it is all about the level of abstraction I am focusing on? If Lean didn't have any natural numbers definitions, I guess for that particular problem I would not be able to avoid mathlib. It is not very different from programming and when we believe that it is worth to depend on a library or not. But you are right I should start using mathlib to have also a clue about what it can provide.

view this post on Zulip Alexandre Rademaker (May 31 2020 at 00:33):

(deleted)

view this post on Zulip Alexandre Rademaker (May 31 2020 at 00:36):

Kevin Buzzard said:

I use the fact that y>x is definitionally x<y

Where is that?

view this post on Zulip Bryan Gin-ge Chen (May 31 2020 at 00:39):

I think Kevin just means that he proves x < y and Lean accepts it as a proof of y > x.

view this post on Zulip Alexandre Rademaker (May 31 2020 at 00:55):

I found in the core.lean

@[reducible] def gt {α : Type u} [has_lt α] (a b : α) : Prop := has_lt.lt b a
...
infix >        := gt

maybe this is the definition of y > x as gt y x := has_lt.lt y x

view this post on Zulip Jalex Stark (May 31 2020 at 01:04):

thanks, I think I understand your goal now. probably you want to look at the proofs of the lemmas that kevin invoked in his proof?

view this post on Zulip Jalex Stark (May 31 2020 at 01:05):

in mathlib we just try to avoid using > in our theorem statements as much as posisble

view this post on Zulip Michael Beeson (Jul 13 2020 at 06:24):

How can I get a \neq p in a hypothesis h (or a goal for that matter) rewritten as p \neq a?

view this post on Zulip Kenny Lau (Jul 13 2020 at 06:24):

replace h := h.symm

view this post on Zulip Kenny Lau (Jul 13 2020 at 06:24):

apply ne.symm

view this post on Zulip Michael Beeson (Jul 13 2020 at 06:25):

ah. I tried among other things neq.sym.... Thank you

view this post on Zulip Kenny Lau (Jul 13 2020 at 06:26):

this reminds me to PR the list of names of symbols

view this post on Zulip Kenny Lau (Jul 13 2020 at 06:32):

https://github.com/leanprover-community/leanprover-community.github.io/pull/93

view this post on Zulip Jalex Stark (Jul 13 2020 at 11:23):

a more tactic-ful answer:

example (a b : ) (h : a  b) : b  a :=
begin
  symmetry at h, exact h,
end

Last updated: May 11 2021 at 13:22 UTC