Zulip Chat Archive

Stream: general

Topic: greater than nat and real


view this post on Zulip Saif Ghobash (Dec 29 2020 at 13:39):

Im new to lean and am trying to formalize some theorems from my lecture notes on real analysis, one of them being

-- ℕ ⊂ ℝ is not bounded above.
theorem theorem_1_1_1 :  x : ,  n : , n > x :=
begin

end

however I am getting a type error

type mismatch at application
  n > x
term
  x
has type
  
but is expected to have type
  

I am not sure how to cast n : ℕ to be a real number so I can apply > or use some form of > that accepts ℕ and ℝ.

view this post on Zulip Johan Commelin (Dec 29 2020 at 13:43):

@Saif Ghobash This is because Lean is reading "outside in, left-to-right"...

view this post on Zulip Patrick Massot (Dec 29 2020 at 13:43):

-- ℕ ⊂ ℝ is not bounded above.
theorem theorem_1_1_1 :  x : ,  n : , (n : ) > x :=
begin

end

view this post on Zulip Patrick Massot (Dec 29 2020 at 13:43):

Note that, as Johan points out, you could also write:

-- ℕ ⊂ ℝ is not bounded above.
theorem theorem_1_1_1 :  x : ,  n : , x < n :=
begin

end

view this post on Zulip Johan Commelin (Dec 29 2020 at 13:43):

So it sees ">" and then "n", and determines you must be comparing two natural numbers, because n is a nat.

view this post on Zulip Johan Commelin (Dec 29 2020 at 13:44):

Patrick just posted the two ways around this (-;

view this post on Zulip Patrick Massot (Dec 29 2020 at 13:44):

Because of order of elaboration, in the second version Lean knows it expects a real when meeting n.

view this post on Zulip Saif Ghobash (Dec 29 2020 at 13:46):

Thank you @Patrick Massot and @Johan Commelin !

view this post on Zulip Johan Commelin (Dec 29 2020 at 13:48):

@Saif Ghobash Also, note that src/data/real/basic.lean contains

200:instance : archimedean  :=
201:archimedean_iff_rat_le.2 $ λ x, quotient.induction_on x $ λ f,
202-let M, M0, H := f.bounded' 0 in
203-M, mk_le_of_forall_le 0, λ i _,
204-  rat.cast_le.2 $ le_of_lt (abs_lt.1 (H i)).2⟩⟩

view this post on Zulip Johan Commelin (Dec 29 2020 at 13:49):

That exactly gives you the result you are looking for.

view this post on Zulip Johan Commelin (Dec 29 2020 at 13:50):

You can use the lemma exists_nat_gt because that instance exists.

view this post on Zulip Saif Ghobash (Dec 29 2020 at 14:51):

@Johan Commelin oh cool! that's exactly what I needed, thank you :)

view this post on Zulip Johan Commelin (Dec 29 2020 at 14:55):

@Saif Ghobash most likely 90-95% of the theorems in an introduction to analysis course are already in mathlib (in one form or another). On the other hand, this doesn't mean that all the exercises in such a course will be trivial to do using mathlib.

view this post on Zulip Johan Commelin (Dec 29 2020 at 14:56):

See also https://leanprover-community.github.io/undergrad.html

view this post on Zulip Sebastian Ullrich (Dec 30 2020 at 10:12):

Johan Commelin said:

So it sees ">" and then "n", and determines you must be comparing two natural numbers, because n is a nat.

https://github.com/leanprover/lean4/commit/eba3983658faef2d41b7ad00fc2c2e540a1e43e6

view this post on Zulip Johan Commelin (Dec 30 2020 at 10:26):

@Sebastian Ullrich Thanks, as always (-;

view this post on Zulip Sebastian Ullrich (Dec 30 2020 at 10:47):

But I didn't even do anything :big_smile:

view this post on Zulip Kevin Buzzard (Dec 30 2020 at 12:40):

One could intentionally or unintentionally abuse this with some random coercion you didn't know was there, which might change the meaning of a statement. This should be fun! Does it mean that (a : T) < b no longer guarantees that < will be T.has_lt?

view this post on Zulip Kevin Buzzard (Dec 30 2020 at 12:41):

Having said that it would make the Bernoulli code look better! So in a real use case it does look like a good idea

view this post on Zulip Kevin Buzzard (Dec 30 2020 at 12:42):

I'm multiplying and dividing what look like naturals, and all of a sudden there's a Bernoulli number at the end and I didn't want to put it at the start but it's rational


Last updated: May 14 2021 at 22:15 UTC