Rational between two reals

Stream: new members

[Julian Gilbey]

I've just managed to formalise my first non-trivial result: between every two distinct real numbers there is a rational. It might already exist in mathlib, though I couldn't find it.
A few questions and a help request:

• I wanted to rearrange a < b - c to get my target c < b - a, where a, b, c are reals. There is a lemma which does exactly this: lt_tsub_comm, but to use it, I had to show that R is an instance of add_comm_monoid (why was that not automatic, given that I had imported data.real.basic?) and has_ordered_sub. The latter requires doing almost as much work as I had already done, so I'm not sure why there is no instantiation of a structure such as the reals as a has_ordered_sub. I know tsub stands for "truncated subtraction", but the same results hold for non-truncated subtraction. So in the end, I gave up and didn't use this lemma, proving the result manually (which was somewhat painful).
• I had to write a number of small lemmas along the way, for example:

lemma nat_pred_lt_of_pos { n : ℕ } (h : 0 < n) : nat.pred n < n := sorry

and a parallel one for n - 1 < n (sorry @Kevin Buzzard, I ended up using natural number subtraction in my argument). I'm sure these might help other people using mathlib, so perhaps I could contribute them?

• The help request: I am convinced that my Lean program is "non-idiomatic" and has various steps I could have simplified using appropriate tactics, for example. I have also used have quite heavily, and perhaps those could have been replaced by other constructions. I'm unconvinced about my lemma naming. If anyone has time to look at my code, please feel free: https://github.com/juliangilbey/lean-rational-between-reals.git Any comments and advice will be gratefully received!
• Finally, once my code is improved, would this be a good thing to submit to mathlib?
  Many thanks to all for your help!

[Alex J. Best]

I think it exists in mathlib in the generality of archimidean fields (which might be why its hard to find) docs#exists_rat_btwn

[Alex J. Best]

Did you try tactic#linarith for your real subtraction goal?

[Alex J. Best]

That does sound really strange that lean couldn't find add_comm_monoid on the reals though, do you have a minimised example of that failing? Some of the tsub type things have changed quite a bit recently so prehaps something is not imported where we expect

[Alex J. Best]

Contributing small lemmas sounds great! And very useful, take a look at https://leanprover-community.github.io/contribute/index.html if you haven't already.

[Alex J. Best]

I really hope you aren't discouraged by some of what you did being in mathlib already, in fact the same thing happened to me with one of the first big projects I tried to prove in Lean, but I still learnt a lot along the way, and there is always interesting value in comparing different proof methods and seeing what works best :smile:

[Julian Gilbey]

Alex J. Best said:

I think it exists in mathlib in the generality of archimidean fields (which might be why its hard to find) docs#exists_rat_btwn

Argh!!! :joy:

[Julian Gilbey]

Alex J. Best said:

Did you try tactic#linarith for your real subtraction goal?

Ah, a new tactic! Worked perfectly, thanks.

[Julian Gilbey]

Alex J. Best said:

That does sound really strange that lean couldn't find add_comm_monoid on the reals though, do you have a minimised example of that failing? Some of the tsub type things have changed quite a bit recently so prehaps something is not imported where we expect

Here is a minimal example:

import data.real.basic
import algebra.order.sub

example { a b c : ℝ } : a < b - c → c < b - a :=
begin
  introv h,
  apply lt_tsub_comm.1,
  exact h,
  -- still two open goals:
  -- ⊢ add_comm_monoid ℝ
  -- ⊢ has_ordered_sub ℝ
end

[Julian Gilbey]

Alex J. Best said:

Contributing small lemmas sounds great! And very useful, take a look at https://leanprover-community.github.io/contribute/index.html if you haven't already.

Ah, thanks! Please may I have write access to non-master branches of the mathlib repository then?

[Julian Gilbey]

Alex J. Best said:

I really hope you aren't discouraged by some of what you did being in mathlib already, in fact the same thing happened to me with one of the first big projects I tried to prove in Lean, but I still learnt a lot along the way, and there is always interesting value in comparing different proof methods and seeing what works best :)

Oh, indeed not. I was rather surprised that it wasn't there already, so was somewhat reassured to find it was. It does indicate one of the bigger issues with formalising mathematics: how do you find the lemma/theorem you want?

[Alex J. Best]

Julian Gilbey said:

Alex J. Best said:

Contributing small lemmas sounds great! And very useful, take a look at https://leanprover-community.github.io/contribute/index.html if you haven't already.

Ah, thanks! Please may I have write access to non-master branches of the mathlib repository then?

@maintainers :up:

[Kevin Buzzard]

Julian Gilbey said:

how do you find the lemma/theorem you want?

#Is there code for X? and library_search and learning the #naming conventions.

[Johan Commelin]

@Julian Gilbey What is your github username?

[Kevin Buzzard]

instance : has_ordered_sub ℝ := infer_instance -- fails

field is ∀ (a b c : ℝ), a - b ≤ c ↔ a ≤ c + b

[Kevin Buzzard]

Julian -- we just did a big refactor of inequalities on algebraic objects and it looks like this one got missed.

[Eric Wieser]

With what imports? I'm surprised that none of the instance for docs#has_ordered_sub match

[Kevin Buzzard]

import data.real.basic
import algebra.order.sub

[Eric Wieser]

Wow, we appear to be missing add_group.has_ordered_sub

[Ruben Van de Velde]

Which one should match? has_ordered_sub was primarily about nat subtraction

[Ruben Van de Velde]

But I guess the "This is satisfied both by the subtraction in additive ordered groups" part implies that that should work as well

[Eric Wieser]

add_group.has_ordered_sub should match, but first it needs to exist

[Ruben Van de Velde]

import data.real.basic
import algebra.order.sub

example { a b c : ℝ } : a < b - c → c < b - a :=
begin
  introv h,
  rwa lt_sub,
end

[Kevin Buzzard]

or

import data.real.basic
import algebra.order.sub

instance : has_ordered_sub ℝ := ⟨λ _ _ _, sub_le_iff_le_add⟩

example { a b c : ℝ } : a < b - c → c < b - a :=
begin
  intro h,
  rw lt_tsub_comm,
  exact h,
end

Julian -- don't apply foo.1 if foo : A <-> B, just rewrite it.

[Ruben Van de Velde]

lt_tsub_comm was the wrong way to proceed - 'tsub' refers to "truncated subtraction"

[Ruben Van de Velde]

But perhaps we should make it work, yes

[Kevin Buzzard]

example { a b c : ℝ } : a < b - c → c < b - a :=
begin
  intro h,
  library_search,
end

is the right way to proceed :-)

[Ruben Van de Velde]

library_search finds it even without the intro

[Patrick Massot]

Julian Gilbey said:

Alex J. Best said:

Did you try tactic#linarith for your real subtraction goal?

Ah, a new tactic! Worked perfectly, thanks.

This shouldn't be a new tactic, it's a fundamental one if you're interested in math formalization in Lean. I strongly suggest you do the tutorials project before trying to contribute. That should save you a lot of frustration.

[Patrick Massot]

Returning to your original question, the correct answer is:

import data.real.basic

example (x y : ℝ) (h : x < y) : ∃ q : ℚ, x < q ∧ (q : ℝ) < y :=
begin
  library_search,
end

[Yaël Dillies]

Eric Wieser said:

Wow, we appear to be missing add_group.has_ordered_sub

Yup, I thought we had that :confused:

[Eric Wieser]

I guess I meant docs#ordered_add_comm_group

[Yaël Dillies]

Well, it's ordered_add_comm_group.to_has_ordered_sub that we're missing.

[Yaël Dillies]

Eheh, yeah

[Eric Wieser]

Whoever posts the correct name of the missing instance is responsible for making the PR, right?

[Kevin Buzzard]

for me the hard part is knowing where to put the instance

[Yaël Dillies]

Sure I can do that!

[Julian Gilbey]

Johan Commelin said:

Julian Gilbey What is your github username?

Johan Commelin juliangilbey Thanks!

[Johan Commelin]

@Julian Gilbey https://github.com/leanprover-community/mathlib/invitations

[Julian Gilbey]

Ah, thanks - I'd forgotten that rw works with <-> as well as with =.

[Yaël Dillies]

#10225 for the missing instance.