inequality

Stream: new members

[Alexandre Rademaker]

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?

[Chris Hughes]

by omega or by linarith should work.

[Alexandre Rademaker]

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

[Jalex Stark]

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

[Alexandre Rademaker]

yes. Lean 3.

[Jalex Stark]

are you able to import anything from mathlib?

[Jalex Stark]

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

[Alexandre Rademaker]

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

[Jalex Stark]

oh, okay, I think that was not clear

[Jalex Stark]

well you could start by unfolding the definition of <

[Jalex Stark]

the NNG-style proof would probably be an induction

[Jalex Stark]

(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)

[Kevin Buzzard]

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.

[Kevin Buzzard]

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

[Jalex Stark]

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

[Alexandre Rademaker]

@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).

[Jalex Stark]

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

[Jalex Stark]

but not using mathlib is silly

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

Enough of what I wanted was in core

[Kevin Buzzard]

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

[Alexandre Rademaker]

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.

[Jalex Stark]

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?

[Alexandre Rademaker]

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

[Alexandre Rademaker]

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.

[Alexandre Rademaker]

(deleted)

[Alexandre Rademaker]

Kevin Buzzard said:

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

Where is that?

[Bryan Gin-ge Chen]

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

[Alexandre Rademaker]

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

[Jalex Stark]

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?

[Jalex Stark]

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

[Michael Beeson]

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

[Kenny Lau]

replace h := h.symm

[Kenny Lau]

apply ne.symm

[Michael Beeson]

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

[Kenny Lau]

this reminds me to PR the list of names of symbols

[Kenny Lau]

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

[Jalex Stark]

a more tactic-ful answer:

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

[tsuki hao]

import Mathlib.Tactic
import Mathlib.Data.Real.Basic

theorem my_lemma4 :
    ∀ {x y ε : ℝ}, 0 < ε → ε ≤ 1 → |x| < ε → |y| < ε → |x * y| < ε := by
  intro x y ε epos ele1 xlt ylt
  calc
    |x * y| = |x| * |y| := by rw[abs_mul] --绝对值的乘法
    _ ≤ |x| * ε := sorry
    _ < 1 * ε := sorry
    _ = ε := by rw[one_mul]

Does anyone know how this code should be written next?

[Johan Commelin]

Did you try gcongr?

[Johan Commelin]

or apply?

[tsuki hao]

Johan Commelin said:

Did you try gcongr?

gcongr does not apply to this problem, I used apply? but did not get the appropriate tactic

[Patrick Massot]

Note there are lemmas mentioned in the text right after this exercise.

[Patrick Massot]

And of course if you are really stuck and simply want the solution then you can find it in the solutions folder.

[tsuki hao]

Patrick Massot said:

Note there are lemmas mentioned in the text right after this exercise.

Thank you, I only followed the previous part at first!

[tsuki hao]

Patrick Massot said:

And of course if you are really stuck and simply want the solution then you can find it in the solutions folder.

Can I ask where I can find the 'solutions folder', which may be of great help to my future studies.

[Patrick Massot]

I'm sorry we have the bad habit of sometimes putting explanations after the exercise statement. We should go through the whole text and systematically fix that. Until we do that you should make sure to check the sentence after each exercise before working on an exercise.

[Patrick Massot]

If you cloned the repository at https://github.com/leanprover-community/mathematics_in_lean then each chapter folder has a solution subfolder.

[tsuki hao]

Patrick Massot said:

If you cloned the repository at https://github.com/leanprover-community/mathematics_in_lean then each chapter folder has a solution subfolder.

Thank you, this really helped me a lot!

[Patrick Massot]

But actually it seems this exercise is missing from the solution file :sad: I'll take a look to understand what happened.

[Patrick Massot]

The missing solution now appears in https://github.com/leanprover-community/mathematics_in_lean/blob/master/MIL/C03_Logic/solutions/Solutions_S01_Implication_and_the_Universal_Quantifier.lean

[tsuki hao]

Patrick Massot said:

The missing solution now appears in https://github.com/leanprover-community/mathematics_in_lean/blob/master/MIL/C03_Logic/solutions/Solutions_S01_Implication_and_the_Universal_Quantifier.lean

Thank you very much!