Zulip Chat Archive

Stream: new members

Topic: adding one inside a function


Alex Kontorovich (Apr 14 2020 at 20:53):

More noob questions. Please help to make this work? (tried library_search, simp, hint, cc, suggest...) Thank you!

lemma z (F:ℕ→)(G:ℕ→) (i:) (fg:  k, G(k)= F (k+i))
:  k, (F(k + nat.succ i)= G (k+1))
:=
begin
    intros k,
    sorry,
end,

Johan Commelin (Apr 14 2020 at 20:58):

Try symmetry and then convert fg (k+1) using 1

Johan Commelin (Apr 14 2020 at 20:59):

Or maybe better symmetry, rw show k + nat.succ i = (k+1) + i,

Johan Commelin (Apr 14 2020 at 21:00):

suffices : k + nat.succ i = (k+1) + i,
{ sorry },
rw this,
symmetry,
apply fg

Patrick Massot (Apr 14 2020 at 21:01):

Why suffices?

Patrick Massot (Apr 14 2020 at 21:01):

Don't you mean have?

Patrick Massot (Apr 14 2020 at 21:01):

And probably rw fg can replace the last two lines.

Patrick Massot (Apr 14 2020 at 21:02):

I say λ k, by rw [show k + nat.succ i = (k+1) + i, by ring, fg]

Patrick Massot (Apr 14 2020 at 21:03):

(But I can see comma haters coming)

Kenny Lau (Apr 14 2020 at 21:04):

import tactic data.real.basic

lemma z (F :   ) (G :   ) (i : ) (fg :  k, G k = F (k+i)) (k : ) :
  F (k + nat.succ i) = G (k + 1) :=
by rw fg; congr' 1; omega

Sebastien Gouezel (Apr 14 2020 at 21:05):

The new mathlib style is

by { rw fg, congr' 1, omega }

Kenny Lau (Apr 14 2020 at 21:05):

oh I didn't know that

Patrick Massot (Apr 14 2020 at 21:05):

Kenny cheated by moving k left of the colon

Patrick Massot (Apr 14 2020 at 21:06):

And ring is shorter than omega, I'm very disappointed by Kenny's golf.

Kevin Buzzard (Apr 14 2020 at 22:43):

That's great to hear that that's the new mathlib style, I had independently come up with it, I know it costs some extra bytes with the brackets but it was getting silly with all the semicolons

Reid Barton (Apr 14 2020 at 22:44):

At least they're not some unicode brackets, so they only cost 1 byte each.


Last updated: Dec 20 2023 at 11:08 UTC