Zulip Chat Archive

Stream: new members

Topic: Combing specialize's


view this post on Zulip Aniruddh Agarwal (Jun 26 2020 at 00:28):

Is there a compound form for specialize, similar to rw? I have a bunch of statements like

  specialize h n,
  specialize h' n,

in a proof.

view this post on Zulip Jalex Stark (Jun 26 2020 at 00:31):

interesting. (i don't think what you ask for exists) can you show the proof?
tactic#specialize

view this post on Zulip Aniruddh Agarwal (Jun 26 2020 at 00:31):

Here:

example (hu : seq_limit u l) (hw : seq_limit w l)
(h :  n, u n  v n)
(h' :  n, v n  w n) : seq_limit v l :=
begin
  intros ε ,
  cases hu ε  with N hN,
  cases hw ε  with M hM,
  use (max N M),
  intros n hn,
  specialize hN n (le_of_max_le_left hn),
  specialize hM n (le_of_max_le_right hn),
  rw [abs_le] at *,
  specialize h n,
  specialize h' n,
  split; linarith,
end

view this post on Zulip Jalex Stark (Jun 26 2020 at 00:32):

what are u, l, w?

view this post on Zulip Aniruddh Agarwal (Jun 26 2020 at 00:33):

real-valued sequences. you can find a compiling version of this (sans the proof) here: https://github.com/leanprover-community/tutorials/blob/master/src/exercises/05_sequence_limits.lean#L149

u, v and w are sequences and l is a real number

view this post on Zulip Aniruddh Agarwal (Jun 26 2020 at 00:35):

I'm just trying to shave a couple of lines off of my proof :)

view this post on Zulip Aniruddh Agarwal (Jun 26 2020 at 00:44):

Actually, I can do this:

example (hu : seq_limit u l) (hw : seq_limit w l)
(h :  n, u n  v n)
(h' :  n, v n  w n) : seq_limit v l :=
begin
  intros ε ,
  cases hu ε  with N hN,
  cases hw ε  with M hM,
  use (max N M),
  intros n hn,
  specialize hN n (le_of_max_le_left hn),
  specialize hM n (le_of_max_le_right hn),
  rw abs_le at *,
  split; linarith[h n, h' n],
end

Last updated: May 10 2021 at 19:16 UTC