Zulip Chat Archive

Stream: new members

Topic: Limit inequality


view this post on Zulip Pedro Minicz (Aug 14 2020 at 22:23):

I am having no luck proving the following example. I looked around mathlib and didn't seem to find anything that would directly help. How do I handle the universal qualified in the hypothesis (I mean, maybe transform the hypothesis into something more usable)? I feel like I am missing something here.

import data.real.basic

example {x : } (h :  n : , x < (n + 1)⁻¹) : x  0 :=
sorry

view this post on Zulip Mario Carneiro (Aug 14 2020 at 22:28):

example {x : } : ( n : , x < (n + 1)⁻¹)  x  0 :=
begin
  contrapose!,
  intro h,
  obtain n, h := exists_nat_one_div_lt h,
  use n,
  simpa using le_of_lt h
end

view this post on Zulip Pedro Minicz (Aug 14 2020 at 22:29):

contrapose! makes it so much easier! Thank you!

view this post on Zulip Pedro Minicz (Aug 14 2020 at 22:31):

By the way, there is a tactic similar to how generalize behaves in Coq. I remember seeing it a Lean/Coq cheatsheet but never managed to use it properly.

view this post on Zulip Mario Carneiro (Aug 14 2020 at 22:31):

alternatively:

example {x : } (h :  n : , x < (n + 1)⁻¹) : x  0 :=
begin
  refine le_of_not_gt (λ x0, _),
  obtain n, h' := exists_nat_one_div_lt x0,
  simp at h',
  exact not_lt_of_lt (h _) h',
end

view this post on Zulip Mario Carneiro (Aug 14 2020 at 22:31):

example {x : } (h :  n : , x < (n + 1)⁻¹) : x  0 :=
begin
  refine le_of_not_gt (λ x0, _),
  obtain n, h' := exists_nat_one_div_lt x0,
  specialize h n,
  simp at *, linarith
end

view this post on Zulip Mario Carneiro (Aug 14 2020 at 22:32):

I think you are thinking of specialize

view this post on Zulip Pedro Minicz (Aug 14 2020 at 22:32):

Oh, I was thinking of revert.

view this post on Zulip Pedro Minicz (Aug 14 2020 at 22:32):

https://github.com/jldodds/coq-lean-cheatsheet

view this post on Zulip Mario Carneiro (Aug 14 2020 at 22:33):

there is also a generalize, but it doesn't do the reverting part, only the find and replace

view this post on Zulip Mario Carneiro (Aug 14 2020 at 22:33):

I don't think you can revert an expression

view this post on Zulip Pedro Minicz (Aug 14 2020 at 22:33):

import data.real.basic

example {x : } (h :  n : , x < (n + 1)⁻¹) : x  0 :=
begin
  revert h,
  contrapose!,
  intro h,
  obtain n, h := exists_nat_one_div_lt h,
  use n,
  simpa using le_of_lt h
end

view this post on Zulip Pedro Minicz (Aug 14 2020 at 22:34):

Mario Carneiro said:

I don't think you can revert an expression

What exactly you mean by expression?

view this post on Zulip Mario Carneiro (Aug 14 2020 at 22:34):

like you can't revert 2 + 2, you would have to generalize : 2 + 2 = x, revert x

view this post on Zulip Mario Carneiro (Aug 14 2020 at 22:35):

this would turn |- P (2+2) into |- \all x, P x

view this post on Zulip Mario Carneiro (Aug 14 2020 at 22:35):

I try to avoid intro and revert as the first line of a proof, as a matter of style

view this post on Zulip Mario Carneiro (Aug 14 2020 at 22:36):

you can almost always set up the theorem statement so that the appropriate things are already intro'd

view this post on Zulip Pedro Minicz (Aug 14 2020 at 22:37):

I see! Good example! I finally understand how generalize works. I tried and failed to use it several times because I was using like generalize is Coq. :grinning_face_with_smiling_eyes:


Last updated: May 11 2021 at 12:15 UTC